harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Algebra/Polynomial/Degree/Domain.lean
lemma eq_zero_of_dvd_of_natDegree_lt (h₁ : p ∣ q) (h₂ : natDegree q < natDegree p) :
    q = 0

Proof state:
R : Type u
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
p q : R[X]
h₁ : p ∣ q
h₂ : q.natDegree < p.natDegree
⊢ q = 0

Tactic:
by_contra hc

Result:
R : Type u
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
p q : R[X]
h₁ : p ∣ q
h₂ : q.natDegree < p.natDegree
hc : ¬q = 0
⊢ False

Proof state:
R : Type u
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
p q : R[X]
h₁ : p ∣ q
h₂ : q.natDegree < p.natDegree
hc : ¬q = 0
⊢ False

Tactic:
exact (lt_iff_not_ge _ _).mp h₂ (natDegree_le_of_dvd h₁ hc)

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Int/Cooper.lean
theorem dvd_mul_emod_add_of_dvd_mul_add {a b c d x : Int}
    (w : a ∣ b * x + c) (h : (a / gcd a b) ∣ d) :
    a ∣ b * (x % d) + c

Proof state:
case intro.intro
a b c x p : Int
w : b * x + c = a * p
q : Int
⊢ a ∣ b * (x % (a / ↑(a.gcd b) * q)) + c

Tactic:
rw [Int.emod_def, Int.mul_sub, Int.sub_eq_add_neg, Int.add_right_comm, w,
  Int.dvd_add_right (Int.dvd_mul_right _ _), ← Int.mul_assoc, ← Int.mul_assoc, Int.dvd_neg,
  ← Int.mul_ediv_assoc b gcd_dvd_left, Int.mul_comm b a, Int.mul_ediv_assoc a gcd_dvd_right,
  Int.mul_assoc, Int.mul_assoc]

Result:
case intro.intro
a b c x p : Int
w : b * x + c = a * p
q : Int
⊢ a ∣ a * (b / ↑(a.gcd b) * (q * (x / (a / ↑(a.gcd b) * q))))

Proof state:
case intro.intro
a b c x p : Int
w : b * x + c = a * p
q : Int
⊢ a ∣ a * (b / ↑(a.gcd b) * (q * (x / (a / ↑(a.gcd b) * q))))

Tactic:
apply Int.dvd_mul_right

Result:
no goals

Proof state:
a b c d x : Int
w : a ∣ b * x + c
h : a / ↑(a.gcd b) ∣ d
⊢ a ∣ b * (x % d) + c

Tactic:
obtain ⟨p, w⟩ := w

Result:
case intro
a b c d x : Int
h : a / ↑(a.gcd b) ∣ d
p : Int
w : b * x + c = a * p
⊢ a ∣ b * (x % d) + c

Proof state:
case intro
a b c d x : Int
h : a / ↑(a.gcd b) ∣ d
p : Int
w : b * x + c = a * p
⊢ a ∣ b * (x % d) + c

Tactic:
obtain ⟨q, rfl⟩ := h

Result:
case intro.intro
a b c x p : Int
w : b * x + c = a * p
q : Int
⊢ a ∣ b * (x % (a / ↑(a.gcd b) * q)) + c
-- Mathlib/CategoryTheory/Sites/DenseSubsite/Basic.lean
theorem sheafHom_restrict_eq (α : G.op ⋙ ℱ ⟶ G.op ⋙ ℱ'.val) :
    whiskerLeft G.op (sheafHom α) = α

Proof state:
case w.h.a.w.h.h
C : Type u_1
inst✝⁴ : Category.{u_6, u_1} C
D : Type u_2
inst✝³ : Category.{u_7, u_2} D
K : GrothendieckTopology D
A : Type u_4
inst✝² : Category.{u_5, u_4} A
G : C ⥤ D
inst✝¹ : G.IsCoverDense K
inst✝ : G.IsLocallyFull K
ℱ : Dᵒᵖ ⥤ A
ℱ' : Sheaf K A
α : G.op ⋙ ℱ ⟶ G.op ⋙ ℱ'.val
X : Cᵒᵖ
U : Aᵒᵖ
a✝ : (yoneda.obj ((G.op ⋙ ℱ).obj X)).obj U
⊢ (let_fun this := (yoneda.map (α.app X)).app U a✝;
    this) =
    ((sheafYonedaHom α).app (G.op.obj X)).app U a✝

Tactic:
apply sheaf_eq_amalgamation ℱ' (G.is_cover_of_isCoverDense _ _)

Result:
case w.h.a.w.h.h.hx
C : Type u_1
inst✝⁴ : Category.{u_6, u_1} C
D : Type u_2
inst✝³ : Category.{u_7, u_2} D
K : GrothendieckTopology D
A : Type u_4
inst✝² : Category.{u_5, u_4} A
G : C ⥤ D
inst✝¹ : G.IsCoverDense K
inst✝ : G.IsLocallyFull K
ℱ : Dᵒᵖ ⥤ A
ℱ' : Sheaf K A
α : G.op ⋙ ℱ ⟶ G.op ⋙ ℱ'.val
X : Cᵒᵖ
U : Aᵒᵖ
a✝ : (yoneda.obj ((G.op ⋙ ℱ).obj X)).obj U
⊢ (pushforwardFamily (homOver α (unop U)) a✝).Compatible

case w.h.a.w.h.h.h
C : Type u_1
inst✝⁴ : Category.{u_6, u_1} C
D : Type u_2
inst✝³ : Category.{u_7, u_2} D
K : GrothendieckTopology D
A : Type u_4
inst✝² : Category.{u_5, u_4} A
G : C ⥤ D
inst✝¹ : G.IsCoverDense K
inst✝ : G.IsLocallyFull K
ℱ : Dᵒᵖ ⥤ A
ℱ' : Sheaf K A
α : G.op ⋙ ℱ ⟶ G.op ⋙ ℱ'.val
X : Cᵒᵖ
U : Aᵒᵖ
a✝ : (yoneda.obj ((G.op ⋙ ℱ).obj X)).obj U
⊢ (pushforwardFamily (homOver α (unop U)) a✝).IsAmalgamation
    (let_fun this := (yoneda.map (α.app X)).app U a✝;
    this)

Proof state:
case w.h.a.w.h.h
C : Type u_1
inst✝⁴ : Category.{u_6, u_1} C
D : Type u_2
inst✝³ : Category.{u_7, u_2} D
K : GrothendieckTopology D
A : Type u_4
inst✝² : Category.{u_5, u_4} A
G : C ⥤ D
inst✝¹ : G.IsCoverDense K
inst✝ : G.IsLocallyFull K
ℱ : Dᵒᵖ ⥤ A
ℱ' : Sheaf K A
α : G.op ⋙ ℱ ⟶ G.op ⋙ ℱ'.val
X : Cᵒᵖ
U : Aᵒᵖ
a✝ : (yoneda.obj ((G.op ⋙ ℱ).obj X)).obj U
⊢ (yoneda.map ((whiskerLeft G.op (sheafHom α)).app X)).app U a✝ = (yoneda.map (α.app X)).app U a✝

Tactic:
erw [yoneda.map_preimage]

Result:
case w.h.a.w.h.h
C : Type u_1
inst✝⁴ : Category.{u_6, u_1} C
D : Type u_2
inst✝³ : Category.{u_7, u_2} D
K : GrothendieckTopology D
A : Type u_4
inst✝² : Category.{u_5, u_4} A
G : C ⥤ D
inst✝¹ : G.IsCoverDense K
inst✝ : G.IsLocallyFull K
ℱ : Dᵒᵖ ⥤ A
ℱ' : Sheaf K A
α : G.op ⋙ ℱ ⟶ G.op ⋙ ℱ'.val
X : Cᵒᵖ
U : Aᵒᵖ
a✝ : (yoneda.obj ((G.op ⋙ ℱ).obj X)).obj U
⊢ ((sheafYonedaHom α).app (G.op.obj X)).app U a✝ = (yoneda.map (α.app X)).app U a✝
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Lemmas.lean
theorem getElem_swap_left (a : Vector α n) {i j : Nat} {hi hj} :
    (a.swap i j hi hj)[i]'(by simpa using hi) = a[j]

Proof state:
α : Type ?u.454655
n : Nat
a : Vector α n
i j : Nat
hi : i < n
hj : j < n
⊢ i < n

Tactic:
simpa using hi

Result:
no goals

Proof state:
α : Type u_1
n : Nat
a : Vector α n
i j : Nat
hi : i < n
hj : j < n
⊢ (a.swap i j hi hj)[i] = a[j]

Tactic:
simp [getElem_swap]

Result:
no goals
-- Mathlib/CategoryTheory/Functor/FullyFaithful.lean
theorem isIso_of_fully_faithful (f : X ⟶ Y) [IsIso (F.map f)] : IsIso f :=
  ⟨⟨F.preimage (inv (F.map f)), ⟨F.map_injective (by simp), F.map_injective (by simp)⟩⟩⟩

Proof state:
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
F : C ⥤ D
inst✝² : F.Full
inst✝¹ : F.Faithful
X Y : C
f : X ⟶ Y
inst✝ : IsIso (F.map f)
⊢ F.map (f ≫ F.preimage (inv (F.map f))) = F.map (𝟙 X)

Tactic:
simp

Result:
no goals

Proof state:
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
F : C ⥤ D
inst✝² : F.Full
inst✝¹ : F.Faithful
X Y : C
f : X ⟶ Y
inst✝ : IsIso (F.map f)
⊢ F.map (F.preimage (inv (F.map f)) ≫ f) = F.map (𝟙 Y)

Tactic:
simp

Result:
no goals
-- Mathlib/NumberTheory/NumberField/CanonicalEmbedding/Basic.lean
theorem norm_eq_of_normAtPlace_eq {x y : mixedSpace K}
    (h : ∀ w, normAtPlace w x = normAtPlace w y) :
    mixedEmbedding.norm x = mixedEmbedding.norm y

Proof state:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x y : mixedSpace K
h : ∀ (w : InfinitePlace K), (normAtPlace w) x = (normAtPlace w) y
⊢ mixedEmbedding.norm x = mixedEmbedding.norm y

Tactic:
simp_rw [mixedEmbedding.norm_apply, h]

Result:
no goals
-- Mathlib/Algebra/Homology/HomotopyCofiber.lean
@[reassoc]
lemma d_fstX (i j k : ι) (hij : c.Rel i j) (hjk : c.Rel j k) :
    d φ i j ≫ fstX φ j k hjk = -fstX φ i j hij ≫ F.d j k

Proof state:
C : Type u_1
inst✝³ : Category.{u_3, u_1} C
inst✝² : Preadditive C
ι : Type u_2
c : ComplexShape ι
F G : HomologicalComplex C c
φ : F ⟶ G
inst✝¹ : HasHomotopyCofiber φ
inst✝ : DecidableRel c.Rel
i j k : ι
hij : c.Rel i j
hjk : c.Rel j k
⊢ d φ i j ≫ fstX φ j k hjk = -fstX φ i j hij ≫ F.d j k

Tactic:
obtain rfl := c.next_eq' hjk

Result:
C : Type u_1
inst✝³ : Category.{u_3, u_1} C
inst✝² : Preadditive C
ι : Type u_2
c : ComplexShape ι
F G : HomologicalComplex C c
φ : F ⟶ G
inst✝¹ : HasHomotopyCofiber φ
inst✝ : DecidableRel c.Rel
i j : ι
hij : c.Rel i j
hjk : c.Rel j (c.next j)
⊢ d φ i j ≫ fstX φ j (c.next j) hjk = -fstX φ i j hij ≫ F.d j (c.next j)

Proof state:
C : Type u_1
inst✝³ : Category.{u_3, u_1} C
inst✝² : Preadditive C
ι : Type u_2
c : ComplexShape ι
F G : HomologicalComplex C c
φ : F ⟶ G
inst✝¹ : HasHomotopyCofiber φ
inst✝ : DecidableRel c.Rel
i j : ι
hij : c.Rel i j
hjk : c.Rel j (c.next j)
⊢ d φ i j ≫ fstX φ j (c.next j) hjk = -fstX φ i j hij ≫ F.d j (c.next j)

Tactic:
simp [d, dif_pos hij, dif_pos hjk]

Result:
no goals
-- Mathlib/Algebra/Exact.lean
lemma comp_injective [Zero P] [Zero P'] (exact : Exact f g)
    (inj : Function.Injective g') (h0 : g' 0 = 0) :
    Exact f (g' ∘ g)

Proof state:
M : Type u_2
N : Type u_4
P : Type u_6
P' : Type u_7
f : M → N
g : N → P
g' : P → P'
inst✝¹ : Zero P
inst✝ : Zero P'
exact : Exact f g
inj : Injective g'
h0 : g' 0 = 0
x : N
H : x ∈ Set.range f
⊢ (g' ∘ g) x = 0

Tactic:
rw [Function.comp_apply, exact x |>.mpr H, h0]

Result:
no goals

Proof state:
M : Type u_2
N : Type u_4
P : Type u_6
P' : Type u_7
f : M → N
g : N → P
g' : P → P'
inst✝¹ : Zero P
inst✝ : Zero P'
exact : Exact f g
inj : Injective g'
h0 : g' 0 = 0
x : N
⊢ (g' ∘ g) x = 0 ↔ x ∈ Set.range f

Tactic:
refine ⟨fun H => exact x |>.mp <| inj <| h0 ▸ H, ?_⟩

Result:
M : Type u_2
N : Type u_4
P : Type u_6
P' : Type u_7
f : M → N
g : N → P
g' : P → P'
inst✝¹ : Zero P
inst✝ : Zero P'
exact : Exact f g
inj : Injective g'
h0 : g' 0 = 0
x : N
⊢ x ∈ Set.range f → (g' ∘ g) x = 0

Proof state:
M : Type u_2
N : Type u_4
P : Type u_6
P' : Type u_7
f : M → N
g : N → P
g' : P → P'
inst✝¹ : Zero P
inst✝ : Zero P'
exact : Exact f g
inj : Injective g'
h0 : g' 0 = 0
x : N
⊢ x ∈ Set.range f → (g' ∘ g) x = 0

Tactic:
intro H

Result:
M : Type u_2
N : Type u_4
P : Type u_6
P' : Type u_7
f : M → N
g : N → P
g' : P → P'
inst✝¹ : Zero P
inst✝ : Zero P'
exact : Exact f g
inj : Injective g'
h0 : g' 0 = 0
x : N
H : x ∈ Set.range f
⊢ (g' ∘ g) x = 0

Proof state:
M : Type u_2
N : Type u_4
P : Type u_6
P' : Type u_7
f : M → N
g : N → P
g' : P → P'
inst✝¹ : Zero P
inst✝ : Zero P'
exact : Exact f g
inj : Injective g'
h0 : g' 0 = 0
⊢ Exact f (g' ∘ g)

Tactic:
intro x

Result:
M : Type u_2
N : Type u_4
P : Type u_6
P' : Type u_7
f : M → N
g : N → P
g' : P → P'
inst✝¹ : Zero P
inst✝ : Zero P'
exact : Exact f g
inj : Injective g'
h0 : g' 0 = 0
x : N
⊢ (g' ∘ g) x = 0 ↔ x ∈ Set.range f
-- Mathlib/Analysis/BoxIntegral/Partition/Split.lean
theorem inf_splitMany {I : Box ι} (π : Prepartition I) (s : Finset (ι × ℝ)) :
    π ⊓ splitMany I s = π.biUnion fun J => splitMany J s

Proof state:
case insert
ι : Type u_1
I : Box ι
π : Prepartition I
p : ι × ℝ
s : Finset (ι × ℝ)
a✝ : p ∉ s
ihp : π ⊓ splitMany I s = π.biUnion fun J => splitMany J s
⊢ π ⊓ splitMany I (insert p s) = π.biUnion fun J => splitMany J (insert p s)

Tactic:
simp_rw [splitMany_insert, ← inf_assoc, ihp, inf_split, biUnion_assoc]

Result:
no goals

Proof state:
case empty
ι : Type u_1
I : Box ι
π : Prepartition I
⊢ π ⊓ splitMany I ∅ = π.biUnion fun J => splitMany J ∅

Tactic:
simp

Result:
no goals

Proof state:
ι : Type u_1
I : Box ι
π : Prepartition I
s : Finset (ι × ℝ)
⊢ π ⊓ splitMany I s = π.biUnion fun J => splitMany J s

Tactic:
induction' s using Finset.induction_on with p s _ ihp

Result:
case empty
ι : Type u_1
I : Box ι
π : Prepartition I
⊢ π ⊓ splitMany I ∅ = π.biUnion fun J => splitMany J ∅

case insert
ι : Type u_1
I : Box ι
π : Prepartition I
p : ι × ℝ
s : Finset (ι × ℝ)
a✝ : p ∉ s
ihp : π ⊓ splitMany I s = π.biUnion fun J => splitMany J s
⊢ π ⊓ splitMany I (insert p s) = π.biUnion fun J => splitMany J (insert p s)
-- Mathlib/FieldTheory/IntermediateField/Adjoin/Basic.lean
theorem bot_eq_top_of_rank_adjoin_eq_one (h : ∀ x : E, Module.rank F F⟮x⟯ = 1) :
    (⊥ : IntermediateField F E) = ⊤

Proof state:
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
h : ∀ (x : E), Module.rank F ↥F⟮x⟯ = 1
⊢ ⊥ = ⊤

Tactic:
ext y

Result:
case h
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
h : ∀ (x : E), Module.rank F ↥F⟮x⟯ = 1
y : E
⊢ y ∈ ⊥ ↔ y ∈ ⊤

Proof state:
case h
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
h : ∀ (x : E), Module.rank F ↥F⟮x⟯ = 1
y : E
⊢ y ∈ ⊥ ↔ y ∈ ⊤

Tactic:
rw [iff_true_right IntermediateField.mem_top]

Result:
case h
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
h : ∀ (x : E), Module.rank F ↥F⟮x⟯ = 1
y : E
⊢ y ∈ ⊥

Proof state:
case h
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
h : ∀ (x : E), Module.rank F ↥F⟮x⟯ = 1
y : E
⊢ y ∈ ⊥

Tactic:
exact rank_adjoin_simple_eq_one_iff.mp (h y)

Result:
no goals
-- Mathlib/MeasureTheory/Function/SimpleFuncDense.lean
theorem edist_nearestPt_le (e : ℕ → α) (x : α) {k N : ℕ} (hk : k ≤ N) :
    edist (nearestPt e N x) x ≤ edist (e k) x

Proof state:
case pos.inl
α : Type u_1
inst✝² : MeasurableSpace α
inst✝¹ : PseudoEMetricSpace α
inst✝ : OpensMeasurableSpace α
e : ℕ → α
x : α
N : ℕ
ihN : ∀ {k : ℕ}, k ≤ N → edist ((nearestPt e N) x) x ≤ edist (e k) x
h : ∀ k ≤ N, edist (e (N + 1)) x < edist (e k) x
hk : N + 1 ≤ N + 1
⊢ edist (e (N + 1)) x ≤ edist (e (N + 1)) x

case pos.inr
α : Type u_1
inst✝² : MeasurableSpace α
inst✝¹ : PseudoEMetricSpace α
inst✝ : OpensMeasurableSpace α
e : ℕ → α
x : α
N : ℕ
ihN : ∀ {k : ℕ}, k ≤ N → edist ((nearestPt e N) x) x ≤ edist (e k) x
k : ℕ
hk✝ : k ≤ N + 1
h : ∀ k ≤ N, edist (e (N + 1)) x < edist (e k) x
hk : k < N + 1
⊢ edist (e (N + 1)) x ≤ edist (e k) x

Tactic:
exacts [le_rfl, (h k (Nat.lt_succ_iff.1 hk)).le]

Result:
no goals
-- Mathlib/RingTheory/Ideal/Quotient/Defs.lean
theorem quotient_ring_saturate (s : Set R) :
    mk I ⁻¹' (mk I '' s) = ⋃ x : I, (fun y => x.1 + y) '' s

Proof state:
case h
R : Type u
inst✝¹ : Ring R
I : Ideal R
inst✝ : I.IsTwoSided
s : Set R
x : R
⊢ x ∈ ⇑(mk I) ⁻¹' (⇑(mk I) '' s) ↔ x ∈ ⋃ x, (fun y => ↑x + y) '' s

Tactic:
simp only [mem_preimage, mem_image, mem_iUnion, Ideal.Quotient.eq]

Result:
case h
R : Type u
inst✝¹ : Ring R
I : Ideal R
inst✝ : I.IsTwoSided
s : Set R
x : R
⊢ (∃ x_1 ∈ s, x_1 - x ∈ I) ↔ ∃ i, ∃ x_1 ∈ s, ↑i + x_1 = x

Proof state:
case h
R : Type u
inst✝¹ : Ring R
I : Ideal R
inst✝ : I.IsTwoSided
s : Set R
x : R
⊢ (∃ x_1 ∈ s, x_1 - x ∈ I) ↔ ∃ i, ∃ x_1 ∈ s, ↑i + x_1 = x

Tactic:
exact
  ⟨fun ⟨a, a_in, h⟩ => ⟨⟨_, I.neg_mem h⟩, a, a_in, by simp⟩, fun ⟨⟨i, hi⟩, a, ha, Eq⟩ =>
    ⟨a, ha, by rw [← Eq, sub_add_eq_sub_sub_swap, sub_self, zero_sub]; exact I.neg_mem hi⟩⟩

Result:
no goals

Proof state:
R : Type u
inst✝¹ : Ring R
I : Ideal R
inst✝ : I.IsTwoSided
s : Set R
⊢ ⇑(mk I) ⁻¹' (⇑(mk I) '' s) = ⋃ x, (fun y => ↑x + y) '' s

Tactic:
ext x

Result:
case h
R : Type u
inst✝¹ : Ring R
I : Ideal R
inst✝ : I.IsTwoSided
s : Set R
x : R
⊢ x ∈ ⇑(mk I) ⁻¹' (⇑(mk I) '' s) ↔ x ∈ ⋃ x, (fun y => ↑x + y) '' s

Proof state:
R : Type u
inst✝¹ : Ring R
I : Ideal R
inst✝ : I.IsTwoSided
s : Set R
x : R
x✝ : ∃ i, ∃ x_1 ∈ s, ↑i + x_1 = x
i : R
hi : i ∈ I
a : R
ha : a ∈ s
Eq : ↑⟨i, hi⟩ + a = x
⊢ -↑⟨i, hi⟩ ∈ I

Tactic:
exact I.neg_mem hi

Result:
no goals

Proof state:
R : Type u
inst✝¹ : Ring R
I : Ideal R
inst✝ : I.IsTwoSided
s : Set R
x : R
x✝ : ∃ x_1 ∈ s, x_1 - x ∈ I
a : R
a_in : a ∈ s
h : a - x ∈ I
⊢ ↑⟨-(a - x), ⋯⟩ + a = x

Tactic:
simp

Result:
no goals

Proof state:
R : Type u
inst✝¹ : Ring R
I : Ideal R
inst✝ : I.IsTwoSided
s : Set R
x : R
x✝ : ∃ i, ∃ x_1 ∈ s, ↑i + x_1 = x
i : R
hi : i ∈ I
a : R
ha : a ∈ s
Eq : ↑⟨i, hi⟩ + a = x
⊢ a - x ∈ I

Tactic:
rw [← Eq, sub_add_eq_sub_sub_swap, sub_self, zero_sub]

Result:
R : Type u
inst✝¹ : Ring R
I : Ideal R
inst✝ : I.IsTwoSided
s : Set R
x : R
x✝ : ∃ i, ∃ x_1 ∈ s, ↑i + x_1 = x
i : R
hi : i ∈ I
a : R
ha : a ∈ s
Eq : ↑⟨i, hi⟩ + a = x
⊢ -↑⟨i, hi⟩ ∈ I
-- Mathlib/Analysis/Calculus/LHopital.lean
theorem lhopital_zero_nhds_right (hff' : ∀ᶠ x in 𝓝[>] a, HasDerivAt f (f' x) x)
    (hgg' : ∀ᶠ x in 𝓝[>] a, HasDerivAt g (g' x) x) (hg' : ∀ᶠ x in 𝓝[>] a, g' x ≠ 0)
    (hfa : Tendsto f (𝓝[>] a) (𝓝 0)) (hga : Tendsto g (𝓝[>] a) (𝓝 0))
    (hdiv : Tendsto (fun x => f' x / g' x) (𝓝[>] a) l) :
    Tendsto (fun x => f x / g x) (𝓝[>] a) l

Proof state:
a : ℝ
l : Filter ℝ
f f' g g' : ℝ → ℝ
hff' : ∃ v ∈ 𝓝[>] a, ∀ y ∈ v, HasDerivAt f (f' y) y
hgg' : ∃ v ∈ 𝓝[>] a, ∀ y ∈ v, HasDerivAt g (g' y) y
hg' : ∃ v ∈ 𝓝[>] a, ∀ y ∈ v, g' y ≠ 0
hfa : Tendsto f (𝓝[>] a) (𝓝 0)
hga : Tendsto g (𝓝[>] a) (𝓝 0)
hdiv : Tendsto (fun x => f' x / g' x) (𝓝[>] a) l
⊢ Tendsto (fun x => f x / g x) (𝓝[>] a) l

Tactic:
rcases hff' with ⟨s₁, hs₁, hff'⟩

Result:
case intro.intro
a : ℝ
l : Filter ℝ
f f' g g' : ℝ → ℝ
hgg' : ∃ v ∈ 𝓝[>] a, ∀ y ∈ v, HasDerivAt g (g' y) y
hg' : ∃ v ∈ 𝓝[>] a, ∀ y ∈ v, g' y ≠ 0
hfa : Tendsto f (𝓝[>] a) (𝓝 0)
hga : Tendsto g (𝓝[>] a) (𝓝 0)
hdiv : Tendsto (fun x => f' x / g' x) (𝓝[>] a) l
s₁ : Set ℝ
hs₁ : s₁ ∈ 𝓝[>] a
hff' : ∀ y ∈ s₁, HasDerivAt f (f' y) y
⊢ Tendsto (fun x => f x / g x) (𝓝[>] a) l

Proof state:
case intro.intro
a : ℝ
l : Filter ℝ
f f' g g' : ℝ → ℝ
hgg' : ∃ v ∈ 𝓝[>] a, ∀ y ∈ v, HasDerivAt g (g' y) y
hg' : ∃ v ∈ 𝓝[>] a, ∀ y ∈ v, g' y ≠ 0
hfa : Tendsto f (𝓝[>] a) (𝓝 0)
hga : Tendsto g (𝓝[>] a) (𝓝 0)
hdiv : Tendsto (fun x => f' x / g' x) (𝓝[>] a) l
s₁ : Set ℝ
hs₁ : s₁ ∈ 𝓝[>] a
hff' : ∀ y ∈ s₁, HasDerivAt f (f' y) y
⊢ Tendsto (fun x => f x / g x) (𝓝[>] a) l

Tactic:
rcases hgg' with ⟨s₂, hs₂, hgg'⟩

Result:
case intro.intro.intro.intro
a : ℝ
l : Filter ℝ
f f' g g' : ℝ → ℝ
hg' : ∃ v ∈ 𝓝[>] a, ∀ y ∈ v, g' y ≠ 0
hfa : Tendsto f (𝓝[>] a) (𝓝 0)
hga : Tendsto g (𝓝[>] a) (𝓝 0)
hdiv : Tendsto (fun x => f' x / g' x) (𝓝[>] a) l
s₁ : Set ℝ
hs₁ : s₁ ∈ 𝓝[>] a
hff' : ∀ y ∈ s₁, HasDerivAt f (f' y) y
s₂ : Set ℝ
hs₂ : s₂ ∈ 𝓝[>] a
hgg' : ∀ y ∈ s₂, HasDerivAt g (g' y) y
⊢ Tendsto (fun x => f x / g x) (𝓝[>] a) l

Proof state:
a : ℝ
l : Filter ℝ
f f' g g' : ℝ → ℝ
hff' : ∀ᶠ (x : ℝ) in 𝓝[>] a, HasDerivAt f (f' x) x
hgg' : ∀ᶠ (x : ℝ) in 𝓝[>] a, HasDerivAt g (g' x) x
hg' : ∀ᶠ (x : ℝ) in 𝓝[>] a, g' x ≠ 0
hfa : Tendsto f (𝓝[>] a) (𝓝 0)
hga : Tendsto g (𝓝[>] a) (𝓝 0)
hdiv : Tendsto (fun x => f' x / g' x) (𝓝[>] a) l
⊢ Tendsto (fun x => f x / g x) (𝓝[>] a) l

Tactic:
rw [eventually_iff_exists_mem] at *

Result:
a : ℝ
l : Filter ℝ
f f' g g' : ℝ → ℝ
hff' : ∃ v ∈ 𝓝[>] a, ∀ y ∈ v, HasDerivAt f (f' y) y
hgg' : ∃ v ∈ 𝓝[>] a, ∀ y ∈ v, HasDerivAt g (g' y) y
hg' : ∃ v ∈ 𝓝[>] a, ∀ y ∈ v, g' y ≠ 0
hfa : Tendsto f (𝓝[>] a) (𝓝 0)
hga : Tendsto g (𝓝[>] a) (𝓝 0)
hdiv : Tendsto (fun x => f' x / g' x) (𝓝[>] a) l
⊢ Tendsto (fun x => f x / g x) (𝓝[>] a) l
-- Mathlib/Data/Finset/NAry.lean
theorem image₂_singleton_inter [DecidableEq β] (t₁ t₂ : Finset β) (hf : Injective (f a)) :
    image₂ f {a} (t₁ ∩ t₂) = image₂ f {a} t₁ ∩ image₂ f {a} t₂

Proof state:
α : Type u_1
β : Type u_3
γ : Type u_5
inst✝¹ : DecidableEq γ
f : α → β → γ
a : α
inst✝ : DecidableEq β
t₁ t₂ : Finset β
hf : Injective (f a)
⊢ image₂ f {a} (t₁ ∩ t₂) = image₂ f {a} t₁ ∩ image₂ f {a} t₂

Tactic:
simp_rw [image₂_singleton_left, image_inter _ _ hf]

Result:
no goals
-- Mathlib/.lake/packages/batteries/Batteries/Data/DList/Lemmas.lean
theorem ofList_toList (l : DList α) : DList.ofList (DList.toList l) = l

Proof state:
α : Type u_1
l : DList α
⊢ ofList l.toList = l

Tactic:
obtain ⟨app, inv⟩ := l

Result:
case mk
α : Type u_1
app : List α → List α
inv : ∀ (l : List α), app l = app [] ++ l
⊢ ofList { apply := app, invariant := inv }.toList = { apply := app, invariant := inv }

Proof state:
case mk.h
α : Type u_1
app : List α → List α
inv : ∀ (l : List α), app l = app [] ++ l
x : List α
⊢ app [] ++ x = app x

Tactic:
rw [(inv x)]

Result:
no goals

Proof state:
case mk
α : Type u_1
app : List α → List α
inv : ∀ (l : List α), app l = app [] ++ l
⊢ ofList { apply := app, invariant := inv }.toList = { apply := app, invariant := inv }

Tactic:
simp only [ofList, toList, mk.injEq]

Result:
case mk
α : Type u_1
app : List α → List α
inv : ∀ (l : List α), app l = app [] ++ l
⊢ (fun x => app [] ++ x) = app

Proof state:
case mk
α : Type u_1
app : List α → List α
inv : ∀ (l : List α), app l = app [] ++ l
⊢ (fun x => app [] ++ x) = app

Tactic:
funext x

Result:
case mk.h
α : Type u_1
app : List α → List α
inv : ∀ (l : List α), app l = app [] ++ l
x : List α
⊢ app [] ++ x = app x
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Zip.lean
theorem getElem?_zipWithAll {f : Option α → Option β → γ} {i : Nat} :
    (zipWithAll f as bs)[i]? = match as[i]?, bs[i]? with
      | none, none => .none | a?, b? => some (f a? b?)

Proof state:
case mk.mk
α : Type u_1
β : Type u_2
γ : Type u_3
f : Option α → Option β → γ
i : Nat
toList✝¹ : List α
toList✝ : List β
⊢ (match toList✝¹[i]?, toList✝[i]? with
    | none, none => none
    | a?, b? => some (f a? b?)) =
    match toList✝¹[i]?, toList✝[i]? with
    | none, none => none
    | a?, b? => some (f a? b?)

Tactic:
rfl

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
as : Array α
bs : Array β
f : Option α → Option β → γ
i : Nat
⊢ (zipWithAll f as bs)[i]? =
    match as[i]?, bs[i]? with
    | none, none => none
    | a?, b? => some (f a? b?)

Tactic:
cases as

Result:
case mk
α : Type u_1
β : Type u_2
γ : Type u_3
bs : Array β
f : Option α → Option β → γ
i : Nat
toList✝ : List α
⊢ (zipWithAll f { toList := toList✝ } bs)[i]? =
    match { toList := toList✝ }[i]?, bs[i]? with
    | none, none => none
    | a?, b? => some (f a? b?)

Proof state:
case mk
α : Type u_1
β : Type u_2
γ : Type u_3
bs : Array β
f : Option α → Option β → γ
i : Nat
toList✝ : List α
⊢ (zipWithAll f { toList := toList✝ } bs)[i]? =
    match { toList := toList✝ }[i]?, bs[i]? with
    | none, none => none
    | a?, b? => some (f a? b?)

Tactic:
cases bs

Result:
case mk.mk
α : Type u_1
β : Type u_2
γ : Type u_3
f : Option α → Option β → γ
i : Nat
toList✝¹ : List α
toList✝ : List β
⊢ (zipWithAll f { toList := toList✝¹ } { toList := toList✝ })[i]? =
    match { toList := toList✝¹ }[i]?, { toList := toList✝ }[i]? with
    | none, none => none
    | a?, b? => some (f a? b?)

Proof state:
case mk.mk
α : Type u_1
β : Type u_2
γ : Type u_3
f : Option α → Option β → γ
i : Nat
toList✝¹ : List α
toList✝ : List β
⊢ (zipWithAll f { toList := toList✝¹ } { toList := toList✝ })[i]? =
    match { toList := toList✝¹ }[i]?, { toList := toList✝ }[i]? with
    | none, none => none
    | a?, b? => some (f a? b?)

Tactic:
simp [List.getElem?_zipWithAll]

Result:
case mk.mk
α : Type u_1
β : Type u_2
γ : Type u_3
f : Option α → Option β → γ
i : Nat
toList✝¹ : List α
toList✝ : List β
⊢ (match toList✝¹[i]?, toList✝[i]? with
    | none, none => none
    | a?, b? => some (f a? b?)) =
    match toList✝¹[i]?, toList✝[i]? with
    | none, none => none
    | a?, b? => some (f a? b?)
-- Mathlib/Algebra/Order/Group/PosPart.lean
@[to_additive (attr := simp)] lemma leOnePart_lt : a⁻ᵐ < b ↔ b⁻¹ < a ∧ 1 < b :=
  sup_lt_iff.trans <| by rw [inv_lt']

Proof state:
α : Type u_1
inst✝³ : LinearOrder α
inst✝² : Group α
a b : α
inst✝¹ : MulLeftMono α
inst✝ : MulRightMono α
⊢ a⁻¹ < b ∧ 1 < b ↔ b⁻¹ < a ∧ 1 < b

Tactic:
rw [inv_lt']

Result:
no goals
-- Mathlib/Order/Defs/LinearOrder.lean
lemma compare_le_iff_le : compare a b ≠ .gt ↔ a ≤ b

Proof state:
case lt
α : Type u_1
inst✝ : LinearOrder α
a b : α
h : compare a b = Ordering.lt
⊢ a ≤ b

Tactic:
exact le_of_lt <| compare_lt_iff_lt.1 h

Result:
no goals

Proof state:
case gt
α : Type u_1
inst✝ : LinearOrder α
a b : α
h : compare a b = Ordering.gt
⊢ b < a

Tactic:
exact compare_gt_iff_gt.1 h

Result:
no goals

Proof state:
case eq
α : Type u_1
inst✝ : LinearOrder α
a b : α
h : compare a b = Ordering.eq
⊢ a ≤ b

Tactic:
exact le_of_eq <| compare_eq_iff_eq.1 h

Result:
no goals

Proof state:
α : Type u_1
inst✝ : LinearOrder α
a b : α
⊢ compare a b ≠ Ordering.gt ↔ a ≤ b

Tactic:
cases h : compare a b <;> simp

Result:
case lt
α : Type u_1
inst✝ : LinearOrder α
a b : α
h : compare a b = Ordering.lt
⊢ a ≤ b

case eq
α : Type u_1
inst✝ : LinearOrder α
a b : α
h : compare a b = Ordering.eq
⊢ a ≤ b

case gt
α : Type u_1
inst✝ : LinearOrder α
a b : α
h : compare a b = Ordering.gt
⊢ b < a
-- Mathlib/Order/SupIndep.lean
theorem SupIndep.biUnion [DecidableEq ι] {s : Finset ι'} {g : ι' → Finset ι} {f : ι → α}
    (hs : s.SupIndep fun i => (g i).sup f) (hg : ∀ i' ∈ s, (g i').SupIndep f) :
    (s.biUnion g).SupIndep f

Proof state:
α : Type u_1
ι : Type u_3
ι' : Type u_4
inst✝² : DistribLattice α
inst✝¹ : OrderBot α
inst✝ : DecidableEq ι
s : Finset ι'
g : ι' → Finset ι
f : ι → α
hs : s.SupIndep fun i => (g i).sup f
hg : ∀ i' ∈ s, (g i').SupIndep f
⊢ (s.biUnion g).SupIndep f

Tactic:
rw [← sup_eq_biUnion]

Result:
α : Type u_1
ι : Type u_3
ι' : Type u_4
inst✝² : DistribLattice α
inst✝¹ : OrderBot α
inst✝ : DecidableEq ι
s : Finset ι'
g : ι' → Finset ι
f : ι → α
hs : s.SupIndep fun i => (g i).sup f
hg : ∀ i' ∈ s, (g i').SupIndep f
⊢ (s.sup g).SupIndep f

Proof state:
α : Type u_1
ι : Type u_3
ι' : Type u_4
inst✝² : DistribLattice α
inst✝¹ : OrderBot α
inst✝ : DecidableEq ι
s : Finset ι'
g : ι' → Finset ι
f : ι → α
hs : s.SupIndep fun i => (g i).sup f
hg : ∀ i' ∈ s, (g i').SupIndep f
⊢ (s.sup g).SupIndep f

Tactic:
exact hs.sup hg

Result:
no goals