harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Topology/Category/Compactum.lean
theorem isClosed_iff {X : Compactum} (S : Set X) :
    IsClosed S ↔ ∀ F : Ultrafilter X, S ∈ F → X.str F ∈ S

Proof state:
case mp
X : Compactum
S : Set X.A
F : Ultrafilter X.A
h : S ∈ F
c : X.str F ∉ S
cond : Sᶜ ∈ F
⊢ False

Tactic:
rw [compl_mem_iff_not_mem] at cond

Result:
case mp
X : Compactum
S : Set X.A
F : Ultrafilter X.A
h : S ∈ F
c : X.str F ∉ S
cond : S ∉ F
⊢ False

Proof state:
case mp
X : Compactum
S : Set X.A
F : Ultrafilter X.A
h : S ∈ F
c : X.str F ∉ S
cond : S ∉ F
⊢ False

Tactic:
contradiction

Result:
no goals

Proof state:
X : Compactum
S : Set X.A
⊢ IsClosed S ↔ ∀ (F : Ultrafilter X.A), S ∈ F → X.str F ∈ S

Tactic:
rw [← isOpen_compl_iff]

Result:
X : Compactum
S : Set X.A
⊢ IsOpen Sᶜ ↔ ∀ (F : Ultrafilter X.A), S ∈ F → X.str F ∈ S

Proof state:
case mpr
X : Compactum
S : Set X.A
h1 : ∀ (F : Ultrafilter X.A), S ∈ F → X.str F ∈ S
F : Ultrafilter X.A
h2 : X.str F ∈ Sᶜ
⊢ Sᶜ ∈ F

Tactic:
specialize h1 F

Result:
case mpr
X : Compactum
S : Set X.A
F : Ultrafilter X.A
h2 : X.str F ∈ Sᶜ
h1 : S ∈ F → X.str F ∈ S
⊢ Sᶜ ∈ F

Proof state:
case mpr
X : Compactum
S : Set X.A
F : Ultrafilter X.A
h2 : X.str F ∈ Sᶜ
h1 : S ∈ F → X.str F ∈ S
⊢ Sᶜ ∈ F

Tactic:
rcases F.mem_or_compl_mem S with h | h

Result:
case mpr.inl
X : Compactum
S : Set X.A
F : Ultrafilter X.A
h2 : X.str F ∈ Sᶜ
h1 : S ∈ F → X.str F ∈ S
h : S ∈ F
⊢ Sᶜ ∈ F

case mpr.inr
X : Compactum
S : Set X.A
F : Ultrafilter X.A
h2 : X.str F ∈ Sᶜ
h1 : S ∈ F → X.str F ∈ S
h : Sᶜ ∈ F
⊢ Sᶜ ∈ F

Proof state:
X : Compactum
S : Set X.A
⊢ IsOpen Sᶜ ↔ ∀ (F : Ultrafilter X.A), S ∈ F → X.str F ∈ S

Tactic:
constructor

Result:
case mp
X : Compactum
S : Set X.A
⊢ IsOpen Sᶜ → ∀ (F : Ultrafilter X.A), S ∈ F → X.str F ∈ S

case mpr
X : Compactum
S : Set X.A
⊢ (∀ (F : Ultrafilter X.A), S ∈ F → X.str F ∈ S) → IsOpen Sᶜ

Proof state:
case mp
X : Compactum
S : Set X.A
⊢ IsOpen Sᶜ → ∀ (F : Ultrafilter X.A), S ∈ F → X.str F ∈ S

Tactic:
intro cond F h

Result:
case mp
X : Compactum
S : Set X.A
cond : IsOpen Sᶜ
F : Ultrafilter X.A
h : S ∈ F
⊢ X.str F ∈ S

Proof state:
case mpr
X : Compactum
S : Set X.A
⊢ (∀ (F : Ultrafilter X.A), S ∈ F → X.str F ∈ S) → IsOpen Sᶜ

Tactic:
intro h1 F h2

Result:
case mpr
X : Compactum
S : Set X.A
h1 : ∀ (F : Ultrafilter X.A), S ∈ F → X.str F ∈ S
F : Ultrafilter X.A
h2 : X.str F ∈ Sᶜ
⊢ Sᶜ ∈ F

Proof state:
case mpr.inl
X : Compactum
S : Set X.A
F : Ultrafilter X.A
h2 : X.str F ∈ Sᶜ
h1 : S ∈ F → X.str F ∈ S
h : S ∈ F
⊢ Sᶜ ∈ F

case mpr.inr
X : Compactum
S : Set X.A
F : Ultrafilter X.A
h2 : X.str F ∈ Sᶜ
h1 : S ∈ F → X.str F ∈ S
h : Sᶜ ∈ F
⊢ Sᶜ ∈ F

Tactic:
exacts [absurd (h1 h) h2, h]

Result:
no goals

Proof state:
case mp
X : Compactum
S : Set X.A
cond : IsOpen Sᶜ
F : Ultrafilter X.A
h : S ∈ F
⊢ X.str F ∈ S

Tactic:
by_contra c

Result:
case mp
X : Compactum
S : Set X.A
cond : IsOpen Sᶜ
F : Ultrafilter X.A
h : S ∈ F
c : X.str F ∉ S
⊢ False

Proof state:
case mp
X : Compactum
S : Set X.A
cond : IsOpen Sᶜ
F : Ultrafilter X.A
h : S ∈ F
c : X.str F ∉ S
⊢ False

Tactic:
specialize cond F c

Result:
case mp
X : Compactum
S : Set X.A
F : Ultrafilter X.A
h : S ∈ F
c : X.str F ∉ S
cond : Sᶜ ∈ F
⊢ False
-- Mathlib/Algebra/Order/Field/Basic.lean
theorem IsLUB.mul_left {s : Set α} (ha : 0 ≤ a) (hs : IsLUB s b) :
    IsLUB ((fun b => a * b) '' s) (a * b)

Proof state:
case inr
α : Type u_2
inst✝ : LinearOrderedField α
b : α
s : Set α
hs : IsLUB s b
ha : 0 ≤ 0
⊢ IsLUB {0} 0

Tactic:
exact isLUB_singleton

Result:
no goals

Proof state:
case inr
α : Type u_2
inst✝ : LinearOrderedField α
b : α
s : Set α
hs : IsLUB s b
ha : 0 ≤ 0
⊢ IsLUB ((fun a => 0) '' s) 0

Tactic:
rw [hs.nonempty.image_const]

Result:
case inr
α : Type u_2
inst✝ : LinearOrderedField α
b : α
s : Set α
hs : IsLUB s b
ha : 0 ≤ 0
⊢ IsLUB {0} 0

Proof state:
case inl
α : Type u_2
inst✝ : LinearOrderedField α
a b : α
s : Set α
ha✝ : 0 ≤ a
hs : IsLUB s b
ha : 0 < a
⊢ IsLUB ((fun b => a * b) '' s) (a * b)

Tactic:
exact (OrderIso.mulLeft₀ _ ha).isLUB_image'.2 hs

Result:
no goals

Proof state:
α : Type u_2
inst✝ : LinearOrderedField α
a b : α
s : Set α
ha : 0 ≤ a
hs : IsLUB s b
⊢ IsLUB ((fun b => a * b) '' s) (a * b)

Tactic:
rcases lt_or_eq_of_le ha with (ha | rfl)

Result:
case inl
α : Type u_2
inst✝ : LinearOrderedField α
a b : α
s : Set α
ha✝ : 0 ≤ a
hs : IsLUB s b
ha : 0 < a
⊢ IsLUB ((fun b => a * b) '' s) (a * b)

case inr
α : Type u_2
inst✝ : LinearOrderedField α
b : α
s : Set α
hs : IsLUB s b
ha : 0 ≤ 0
⊢ IsLUB ((fun b => 0 * b) '' s) (0 * b)

Proof state:
case inr
α : Type u_2
inst✝ : LinearOrderedField α
b : α
s : Set α
hs : IsLUB s b
ha : 0 ≤ 0
⊢ IsLUB ((fun b => 0 * b) '' s) (0 * b)

Tactic:
simp_rw [zero_mul]

Result:
case inr
α : Type u_2
inst✝ : LinearOrderedField α
b : α
s : Set α
hs : IsLUB s b
ha : 0 ≤ 0
⊢ IsLUB ((fun a => 0) '' s) 0
-- Mathlib/CategoryTheory/Localization/Resolution.lean
lemma essSurj_of_hasLeftResolutions [Φ.HasLeftResolutions] : (Φ.functor ⋙ L₂).EssSurj where
  mem_essImage X₂

Proof state:
C₁ : Type u_1
C₂ : Type u_2
D₂ : Type u_3
inst✝⁴ : Category.{u_5, u_1} C₁
inst✝³ : Category.{u_6, u_2} C₂
inst✝² : Category.{u_7, u_3} D₂
W₁ : MorphismProperty C₁
W₂ : MorphismProperty C₂
Φ : LocalizerMorphism W₁ W₂
L₂ : C₂ ⥤ D₂
inst✝¹ : L₂.IsLocalization W₂
inst✝ : Φ.HasLeftResolutions
X₂ : D₂
⊢ (Φ.functor ⋙ L₂).essImage X₂

Tactic:
have := Localization.essSurj L₂ W₂

Result:
C₁ : Type u_1
C₂ : Type u_2
D₂ : Type u_3
inst✝⁴ : Category.{u_5, u_1} C₁
inst✝³ : Category.{u_6, u_2} C₂
inst✝² : Category.{u_7, u_3} D₂
W₁ : MorphismProperty C₁
W₂ : MorphismProperty C₂
Φ : LocalizerMorphism W₁ W₂
L₂ : C₂ ⥤ D₂
inst✝¹ : L₂.IsLocalization W₂
inst✝ : Φ.HasLeftResolutions
X₂ : D₂
this : L₂.EssSurj
⊢ (Φ.functor ⋙ L₂).essImage X₂

Proof state:
C₁ : Type u_1
C₂ : Type u_2
D₂ : Type u_3
inst✝⁴ : Category.{u_5, u_1} C₁
inst✝³ : Category.{u_6, u_2} C₂
inst✝² : Category.{u_7, u_3} D₂
W₁ : MorphismProperty C₁
W₂ : MorphismProperty C₂
Φ : LocalizerMorphism W₁ W₂
L₂ : C₂ ⥤ D₂
inst✝¹ : L₂.IsLocalization W₂
inst✝ : Φ.HasLeftResolutions
X₂ : D₂
this : L₂.EssSurj
⊢ (Φ.functor ⋙ L₂).essImage X₂

Tactic:
have L : Φ.LeftResolution (L₂.objPreimage X₂) := Classical.arbitrary _

Result:
C₁ : Type u_1
C₂ : Type u_2
D₂ : Type u_3
inst✝⁴ : Category.{u_5, u_1} C₁
inst✝³ : Category.{u_6, u_2} C₂
inst✝² : Category.{u_7, u_3} D₂
W₁ : MorphismProperty C₁
W₂ : MorphismProperty C₂
Φ : LocalizerMorphism W₁ W₂
L₂ : C₂ ⥤ D₂
inst✝¹ : L₂.IsLocalization W₂
inst✝ : Φ.HasLeftResolutions
X₂ : D₂
this : L₂.EssSurj
L : Φ.LeftResolution (L₂.objPreimage X₂)
⊢ (Φ.functor ⋙ L₂).essImage X₂

Proof state:
C₁ : Type u_1
C₂ : Type u_2
D₂ : Type u_3
inst✝⁴ : Category.{u_5, u_1} C₁
inst✝³ : Category.{u_6, u_2} C₂
inst✝² : Category.{u_7, u_3} D₂
W₁ : MorphismProperty C₁
W₂ : MorphismProperty C₂
Φ : LocalizerMorphism W₁ W₂
L₂ : C₂ ⥤ D₂
inst✝¹ : L₂.IsLocalization W₂
inst✝ : Φ.HasLeftResolutions
X₂ : D₂
this : L₂.EssSurj
L : Φ.LeftResolution (L₂.objPreimage X₂)
⊢ (Φ.functor ⋙ L₂).essImage X₂

Tactic:
exact ⟨L.X₁, ⟨Localization.isoOfHom L₂ W₂ _ L.hw ≪≫ L₂.objObjPreimageIso X₂⟩⟩

Result:
no goals
-- Mathlib/Data/List/Count.lean
lemma countP_diff (hl : l₂ <+~ l₁) (p : α → Bool) :
    countP p (l₁.diff l₂) = countP p l₁ - countP p l₂

Proof state:
α : Type u_1
inst✝ : DecidableEq α
l₁ l₂ : List α
hl : l₂ <+~ l₁
p : α → Bool
⊢ countP p (l₁.diff l₂) = countP p l₁ - countP p l₂

Tactic:
refine (Nat.sub_eq_of_eq_add ?_).symm

Result:
α : Type u_1
inst✝ : DecidableEq α
l₁ l₂ : List α
hl : l₂ <+~ l₁
p : α → Bool
⊢ countP p l₁ = countP p (l₁.diff l₂) + countP p l₂

Proof state:
α : Type u_1
inst✝ : DecidableEq α
l₁ l₂ : List α
hl : l₂ <+~ l₁
p : α → Bool
⊢ countP p l₁ = countP p (l₁.diff l₂ ++ l₂)

Tactic:
exact ((subperm_append_diff_self_of_count_le <| subperm_ext_iff.1 hl).symm.trans
  perm_append_comm).countP_eq _

Result:
no goals

Proof state:
α : Type u_1
inst✝ : DecidableEq α
l₁ l₂ : List α
hl : l₂ <+~ l₁
p : α → Bool
⊢ countP p l₁ = countP p (l₁.diff l₂) + countP p l₂

Tactic:
rw [← countP_append]

Result:
α : Type u_1
inst✝ : DecidableEq α
l₁ l₂ : List α
hl : l₂ <+~ l₁
p : α → Bool
⊢ countP p l₁ = countP p (l₁.diff l₂ ++ l₂)
-- Mathlib/Topology/MetricSpace/PiNat.lean
theorem apply_firstDiff_ne {x y : ∀ n, E n} (h : x ≠ y) :
    x (firstDiff x y) ≠ y (firstDiff x y)

Proof state:
E : ℕ → Type u_1
x y : (n : ℕ) → E n
h : x ≠ y
⊢ x (Nat.find ⋯) ≠ y (Nat.find ⋯)

Tactic:
classical
exact Nat.find_spec (ne_iff.1 h)

Result:
no goals

Proof state:
E : ℕ → Type u_1
x y : (n : ℕ) → E n
h : x ≠ y
⊢ x (firstDiff x y) ≠ y (firstDiff x y)

Tactic:
rw [firstDiff_def, dif_pos h]

Result:
E : ℕ → Type u_1
x y : (n : ℕ) → E n
h : x ≠ y
⊢ x (Nat.find ⋯) ≠ y (Nat.find ⋯)

Proof state:
E : ℕ → Type u_1
x y : (n : ℕ) → E n
h : x ≠ y
⊢ x (Nat.find ⋯) ≠ y (Nat.find ⋯)

Tactic:
exact Nat.find_spec (ne_iff.1 h)

Result:
no goals
-- Mathlib/CategoryTheory/CofilteredSystem.lean
theorem eventualRange_eq_range_precomp (f : i ⟶ j) (g : j ⟶ k)
    (h : F.eventualRange k = range (F.map g)) : F.eventualRange k = range (F.map <| f ≫ g)

Proof state:
J : Type u
inst✝ : Category.{u_1, u} J
F : J ⥤ Type v
i j k : J
f : i ⟶ j
g : j ⟶ k
h : F.eventualRange k = range (F.map g)
⊢ F.eventualRange k = range (F.map (f ≫ g))

Tactic:
apply subset_antisymm

Result:
case a
J : Type u
inst✝ : Category.{u_1, u} J
F : J ⥤ Type v
i j k : J
f : i ⟶ j
g : j ⟶ k
h : F.eventualRange k = range (F.map g)
⊢ F.eventualRange k ⊆ range (F.map (f ≫ g))

case a
J : Type u
inst✝ : Category.{u_1, u} J
F : J ⥤ Type v
i j k : J
f : i ⟶ j
g : j ⟶ k
h : F.eventualRange k = range (F.map g)
⊢ range (F.map (f ≫ g)) ⊆ F.eventualRange k

Proof state:
case a
J : Type u
inst✝ : Category.{u_1, u} J
F : J ⥤ Type v
i j k : J
f : i ⟶ j
g : j ⟶ k
h : F.eventualRange k = range (F.map g)
⊢ range (F.map (f ≫ g)) ⊆ F.eventualRange k

Tactic:
rw [h, F.map_comp]

Result:
case a
J : Type u
inst✝ : Category.{u_1, u} J
F : J ⥤ Type v
i j k : J
f : i ⟶ j
g : j ⟶ k
h : F.eventualRange k = range (F.map g)
⊢ range (F.map f ≫ F.map g) ⊆ range (F.map g)

Proof state:
case a
J : Type u
inst✝ : Category.{u_1, u} J
F : J ⥤ Type v
i j k : J
f : i ⟶ j
g : j ⟶ k
h : F.eventualRange k = range (F.map g)
⊢ range (F.map f ≫ F.map g) ⊆ range (F.map g)

Tactic:
apply range_comp_subset_range

Result:
no goals

Proof state:
case a
J : Type u
inst✝ : Category.{u_1, u} J
F : J ⥤ Type v
i j k : J
f : i ⟶ j
g : j ⟶ k
h : F.eventualRange k = range (F.map g)
⊢ F.eventualRange k ⊆ range (F.map (f ≫ g))

Tactic:
apply iInter₂_subset

Result:
no goals
-- Mathlib/Data/Sum/Interval.lean
theorem Ioo_inl_inr : Ioo (inl a₁) (inr b₂) = ∅

Proof state:
α : Type u_1
β : Type u_2
inst✝³ : Preorder α
inst✝² : Preorder β
inst✝¹ : LocallyFiniteOrder α
inst✝ : LocallyFiniteOrder β
a₁ : α
b₂ : β
⊢ Ioo (inl a₁) (inr b₂) = ∅

Tactic:
rfl

Result:
no goals
-- Mathlib/Algebra/Group/Fin/Basic.lean
lemma sub_one_lt_iff {k : Fin (n + 1)} : k - 1 < k ↔ 0 < k :=
  not_iff_not.1 <| by simp only [lt_def, not_lt, val_fin_le, le_sub_one_iff, le_zero_iff]

Proof state:
n : ℕ
k : Fin (n + 1)
⊢ ¬k - 1 < k ↔ ¬0 < k

Tactic:
simp only [lt_def, not_lt, val_fin_le, le_sub_one_iff, le_zero_iff]

Result:
no goals
-- Mathlib/LinearAlgebra/Matrix/Charpoly/Coeff.lean
theorem charpoly_monic (M : Matrix n n R) : M.charpoly.Monic

Proof state:
case neg
R : Type u
inst✝² : CommRing R
n : Type v
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : Matrix n n R
a✝ : Nontrivial R
h : ¬Fintype.card n = 0
mon : (∏ i : n, (X - C (M i i)) - M.charpoly + M.charpoly).leadingCoeff = 1
⊢ (∏ i : n, (X - C (M i i)) - M.charpoly).degree < ↑(Fintype.card n)

Tactic:
rw [← neg_sub]

Result:
case neg
R : Type u
inst✝² : CommRing R
n : Type v
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : Matrix n n R
a✝ : Nontrivial R
h : ¬Fintype.card n = 0
mon : (∏ i : n, (X - C (M i i)) - M.charpoly + M.charpoly).leadingCoeff = 1
⊢ (-(M.charpoly - ∏ i : n, (X - C (M i i)))).degree < ↑(Fintype.card n)

Proof state:
case neg
R : Type u
inst✝² : CommRing R
n : Type v
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : Matrix n n R
a✝ : Nontrivial R
h : ¬Fintype.card n = 0
mon : (∏ i : n, (X - C (M i i))).Monic
⊢ M.charpoly.Monic

Tactic:
rw [← sub_add_cancel (∏ i : n, (X - C (M i i))) M.charpoly] at mon

Result:
case neg
R : Type u
inst✝² : CommRing R
n : Type v
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : Matrix n n R
a✝ : Nontrivial R
h : ¬Fintype.card n = 0
mon : (∏ i : n, (X - C (M i i)) - M.charpoly + M.charpoly).Monic
⊢ M.charpoly.Monic
-- Mathlib/Data/Finset/Card.lean
theorem exists_eq_insert_iff [DecidableEq α] {s t : Finset α} :
    (∃ a ∉ s, insert a s = t) ↔ s ⊆ t ∧ #s + 1 = #t

Proof state:
case mpr
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
⊢ s ⊆ t ∧ #s + 1 = #t → ∃ a ∉ s, insert a s = t

Tactic:
rintro ⟨hst, h⟩

Result:
case mpr.intro
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
hst : s ⊆ t
h : #s + 1 = #t
⊢ ∃ a ∉ s, insert a s = t

Proof state:
case mpr.intro.intro
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
hst : s ⊆ t
h : #s + 1 = #t
a : α
ha : t \ s = {a}
hs : a ∈ s
⊢ a ∉ {a}

Tactic:
rw [← ha]

Result:
case mpr.intro.intro
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
hst : s ⊆ t
h : #s + 1 = #t
a : α
ha : t \ s = {a}
hs : a ∈ s
⊢ a ∉ t \ s

Proof state:
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
⊢ (∃ a ∉ s, insert a s = t) ↔ s ⊆ t ∧ #s + 1 = #t

Tactic:
constructor

Result:
case mp
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
⊢ (∃ a ∉ s, insert a s = t) → s ⊆ t ∧ #s + 1 = #t

case mpr
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
⊢ s ⊆ t ∧ #s + 1 = #t → ∃ a ∉ s, insert a s = t

Proof state:
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
hst : s ⊆ t
h : #s + 1 = #t
a : α
ha : t \ s = {a}
⊢ insert a s = t

Tactic:
rw [insert_eq, ← ha, sdiff_union_of_subset hst]

Result:
no goals

Proof state:
case mp.intro.intro
α : Type u_1
inst✝ : DecidableEq α
s : Finset α
a : α
ha : a ∉ s
⊢ s ⊆ insert a s ∧ #s + 1 = #(insert a s)

Tactic:
exact ⟨subset_insert _ _, (card_insert_of_not_mem ha).symm⟩

Result:
no goals

Proof state:
case mpr.intro.intro
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
hst : s ⊆ t
h : #s + 1 = #t
a : α
ha : t \ s = {a}
hs : a ∈ s
⊢ a ∉ t \ s

Tactic:
exact not_mem_sdiff_of_mem_right hs

Result:
no goals

Proof state:
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
hst : s ⊆ t
h : #s + 1 = #t
⊢ #(t \ s) = 1

Tactic:
rw [card_sdiff hst, ← h, Nat.add_sub_cancel_left]

Result:
no goals

Proof state:
case mp
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
⊢ (∃ a ∉ s, insert a s = t) → s ⊆ t ∧ #s + 1 = #t

Tactic:
rintro ⟨a, ha, rfl⟩

Result:
case mp.intro.intro
α : Type u_1
inst✝ : DecidableEq α
s : Finset α
a : α
ha : a ∉ s
⊢ s ⊆ insert a s ∧ #s + 1 = #(insert a s)

Proof state:
case mpr.intro
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
hst : s ⊆ t
h : #s + 1 = #t
⊢ ∃ a ∉ s, insert a s = t

Tactic:
obtain ⟨a, ha⟩ : ∃ a, t \ s = {a} :=
  card_eq_one.1 (by rw [card_sdiff hst, ← h, Nat.add_sub_cancel_left])

Result:
case mpr.intro.intro
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
hst : s ⊆ t
h : #s + 1 = #t
a : α
ha : t \ s = {a}
⊢ ∃ a ∉ s, insert a s = t

Proof state:
case mpr.intro.intro
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
hst : s ⊆ t
h : #s + 1 = #t
a : α
ha : t \ s = {a}
⊢ ∃ a ∉ s, insert a s = t

Tactic:
refine
  ⟨a, fun hs => (?_ : a ∉ {a}) <| mem_singleton_self _, by
    rw [insert_eq, ← ha, sdiff_union_of_subset hst]⟩

Result:
case mpr.intro.intro
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
hst : s ⊆ t
h : #s + 1 = #t
a : α
ha : t \ s = {a}
hs : a ∈ s
⊢ a ∉ {a}
-- Mathlib/Order/Chain.lean
lemma IsMaxChain.image {s : β → β → Prop} (e : r ≃r s) {c : Set α} (hc : IsMaxChain r c) :
    IsMaxChain s (e '' c) where
  left := hc.isChain.image _ _ _ fun _ _ ↦ by exact e.map_rel_iff.2
  right t ht hf

Proof state:
α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
e : r ≃r s
c : Set α
hc : IsMaxChain r c
t : Set β
ht : IsChain s t
hf : ⇑e '' c ⊆ t
⊢ ⇑e '' c = t

Tactic:
rw [← e.coe_fn_toEquiv, ← e.toEquiv.eq_preimage_iff_image_eq, preimage_equiv_eq_image_symm]

Result:
α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
e : r ≃r s
c : Set α
hc : IsMaxChain r c
t : Set β
ht : IsChain s t
hf : ⇑e '' c ⊆ t
⊢ c = ⇑e.symm '' t

Proof state:
α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
e : r ≃r s
c : Set α
hc : IsMaxChain r c
x✝¹ x✝ : α
⊢ r x✝¹ x✝ → s (e x✝¹) (e x✝)

Tactic:
exact e.map_rel_iff.2

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
e : r ≃r s
c : Set α
hc : IsMaxChain r c
t : Set β
ht : IsChain s t
hf : ⇑e '' c ⊆ t
⊢ c = ⇑e.symm '' t

Tactic:
exact hc.2 (ht.image _ _ _ fun _ _ ↦ by exact e.symm.map_rel_iff.2)
  ((e.toEquiv.subset_symm_image _ _).2 hf)

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
e : r ≃r s
c : Set α
hc : IsMaxChain r c
t : Set β
ht : IsChain s t
hf : ⇑e '' c ⊆ t
x✝¹ x✝ : β
⊢ s x✝¹ x✝ → r (e.symm x✝¹) (e.symm x✝)

Tactic:
exact e.symm.map_rel_iff.2

Result:
no goals
-- Mathlib/RingTheory/Coprime/Basic.lean
theorem IsCoprime.of_mul_add_right_left (h : IsCoprime (z * y + x) y) : IsCoprime x y

Proof state:
R : Type u
inst✝ : CommSemiring R
x y z : R
h : IsCoprime (z * y + x) y
⊢ IsCoprime x y

Tactic:
rw [add_comm] at h

Result:
R : Type u
inst✝ : CommSemiring R
x y z : R
h : IsCoprime (x + z * y) y
⊢ IsCoprime x y

Proof state:
R : Type u
inst✝ : CommSemiring R
x y z : R
h : IsCoprime (x + z * y) y
⊢ IsCoprime x y

Tactic:
exact h.of_add_mul_right_left

Result:
no goals
-- Mathlib/Algebra/Lie/Submodule.lean
theorem lie_mem_left (I : LieIdeal R L) (x y : L) (h : x ∈ I) : ⁅x, y⁆ ∈ I

Proof state:
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
I : LieIdeal R L
x y : L
h : x ∈ I
⊢ ⁅-y, x⁆ ∈ I

Tactic:
apply lie_mem_right

Result:
case h
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
I : LieIdeal R L
x y : L
h : x ∈ I
⊢ x ∈ I

Proof state:
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
I : LieIdeal R L
x y : L
h : x ∈ I
⊢ ⁅x, y⁆ ∈ I

Tactic:
rw [← lie_skew, ← neg_lie]

Result:
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
I : LieIdeal R L
x y : L
h : x ∈ I
⊢ ⁅-y, x⁆ ∈ I

Proof state:
case h
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
I : LieIdeal R L
x y : L
h : x ∈ I
⊢ x ∈ I

Tactic:
assumption

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Lemmas.lean
theorem getElem?_set (v : Vector α n) (i : Nat) (hi : i < n) (x : α) (j : Nat) :
    (v.set i x hi)[j]? = if i = j then some x else v[j]?

Proof state:
case mk
α : Type u_1
n i : Nat
hi : i < n
x : α
j : Nat
toArray✝ : Array α
size_toArray✝ : toArray✝.size = n
⊢ ({ toArray := toArray✝, size_toArray := size_toArray✝ }.set i x hi)[j]? =
    if i = j then some x else { toArray := toArray✝, size_toArray := size_toArray✝ }[j]?

Tactic:
split <;> simp_all [getElem?_eq_getElem, getElem_set]

Result:
no goals

Proof state:
α : Type u_1
n : Nat
v : Vector α n
i : Nat
hi : i < n
x : α
j : Nat
⊢ (v.set i x hi)[j]? = if i = j then some x else v[j]?

Tactic:
cases v

Result:
case mk
α : Type u_1
n i : Nat
hi : i < n
x : α
j : Nat
toArray✝ : Array α
size_toArray✝ : toArray✝.size = n
⊢ ({ toArray := toArray✝, size_toArray := size_toArray✝ }.set i x hi)[j]? =
    if i = j then some x else { toArray := toArray✝, size_toArray := size_toArray✝ }[j]?
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Lemmas.lean
theorem getLast_eq_get (l : List α) (h : l ≠ []) :
    getLast l h = l.get ⟨l.length - 1, by
      match l with
      | [] => contradiction
      | a :: l => exact Nat.le_refl _⟩

Proof state:
α : Type ?u.95475
l✝ : List α
a : α
l : List α
h : a :: l ≠ []
⊢ (a :: l).length - 1 < (a :: l).length

Tactic:
exact Nat.le_refl _

Result:
no goals

Proof state:
α : Type ?u.95475
l : List α
h : l ≠ []
⊢ l.length - 1 < l.length

Tactic:
match l with
| [] => contradiction
| a :: l => exact Nat.le_refl _

Result:
no goals

Proof state:
α : Type u_1
l : List α
h : l ≠ []
⊢ l.getLast h = l.get ⟨l.length - 1, ⋯⟩

Tactic:
simp [getLast_eq_getElem]

Result:
no goals

Proof state:
α : Type ?u.95475
l : List α
h : [] ≠ []
⊢ [].length - 1 < [].length

Tactic:
contradiction

Result:
no goals
-- Mathlib/Algebra/Polynomial/Div.lean
theorem pow_rootMultiplicity_dvd (p : R[X]) (a : R) : (X - C a) ^ rootMultiplicity a p ∣ p :=
  letI := Classical.decEq R
  if h : p = 0 then by simp [h]
  else by
    classical
    rw [rootMultiplicity_eq_multiplicity, if_neg h]; apply pow_multiplicity_dvd

Proof state:
R : Type u
inst✝ : Ring R
p : R[X]
a : R
this : DecidableEq R := Classical.decEq R
h : ¬p = 0
⊢ (X - C a) ^ multiplicity (X - C a) p ∣ p

Tactic:
apply pow_multiplicity_dvd

Result:
no goals

Proof state:
R : Type u
inst✝ : Ring R
p : R[X]
a : R
this : DecidableEq R := Classical.decEq R
h : ¬p = 0
⊢ (X - C a) ^ rootMultiplicity a p ∣ p

Tactic:
classical
rw [rootMultiplicity_eq_multiplicity, if_neg h]; apply pow_multiplicity_dvd

Result:
no goals

Proof state:
R : Type u
inst✝ : Ring R
p : R[X]
a : R
this : DecidableEq R := Classical.decEq R
h : ¬p = 0
⊢ (X - C a) ^ rootMultiplicity a p ∣ p

Tactic:
rw [rootMultiplicity_eq_multiplicity, if_neg h]

Result:
R : Type u
inst✝ : Ring R
p : R[X]
a : R
this : DecidableEq R := Classical.decEq R
h : ¬p = 0
⊢ (X - C a) ^ multiplicity (X - C a) p ∣ p

Proof state:
R : Type u
inst✝ : Ring R
p : R[X]
a : R
this : DecidableEq R := Classical.decEq R
h : p = 0
⊢ (X - C a) ^ rootMultiplicity a p ∣ p

Tactic:
simp [h]

Result:
no goals
-- Mathlib/NumberTheory/Bernoulli.lean
theorem bernoulli'PowerSeries_mul_exp_sub_one :
    bernoulli'PowerSeries A * (exp A - 1) = X * exp A

Proof state:
case h.zero
A : Type u_1
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
⊢ (coeff A 0) (bernoulli'PowerSeries A * (exp A - 1)) = (coeff A 0) (X * exp A)

Tactic:
simp

Result:
no goals
-- Mathlib/Topology/Path.lean
theorem symm_range {a b : X} (γ : Path a b) : range γ.symm = range γ

Proof state:
X : Type u_1
inst✝ : TopologicalSpace X
a b : X
γ : Path a b
⊢ range ⇑γ.symm = range ⇑γ

Tactic:
ext x

Result:
case h
X : Type u_1
inst✝ : TopologicalSpace X
a b : X
γ : Path a b
x : X
⊢ x ∈ range ⇑γ.symm ↔ x ∈ range ⇑γ

Proof state:
case h.e'_2.h.e'_6.h.e'_3
X : Type u_1
inst✝ : TopologicalSpace X
a b : X
γ : Path a b
x : X
y : ℝ
hy : y ∈ I
hxy : γ.toFun ⟨y, hy⟩ = x
⊢ 1 - (1 - y) = y

Tactic:
simp

Result:
no goals

Proof state:
case h
X : Type u_1
inst✝ : TopologicalSpace X
a b : X
γ : Path a b
x : X
⊢ x ∈ range ⇑γ.symm ↔ x ∈ range ⇑γ

Tactic:
simp only [mem_range, Path.symm, DFunLike.coe, unitInterval.symm, SetCoe.exists, comp_apply,
  Subtype.coe_mk]

Result:
case h
X : Type u_1
inst✝ : TopologicalSpace X
a b : X
γ : Path a b
x : X
⊢ (∃ x_1, ∃ (h : x_1 ∈ I), γ.toFun ⟨1 - x_1, ⋯⟩ = x) ↔ ∃ x_1, ∃ (h : x_1 ∈ I), γ.toFun ⟨x_1, h⟩ = x

Proof state:
case h
X : Type u_1
inst✝ : TopologicalSpace X
a b : X
γ : Path a b
x : X
⊢ (∃ x_1, ∃ (h : x_1 ∈ I), γ.toFun ⟨1 - x_1, ⋯⟩ = x) ↔ ∃ x_1, ∃ (h : x_1 ∈ I), γ.toFun ⟨x_1, h⟩ = x

Tactic:
constructor <;> rintro ⟨y, hy, hxy⟩ <;> refine ⟨1 - y, mem_iff_one_sub_mem.mp hy, ?_⟩ <;>
  convert hxy

Result:
case h.e'_2.h.e'_6.h.e'_3
X : Type u_1
inst✝ : TopologicalSpace X
a b : X
γ : Path a b
x : X
y : ℝ
hy : y ∈ I
hxy : γ.toFun ⟨y, hy⟩ = x
⊢ 1 - (1 - y) = y
-- Mathlib/Algebra/MvPolynomial/Division.lean
theorem X_dvd_monomial {i : σ} {j : σ →₀ ℕ} {r : R} :
    (X i : MvPolynomial σ R) ∣ monomial j r ↔ r = 0 ∨ j i ≠ 0

Proof state:
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
i : σ
j : σ →₀ ℕ
r : R
⊢ (r = 0 ∨ Finsupp.single i 1 ≤ j) ∧ 1 ∣ r ↔ r = 0 ∨ j i ≠ 0

Tactic:
simp_rw [one_dvd, and_true, Finsupp.single_le_iff, Nat.one_le_iff_ne_zero]

Result:
no goals

Proof state:
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
i : σ
j : σ →₀ ℕ
r : R
⊢ X i ∣ (monomial j) r ↔ r = 0 ∨ j i ≠ 0

Tactic:
refine monomial_dvd_monomial.trans ?_

Result:
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
i : σ
j : σ →₀ ℕ
r : R
⊢ (r = 0 ∨ Finsupp.single i 1 ≤ j) ∧ 1 ∣ r ↔ r = 0 ∨ j i ≠ 0