harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Data/Stream/Init.lean
theorem tail_even (s : Stream' α) : tail (even s) = even (tail (tail s))

Proof state:
α : Type u
s : Stream' α
⊢ (corec head (fun s => s.tail.tail) s).tail = corec head (fun s => s.tail.tail) s.tail.tail

Tactic:
rw [corec_eq]

Result:
α : Type u
s : Stream' α
⊢ (s.head :: corec head (fun s => s.tail.tail) s.tail.tail).tail = corec head (fun s => s.tail.tail) s.tail.tail

Proof state:
α : Type u
s : Stream' α
⊢ s.even.tail = s.tail.tail.even

Tactic:
unfold even

Result:
α : Type u
s : Stream' α
⊢ (corec head (fun s => s.tail.tail) s).tail = corec head (fun s => s.tail.tail) s.tail.tail

Proof state:
α : Type u
s : Stream' α
⊢ (s.head :: corec head (fun s => s.tail.tail) s.tail.tail).tail = corec head (fun s => s.tail.tail) s.tail.tail

Tactic:
rfl

Result:
no goals
-- Mathlib/Data/Fin/Tuple/Take.lean
theorem take_init {α : Fin (n + 1) → Sort*} (m : ℕ) (h : m ≤ n) (v : (i : Fin (n + 1)) → α i) :
    take m h (init v) = take m (Nat.le_succ_of_le h) v

Proof state:
case h
n : ℕ
α : Fin (n + 1) → Sort u_2
m : ℕ
h : m ≤ n
v : (i : Fin (n + 1)) → α i
i : Fin m
⊢ v (castLE h i).castSucc = v (castLE ⋯ i)

Tactic:
congr

Result:
no goals

Proof state:
n : ℕ
α : Fin (n + 1) → Sort u_2
m : ℕ
h : m ≤ n
v : (i : Fin (n + 1)) → α i
⊢ take m h (init v) = take m ⋯ v

Tactic:
ext i

Result:
case h
n : ℕ
α : Fin (n + 1) → Sort u_2
m : ℕ
h : m ≤ n
v : (i : Fin (n + 1)) → α i
i : Fin m
⊢ take m h (init v) i = take m ⋯ v i

Proof state:
case h
n : ℕ
α : Fin (n + 1) → Sort u_2
m : ℕ
h : m ≤ n
v : (i : Fin (n + 1)) → α i
i : Fin m
⊢ take m h (init v) i = take m ⋯ v i

Tactic:
simp only [take, init]

Result:
case h
n : ℕ
α : Fin (n + 1) → Sort u_2
m : ℕ
h : m ≤ n
v : (i : Fin (n + 1)) → α i
i : Fin m
⊢ v (castLE h i).castSucc = v (castLE ⋯ i)
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Nat/Sublist.lean
theorem append_left_sublist_self {xs : List α} (ys : List α) : xs ++ ys <+ ys ↔ xs = []

Proof state:
case mp
α : Type u_1
xs ys : List α
h : (xs ++ ys).length ≤ ys.length
⊢ xs = []

Tactic:
simp only [length_append] at h

Result:
case mp
α : Type u_1
xs ys : List α
h : xs.length + ys.length ≤ ys.length
⊢ xs = []

Proof state:
case mp
α : Type u_1
xs ys : List α
h : xs.length + ys.length ≤ ys.length
this : xs.length = 0
⊢ xs = []

Tactic:
simp_all

Result:
no goals

Proof state:
case mpr
α : Type u_1
ys : List α
⊢ [] ++ ys <+ ys

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
xs ys : List α
⊢ xs ++ ys <+ ys ↔ xs = []

Tactic:
constructor

Result:
case mp
α : Type u_1
xs ys : List α
⊢ xs ++ ys <+ ys → xs = []

case mpr
α : Type u_1
xs ys : List α
⊢ xs = [] → xs ++ ys <+ ys

Proof state:
case mpr
α : Type u_1
xs ys : List α
⊢ xs = [] → xs ++ ys <+ ys

Tactic:
rintro rfl

Result:
case mpr
α : Type u_1
ys : List α
⊢ [] ++ ys <+ ys

Proof state:
case mp
α : Type u_1
xs ys : List α
⊢ xs ++ ys <+ ys → xs = []

Tactic:
intro h

Result:
case mp
α : Type u_1
xs ys : List α
h : xs ++ ys <+ ys
⊢ xs = []

Proof state:
α : Type u_1
xs ys : List α
h : xs.length + ys.length ≤ ys.length
⊢ xs.length = 0

Tactic:
omega

Result:
no goals

Proof state:
case mp
α : Type u_1
xs ys : List α
h : xs.length + ys.length ≤ ys.length
⊢ xs = []

Tactic:
have : xs.length = 0 := by omega

Result:
case mp
α : Type u_1
xs ys : List α
h : xs.length + ys.length ≤ ys.length
this : xs.length = 0
⊢ xs = []

Proof state:
case mp
α : Type u_1
xs ys : List α
h : xs ++ ys <+ ys
⊢ xs = []

Tactic:
replace h := h.length_le

Result:
case mp
α : Type u_1
xs ys : List α
h : (xs ++ ys).length ≤ ys.length
⊢ xs = []
-- Mathlib/NumberTheory/Padics/RingHoms.lean
theorem zmod_congr_of_sub_mem_span_aux (n : ℕ) (x : ℤ_[p]) (a b : ℤ)
    (ha : x - a ∈ (Ideal.span {(p : ℤ_[p]) ^ n}))
    (hb : x - b ∈ (Ideal.span {(p : ℤ_[p]) ^ n})) : (a : ZMod (p ^ n)) = b

Proof state:
p : ℕ
hp_prime : Fact (Nat.Prime p)
n : ℕ
x : ℤ_[p]
a b : ℤ
ha : ↑p ^ n ∣ ↑a - x
hb : ↑p ^ n ∣ x - ↑b
this : ↑p ^ n ∣ ↑a - x + (x - ↑b)
⊢ ↑p ^ n ∣ a - b

Tactic:
rwa [sub_eq_add_neg, sub_eq_add_neg, add_assoc, neg_add_cancel_left, ← sub_eq_add_neg, ←
  Int.cast_sub, pow_p_dvd_int_iff] at this

Result:
no goals

Proof state:
p : ℕ
hp_prime : Fact (Nat.Prime p)
n : ℕ
x : ℤ_[p]
a b : ℤ
ha : ↑p ^ n ∣ x - ↑a
hb : ↑p ^ n ∣ x - ↑b
⊢ ↑p ^ n ∣ a - b

Tactic:
rw [← dvd_neg, neg_sub] at ha

Result:
p : ℕ
hp_prime : Fact (Nat.Prime p)
n : ℕ
x : ℤ_[p]
a b : ℤ
ha : ↑p ^ n ∣ ↑a - x
hb : ↑p ^ n ∣ x - ↑b
⊢ ↑p ^ n ∣ a - b

Proof state:
p : ℕ
hp_prime : Fact (Nat.Prime p)
n : ℕ
x : ℤ_[p]
a b : ℤ
ha : x - ↑a ∈ Ideal.span {↑p ^ n}
hb : x - ↑b ∈ Ideal.span {↑p ^ n}
⊢ ↑a = ↑b

Tactic:
rw [Ideal.mem_span_singleton] at ha hb

Result:
p : ℕ
hp_prime : Fact (Nat.Prime p)
n : ℕ
x : ℤ_[p]
a b : ℤ
ha : ↑p ^ n ∣ x - ↑a
hb : ↑p ^ n ∣ x - ↑b
⊢ ↑a = ↑b

Proof state:
p : ℕ
hp_prime : Fact (Nat.Prime p)
n : ℕ
x : ℤ_[p]
a b : ℤ
ha : ↑p ^ n ∣ ↑a - x
hb : ↑p ^ n ∣ x - ↑b
⊢ ↑p ^ n ∣ a - b

Tactic:
have := dvd_add ha hb

Result:
p : ℕ
hp_prime : Fact (Nat.Prime p)
n : ℕ
x : ℤ_[p]
a b : ℤ
ha : ↑p ^ n ∣ ↑a - x
hb : ↑p ^ n ∣ x - ↑b
this : ↑p ^ n ∣ ↑a - x + (x - ↑b)
⊢ ↑p ^ n ∣ a - b

Proof state:
p : ℕ
hp_prime : Fact (Nat.Prime p)
n : ℕ
x : ℤ_[p]
a b : ℤ
ha : ↑p ^ n ∣ x - ↑a
hb : ↑p ^ n ∣ x - ↑b
⊢ ↑a = ↑b

Tactic:
rw [← sub_eq_zero, ← Int.cast_sub, ZMod.intCast_zmod_eq_zero_iff_dvd, Int.natCast_pow]

Result:
p : ℕ
hp_prime : Fact (Nat.Prime p)
n : ℕ
x : ℤ_[p]
a b : ℤ
ha : ↑p ^ n ∣ x - ↑a
hb : ↑p ^ n ∣ x - ↑b
⊢ ↑p ^ n ∣ a - b
-- Mathlib/Topology/Algebra/Group/SubmonoidClosure.lean
theorem dense_submonoidClosure_iff_subgroupClosure {s : Set G} :
    Dense (Submonoid.closure s : Set G) ↔ Dense (Subgroup.closure s : Set G)

Proof state:
G : Type u_1
inst✝³ : Group G
inst✝² : TopologicalSpace G
inst✝¹ : CompactSpace G
inst✝ : IsTopologicalGroup G
s : Set G
⊢ Dense ↑(Submonoid.closure s) ↔ Dense ↑(Subgroup.closure s)

Tactic:
simp only [dense_iff_closure_eq, closure_submonoidClosure_eq_closure_subgroupClosure]

Result:
no goals
-- Mathlib/RingTheory/IsTensorProduct.lean
lemma IsTensorProduct.of_equiv (e : M₁ ⊗[R] M₂ ≃ₗ[R] M) (he : ∀ x y, e (x ⊗ₜ y) = f x y) :
    IsTensorProduct f

Proof state:
case a.h.h
R : Type u_1
inst✝⁶ : CommSemiring R
M₁ : Type u_2
M₂ : Type u_3
M : Type u_4
inst✝⁵ : AddCommMonoid M₁
inst✝⁴ : AddCommMonoid M₂
inst✝³ : AddCommMonoid M
inst✝² : Module R M₁
inst✝¹ : Module R M₂
inst✝ : Module R M
f : M₁ →ₗ[R] M₂ →ₗ[R] M
e : M₁ ⊗[R] M₂ ≃ₗ[R] M
he : ∀ (x : M₁) (y : M₂), e (x ⊗ₜ[R] y) = (f x) y
x : M₁
y : M₂
⊢ ((AlgebraTensorModule.curry (TensorProduct.lift f)) x) y = ((AlgebraTensorModule.curry ↑e) x) y

Tactic:
simp [he]

Result:
no goals

Proof state:
R : Type u_1
inst✝⁶ : CommSemiring R
M₁ : Type u_2
M₂ : Type u_3
M : Type u_4
inst✝⁵ : AddCommMonoid M₁
inst✝⁴ : AddCommMonoid M₂
inst✝³ : AddCommMonoid M
inst✝² : Module R M₁
inst✝¹ : Module R M₂
inst✝ : Module R M
f : M₁ →ₗ[R] M₂ →ₗ[R] M
e : M₁ ⊗[R] M₂ ≃ₗ[R] M
he : ∀ (x : M₁) (y : M₂), e (x ⊗ₜ[R] y) = (f x) y
⊢ IsTensorProduct f

Tactic:
have : TensorProduct.lift f = e := by
  ext x y
  simp [he]

Result:
R : Type u_1
inst✝⁶ : CommSemiring R
M₁ : Type u_2
M₂ : Type u_3
M : Type u_4
inst✝⁵ : AddCommMonoid M₁
inst✝⁴ : AddCommMonoid M₂
inst✝³ : AddCommMonoid M
inst✝² : Module R M₁
inst✝¹ : Module R M₂
inst✝ : Module R M
f : M₁ →ₗ[R] M₂ →ₗ[R] M
e : M₁ ⊗[R] M₂ ≃ₗ[R] M
he : ∀ (x : M₁) (y : M₂), e (x ⊗ₜ[R] y) = (f x) y
this : TensorProduct.lift f = ↑e
⊢ IsTensorProduct f

Proof state:
R : Type u_1
inst✝⁶ : CommSemiring R
M₁ : Type u_2
M₂ : Type u_3
M : Type u_4
inst✝⁵ : AddCommMonoid M₁
inst✝⁴ : AddCommMonoid M₂
inst✝³ : AddCommMonoid M
inst✝² : Module R M₁
inst✝¹ : Module R M₂
inst✝ : Module R M
f : M₁ →ₗ[R] M₂ →ₗ[R] M
e : M₁ ⊗[R] M₂ ≃ₗ[R] M
he : ∀ (x : M₁) (y : M₂), e (x ⊗ₜ[R] y) = (f x) y
this : TensorProduct.lift f = ↑e
⊢ IsTensorProduct f

Tactic:
simpa [IsTensorProduct, this] using e.bijective

Result:
no goals

Proof state:
R : Type u_1
inst✝⁶ : CommSemiring R
M₁ : Type u_2
M₂ : Type u_3
M : Type u_4
inst✝⁵ : AddCommMonoid M₁
inst✝⁴ : AddCommMonoid M₂
inst✝³ : AddCommMonoid M
inst✝² : Module R M₁
inst✝¹ : Module R M₂
inst✝ : Module R M
f : M₁ →ₗ[R] M₂ →ₗ[R] M
e : M₁ ⊗[R] M₂ ≃ₗ[R] M
he : ∀ (x : M₁) (y : M₂), e (x ⊗ₜ[R] y) = (f x) y
⊢ TensorProduct.lift f = ↑e

Tactic:
ext x y

Result:
case a.h.h
R : Type u_1
inst✝⁶ : CommSemiring R
M₁ : Type u_2
M₂ : Type u_3
M : Type u_4
inst✝⁵ : AddCommMonoid M₁
inst✝⁴ : AddCommMonoid M₂
inst✝³ : AddCommMonoid M
inst✝² : Module R M₁
inst✝¹ : Module R M₂
inst✝ : Module R M
f : M₁ →ₗ[R] M₂ →ₗ[R] M
e : M₁ ⊗[R] M₂ ≃ₗ[R] M
he : ∀ (x : M₁) (y : M₂), e (x ⊗ₜ[R] y) = (f x) y
x : M₁
y : M₂
⊢ ((AlgebraTensorModule.curry (TensorProduct.lift f)) x) y = ((AlgebraTensorModule.curry ↑e) x) y
-- Mathlib/RingTheory/GradedAlgebra/Homogeneous/Ideal.lean
theorem HomogeneousIdeal.toIdeal_homogeneousCore_eq_self (I : HomogeneousIdeal 𝒜) :
    I.toIdeal.homogeneousCore 𝒜 = I

Proof state:
ι : Type u_1
σ : Type u_2
A : Type u_3
inst✝⁵ : Semiring A
inst✝⁴ : SetLike σ A
inst✝³ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝² : DecidableEq ι
inst✝¹ : AddMonoid ι
inst✝ : GradedRing 𝒜
I : HomogeneousIdeal 𝒜
⊢ Ideal.homogeneousCore 𝒜 I.toIdeal = I

Tactic:
ext1

Result:
case h
ι : Type u_1
σ : Type u_2
A : Type u_3
inst✝⁵ : Semiring A
inst✝⁴ : SetLike σ A
inst✝³ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝² : DecidableEq ι
inst✝¹ : AddMonoid ι
inst✝ : GradedRing 𝒜
I : HomogeneousIdeal 𝒜
⊢ (Ideal.homogeneousCore 𝒜 I.toIdeal).toIdeal = I.toIdeal

Proof state:
case h
ι : Type u_1
σ : Type u_2
A : Type u_3
inst✝⁵ : Semiring A
inst✝⁴ : SetLike σ A
inst✝³ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝² : DecidableEq ι
inst✝¹ : AddMonoid ι
inst✝ : GradedRing 𝒜
I : HomogeneousIdeal 𝒜
⊢ (Ideal.homogeneousCore 𝒜 I.toIdeal).toIdeal = I.toIdeal

Tactic:
convert Ideal.IsHomogeneous.toIdeal_homogeneousCore_eq_self I.isHomogeneous

Result:
no goals
-- Mathlib/ModelTheory/Substructures.lean
theorem lift_card_closure_le_card_term : Cardinal.lift.{max u w} #(closure L s) ≤ #(L.Term s)

Proof state:
L : Language
M : Type w
inst✝ : L.Structure M
s : Set M
⊢ lift.{max u w, w} #↥((closure L).toFun s) ≤ #(L.Term ↑s)

Tactic:
rw [← SetLike.coe_sort_coe, coe_closure_eq_range_term_realize]

Result:
L : Language
M : Type w
inst✝ : L.Structure M
s : Set M
⊢ lift.{max u w, w} #↑(range (Term.realize Subtype.val)) ≤ #(L.Term ↑s)

Proof state:
L : Language
M : Type w
inst✝ : L.Structure M
s : Set M
⊢ lift.{max u w, w} #↑(range (Term.realize Subtype.val)) ≤ #(L.Term ↑s)

Tactic:
rw [← Cardinal.lift_id'.{w, max u w} #(L.Term s)]

Result:
L : Language
M : Type w
inst✝ : L.Structure M
s : Set M
⊢ lift.{max u w, w} #↑(range (Term.realize Subtype.val)) ≤ lift.{w, max u w} #(L.Term ↑s)

Proof state:
L : Language
M : Type w
inst✝ : L.Structure M
s : Set M
⊢ lift.{max u w, w} #↑(range (Term.realize Subtype.val)) ≤ lift.{w, max u w} #(L.Term ↑s)

Tactic:
exact Cardinal.mk_range_le_lift

Result:
no goals
-- Mathlib/MeasureTheory/Function/SimpleFunc.lean
theorem approx_comp [TopologicalSpace β] [OrderClosedTopology β] [MeasurableSpace β]
    [OpensMeasurableSpace β] [MeasurableSpace γ] {i : ℕ → β} {f : γ → β} {g : α → γ} {n : ℕ} (a : α)
    (hf : Measurable f) (hg : Measurable g) :
    (approx i (f ∘ g) n : α →ₛ β) a = (approx i f n : γ →ₛ β) (g a)

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝⁸ : MeasurableSpace α
inst✝⁷ : SemilatticeSup β
inst✝⁶ : OrderBot β
inst✝⁵ : Zero β
inst✝⁴ : TopologicalSpace β
inst✝³ : OrderClosedTopology β
inst✝² : MeasurableSpace β
inst✝¹ : OpensMeasurableSpace β
inst✝ : MeasurableSpace γ
i : ℕ → β
f : γ → β
g : α → γ
n : ℕ
a : α
hf : Measurable f
hg : Measurable g
⊢ (approx i (f ∘ g) n) a = (approx i f n) (g a)

Tactic:
rw [approx_apply _ hf, approx_apply _ (hf.comp hg), Function.comp_apply]

Result:
no goals
-- Mathlib/Data/Ordering/Lemmas.lean
theorem cmpUsing_eq_lt (a b : α) : (cmpUsing lt a b = Ordering.lt) = lt a b

Proof state:
α : Type u
lt : α → α → Prop
inst✝ : DecidableRel lt
a b : α
⊢ (cmpUsing lt a b = Ordering.lt) = lt a b

Tactic:
simp only [cmpUsing, Ordering.ite_eq_lt_distrib, ite_self, if_false_right, and_true, reduceCtorEq]

Result:
no goals
-- Mathlib/Data/Bool/Count.lean
theorem Chain.count_not :
    ∀ {b : Bool} {l : List Bool}, Chain (· ≠ ·) b l → count (!b) l = count b l + length l % 2
  | _, [], _h => rfl
  | b, x :: l, h => by
    obtain rfl : b = !x := Bool.eq_not_iff.2 (rel_of_chain_cons h)
    rw [Bool.not_not, count_cons_self, count_cons_of_ne x.not_ne_self,
      Chain.count_not (chain_of_chain_cons h), length, add_assoc, Nat.mod_two_add_succ_mod_two]

Proof state:
b x : Bool
l : List Bool
h : Chain (fun x1 x2 => x1 ≠ x2) b (x :: l)
⊢ count (!b) (x :: l) = count b (x :: l) + (x :: l).length % 2

Tactic:
obtain rfl : b = !x := Bool.eq_not_iff.2 (rel_of_chain_cons h)

Result:
x : Bool
l : List Bool
h : Chain (fun x1 x2 => x1 ≠ x2) (!x) (x :: l)
⊢ count (!!x) (x :: l) = count (!x) (x :: l) + (x :: l).length % 2

Proof state:
x : Bool
l : List Bool
h : Chain (fun x1 x2 => x1 ≠ x2) (!x) (x :: l)
⊢ count (!!x) (x :: l) = count (!x) (x :: l) + (x :: l).length % 2

Tactic:
rw [Bool.not_not, count_cons_self, count_cons_of_ne x.not_ne_self,
  Chain.count_not (chain_of_chain_cons h), length, add_assoc, Nat.mod_two_add_succ_mod_two]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem mem_dite_empty_right {x : α} [Decidable p] {l : p → Array α} :
    (x ∈ if h : p then l h else #[]) ↔ ∃ h : p, x ∈ l h

Proof state:
α : Type u_1
p : Prop
x : α
inst✝ : Decidable p
l : p → Array α
⊢ (x ∈ if h : p then l h else #[]) ↔ ∃ h, x ∈ l h

Tactic:
split <;> simp_all

Result:
no goals
-- Mathlib/Order/CompactlyGenerated/Basic.lean
theorem DirectedOn.disjoint_sSup_left (h : DirectedOn (· ≤ ·) s) :
    Disjoint (sSup s) a ↔ ∀ ⦃b⦄, b ∈ s → Disjoint b a

Proof state:
α : Type u_2
inst✝¹ : CompleteLattice α
inst✝ : IsCompactlyGenerated α
a : α
s : Set α
h : DirectedOn (fun x1 x2 => x1 ≤ x2) s
⊢ Disjoint (sSup s) a ↔ ∀ ⦃b : α⦄, b ∈ s → Disjoint b a

Tactic:
simp_rw [disjoint_iff, h.sSup_inf_eq, iSup_eq_bot]

Result:
no goals
-- Mathlib/RingTheory/Perfection.lean
theorem preVal_mk {x : O} (hx : (Ideal.Quotient.mk _ x : ModP O p) ≠ 0) :
    preVal K v O p (Ideal.Quotient.mk _ x) = v (algebraMap O K x)

Proof state:
case intro
K : Type u₁
inst✝² : Field K
v : Valuation K ℝ≥0
O : Type u₂
inst✝¹ : CommRing O
inst✝ : Algebra O K
hv : v.Integers O
p : ℕ
x : O
hx : (Ideal.Quotient.mk (Ideal.span {↑p})) x ≠ 0
r : O
hr : r * ↑p = (Quotient.mk'' x).out - x
⊢ ¬r * ↑p ∣ x

Tactic:
exact fun hprx =>
  hx (Ideal.Quotient.eq_zero_iff_mem.2 <| Ideal.mem_span_singleton.2 <| dvd_of_mul_left_dvd hprx)

Result:
no goals

Proof state:
case intro
K : Type u₁
inst✝² : Field K
v : Valuation K ℝ≥0
O : Type u₂
inst✝¹ : CommRing O
inst✝ : Algebra O K
hv : v.Integers O
p : ℕ
x : O
hx : (Ideal.Quotient.mk (Ideal.span {↑p})) x ≠ 0
r : O
hr : r * ↑p = (Quotient.mk'' x).out - x
⊢ preVal K v O p ((Ideal.Quotient.mk (Ideal.span {↑p})) x) = v ((algebraMap O K) x)

Tactic:
refine (if_neg hx).trans (v.map_eq_of_sub_lt <| lt_of_not_le ?_)

Result:
case intro
K : Type u₁
inst✝² : Field K
v : Valuation K ℝ≥0
O : Type u₂
inst✝¹ : CommRing O
inst✝ : Algebra O K
hv : v.Integers O
p : ℕ
x : O
hx : (Ideal.Quotient.mk (Ideal.span {↑p})) x ≠ 0
r : O
hr : r * ↑p = (Quotient.mk'' x).out - x
⊢ ¬v ((algebraMap O K) x) ≤
      v ((algebraMap O K) (Quotient.out ((Ideal.Quotient.mk (Ideal.span {↑p})) x)) - (algebraMap O K) x)

Proof state:
K : Type u₁
inst✝² : Field K
v : Valuation K ℝ≥0
O : Type u₂
inst✝¹ : CommRing O
inst✝ : Algebra O K
hv : v.Integers O
p : ℕ
x : O
hx : (Ideal.Quotient.mk (Ideal.span {↑p})) x ≠ 0
⊢ preVal K v O p ((Ideal.Quotient.mk (Ideal.span {↑p})) x) = v ((algebraMap O K) x)

Tactic:
obtain ⟨r, hr⟩ : ∃ (a : O), a * (p : O) = (Quotient.mk'' x).out - x :=
  Ideal.mem_span_singleton'.1 <| Ideal.Quotient.eq.1 <| Quotient.sound' <| Quotient.mk_out' _

Result:
case intro
K : Type u₁
inst✝² : Field K
v : Valuation K ℝ≥0
O : Type u₂
inst✝¹ : CommRing O
inst✝ : Algebra O K
hv : v.Integers O
p : ℕ
x : O
hx : (Ideal.Quotient.mk (Ideal.span {↑p})) x ≠ 0
r : O
hr : r * ↑p = (Quotient.mk'' x).out - x
⊢ preVal K v O p ((Ideal.Quotient.mk (Ideal.span {↑p})) x) = v ((algebraMap O K) x)

Proof state:
case intro
K : Type u₁
inst✝² : Field K
v : Valuation K ℝ≥0
O : Type u₂
inst✝¹ : CommRing O
inst✝ : Algebra O K
hv : v.Integers O
p : ℕ
x : O
hx : (Ideal.Quotient.mk (Ideal.span {↑p})) x ≠ 0
r : O
hr : r * ↑p = (Quotient.mk'' x).out - x
⊢ ¬v ((algebraMap O K) x) ≤
      v ((algebraMap O K) (Quotient.out ((Ideal.Quotient.mk (Ideal.span {↑p})) x)) - (algebraMap O K) x)

Tactic:
erw [← RingHom.map_sub, ← hr, hv.le_iff_dvd]

Result:
case intro
K : Type u₁
inst✝² : Field K
v : Valuation K ℝ≥0
O : Type u₂
inst✝¹ : CommRing O
inst✝ : Algebra O K
hv : v.Integers O
p : ℕ
x : O
hx : (Ideal.Quotient.mk (Ideal.span {↑p})) x ≠ 0
r : O
hr : r * ↑p = (Quotient.mk'' x).out - x
⊢ ¬r * ↑p ∣ x
-- Mathlib/Algebra/Order/ToIntervalMod.lean
theorem iUnion_Ico_add_zsmul : ⋃ n : ℤ, Ico (a + n • p) (a + (n + 1) • p) = univ

Proof state:
case intro
α : Type u_1
inst✝¹ : LinearOrderedAddCommGroup α
inst✝ : Archimedean α
p : α
hp : 0 < p
a b : α
hl : a ≤ b - toIcoDiv hp a b • p
hr : b - toIcoDiv hp a b • p < a + p
⊢ b < a + toIcoDiv hp a b • p + p

Tactic:
convert sub_lt_iff_lt_add.mp hr using 1

Result:
case h.e'_4
α : Type u_1
inst✝¹ : LinearOrderedAddCommGroup α
inst✝ : Archimedean α
p : α
hp : 0 < p
a b : α
hl : a ≤ b - toIcoDiv hp a b • p
hr : b - toIcoDiv hp a b • p < a + p
⊢ a + toIcoDiv hp a b • p + p = a + p + toIcoDiv hp a b • p

Proof state:
α : Type u_1
inst✝¹ : LinearOrderedAddCommGroup α
inst✝ : Archimedean α
p : α
hp : 0 < p
a b : α
⊢ ∃ i, b ∈ Ico (a + i • p) (a + (i + 1) • p)

Tactic:
rcases sub_toIcoDiv_zsmul_mem_Ico hp a b with ⟨hl, hr⟩

Result:
case intro
α : Type u_1
inst✝¹ : LinearOrderedAddCommGroup α
inst✝ : Archimedean α
p : α
hp : 0 < p
a b : α
hl : a ≤ b - toIcoDiv hp a b • p
hr : b - toIcoDiv hp a b • p < a + p
⊢ ∃ i, b ∈ Ico (a + i • p) (a + (i + 1) • p)

Proof state:
α : Type u_1
inst✝¹ : LinearOrderedAddCommGroup α
inst✝ : Archimedean α
p : α
hp : 0 < p
a : α
⊢ ⋃ n, Ico (a + n • p) (a + (n + 1) • p) = univ

Tactic:
refine eq_univ_iff_forall.mpr fun b => mem_iUnion.mpr ?_

Result:
α : Type u_1
inst✝¹ : LinearOrderedAddCommGroup α
inst✝ : Archimedean α
p : α
hp : 0 < p
a b : α
⊢ ∃ i, b ∈ Ico (a + i • p) (a + (i + 1) • p)

Proof state:
case h.e'_4
α : Type u_1
inst✝¹ : LinearOrderedAddCommGroup α
inst✝ : Archimedean α
p : α
hp : 0 < p
a b : α
hl : a ≤ b - toIcoDiv hp a b • p
hr : b - toIcoDiv hp a b • p < a + p
⊢ a + toIcoDiv hp a b • p + p = a + p + toIcoDiv hp a b • p

Tactic:
abel

Result:
no goals

Proof state:
case intro
α : Type u_1
inst✝¹ : LinearOrderedAddCommGroup α
inst✝ : Archimedean α
p : α
hp : 0 < p
a b : α
hl : a ≤ b - toIcoDiv hp a b • p
hr : b - toIcoDiv hp a b • p < a + p
⊢ b < a + (toIcoDiv hp a b + 1) • p

Tactic:
rw [add_smul, one_smul, ← add_assoc]

Result:
case intro
α : Type u_1
inst✝¹ : LinearOrderedAddCommGroup α
inst✝ : Archimedean α
p : α
hp : 0 < p
a b : α
hl : a ≤ b - toIcoDiv hp a b • p
hr : b - toIcoDiv hp a b • p < a + p
⊢ b < a + toIcoDiv hp a b • p + p

Proof state:
case intro
α : Type u_1
inst✝¹ : LinearOrderedAddCommGroup α
inst✝ : Archimedean α
p : α
hp : 0 < p
a b : α
hl : a ≤ b - toIcoDiv hp a b • p
hr : b - toIcoDiv hp a b • p < a + p
⊢ ∃ i, b ∈ Ico (a + i • p) (a + (i + 1) • p)

Tactic:
refine ⟨toIcoDiv hp a b, ⟨le_sub_iff_add_le.mp hl, ?_⟩⟩

Result:
case intro
α : Type u_1
inst✝¹ : LinearOrderedAddCommGroup α
inst✝ : Archimedean α
p : α
hp : 0 < p
a b : α
hl : a ≤ b - toIcoDiv hp a b • p
hr : b - toIcoDiv hp a b • p < a + p
⊢ b < a + (toIcoDiv hp a b + 1) • p
-- Mathlib/Data/Seq/Computation.lean
theorem orElse_pure (c₁ : Computation α) (a : α) : (think c₁ <|> pure a) = pure a :=
  destruct_eq_pure <| by
    unfold_projs
    simp [orElse]

Proof state:
α : Type u
c₁ : Computation α
a : α
⊢ (c₁.think <|> pure a).destruct = Sum.inl a

Tactic:
unfold_projs

Result:
α : Type u
c₁ : Computation α
a : α
⊢ (c₁.think.orElse fun x => pure a).destruct = Sum.inl a

Proof state:
α : Type u
c₁ : Computation α
a : α
⊢ (c₁.think.orElse fun x => pure a).destruct = Sum.inl a

Tactic:
simp [orElse]

Result:
no goals
-- Mathlib/CategoryTheory/Limits/Types.lean
lemma Quot.desc_quotQuotUliftEquiv {F : J ⥤ Type u} (c : Cocone F) :
    Quot.desc (uliftFunctor.{u'}.mapCocone c) ∘ quotQuotUliftEquiv F = ULift.up ∘ Quot.desc c

Proof state:
case h.intro.intro
J : Type v
inst✝ : Category.{w, v} J
F : J ⥤ Type u
c : Cocone F
w✝¹ : J
w✝ : F.obj w✝¹
⊢ (desc (uliftFunctor.{u', u}.mapCocone c) ∘ ⇑(quotQuotUliftEquiv F)) (ι F w✝¹ w✝) = (ULift.up ∘ desc c) (ι F w✝¹ w✝)

Tactic:
dsimp

Result:
no goals

Proof state:
J : Type v
inst✝ : Category.{w, v} J
F : J ⥤ Type u
c : Cocone F
⊢ desc (uliftFunctor.{u', u}.mapCocone c) ∘ ⇑(quotQuotUliftEquiv F) = ULift.up ∘ desc c

Tactic:
ext x

Result:
case h
J : Type v
inst✝ : Category.{w, v} J
F : J ⥤ Type u
c : Cocone F
x : Quot F
⊢ (desc (uliftFunctor.{u', u}.mapCocone c) ∘ ⇑(quotQuotUliftEquiv F)) x = (ULift.up ∘ desc c) x

Proof state:
case h
J : Type v
inst✝ : Category.{w, v} J
F : J ⥤ Type u
c : Cocone F
x : Quot F
⊢ (desc (uliftFunctor.{u', u}.mapCocone c) ∘ ⇑(quotQuotUliftEquiv F)) x = (ULift.up ∘ desc c) x

Tactic:
obtain ⟨_, _, rfl⟩ := Quot.jointly_surjective x

Result:
case h.intro.intro
J : Type v
inst✝ : Category.{w, v} J
F : J ⥤ Type u
c : Cocone F
w✝¹ : J
w✝ : F.obj w✝¹
⊢ (desc (uliftFunctor.{u', u}.mapCocone c) ∘ ⇑(quotQuotUliftEquiv F)) (ι F w✝¹ w✝) = (ULift.up ∘ desc c) (ι F w✝¹ w✝)
-- Mathlib/CategoryTheory/Limits/Shapes/Multiequalizer.lean
theorem fstPiMap_π (b) : I.fstPiMap ≫ Pi.π I.right b = Pi.π I.left _ ≫ I.fst b

Proof state:
C : Type u
inst✝² : Category.{v, u} C
J : MulticospanShape
I : MulticospanIndex J C
inst✝¹ : HasProduct I.left
inst✝ : HasProduct I.right
b : J.R
⊢ I.fstPiMap ≫ Pi.π I.right b = Pi.π I.left (J.fst b) ≫ I.fst b

Tactic:
simp [fstPiMap]

Result:
no goals
-- Mathlib/Combinatorics/Enumerative/Composition.lean
theorem blocks_sum : c.blocks.sum = n

Proof state:
n : ℕ
c : CompositionAsSet n
⊢ c.blocks.sum = n

Tactic:
have : c.blocks.take c.length = c.blocks := take_of_length_le (by simp [blocks])

Result:
n : ℕ
c : CompositionAsSet n
this : take c.length c.blocks = c.blocks
⊢ c.blocks.sum = n

Proof state:
n : ℕ
c : CompositionAsSet n
⊢ c.blocks.length ≤ c.length

Tactic:
simp [blocks]

Result:
no goals

Proof state:
n : ℕ
c : CompositionAsSet n
this : take c.length c.blocks = c.blocks
⊢ c.blocks.sum = n

Tactic:
rw [← this, c.blocks_partial_sum c.length_lt_card_boundaries, c.boundary_length]

Result:
n : ℕ
c : CompositionAsSet n
this : take c.length c.blocks = c.blocks
⊢ ↑(Fin.last n) = n

Proof state:
n : ℕ
c : CompositionAsSet n
this : take c.length c.blocks = c.blocks
⊢ ↑(Fin.last n) = n

Tactic:
rfl

Result:
no goals
-- Mathlib/Data/Set/Lattice.lean
theorem sInter_eq_iInter {s : Set (Set α)} : ⋂₀ s = ⋂ i : s, i

Proof state:
α : Type u_1
s : Set (Set α)
⊢ ⋂₀ s = ⋂ i, ↑i

Tactic:
simp only [← sInter_range, Subtype.range_coe]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/List/Associative.lean
theorem getValue!_eraseKey_self {β : Type v} [BEq α] [PartialEquivBEq α] [Inhabited β]
    {l : List ((_ : α) × β)} {k : α} (hl : DistinctKeys l) :
    getValue! k (eraseKey k l) = default

Proof state:
α : Type u
β : Type v
inst✝² : BEq α
inst✝¹ : PartialEquivBEq α
inst✝ : Inhabited β
l : List ((_ : α) × β)
k : α
hl : DistinctKeys l
⊢ getValue! k (eraseKey k l) = default

Tactic:
simp [getValue!_eq_getValue?, getValue?_eraseKey_self hl]

Result:
no goals