harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Data/List/SplitLengths.lean
theorem map_splitLengths_length (h : sz.sum ≤ l.length) :
    (sz.splitLengths l).map length = sz

Proof state:
case nil
α : Type u_1
l : List α
h : [].sum ≤ l.length
⊢ map length ([].splitLengths l) = []

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
head : ℕ
tail : List ℕ
ih : ∀ (l : List α), tail.sum ≤ l.length → map length (tail.splitLengths l) = tail
l : List α
h : head + tail.sum ≤ l.length
⊢ head ≤ l.length ∧ map length (tail.splitLengths (drop head l)) = tail

Tactic:
rw [ih]

Result:
α : Type u_1
head : ℕ
tail : List ℕ
ih : ∀ (l : List α), tail.sum ≤ l.length → map length (tail.splitLengths l) = tail
l : List α
h : head + tail.sum ≤ l.length
⊢ head ≤ l.length ∧ tail = tail

case h
α : Type u_1
head : ℕ
tail : List ℕ
ih : ∀ (l : List α), tail.sum ≤ l.length → map length (tail.splitLengths l) = tail
l : List α
h : head + tail.sum ≤ l.length
⊢ tail.sum ≤ (drop head l).length

Proof state:
α : Type u_1
l : List α
sz : List ℕ
h : sz.sum ≤ l.length
⊢ map length (sz.splitLengths l) = sz

Tactic:
induction sz generalizing l

Result:
case nil
α : Type u_1
l : List α
h : [].sum ≤ l.length
⊢ map length ([].splitLengths l) = []

case cons
α : Type u_1
head✝ : ℕ
tail✝ : List ℕ
tail_ih✝ : ∀ (l : List α), tail✝.sum ≤ l.length → map length (tail✝.splitLengths l) = tail✝
l : List α
h : (head✝ :: tail✝).sum ≤ l.length
⊢ map length ((head✝ :: tail✝).splitLengths l) = head✝ :: tail✝

Proof state:
α : Type u_1
head : ℕ
tail : List ℕ
ih : ∀ (l : List α), tail.sum ≤ l.length → map length (tail.splitLengths l) = tail
l : List α
h : head + tail.sum ≤ l.length
⊢ map length ((head :: tail).splitLengths l) = head :: tail

Tactic:
simp only [splitLengths_cons, map_cons, length_take, cons.injEq, min_eq_left_iff]

Result:
α : Type u_1
head : ℕ
tail : List ℕ
ih : ∀ (l : List α), tail.sum ≤ l.length → map length (tail.splitLengths l) = tail
l : List α
h : head + tail.sum ≤ l.length
⊢ head ≤ l.length ∧ map length (tail.splitLengths (drop head l)) = tail

Proof state:
α : Type u_1
head : ℕ
tail : List ℕ
ih : ∀ (l : List α), tail.sum ≤ l.length → map length (tail.splitLengths l) = tail
l : List α
h : head + tail.sum ≤ l.length
⊢ head ≤ l.length ∧ tail = tail

Tactic:
simp [Nat.le_of_add_right_le h]

Result:
no goals

Proof state:
case h
α : Type u_1
head : ℕ
tail : List ℕ
ih : ∀ (l : List α), tail.sum ≤ l.length → map length (tail.splitLengths l) = tail
l : List α
h : head + tail.sum ≤ l.length
⊢ tail.sum ≤ (drop head l).length

Tactic:
simp [Nat.le_sub_of_add_le' h]

Result:
no goals

Proof state:
α : Type u_1
head : ℕ
tail : List ℕ
ih : ∀ (l : List α), tail.sum ≤ l.length → map length (tail.splitLengths l) = tail
l : List α
h : (head :: tail).sum ≤ l.length
⊢ map length ((head :: tail).splitLengths l) = head :: tail

Tactic:
simp only [sum_cons] at h

Result:
α : Type u_1
head : ℕ
tail : List ℕ
ih : ∀ (l : List α), tail.sum ≤ l.length → map length (tail.splitLengths l) = tail
l : List α
h : head + tail.sum ≤ l.length
⊢ map length ((head :: tail).splitLengths l) = head :: tail
-- Mathlib/GroupTheory/EckmannHilton.lean
theorem mul : m₁ = m₂

Proof state:
X : Type u
m₁ m₂ : X → X → X
e₁ e₂ : X
h₁ : IsUnital m₁ e₁
h₂ : IsUnital m₂ e₂
distrib : ∀ (a b c d : X), m₁ (m₂ a b) (m₂ c d) = m₂ (m₁ a c) (m₁ b d)
⊢ m₁ = m₂

Tactic:
funext a b

Result:
case h.h
X : Type u
m₁ m₂ : X → X → X
e₁ e₂ : X
h₁ : IsUnital m₁ e₁
h₂ : IsUnital m₂ e₂
distrib : ∀ (a b c d : X), m₁ (m₂ a b) (m₂ c d) = m₂ (m₁ a c) (m₁ b d)
a b : X
⊢ m₁ a b = m₂ a b

Proof state:
X : Type u
m₁ m₂ : X → X → X
e₁ e₂ : X
h₁ : IsUnital m₁ e₁
h₂ : IsUnital m₂ e₂
distrib : ∀ (a b c d : X), m₁ (m₂ a b) (m₂ c d) = m₂ (m₁ a c) (m₁ b d)
a b : X
⊢ m₁ a b = m₁ (m₂ a e₁) (m₂ e₁ b)

Tactic:
simp only [one h₁ h₂ distrib, h₁.left_id, h₁.right_id, h₂.left_id, h₂.right_id]

Result:
no goals

Proof state:
X : Type u
m₁ m₂ : X → X → X
e₁ e₂ : X
h₁ : IsUnital m₁ e₁
h₂ : IsUnital m₂ e₂
distrib : ∀ (a b c d : X), m₁ (m₂ a b) (m₂ c d) = m₂ (m₁ a c) (m₁ b d)
a b : X
⊢ m₁ (m₂ a e₁) (m₂ e₁ b) = m₂ a b

Tactic:
simp only [distrib, h₁.left_id, h₁.right_id, h₂.left_id, h₂.right_id]

Result:
no goals

Proof state:
case h.h
X : Type u
m₁ m₂ : X → X → X
e₁ e₂ : X
h₁ : IsUnital m₁ e₁
h₂ : IsUnital m₂ e₂
distrib : ∀ (a b c d : X), m₁ (m₂ a b) (m₂ c d) = m₂ (m₁ a c) (m₁ b d)
a b : X
⊢ m₁ a b = m₂ a b

Tactic:
calc
  m₁ a b = m₁ (m₂ a e₁) (m₂ e₁ b) := by
    { simp only [one h₁ h₂ distrib, h₁.left_id, h₁.right_id, h₂.left_id, h₂.right_id] }
  _ = m₂ a b := by simp only [distrib, h₁.left_id, h₁.right_id, h₂.left_id, h₂.right_id]

Result:
no goals
-- Mathlib/NumberTheory/Pell.lean
theorem d_pos_of_one_lt_x {a : Solution₁ d} (ha : 1 < a.x) : 0 < d

Proof state:
d : ℤ
a : Solution₁ d
ha : 1 < a.x
⊢ 0 < d * a.y ^ 2

Tactic:
rw [a.prop_y, sub_pos]

Result:
d : ℤ
a : Solution₁ d
ha : 1 < a.x
⊢ 1 < a.x ^ 2

Proof state:
d : ℤ
a : Solution₁ d
ha : 1 < a.x
⊢ 0 < d

Tactic:
refine pos_of_mul_pos_left ?_ (sq_nonneg a.y)

Result:
d : ℤ
a : Solution₁ d
ha : 1 < a.x
⊢ 0 < d * a.y ^ 2

Proof state:
d : ℤ
a : Solution₁ d
ha : 1 < a.x
⊢ 1 < a.x ^ 2

Tactic:
exact one_lt_pow₀ ha two_ne_zero

Result:
no goals
-- Mathlib/Geometry/Euclidean/Angle/Unoriented/Basic.lean
theorem angle_neg_left (x y : V) : angle (-x) y = π - angle x y

Proof state:
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
⊢ angle (-x) y = π - angle x y

Tactic:
rw [← angle_neg_neg, neg_neg, angle_neg_right]

Result:
no goals
-- Mathlib/MeasureTheory/Integral/IntegrableOn.lean
theorem IntegrableAtFilter.neg {f : α → E} (hf : IntegrableAtFilter f l μ) :
    IntegrableAtFilter (-f) l μ

Proof state:
α : Type u_1
E : Type u_4
inst✝¹ : MeasurableSpace α
inst✝ : NormedAddCommGroup E
μ : Measure α
l : Filter α
f : α → E
hf : IntegrableAtFilter f l μ
⊢ IntegrableAtFilter (-f) l μ

Tactic:
rcases hf with ⟨s, sl, hs⟩

Result:
case intro.intro
α : Type u_1
E : Type u_4
inst✝¹ : MeasurableSpace α
inst✝ : NormedAddCommGroup E
μ : Measure α
l : Filter α
f : α → E
s : Set α
sl : s ∈ l
hs : IntegrableOn f s μ
⊢ IntegrableAtFilter (-f) l μ

Proof state:
case intro.intro
α : Type u_1
E : Type u_4
inst✝¹ : MeasurableSpace α
inst✝ : NormedAddCommGroup E
μ : Measure α
l : Filter α
f : α → E
s : Set α
sl : s ∈ l
hs : IntegrableOn f s μ
⊢ IntegrableAtFilter (-f) l μ

Tactic:
exact ⟨s, sl, hs.neg⟩

Result:
no goals
-- Mathlib/MeasureTheory/Function/L1Space/Integrable.lean
/-- if `f` is integrable, then `f + g` is integrable iff `g` is.
See `integrable_add_iff_integrable_right'` for the same statement with `fun x ↦ f x + g x` instead
of `f + g`. -/
@[simp]
lemma integrable_add_iff_integrable_right {f g : α → β} (hf : Integrable f μ) :
    Integrable (f + g) μ ↔ Integrable g μ :=
  ⟨fun h ↦ show g = f + g + (-f) by simp only [add_neg_cancel_comm] ▸ h.add hf.neg,
    fun h ↦ hf.add h⟩

Proof state:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
f g : α → β
hf : Integrable f μ
h : Integrable (f + g) μ
⊢ g = f + g + -f

Tactic:
simp only [add_neg_cancel_comm]

Result:
no goals
-- Mathlib/Logic/Basic.lean
theorem exists_mem_or_left :
    (∃ (x : _) (_ : p x ∨ q x), r x) ↔ (∃ (x : _) (_ : p x), r x) ∨ ∃ (x : _) (_ : q x), r x

Proof state:
α : Sort u_1
r p q : α → Prop
⊢ (∃ x, (p x ∨ q x) ∧ r x) ↔ (∃ x, p x ∧ r x) ∨ ∃ x, q x ∧ r x

Tactic:
exact Iff.trans (exists_congr fun x ↦ or_and_right) exists_or

Result:
no goals

Proof state:
α : Sort u_1
r p q : α → Prop
⊢ (∃ x x_1, r x) ↔ (∃ x x_1, r x) ∨ ∃ x x_1, r x

Tactic:
simp only [exists_prop]

Result:
α : Sort u_1
r p q : α → Prop
⊢ (∃ x, (p x ∨ q x) ∧ r x) ↔ (∃ x, p x ∧ r x) ∨ ∃ x, q x ∧ r x
-- Mathlib/.lake/packages/batteries/Batteries/Data/Nat/Bisect.lean
theorem avg_le_left (h : b ≤ a) : avg a b ≤ a

Proof state:
b a : Nat
h : b ≤ a
⊢ a.avg b ≤ a

Tactic:
apply Nat.div_le_of_le_mul

Result:
case a
b a : Nat
h : b ≤ a
⊢ a + b ≤ 2 * a

Proof state:
case a
b a : Nat
h : b ≤ a
⊢ a + b ≤ 2 * a

Tactic:
simp_arith [*]

Result:
no goals
-- Mathlib/Algebra/BigOperators/Group/List/Basic.lean
lemma sum_int_mod (l : List ℤ) (n : ℤ) : l.sum % n = (l.map (· % n)).sum % n

Proof state:
l : List ℤ
n : ℤ
⊢ l.sum % n = (map (fun x => x % n) l).sum % n

Tactic:
induction l <;> simp [Int.add_emod, *]

Result:
no goals
-- Mathlib/Data/Nat/Factors.lean
theorem coprime_primeFactorsList_disjoint {a b : ℕ} (hab : a.Coprime b) :
    List.Disjoint a.primeFactorsList b.primeFactorsList

Proof state:
a b : ℕ
hab : a.Coprime b
q : ℕ
hqa : q ∈ a.primeFactorsList
hqb : q ∈ b.primeFactorsList
⊢ False

Tactic:
apply not_prime_one

Result:
a b : ℕ
hab : a.Coprime b
q : ℕ
hqa : q ∈ a.primeFactorsList
hqb : q ∈ b.primeFactorsList
⊢ Prime 1

Proof state:
a b : ℕ
hab : a.Coprime b
q : ℕ
hqa : q ∈ a.primeFactorsList
hqb : q ∈ b.primeFactorsList
⊢ Prime 1

Tactic:
rw [← eq_one_of_dvd_coprimes hab (dvd_of_mem_primeFactorsList hqa)
  (dvd_of_mem_primeFactorsList hqb)]

Result:
a b : ℕ
hab : a.Coprime b
q : ℕ
hqa : q ∈ a.primeFactorsList
hqb : q ∈ b.primeFactorsList
⊢ Prime q

Proof state:
a b : ℕ
hab : a.Coprime b
q : ℕ
hqa : q ∈ a.primeFactorsList
hqb : q ∈ b.primeFactorsList
⊢ Prime q

Tactic:
exact prime_of_mem_primeFactorsList hqa

Result:
no goals

Proof state:
a b : ℕ
hab : a.Coprime b
⊢ a.primeFactorsList.Disjoint b.primeFactorsList

Tactic:
intro q hqa hqb

Result:
a b : ℕ
hab : a.Coprime b
q : ℕ
hqa : q ∈ a.primeFactorsList
hqb : q ∈ b.primeFactorsList
⊢ False
-- Mathlib/Analysis/Normed/Lp/ProdLp.lean
theorem prod_dist_eq_of_L1 (x y : WithLp 1 (α × β)) :
    dist x y = dist x.fst y.fst + dist x.snd y.snd

Proof state:
α : Type u_2
β : Type u_3
inst✝¹ : SeminormedAddCommGroup α
inst✝ : SeminormedAddCommGroup β
x y : WithLp 1 (α × β)
⊢ dist x y = dist x.1 y.1 + dist x.2 y.2

Tactic:
simp_rw [dist_eq_norm, prod_norm_eq_of_L1, sub_fst, sub_snd]

Result:
no goals
-- Mathlib/Geometry/Manifold/IsManifold/Basic.lean
theorem of_le {m n : WithTop ℕ∞} (hmn : m ≤ n)
    [IsManifold I n M] : IsManifold I m M

Proof state:
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
H : Type u_3
inst✝³ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝² : TopologicalSpace M
inst✝¹ : ChartedSpace H M
m n : WithTop ℕ∞
hmn : m ≤ n
inst✝ : IsManifold I n M
this : HasGroupoid M (contDiffGroupoid m I)
⊢ IsManifold I m M

Tactic:
exact mk' I m M

Result:
no goals

Proof state:
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
H : Type u_3
inst✝³ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝² : TopologicalSpace M
inst✝¹ : ChartedSpace H M
m n : WithTop ℕ∞
hmn : m ≤ n
inst✝ : IsManifold I n M
⊢ IsManifold I m M

Tactic:
have : HasGroupoid M (contDiffGroupoid m I) :=
  hasGroupoid_of_le (G₁ := contDiffGroupoid n I) (by infer_instance)
    (contDiffGroupoid_le hmn)

Result:
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
H : Type u_3
inst✝³ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝² : TopologicalSpace M
inst✝¹ : ChartedSpace H M
m n : WithTop ℕ∞
hmn : m ≤ n
inst✝ : IsManifold I n M
this : HasGroupoid M (contDiffGroupoid m I)
⊢ IsManifold I m M

Proof state:
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
H : Type u_3
inst✝³ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝² : TopologicalSpace M
inst✝¹ : ChartedSpace H M
m n : WithTop ℕ∞
hmn : m ≤ n
inst✝ : IsManifold I n M
⊢ HasGroupoid M (contDiffGroupoid n I)

Tactic:
infer_instance

Result:
no goals
-- Mathlib/Data/Part.lean
theorem toOption_eq_some_iff {o : Part α} [Decidable o.Dom] {a : α} :
    toOption o = Option.some a ↔ a ∈ o

Proof state:
α : Type u_1
o : Part α
inst✝ : Decidable o.Dom
a : α
⊢ o.toOption = Option.some a ↔ a ∈ o

Tactic:
rw [← Option.mem_def, mem_toOption]

Result:
no goals
-- Mathlib/SetTheory/Ordinal/Basic.lean
theorem card_typein_lt (r : α → α → Prop) [IsWellOrder α r] (x : α) (h : ord #α = type r) :
    card (typein r x) < #α

Proof state:
α : Type u
r : α → α → Prop
inst✝ : IsWellOrder α r
x : α
h : (#α).ord = type r
⊢ ((typein r).toRelEmbedding x).card < #α

Tactic:
rw [← lt_ord, h]

Result:
α : Type u
r : α → α → Prop
inst✝ : IsWellOrder α r
x : α
h : (#α).ord = type r
⊢ (typein r).toRelEmbedding x < type r

Proof state:
α : Type u
r : α → α → Prop
inst✝ : IsWellOrder α r
x : α
h : (#α).ord = type r
⊢ (typein r).toRelEmbedding x < type r

Tactic:
apply typein_lt_type

Result:
no goals
-- Mathlib/Data/Matroid/Basic.lean
theorem ext_iff_indep {M₁ M₂ : Matroid α} :
    M₁ = M₂ ↔ (M₁.E = M₂.E) ∧ ∀ ⦃I⦄, I ⊆ M₁.E → (M₁.Indep I ↔ M₂.Indep I) :=
  ⟨fun h ↦ by (subst h; simp), fun h ↦ ext_indep h.1 h.2⟩

Proof state:
α : Type u_1
M₁ M₂ : Matroid α
h : M₁ = M₂
⊢ M₁.E = M₂.E ∧ ∀ ⦃I : Set α⦄, I ⊆ M₁.E → (M₁.Indep I ↔ M₂.Indep I)

Tactic:
subst h

Result:
α : Type u_1
M₁ : Matroid α
⊢ M₁.E = M₁.E ∧ ∀ ⦃I : Set α⦄, I ⊆ M₁.E → (M₁.Indep I ↔ M₁.Indep I)

Proof state:
α : Type u_1
M₁ : Matroid α
⊢ M₁.E = M₁.E ∧ ∀ ⦃I : Set α⦄, I ⊆ M₁.E → (M₁.Indep I ↔ M₁.Indep I)

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
M₁ M₂ : Matroid α
h : M₁ = M₂
⊢ M₁.E = M₂.E ∧ ∀ ⦃I : Set α⦄, I ⊆ M₁.E → (M₁.Indep I ↔ M₂.Indep I)

Tactic:
(subst h; simp)

Result:
no goals
-- Mathlib/Order/SymmDiff.lean
theorem symmDiff_sdiff_right : a ∆ b \ b = a \ b

Proof state:
α : Type u_2
inst✝ : GeneralizedBooleanAlgebra α
a b : α
⊢ a ∆ b \ b = a \ b

Tactic:
rw [symmDiff_comm, symmDiff_sdiff_left]

Result:
no goals
-- Mathlib/LinearAlgebra/AffineSpace/AffineEquiv.lean
theorem injective_pointReflection_left_of_module [Invertible (2 : k)] :
    ∀ y, Injective fun x : P₁ => pointReflection k x y :=
  injective_pointReflection_left_of_injective_two_nsmul k fun x y h => by
    dsimp at h
    rwa [two_nsmul, two_nsmul, ← two_smul k x, ← two_smul k y,
      (isUnit_of_invertible (2 : k)).smul_left_cancel] at h

Proof state:
k : Type u_1
P₁ : Type u_2
V₁ : Type u_6
inst✝⁴ : Ring k
inst✝³ : AddCommGroup V₁
inst✝² : Module k V₁
inst✝¹ : AffineSpace V₁ P₁
inst✝ : Invertible 2
x y : V₁
h : 2 • x = 2 • y
⊢ x = y

Tactic:
rwa [two_nsmul, two_nsmul, ← two_smul k x, ← two_smul k y,
  (isUnit_of_invertible (2 : k)).smul_left_cancel] at h

Result:
no goals

Proof state:
k : Type u_1
P₁ : Type u_2
V₁ : Type u_6
inst✝⁴ : Ring k
inst✝³ : AddCommGroup V₁
inst✝² : Module k V₁
inst✝¹ : AffineSpace V₁ P₁
inst✝ : Invertible 2
x y : V₁
h : (fun x => 2 • x) x = (fun x => 2 • x) y
⊢ x = y

Tactic:
dsimp at h

Result:
k : Type u_1
P₁ : Type u_2
V₁ : Type u_6
inst✝⁴ : Ring k
inst✝³ : AddCommGroup V₁
inst✝² : Module k V₁
inst✝¹ : AffineSpace V₁ P₁
inst✝ : Invertible 2
x y : V₁
h : 2 • x = 2 • y
⊢ x = y
-- Mathlib/Algebra/Polynomial/Roots.lean
theorem roots_X : roots (X : R[X]) = {0}

Proof state:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
⊢ X.roots = {0}

Tactic:
rw [← roots_X_sub_C, C_0, sub_zero]

Result:
no goals
-- Mathlib/RingTheory/UniqueFactorizationDomain/Finsupp.lean
theorem factorization_pow {x : α} {n : ℕ} : factorization (x ^ n) = n • factorization x

Proof state:
α : Type u_1
inst✝³ : CancelCommMonoidWithZero α
inst✝² : UniqueFactorizationMonoid α
inst✝¹ : NormalizationMonoid α
inst✝ : DecidableEq α
x : α
n : ℕ
⊢ factorization (x ^ n) = n • factorization x

Tactic:
ext

Result:
case h
α : Type u_1
inst✝³ : CancelCommMonoidWithZero α
inst✝² : UniqueFactorizationMonoid α
inst✝¹ : NormalizationMonoid α
inst✝ : DecidableEq α
x : α
n : ℕ
a✝ : α
⊢ (factorization (x ^ n)) a✝ = (n • factorization x) a✝

Proof state:
case h
α : Type u_1
inst✝³ : CancelCommMonoidWithZero α
inst✝² : UniqueFactorizationMonoid α
inst✝¹ : NormalizationMonoid α
inst✝ : DecidableEq α
x : α
n : ℕ
a✝ : α
⊢ (factorization (x ^ n)) a✝ = (n • factorization x) a✝

Tactic:
simp [factorization]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/List/Associative.lean
theorem keys_eraseKey [BEq α] [PartialEquivBEq α] {l : List ((a : α) × β a)} {k : α} :
    keys (eraseKey k l) = (keys l).erase k

Proof state:
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : PartialEquivBEq α
k k' : α
v' : β k'
l : List ((a : α) × β a)
ih : keys (eraseKey k l) = (keys l).erase k
⊢ keys (bif k' == k then l else ⟨k', v'⟩ :: eraseKey k l) = if (k' == k) = true then keys l else k' :: (keys l).erase k

Tactic:
rw [BEq.comm]

Result:
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : PartialEquivBEq α
k k' : α
v' : β k'
l : List ((a : α) × β a)
ih : keys (eraseKey k l) = (keys l).erase k
⊢ keys (bif k == k' then l else ⟨k', v'⟩ :: eraseKey k l) = if (k == k') = true then keys l else k' :: (keys l).erase k

Proof state:
case cons
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : PartialEquivBEq α
k k✝ : α
v✝ : β k✝
tail✝ : List ((a : α) × β a)
a✝ : keys (eraseKey k tail✝) = (keys tail✝).erase k
⊢ keys (eraseKey k (⟨k✝, v✝⟩ :: tail✝)) = (keys (⟨k✝, v✝⟩ :: tail✝)).erase k

Tactic:
next k' v' l ih =>
simp only [eraseKey_cons, keys_cons, List.erase_cons]
rw [BEq.comm]
cases k == k' <;> simp [ih]

Result:
no goals

Proof state:
case nil
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : PartialEquivBEq α
k : α
⊢ keys (eraseKey k []) = (keys []).erase k

Tactic:
rfl

Result:
no goals

Proof state:
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : PartialEquivBEq α
l : List ((a : α) × β a)
k : α
⊢ keys (eraseKey k l) = (keys l).erase k

Tactic:
induction l using assoc_induction

Result:
case nil
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : PartialEquivBEq α
k : α
⊢ keys (eraseKey k []) = (keys []).erase k

case cons
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : PartialEquivBEq α
k k✝ : α
v✝ : β k✝
tail✝ : List ((a : α) × β a)
a✝ : keys (eraseKey k tail✝) = (keys tail✝).erase k
⊢ keys (eraseKey k (⟨k✝, v✝⟩ :: tail✝)) = (keys (⟨k✝, v✝⟩ :: tail✝)).erase k

Proof state:
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : PartialEquivBEq α
k k' : α
v' : β k'
l : List ((a : α) × β a)
ih : keys (eraseKey k l) = (keys l).erase k
⊢ keys (eraseKey k (⟨k', v'⟩ :: l)) = (keys (⟨k', v'⟩ :: l)).erase k

Tactic:
simp only [eraseKey_cons, keys_cons, List.erase_cons]

Result:
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : PartialEquivBEq α
k k' : α
v' : β k'
l : List ((a : α) × β a)
ih : keys (eraseKey k l) = (keys l).erase k
⊢ keys (bif k' == k then l else ⟨k', v'⟩ :: eraseKey k l) = if (k' == k) = true then keys l else k' :: (keys l).erase k

Proof state:
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : PartialEquivBEq α
k k' : α
v' : β k'
l : List ((a : α) × β a)
ih : keys (eraseKey k l) = (keys l).erase k
⊢ keys (bif k == k' then l else ⟨k', v'⟩ :: eraseKey k l) = if (k == k') = true then keys l else k' :: (keys l).erase k

Tactic:
cases k == k' <;> simp [ih]

Result:
no goals
-- Mathlib/Topology/Separation/Basic.lean
lemma nhdsWithin_compl_singleton_le [T1Space X] (x y : X) : 𝓝[{x}ᶜ] x ≤ 𝓝[{y}ᶜ] x

Proof state:
case inr
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : T1Space X
x y : X
hy : x ≠ y
⊢ 𝓝[≠] x ≤ 𝓝[{y}ᶜ] x

Tactic:
rw [Ne.nhdsWithin_compl_singleton hy]

Result:
case inr
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : T1Space X
x y : X
hy : x ≠ y
⊢ 𝓝[≠] x ≤ 𝓝 x

Proof state:
case inl
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : T1Space X
x : X
⊢ 𝓝[≠] x ≤ 𝓝[≠] x

Tactic:
exact Eq.le rfl

Result:
no goals

Proof state:
case inr
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : T1Space X
x y : X
hy : x ≠ y
⊢ 𝓝[≠] x ≤ 𝓝 x

Tactic:
exact nhdsWithin_le_nhds

Result:
no goals

Proof state:
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : T1Space X
x y : X
⊢ 𝓝[≠] x ≤ 𝓝[{y}ᶜ] x

Tactic:
rcases eq_or_ne x y with rfl|hy

Result:
case inl
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : T1Space X
x : X
⊢ 𝓝[≠] x ≤ 𝓝[≠] x

case inr
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : T1Space X
x y : X
hy : x ≠ y
⊢ 𝓝[≠] x ≤ 𝓝[{y}ᶜ] x
-- Mathlib/Data/Nat/Sqrt.lean
lemma sqrt_add_eq (n : ℕ) (h : a ≤ n + n) : sqrt (n * n + a) = n :=
  le_antisymm
    (le_of_lt_succ <|
      sqrt_lt.2 <| by
        rw [succ_mul, mul_succ, add_succ, Nat.add_assoc]
        exact lt_succ_of_le (Nat.add_le_add_left h _))
    (le_sqrt.2 <| Nat.le_add_right _ _)

Proof state:
a n : ℕ
h : a ≤ n + n
⊢ n * n + a < n.succ * n.succ

Tactic:
rw [succ_mul, mul_succ, add_succ, Nat.add_assoc]

Result:
a n : ℕ
h : a ≤ n + n
⊢ n * n + a < (n * n + (n + n)).succ

Proof state:
a n : ℕ
h : a ≤ n + n
⊢ n * n + a < (n * n + (n + n)).succ

Tactic:
exact lt_succ_of_le (Nat.add_le_add_left h _)

Result:
no goals
-- Mathlib/Order/Birkhoff.lean
@[simp] lemma supIrredLowerSet_symm_apply (s : {s : LowerSet α // SupIrred s}) [Fintype s] :
    supIrredLowerSet.symm s = (s.1 : Set α).toFinset.sup id

Proof state:
case mk
α : Type u_1
inst✝³ : SemilatticeSup α
inst✝² : OrderBot α
inst✝¹ : Finite α
s : LowerSet α
hs : SupIrred s
inst✝ : Fintype ↥↑⟨s, hs⟩
⊢ supIrredLowerSet.symm ⟨s, hs⟩ = (↑↑⟨s, hs⟩).toFinset.sup id

Tactic:
obtain ⟨a, rfl⟩ := supIrred_iff_of_finite.1 hs

Result:
case mk.intro
α : Type u_1
inst✝³ : SemilatticeSup α
inst✝² : OrderBot α
inst✝¹ : Finite α
a : α
hs : SupIrred (LowerSet.Iic a)
inst✝ : Fintype ↥↑⟨LowerSet.Iic a, hs⟩
⊢ supIrredLowerSet.symm ⟨LowerSet.Iic a, hs⟩ = (↑↑⟨LowerSet.Iic a, hs⟩).toFinset.sup id

Proof state:
α : Type u_1
inst✝³ : SemilatticeSup α
inst✝² : OrderBot α
inst✝¹ : Finite α
s : { s // SupIrred s }
inst✝ : Fintype ↥↑s
⊢ supIrredLowerSet.symm s = (↑↑s).toFinset.sup id

Tactic:
classical
obtain ⟨s, hs⟩ := s
obtain ⟨a, rfl⟩ := supIrred_iff_of_finite.1 hs
cases nonempty_fintype α
have : LocallyFiniteOrder α := Fintype.toLocallyFiniteOrder
simp [symm_apply_eq]

Result:
no goals

Proof state:
case mk.intro.intro
α : Type u_1
inst✝³ : SemilatticeSup α
inst✝² : OrderBot α
inst✝¹ : Finite α
a : α
hs : SupIrred (LowerSet.Iic a)
inst✝ : Fintype ↥↑⟨LowerSet.Iic a, hs⟩
val✝ : Fintype α
⊢ supIrredLowerSet.symm ⟨LowerSet.Iic a, hs⟩ = (↑↑⟨LowerSet.Iic a, hs⟩).toFinset.sup id

Tactic:
have : LocallyFiniteOrder α := Fintype.toLocallyFiniteOrder

Result:
case mk.intro.intro
α : Type u_1
inst✝³ : SemilatticeSup α
inst✝² : OrderBot α
inst✝¹ : Finite α
a : α
hs : SupIrred (LowerSet.Iic a)
inst✝ : Fintype ↥↑⟨LowerSet.Iic a, hs⟩
val✝ : Fintype α
this : LocallyFiniteOrder α
⊢ supIrredLowerSet.symm ⟨LowerSet.Iic a, hs⟩ = (↑↑⟨LowerSet.Iic a, hs⟩).toFinset.sup id

Proof state:
case mk.intro.intro
α : Type u_1
inst✝³ : SemilatticeSup α
inst✝² : OrderBot α
inst✝¹ : Finite α
a : α
hs : SupIrred (LowerSet.Iic a)
inst✝ : Fintype ↥↑⟨LowerSet.Iic a, hs⟩
val✝ : Fintype α
this : LocallyFiniteOrder α
⊢ supIrredLowerSet.symm ⟨LowerSet.Iic a, hs⟩ = (↑↑⟨LowerSet.Iic a, hs⟩).toFinset.sup id

Tactic:
simp [symm_apply_eq]

Result:
no goals

Proof state:
case mk.intro
α : Type u_1
inst✝³ : SemilatticeSup α
inst✝² : OrderBot α
inst✝¹ : Finite α
a : α
hs : SupIrred (LowerSet.Iic a)
inst✝ : Fintype ↥↑⟨LowerSet.Iic a, hs⟩
⊢ supIrredLowerSet.symm ⟨LowerSet.Iic a, hs⟩ = (↑↑⟨LowerSet.Iic a, hs⟩).toFinset.sup id

Tactic:
cases nonempty_fintype α

Result:
case mk.intro.intro
α : Type u_1
inst✝³ : SemilatticeSup α
inst✝² : OrderBot α
inst✝¹ : Finite α
a : α
hs : SupIrred (LowerSet.Iic a)
inst✝ : Fintype ↥↑⟨LowerSet.Iic a, hs⟩
val✝ : Fintype α
⊢ supIrredLowerSet.symm ⟨LowerSet.Iic a, hs⟩ = (↑↑⟨LowerSet.Iic a, hs⟩).toFinset.sup id

Proof state:
α : Type u_1
inst✝³ : SemilatticeSup α
inst✝² : OrderBot α
inst✝¹ : Finite α
s : { s // SupIrred s }
inst✝ : Fintype ↥↑s
⊢ supIrredLowerSet.symm s = (↑↑s).toFinset.sup id

Tactic:
obtain ⟨s, hs⟩ := s

Result:
case mk
α : Type u_1
inst✝³ : SemilatticeSup α
inst✝² : OrderBot α
inst✝¹ : Finite α
s : LowerSet α
hs : SupIrred s
inst✝ : Fintype ↥↑⟨s, hs⟩
⊢ supIrredLowerSet.symm ⟨s, hs⟩ = (↑↑⟨s, hs⟩).toFinset.sup id