harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Analysis/BoxIntegral/Partition/Basic.lean
theorem restrict_mono {π₁ π₂ : Prepartition I} (Hle : π₁ ≤ π₂) : π₁.restrict J ≤ π₂.restrict J

Proof state:
ι : Type u_1
I J : Box ι
π₁ π₂ : Prepartition I
Hle : π₁ ≤ π₂
⊢ π₁.restrict J ≤ π₂.restrict J

Tactic:
classical
refine ofWithBot_mono fun J₁ hJ₁ hne => ?_
rw [Finset.mem_image] at hJ₁; rcases hJ₁ with ⟨J₁, hJ₁, rfl⟩
rcases Hle hJ₁ with ⟨J₂, hJ₂, hle⟩
exact ⟨_, Finset.mem_image_of_mem _ hJ₂, inf_le_inf_left _ <| WithBot.coe_le_coe.2 hle⟩

Result:
no goals

Proof state:
ι : Type u_1
I J : Box ι
π₁ π₂ : Prepartition I
Hle : π₁ ≤ π₂
⊢ π₁.restrict J ≤ π₂.restrict J

Tactic:
refine ofWithBot_mono fun J₁ hJ₁ hne => ?_

Result:
ι : Type u_1
I J : Box ι
π₁ π₂ : Prepartition I
Hle : π₁ ≤ π₂
J₁ : WithBot (Box ι)
hJ₁ : J₁ ∈ Finset.image (fun J' => ↑J ⊓ ↑J') π₁.boxes
hne : J₁ ≠ ⊥
⊢ ∃ J' ∈ Finset.image (fun J' => ↑J ⊓ ↑J') π₂.boxes, J₁ ≤ J'

Proof state:
ι : Type u_1
I J : Box ι
π₁ π₂ : Prepartition I
Hle : π₁ ≤ π₂
J₁ : WithBot (Box ι)
hJ₁ : ∃ a ∈ π₁.boxes, ↑J ⊓ ↑a = J₁
hne : J₁ ≠ ⊥
⊢ ∃ J' ∈ Finset.image (fun J' => ↑J ⊓ ↑J') π₂.boxes, J₁ ≤ J'

Tactic:
rcases hJ₁ with ⟨J₁, hJ₁, rfl⟩

Result:
case intro.intro
ι : Type u_1
I J : Box ι
π₁ π₂ : Prepartition I
Hle : π₁ ≤ π₂
J₁ : Box ι
hJ₁ : J₁ ∈ π₁.boxes
hne : ↑J ⊓ ↑J₁ ≠ ⊥
⊢ ∃ J' ∈ Finset.image (fun J' => ↑J ⊓ ↑J') π₂.boxes, ↑J ⊓ ↑J₁ ≤ J'

Proof state:
case intro.intro
ι : Type u_1
I J : Box ι
π₁ π₂ : Prepartition I
Hle : π₁ ≤ π₂
J₁ : Box ι
hJ₁ : J₁ ∈ π₁.boxes
hne : ↑J ⊓ ↑J₁ ≠ ⊥
⊢ ∃ J' ∈ Finset.image (fun J' => ↑J ⊓ ↑J') π₂.boxes, ↑J ⊓ ↑J₁ ≤ J'

Tactic:
rcases Hle hJ₁ with ⟨J₂, hJ₂, hle⟩

Result:
case intro.intro.intro.intro
ι : Type u_1
I J : Box ι
π₁ π₂ : Prepartition I
Hle : π₁ ≤ π₂
J₁ : Box ι
hJ₁ : J₁ ∈ π₁.boxes
hne : ↑J ⊓ ↑J₁ ≠ ⊥
J₂ : Box ι
hJ₂ : J₂ ∈ π₂
hle : J₁ ≤ J₂
⊢ ∃ J' ∈ Finset.image (fun J' => ↑J ⊓ ↑J') π₂.boxes, ↑J ⊓ ↑J₁ ≤ J'

Proof state:
case intro.intro.intro.intro
ι : Type u_1
I J : Box ι
π₁ π₂ : Prepartition I
Hle : π₁ ≤ π₂
J₁ : Box ι
hJ₁ : J₁ ∈ π₁.boxes
hne : ↑J ⊓ ↑J₁ ≠ ⊥
J₂ : Box ι
hJ₂ : J₂ ∈ π₂
hle : J₁ ≤ J₂
⊢ ∃ J' ∈ Finset.image (fun J' => ↑J ⊓ ↑J') π₂.boxes, ↑J ⊓ ↑J₁ ≤ J'

Tactic:
exact ⟨_, Finset.mem_image_of_mem _ hJ₂, inf_le_inf_left _ <| WithBot.coe_le_coe.2 hle⟩

Result:
no goals

Proof state:
ι : Type u_1
I J : Box ι
π₁ π₂ : Prepartition I
Hle : π₁ ≤ π₂
J₁ : WithBot (Box ι)
hJ₁ : J₁ ∈ Finset.image (fun J' => ↑J ⊓ ↑J') π₁.boxes
hne : J₁ ≠ ⊥
⊢ ∃ J' ∈ Finset.image (fun J' => ↑J ⊓ ↑J') π₂.boxes, J₁ ≤ J'

Tactic:
rw [Finset.mem_image] at hJ₁

Result:
ι : Type u_1
I J : Box ι
π₁ π₂ : Prepartition I
Hle : π₁ ≤ π₂
J₁ : WithBot (Box ι)
hJ₁ : ∃ a ∈ π₁.boxes, ↑J ⊓ ↑a = J₁
hne : J₁ ≠ ⊥
⊢ ∃ J' ∈ Finset.image (fun J' => ↑J ⊓ ↑J') π₂.boxes, J₁ ≤ J'
-- Mathlib/NumberTheory/LucasLehmer.lean
theorem right_distrib (x y z : X q) : (x + y) * z = x * z + y * z

Proof state:
q : ℕ+
x y z : X q
⊢ (x + y) * z = x * z + y * z

Tactic:
ext <;> dsimp <;> ring

Result:
no goals
-- Mathlib/MeasureTheory/MeasurableSpace/Basic.lean
theorem measurableSet_range_inr [MeasurableSpace α] :
    MeasurableSet (range Sum.inr : Set (α ⊕ β))

Proof state:
α : Type u_1
β : Type u_2
mβ : MeasurableSpace β
inst✝ : MeasurableSpace α
⊢ MeasurableSet (Sum.inr '' univ)

Tactic:
exact MeasurableSet.univ.inr_image

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
mβ : MeasurableSpace β
inst✝ : MeasurableSpace α
⊢ MeasurableSet (range Sum.inr)

Tactic:
rw [← image_univ]

Result:
α : Type u_1
β : Type u_2
mβ : MeasurableSpace β
inst✝ : MeasurableSpace α
⊢ MeasurableSet (Sum.inr '' univ)
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Int/Order.lean
theorem zero_max_ofNat (n : Nat) : (max 0 (n : Int)) = n

Proof state:
n : Nat
⊢ max 0 ↑n = ↑n

Tactic:
rw [Int.max_eq_right (ofNat_zero_le n)]

Result:
no goals
-- Mathlib/Data/Seq/WSeq.lean
theorem dropn_congr {s t : WSeq α} (h : s ~ʷ t) (n) : drop s n ~ʷ drop t n

Proof state:
α : Type u
s t : WSeq α
h : s ~ʷ t
n : ℕ
⊢ s.drop n ~ʷ t.drop n

Tactic:
induction n <;> simp [*, tail_congr, drop]

Result:
no goals
-- Mathlib/Data/Finset/Lattice/Fold.lean
theorem sup_eq_top_iff {α : Type*} [LinearOrder α] [BoundedOrder α] [Nontrivial α]
    {s : Finset ι} {f : ι → α} : s.sup f = ⊤ ↔ ∃ b ∈ s, f b = ⊤

Proof state:
ι : Type u_5
α : Type u_7
inst✝² : LinearOrder α
inst✝¹ : BoundedOrder α
inst✝ : Nontrivial α
s : Finset ι
f : ι → α
⊢ s.sup f = ⊤ ↔ ∃ b ∈ s, f b = ⊤

Tactic:
simp only [← top_le_iff]

Result:
ι : Type u_5
α : Type u_7
inst✝² : LinearOrder α
inst✝¹ : BoundedOrder α
inst✝ : Nontrivial α
s : Finset ι
f : ι → α
⊢ ⊤ ≤ s.sup f ↔ ∃ b ∈ s, ⊤ ≤ f b

Proof state:
ι : Type u_5
α : Type u_7
inst✝² : LinearOrder α
inst✝¹ : BoundedOrder α
inst✝ : Nontrivial α
s : Finset ι
f : ι → α
⊢ ⊤ ≤ s.sup f ↔ ∃ b ∈ s, ⊤ ≤ f b

Tactic:
exact Finset.le_sup_iff bot_lt_top

Result:
no goals
-- Mathlib/AlgebraicGeometry/Morphisms/Preimmersion.lean
theorem of_comp {X Y Z : Scheme} (f : X ⟶ Y) (g : Y ⟶ Z) [IsPreimmersion g]
    [IsPreimmersion (f ≫ g)] : IsPreimmersion f where
  base_embedding

Proof state:
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
inst✝¹ : IsPreimmersion g
inst✝ : IsPreimmersion (f ≫ g)
x : ↑↑X.toPresheafedSpace
h : Function.Surjective ⇑(ConcreteCategory.hom (Scheme.Hom.stalkMap (f ≫ g) x))
⊢ Function.Surjective ⇑(ConcreteCategory.hom (Scheme.Hom.stalkMap f x))

Tactic:
rw [Scheme.stalkMap_comp] at h

Result:
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
inst✝¹ : IsPreimmersion g
inst✝ : IsPreimmersion (f ≫ g)
x : ↑↑X.toPresheafedSpace
h :
  Function.Surjective
    ⇑(ConcreteCategory.hom (Scheme.Hom.stalkMap g ((ConcreteCategory.hom f.base) x) ≫ Scheme.Hom.stalkMap f x))
⊢ Function.Surjective ⇑(ConcreteCategory.hom (Scheme.Hom.stalkMap f x))

Proof state:
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
inst✝¹ : IsPreimmersion g
inst✝ : IsPreimmersion (f ≫ g)
x : ↑↑X.toPresheafedSpace
h :
  Function.Surjective
    ⇑(ConcreteCategory.hom (Scheme.Hom.stalkMap g ((ConcreteCategory.hom f.base) x) ≫ Scheme.Hom.stalkMap f x))
⊢ Function.Surjective ⇑(ConcreteCategory.hom (Scheme.Hom.stalkMap f x))

Tactic:
exact Function.Surjective.of_comp h

Result:
no goals

Proof state:
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
inst✝¹ : IsPreimmersion g
inst✝ : IsPreimmersion (f ≫ g)
x : ↑↑X.toPresheafedSpace
⊢ Function.Surjective ⇑(ConcreteCategory.hom (Scheme.Hom.stalkMap f x))

Tactic:
have h := (f ≫ g).stalkMap_surjective x

Result:
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
inst✝¹ : IsPreimmersion g
inst✝ : IsPreimmersion (f ≫ g)
x : ↑↑X.toPresheafedSpace
h : Function.Surjective ⇑(ConcreteCategory.hom (Scheme.Hom.stalkMap (f ≫ g) x))
⊢ Function.Surjective ⇑(ConcreteCategory.hom (Scheme.Hom.stalkMap f x))

Proof state:
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
inst✝¹ : IsPreimmersion g
inst✝ : IsPreimmersion (f ≫ g)
⊢ IsEmbedding ⇑(ConcreteCategory.hom f.base)

Tactic:
have h := (f ≫ g).isEmbedding

Result:
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
inst✝¹ : IsPreimmersion g
inst✝ : IsPreimmersion (f ≫ g)
h : IsEmbedding ⇑(ConcreteCategory.hom (f ≫ g).base)
⊢ IsEmbedding ⇑(ConcreteCategory.hom f.base)

Proof state:
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
inst✝¹ : IsPreimmersion g
inst✝ : IsPreimmersion (f ≫ g)
h : IsEmbedding ⇑(ConcreteCategory.hom (f ≫ g).base)
⊢ IsEmbedding ⇑(ConcreteCategory.hom f.base)

Tactic:
rwa [← g.isEmbedding.of_comp_iff]

Result:
no goals
-- Mathlib/Algebra/Colimit/Ring.lean
theorem mul_inv_cancel {p : Ring.DirectLimit G f} (hp : p ≠ 0) : p * inv G f p = 1

Proof state:
ι : Type u_1
inst✝³ : Preorder ι
G : ι → Type u_2
inst✝² : Nonempty ι
inst✝¹ : IsDirected ι fun x1 x2 => x1 ≤ x2
inst✝ : (i : ι) → Field (G i)
f : (i j : ι) → i ≤ j → G i → G j
p : Ring.DirectLimit G f
hp : p ≠ 0
⊢ p * inv G f p = 1

Tactic:
rw [inv, dif_neg hp, Classical.choose_spec (DirectLimit.exists_inv G f hp)]

Result:
no goals
-- Mathlib/LinearAlgebra/AffineSpace/FiniteDimensional.lean
theorem AffineIndependent.finrank_vectorSpan [Fintype ι] {p : ι → P} (hi : AffineIndependent k p)
    {n : ℕ} (hc : Fintype.card ι = n + 1) : finrank k (vectorSpan k (Set.range p)) = n

Proof state:
k : Type u_1
V : Type u_2
P : Type u_3
ι : Type u_4
inst✝⁴ : DivisionRing k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AffineSpace V P
inst✝ : Fintype ι
p : ι → P
hi : AffineIndependent k p
n : ℕ
hc : #Finset.univ = n + 1
⊢ finrank k ↥(vectorSpan k ↑(Finset.image p Finset.univ)) = n

Tactic:
exact hi.finrank_vectorSpan_image_finset hc

Result:
no goals

Proof state:
k : Type u_1
V : Type u_2
P : Type u_3
ι : Type u_4
inst✝⁴ : DivisionRing k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AffineSpace V P
inst✝ : Fintype ι
p : ι → P
hi : AffineIndependent k p
n : ℕ
hc : Fintype.card ι = n + 1
⊢ finrank k ↥(vectorSpan k (Set.range p)) = n

Tactic:
classical
rw [← Finset.card_univ] at hc
rw [← Set.image_univ, ← Finset.coe_univ, ← Finset.coe_image]
exact hi.finrank_vectorSpan_image_finset hc

Result:
no goals

Proof state:
k : Type u_1
V : Type u_2
P : Type u_3
ι : Type u_4
inst✝⁴ : DivisionRing k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AffineSpace V P
inst✝ : Fintype ι
p : ι → P
hi : AffineIndependent k p
n : ℕ
hc : Fintype.card ι = n + 1
⊢ finrank k ↥(vectorSpan k (Set.range p)) = n

Tactic:
rw [← Finset.card_univ] at hc

Result:
k : Type u_1
V : Type u_2
P : Type u_3
ι : Type u_4
inst✝⁴ : DivisionRing k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AffineSpace V P
inst✝ : Fintype ι
p : ι → P
hi : AffineIndependent k p
n : ℕ
hc : #Finset.univ = n + 1
⊢ finrank k ↥(vectorSpan k (Set.range p)) = n

Proof state:
k : Type u_1
V : Type u_2
P : Type u_3
ι : Type u_4
inst✝⁴ : DivisionRing k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AffineSpace V P
inst✝ : Fintype ι
p : ι → P
hi : AffineIndependent k p
n : ℕ
hc : #Finset.univ = n + 1
⊢ finrank k ↥(vectorSpan k (Set.range p)) = n

Tactic:
rw [← Set.image_univ, ← Finset.coe_univ, ← Finset.coe_image]

Result:
k : Type u_1
V : Type u_2
P : Type u_3
ι : Type u_4
inst✝⁴ : DivisionRing k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AffineSpace V P
inst✝ : Fintype ι
p : ι → P
hi : AffineIndependent k p
n : ℕ
hc : #Finset.univ = n + 1
⊢ finrank k ↥(vectorSpan k ↑(Finset.image p Finset.univ)) = n
-- Mathlib/AlgebraicGeometry/EllipticCurve/Weierstrass.lean
lemma map_injective {φ : R →+* A} (hφ : Function.Injective φ) :
    Function.Injective <| map (φ := φ) := fun _ _ h => by
  rcases mk.inj h with ⟨_, _, _, _, _⟩
  ext <;> apply_fun _ using hφ <;> assumption

Proof state:
R : Type u
inst✝¹ : CommRing R
A : Type v
inst✝ : CommRing A
φ : R →+* A
hφ : Function.Injective ⇑φ
x✝¹ x✝ : WeierstrassCurve R
h : (fun W => W.map φ) x✝¹ = (fun W => W.map φ) x✝
⊢ x✝¹ = x✝

Tactic:
rcases mk.inj h with ⟨_, _, _, _, _⟩

Result:
case intro.intro.intro.intro
R : Type u
inst✝¹ : CommRing R
A : Type v
inst✝ : CommRing A
φ : R →+* A
hφ : Function.Injective ⇑φ
x✝¹ x✝ : WeierstrassCurve R
h : (fun W => W.map φ) x✝¹ = (fun W => W.map φ) x✝
left✝³ : φ x✝¹.a₁ = φ x✝.a₁
left✝² : φ x✝¹.a₂ = φ x✝.a₂
left✝¹ : φ x✝¹.a₃ = φ x✝.a₃
left✝ : φ x✝¹.a₄ = φ x✝.a₄
right✝ : φ x✝¹.a₆ = φ x✝.a₆
⊢ x✝¹ = x✝

Proof state:
case intro.intro.intro.intro
R : Type u
inst✝¹ : CommRing R
A : Type v
inst✝ : CommRing A
φ : R →+* A
hφ : Function.Injective ⇑φ
x✝¹ x✝ : WeierstrassCurve R
h : (fun W => W.map φ) x✝¹ = (fun W => W.map φ) x✝
left✝³ : φ x✝¹.a₁ = φ x✝.a₁
left✝² : φ x✝¹.a₂ = φ x✝.a₂
left✝¹ : φ x✝¹.a₃ = φ x✝.a₃
left✝ : φ x✝¹.a₄ = φ x✝.a₄
right✝ : φ x✝¹.a₆ = φ x✝.a₆
⊢ x✝¹ = x✝

Tactic:
ext <;> apply_fun _ using hφ <;> assumption

Result:
no goals
-- Mathlib/FieldTheory/Separable.lean
theorem Separable.eval₂_derivative_ne_zero [Nontrivial S] (f : R →+* S) {p : R[X]}
    (h : p.Separable) {x : S} (hx : p.eval₂ f x = 0) :
    (derivative p).eval₂ f x ≠ 0

Proof state:
R : Type u
inst✝² : CommSemiring R
S : Type v
inst✝¹ : CommSemiring S
inst✝ : Nontrivial S
f : R →+* S
p : R[X]
h : p.Separable
x : S
hx : eval₂ f x p = 0
hx' : eval₂ f x (derivative p) = 0
⊢ False

Tactic:
obtain ⟨a, b, e⟩ := h

Result:
case intro.intro
R : Type u
inst✝² : CommSemiring R
S : Type v
inst✝¹ : CommSemiring S
inst✝ : Nontrivial S
f : R →+* S
p : R[X]
x : S
hx : eval₂ f x p = 0
hx' : eval₂ f x (derivative p) = 0
a b : R[X]
e : a * p + b * derivative p = 1
⊢ False

Proof state:
case intro.intro
R : Type u
inst✝² : CommSemiring R
S : Type v
inst✝¹ : CommSemiring S
inst✝ : Nontrivial S
f : R →+* S
p : R[X]
x : S
hx : eval₂ f x p = 0
hx' : eval₂ f x (derivative p) = 0
a b : R[X]
e : a * p + b * derivative p = 1
⊢ False

Tactic:
apply_fun Polynomial.eval₂ f x at e

Result:
case intro.intro
R : Type u
inst✝² : CommSemiring R
S : Type v
inst✝¹ : CommSemiring S
inst✝ : Nontrivial S
f : R →+* S
p : R[X]
x : S
hx : eval₂ f x p = 0
hx' : eval₂ f x (derivative p) = 0
a b : R[X]
e : eval₂ f x (a * p + b * derivative p) = eval₂ f x 1
⊢ False

Proof state:
R : Type u
inst✝² : CommSemiring R
S : Type v
inst✝¹ : CommSemiring S
inst✝ : Nontrivial S
f : R →+* S
p : R[X]
h : p.Separable
x : S
hx : eval₂ f x p = 0
⊢ eval₂ f x (derivative p) ≠ 0

Tactic:
intro hx'

Result:
R : Type u
inst✝² : CommSemiring R
S : Type v
inst✝¹ : CommSemiring S
inst✝ : Nontrivial S
f : R →+* S
p : R[X]
h : p.Separable
x : S
hx : eval₂ f x p = 0
hx' : eval₂ f x (derivative p) = 0
⊢ False

Proof state:
case intro.intro
R : Type u
inst✝² : CommSemiring R
S : Type v
inst✝¹ : CommSemiring S
inst✝ : Nontrivial S
f : R →+* S
p : R[X]
x : S
hx : eval₂ f x p = 0
hx' : eval₂ f x (derivative p) = 0
a b : R[X]
e : eval₂ f x (a * p + b * derivative p) = eval₂ f x 1
⊢ False

Tactic:
simp only [eval₂_add, eval₂_mul, hx, mul_zero, hx', add_zero, eval₂_one, zero_ne_one] at e

Result:
no goals
-- Mathlib/.lake/packages/batteries/Batteries/Data/RBMap/Lemmas.lean
theorem zoom_del {t : RBNode α} :
    t.zoom cut path = (t', path') →
    path.del (t.del cut) (match t with | node c .. => c | _ => red) =
    path'.del t'.delRoot (match t' with | node c .. => c | _ => red)

Proof state:
α : Type u_1
cut : α → Ordering
path : Path α
t' : RBNode α
path' : Path α
t : RBNode α
⊢ zoom cut t path = (t', path') →
    path.del (RBNode.del cut t)
        (match t with
        | node c l v r => c
        | x => red) =
      path'.del t'.delRoot
        (match t' with
        | node c l v r => c
        | x => red)

Tactic:
unfold RBNode.del

Result:
α : Type u_1
cut : α → Ordering
path : Path α
t' : RBNode α
path' : Path α
t : RBNode α
⊢ zoom cut t path = (t', path') →
    path.del
        (match t with
        | nil => nil
        | node c a y b =>
          match cut y with
          | Ordering.lt =>
            match a.isBlack with
            | black => (RBNode.del cut a).balLeft y b
            | red => node red (RBNode.del cut a) y b
          | Ordering.gt =>
            match b.isBlack with
            | black => a.balRight y (RBNode.del cut b)
            | red => node red a y (RBNode.del cut b)
          | Ordering.eq => a.append b)
        (match t with
        | node c l v r => c
        | x => red) =
      path'.del t'.delRoot
        (match t' with
        | node c l v r => c
        | x => red)

Proof state:
α : Type u_1
cut : α → Ordering
path : Path α
t' : RBNode α
path' : Path α
x✝¹ : RBNode α
c : RBColor
a : RBNode α
y : α
b : RBNode α
x✝ : Ordering
heq✝ : cut y = Ordering.lt
l✝ : RBNode α
v✝ : α
r✝ : RBNode α
IH :
  ∀ (cut : α → Ordering) (path : Path α) (t' : RBNode α) (path' : Path α),
    zoom cut (node red l✝ v✝ r✝) path = (t', path') →
      path.del (RBNode.del cut (node red l✝ v✝ r✝))
          (match node red l✝ v✝ r✝ with
          | node c l v r => c
          | x => red) =
        path'.del t'.delRoot
          (match t' with
          | node c l v r => c
          | x => red)
⊢ zoom cut (node red l✝ v✝ r✝) (left c path y b) = (t', path') →
    path.del
        (match (node red l✝ v✝ r✝).isBlack with
        | black => (RBNode.del cut (node red l✝ v✝ r✝)).balLeft y b
        | red => node red (RBNode.del cut (node red l✝ v✝ r✝)) y b)
        c =
      path'.del t'.delRoot
        (match t' with
        | node c l v r => c
        | x => red)

Tactic:
apply IH

Result:
no goals

Proof state:
case h_3
α : Type u_1
cut : α → Ordering
path : Path α
t' : RBNode α
path' : Path α
x✝¹ : RBNode α
c : RBColor
a : RBNode α
y : α
b : RBNode α
x✝ : Ordering
heq✝ : cut y = Ordering.eq
⊢ (node c a y b, path) = (t', path') →
    path.del (a.append b) c =
      path'.del t'.delRoot
        (match t' with
        | node c l v r => c
        | x => red)

Tactic:
intro | rfl => rfl

Result:
no goals
-- Mathlib/Analysis/Calculus/ContDiff/Bounds.lean
theorem norm_iteratedFDeriv_comp_le {g : F → G} {f : E → F} {n : ℕ} {N : WithTop ℕ∞}
    (hg : ContDiff 𝕜 N g) (hf : ContDiff 𝕜 N f) (hn : n ≤ N) (x : E) {C : ℝ} {D : ℝ}
    (hC : ∀ i, i ≤ n → ‖iteratedFDeriv 𝕜 i g (f x)‖ ≤ C)
    (hD : ∀ i, 1 ≤ i → i ≤ n → ‖iteratedFDeriv 𝕜 i f x‖ ≤ D ^ i) :
    ‖iteratedFDeriv 𝕜 n (g ∘ f) x‖ ≤ n ! * C * D ^ n

Proof state:
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type uE
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type uF
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
G : Type uG
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
g : F → G
f : E → F
n : ℕ
N : WithTop ℕ∞
hg : ContDiff 𝕜 N g
hf : ContDiff 𝕜 N f
hn : ↑n ≤ N
x : E
C D : ℝ
hC : ∀ i ≤ n, ‖iteratedFDeriv 𝕜 i g (f x)‖ ≤ C
hD : ∀ (i : ℕ), 1 ≤ i → i ≤ n → ‖iteratedFDeriv 𝕜 i f x‖ ≤ D ^ i
⊢ ‖iteratedFDeriv 𝕜 n (g ∘ f) x‖ ≤ ↑n ! * C * D ^ n

Tactic:
simp_rw [← iteratedFDerivWithin_univ] at hC hD ⊢

Result:
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type uE
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type uF
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
G : Type uG
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
g : F → G
f : E → F
n : ℕ
N : WithTop ℕ∞
hg : ContDiff 𝕜 N g
hf : ContDiff 𝕜 N f
hn : ↑n ≤ N
x : E
C D : ℝ
hC : ∀ i ≤ n, ‖iteratedFDerivWithin 𝕜 i g univ (f x)‖ ≤ C
hD : ∀ (i : ℕ), 1 ≤ i → i ≤ n → ‖iteratedFDerivWithin 𝕜 i f univ x‖ ≤ D ^ i
⊢ ‖iteratedFDerivWithin 𝕜 n (g ∘ f) univ x‖ ≤ ↑n ! * C * D ^ n

Proof state:
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type uE
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type uF
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
G : Type uG
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
g : F → G
f : E → F
n : ℕ
N : WithTop ℕ∞
hg : ContDiff 𝕜 N g
hf : ContDiff 𝕜 N f
hn : ↑n ≤ N
x : E
C D : ℝ
hC : ∀ i ≤ n, ‖iteratedFDerivWithin 𝕜 i g univ (f x)‖ ≤ C
hD : ∀ (i : ℕ), 1 ≤ i → i ≤ n → ‖iteratedFDerivWithin 𝕜 i f univ x‖ ≤ D ^ i
⊢ ‖iteratedFDerivWithin 𝕜 n (g ∘ f) univ x‖ ≤ ↑n ! * C * D ^ n

Tactic:
exact norm_iteratedFDerivWithin_comp_le hg.contDiffOn hf.contDiffOn hn uniqueDiffOn_univ
  uniqueDiffOn_univ (mapsTo_univ _ _) (mem_univ x) hC hD

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Pow/Real.lean
theorem rpow_inv_lt_iff_of_neg (hx : 0 < x) (hy : 0 < y) (hz : z < 0) :
    x ^ z⁻¹ < y ↔ y ^ z < x

Proof state:
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : z < 0
⊢ x ^ z⁻¹ < y ↔ y ^ z < x

Tactic:
rw [← rpow_lt_rpow_iff_of_neg hy _ hz, rpow_inv_rpow _ hz.ne] <;> positivity

Result:
no goals
-- Mathlib/CategoryTheory/Functor/KanExtension/Basic.lean
@[reassoc (attr := simp)]
lemma limitIsoOfIsRightKanExtension_hom_π (i : C) :
    (F'.limitIsoOfIsRightKanExtension α).hom ≫ limit.π F i = limit.π F' (L.obj i) ≫ α.app i

Proof state:
C : Type u_1
H : Type u_3
D : Type u_4
inst✝⁵ : Category.{u_8, u_1} C
inst✝⁴ : Category.{u_6, u_3} H
inst✝³ : Category.{u_7, u_4} D
F' : D ⥤ H
L : C ⥤ D
F : C ⥤ H
α : L ⋙ F' ⟶ F
inst✝² : F'.IsRightKanExtension α
inst✝¹ : HasLimit F
inst✝ : HasLimit F'
i : C
⊢ (F'.limitIsoOfIsRightKanExtension α).hom ≫ limit.π F i = limit.π F' (L.obj i) ≫ α.app i

Tactic:
rw [← Iso.eq_inv_comp, limitIsoOfIsRightKanExtension_inv_π]

Result:
no goals
-- Mathlib/Combinatorics/Quiver/Cast.lean
theorem Hom.cast_eq_iff_heq {u v u' v' : U} (hu : u = u') (hv : v = v') (e : u ⟶ v) (e' : u' ⟶ v') :
    e.cast hu hv = e' ↔ HEq e e'

Proof state:
U : Type u_1
inst✝ : Quiver U
u v u' v' : U
hu : u = u'
hv : v = v'
e : u ⟶ v
e' : u' ⟶ v'
⊢ _root_.cast ⋯ e = e' ↔ HEq e e'

Tactic:
exact _root_.cast_eq_iff_heq

Result:
no goals

Proof state:
U : Type u_1
inst✝ : Quiver U
u v u' v' : U
hu : u = u'
hv : v = v'
e : u ⟶ v
e' : u' ⟶ v'
⊢ cast hu hv e = e' ↔ HEq e e'

Tactic:
rw [Hom.cast_eq_cast]

Result:
U : Type u_1
inst✝ : Quiver U
u v u' v' : U
hu : u = u'
hv : v = v'
e : u ⟶ v
e' : u' ⟶ v'
⊢ _root_.cast ⋯ e = e' ↔ HEq e e'
-- Mathlib/Data/Finset/Union.lean
lemma biUnion_biUnion [DecidableEq γ] (s : Finset α) (f : α → Finset β) (g : β → Finset γ) :
    (s.biUnion f).biUnion g = s.biUnion fun a ↦ (f a).biUnion g

Proof state:
case h
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : DecidableEq β
inst✝ : DecidableEq γ
s : Finset α
f : α → Finset β
g : β → Finset γ
a✝ : γ
⊢ (∃ a, ∃ x ∈ s, a ∈ f x ∧ a✝ ∈ g a) ↔ ∃ a x, a ∈ s ∧ x ∈ f a ∧ a✝ ∈ g x

Tactic:
rw [exists_comm]

Result:
no goals

Proof state:
case h
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : DecidableEq β
inst✝ : DecidableEq γ
s : Finset α
f : α → Finset β
g : β → Finset γ
a✝ : γ
⊢ (∃ a, (∃ a_1 ∈ s, a ∈ f a_1) ∧ a✝ ∈ g a) ↔ ∃ a ∈ s, ∃ a_1 ∈ f a, a✝ ∈ g a_1

Tactic:
simp_rw [← exists_and_right, ← exists_and_left, and_assoc]

Result:
case h
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : DecidableEq β
inst✝ : DecidableEq γ
s : Finset α
f : α → Finset β
g : β → Finset γ
a✝ : γ
⊢ (∃ a, ∃ x ∈ s, a ∈ f x ∧ a✝ ∈ g a) ↔ ∃ a x, a ∈ s ∧ x ∈ f a ∧ a✝ ∈ g x

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : DecidableEq β
inst✝ : DecidableEq γ
s : Finset α
f : α → Finset β
g : β → Finset γ
⊢ (s.biUnion f).biUnion g = s.biUnion fun a => (f a).biUnion g

Tactic:
ext

Result:
case h
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : DecidableEq β
inst✝ : DecidableEq γ
s : Finset α
f : α → Finset β
g : β → Finset γ
a✝ : γ
⊢ a✝ ∈ (s.biUnion f).biUnion g ↔ a✝ ∈ s.biUnion fun a => (f a).biUnion g

Proof state:
case h
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : DecidableEq β
inst✝ : DecidableEq γ
s : Finset α
f : α → Finset β
g : β → Finset γ
a✝ : γ
⊢ a✝ ∈ (s.biUnion f).biUnion g ↔ a✝ ∈ s.biUnion fun a => (f a).biUnion g

Tactic:
simp only [Finset.mem_biUnion, exists_prop]

Result:
case h
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : DecidableEq β
inst✝ : DecidableEq γ
s : Finset α
f : α → Finset β
g : β → Finset γ
a✝ : γ
⊢ (∃ a, (∃ a_1 ∈ s, a ∈ f a_1) ∧ a✝ ∈ g a) ↔ ∃ a ∈ s, ∃ a_1 ∈ f a, a✝ ∈ g a_1
-- Mathlib/Topology/Basic.lean
theorem ClusterPt.of_nhds_le {f : Filter X} (H : 𝓝 x ≤ f) : ClusterPt x f

Proof state:
X : Type u
x : X
inst✝ : TopologicalSpace X
f : Filter X
H : 𝓝 x ≤ f
⊢ ClusterPt x f

Tactic:
simp only [ClusterPt, inf_eq_left.mpr H, nhds_neBot]

Result:
no goals
-- Mathlib/Algebra/Polynomial/Splits.lean
theorem eq_X_sub_C_of_splits_of_single_root {x : K} {h : K[X]} (h_splits : Splits i h)
    (h_roots : (h.map i).roots = {i x}) : h = C h.leadingCoeff * (X - C x)

Proof state:
K : Type v
L : Type w
inst✝¹ : Field K
inst✝ : Field L
i : K →+* L
x : K
h : K[X]
h_splits : Splits i h
h_roots : (map i h).roots = {i x}
⊢ h = C h.leadingCoeff * (X - C x)

Tactic:
apply Polynomial.map_injective _ i.injective

Result:
case a
K : Type v
L : Type w
inst✝¹ : Field K
inst✝ : Field L
i : K →+* L
x : K
h : K[X]
h_splits : Splits i h
h_roots : (map i h).roots = {i x}
⊢ map i h = map i (C h.leadingCoeff * (X - C x))

Proof state:
case a
K : Type v
L : Type w
inst✝¹ : Field K
inst✝ : Field L
i : K →+* L
x : K
h : K[X]
h_splits : Splits i h
h_roots : (map i h).roots = {i x}
⊢ map i h = map i (C h.leadingCoeff * (X - C x))

Tactic:
rw [eq_prod_roots_of_splits h_splits, h_roots]

Result:
case a
K : Type v
L : Type w
inst✝¹ : Field K
inst✝ : Field L
i : K →+* L
x : K
h : K[X]
h_splits : Splits i h
h_roots : (map i h).roots = {i x}
⊢ C (i h.leadingCoeff) * (Multiset.map (fun a => X - C a) {i x}).prod = map i (C h.leadingCoeff * (X - C x))

Proof state:
case a
K : Type v
L : Type w
inst✝¹ : Field K
inst✝ : Field L
i : K →+* L
x : K
h : K[X]
h_splits : Splits i h
h_roots : (map i h).roots = {i x}
⊢ C (i h.leadingCoeff) * (Multiset.map (fun a => X - C a) {i x}).prod = map i (C h.leadingCoeff * (X - C x))

Tactic:
simp

Result:
no goals