harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Topology/Instances/Matrix.lean
theorem Matrix.diagonal_tsum [DecidableEq n] [T2Space R] {f : X → n → R} :
    diagonal (∑' x, f x) = ∑' x, diagonal (f x)

Proof state:
case neg
X : Type u_1
n : Type u_5
R : Type u_8
inst✝³ : AddCommMonoid R
inst✝² : TopologicalSpace R
inst✝¹ : DecidableEq n
inst✝ : T2Space R
f : X → n → R
hf : ¬Summable f
⊢ diagonal (∑' (x : X), f x) = ∑' (x : X), diagonal (f x)

Tactic:
have hft := summable_matrix_diagonal.not.mpr hf

Result:
case neg
X : Type u_1
n : Type u_5
R : Type u_8
inst✝³ : AddCommMonoid R
inst✝² : TopologicalSpace R
inst✝¹ : DecidableEq n
inst✝ : T2Space R
f : X → n → R
hf : ¬Summable f
hft : ¬Summable fun x => diagonal (f x)
⊢ diagonal (∑' (x : X), f x) = ∑' (x : X), diagonal (f x)

Proof state:
X : Type u_1
n : Type u_5
R : Type u_8
inst✝³ : AddCommMonoid R
inst✝² : TopologicalSpace R
inst✝¹ : DecidableEq n
inst✝ : T2Space R
f : X → n → R
⊢ diagonal (∑' (x : X), f x) = ∑' (x : X), diagonal (f x)

Tactic:
by_cases hf : Summable f

Result:
case pos
X : Type u_1
n : Type u_5
R : Type u_8
inst✝³ : AddCommMonoid R
inst✝² : TopologicalSpace R
inst✝¹ : DecidableEq n
inst✝ : T2Space R
f : X → n → R
hf : Summable f
⊢ diagonal (∑' (x : X), f x) = ∑' (x : X), diagonal (f x)

case neg
X : Type u_1
n : Type u_5
R : Type u_8
inst✝³ : AddCommMonoid R
inst✝² : TopologicalSpace R
inst✝¹ : DecidableEq n
inst✝ : T2Space R
f : X → n → R
hf : ¬Summable f
⊢ diagonal (∑' (x : X), f x) = ∑' (x : X), diagonal (f x)

Proof state:
case neg
X : Type u_1
n : Type u_5
R : Type u_8
inst✝³ : AddCommMonoid R
inst✝² : TopologicalSpace R
inst✝¹ : DecidableEq n
inst✝ : T2Space R
f : X → n → R
hf : ¬Summable f
hft : ¬Summable fun x => diagonal (f x)
⊢ diagonal 0 = 0

Tactic:
exact diagonal_zero

Result:
no goals

Proof state:
case pos
X : Type u_1
n : Type u_5
R : Type u_8
inst✝³ : AddCommMonoid R
inst✝² : TopologicalSpace R
inst✝¹ : DecidableEq n
inst✝ : T2Space R
f : X → n → R
hf : Summable f
⊢ diagonal (∑' (x : X), f x) = ∑' (x : X), diagonal (f x)

Tactic:
exact hf.hasSum.matrix_diagonal.tsum_eq.symm

Result:
no goals

Proof state:
case neg
X : Type u_1
n : Type u_5
R : Type u_8
inst✝³ : AddCommMonoid R
inst✝² : TopologicalSpace R
inst✝¹ : DecidableEq n
inst✝ : T2Space R
f : X → n → R
hf : ¬Summable f
hft : ¬Summable fun x => diagonal (f x)
⊢ diagonal (∑' (x : X), f x) = ∑' (x : X), diagonal (f x)

Tactic:
rw [tsum_eq_zero_of_not_summable hf, tsum_eq_zero_of_not_summable hft]

Result:
case neg
X : Type u_1
n : Type u_5
R : Type u_8
inst✝³ : AddCommMonoid R
inst✝² : TopologicalSpace R
inst✝¹ : DecidableEq n
inst✝ : T2Space R
f : X → n → R
hf : ¬Summable f
hft : ¬Summable fun x => diagonal (f x)
⊢ diagonal 0 = 0
-- Mathlib/Data/Finset/Update.lean
theorem _root_.DependsOn.update {α : Type*} {f : (Π i, π i) → α} {s : Finset ι} (hf : DependsOn f s)
    (i : ι) (y : π i) : DependsOn (fun x ↦ f (Function.update x i y)) (s.erase i)

Proof state:
ι : Type u_2
π : ι → Type u_3
inst✝ : DecidableEq ι
α : Type u_1
f : ((i : ι) → π i) → α
s : Finset ι
hf : DependsOn f ↑s
i : ι
y : π i
⊢ DependsOn (fun x => f (Function.update x i y)) ↑(s.erase i)

Tactic:
simp_rw [Function.update_eq_updateFinset, erase_eq, coe_sdiff]

Result:
ι : Type u_2
π : ι → Type u_3
inst✝ : DecidableEq ι
α : Type u_1
f : ((i : ι) → π i) → α
s : Finset ι
hf : DependsOn f ↑s
i : ι
y : π i
⊢ DependsOn (fun x => f (updateFinset x {i} (uniqueElim y))) (↑s \ ↑{i})

Proof state:
ι : Type u_2
π : ι → Type u_3
inst✝ : DecidableEq ι
α : Type u_1
f : ((i : ι) → π i) → α
s : Finset ι
hf : DependsOn f ↑s
i : ι
y : π i
⊢ DependsOn (fun x => f (updateFinset x {i} (uniqueElim y))) (↑s \ ↑{i})

Tactic:
exact hf.updateFinset _

Result:
no goals
-- Mathlib/NumberTheory/Padics/RingHoms.lean
theorem nthHomSeq_add (r s : R) :
    nthHomSeq f_compat (r + s) ≈ nthHomSeq f_compat r + nthHomSeq f_compat s

Proof state:
case h
R : Type u_1
inst✝ : NonAssocSemiring R
p : ℕ
f : (k : ℕ) → R →+* ZMod (p ^ k)
hp_prime : Fact (Nat.Prime p)
f_compat : ∀ (k1 k2 : ℕ) (hk : k1 ≤ k2), (ZMod.castHom ⋯ (ZMod (p ^ k1))).comp (f k2) = f k1
r s : R
ε : ℚ
hε : ε > 0
n : ℕ
hn : ↑p ^ (-↑n) < ε
j : ℕ
hj : j ≥ n
⊢ padicNorm p (↑(nthHom f (r + s) j) - (↑(nthHom f r j) + ↑(nthHom f s j))) < ε

Tactic:
apply lt_of_le_of_lt _ hn

Result:
R : Type u_1
inst✝ : NonAssocSemiring R
p : ℕ
f : (k : ℕ) → R →+* ZMod (p ^ k)
hp_prime : Fact (Nat.Prime p)
f_compat : ∀ (k1 k2 : ℕ) (hk : k1 ≤ k2), (ZMod.castHom ⋯ (ZMod (p ^ k1))).comp (f k2) = f k1
r s : R
ε : ℚ
hε : ε > 0
n : ℕ
hn : ↑p ^ (-↑n) < ε
j : ℕ
hj : j ≥ n
⊢ padicNorm p (↑(nthHom f (r + s) j) - (↑(nthHom f r j) + ↑(nthHom f s j))) ≤ ↑p ^ (-↑n)
-- Mathlib/NumberTheory/PythagoreanTriples.lean
theorem classification :
    PythagoreanTriple x y z ↔
      ∃ k m n,
        (x = k * (m ^ 2 - n ^ 2) ∧ y = k * (2 * m * n) ∨
            x = k * (2 * m * n) ∧ y = k * (m ^ 2 - n ^ 2)) ∧
          (z = k * (m ^ 2 + n ^ 2) ∨ z = -k * (m ^ 2 + n ^ 2))

Proof state:
case mp
x y z : ℤ
h : PythagoreanTriple x y z
⊢ ∃ k m n,
    (x = k * (m ^ 2 - n ^ 2) ∧ y = k * (2 * m * n) ∨ x = k * (2 * m * n) ∧ y = k * (m ^ 2 - n ^ 2)) ∧
      (z = k * (m ^ 2 + n ^ 2) ∨ z = -k * (m ^ 2 + n ^ 2))

Tactic:
obtain ⟨k, m, n, H⟩ := h.classified

Result:
case mp.intro.intro.intro
x y z : ℤ
h : PythagoreanTriple x y z
k m n : ℤ
H : (x = k * (m ^ 2 - n ^ 2) ∧ y = k * (2 * m * n) ∨ x = k * (2 * m * n) ∧ y = k * (m ^ 2 - n ^ 2)) ∧ m.gcd n = 1
⊢ ∃ k m n,
    (x = k * (m ^ 2 - n ^ 2) ∧ y = k * (2 * m * n) ∨ x = k * (2 * m * n) ∧ y = k * (m ^ 2 - n ^ 2)) ∧
      (z = k * (m ^ 2 + n ^ 2) ∨ z = -k * (m ^ 2 + n ^ 2))

Proof state:
z k m n : ℤ
right✝ : m.gcd n = 1
h : PythagoreanTriple (k * (m ^ 2 - n ^ 2)) (k * (2 * m * n)) z
⊢ k * (m ^ 2 - n ^ 2) * (k * (m ^ 2 - n ^ 2)) + k * (2 * m * n) * (k * (2 * m * n)) = (k * (m ^ 2 + n ^ 2)) ^ 2

Tactic:
ring

Result:
no goals
-- Mathlib/Dynamics/Circle/RotationNumber/TranslationNumber.lean
theorem le_iterate_of_add_int_le_map {x : ℝ} {m : ℤ} (h : x + m ≤ f x) (n : ℕ) :
    x + n * m ≤ f^[n] x

Proof state:
f : CircleDeg1Lift
x : ℝ
m : ℤ
h : x + ↑m ≤ f x
n : ℕ
⊢ x + ↑n * ↑m ≤ (⇑f)^[n] x

Tactic:
simpa only [nsmul_eq_mul, add_right_iterate] using
  (f.commute_add_int m).symm.iterate_le_of_map_le (monotone_id.add_const (m : ℝ)) f.monotone h n

Result:
no goals
-- Mathlib/Data/Seq/WSeq.lean
theorem flatten_think (c : Computation (WSeq α)) : flatten c.think = think (flatten c) :=
  Seq.destruct_eq_cons <| by simp [flatten, think]

Proof state:
α : Type u
c : Computation (WSeq α)
⊢ Seq.destruct (flatten c.think) = some (none, flatten c)

Tactic:
simp [flatten, think]

Result:
no goals
-- Mathlib/Analysis/Matrix.lean
theorem norm_le_iff {r : ℝ} (hr : 0 ≤ r) {A : Matrix m n α} : ‖A‖ ≤ r ↔ ∀ i j, ‖A i j‖ ≤ r

Proof state:
m : Type u_3
n : Type u_4
α : Type u_5
inst✝² : Fintype m
inst✝¹ : Fintype n
inst✝ : SeminormedAddCommGroup α
r : ℝ
hr : 0 ≤ r
A : Matrix m n α
⊢ ‖A‖ ≤ r ↔ ∀ (i : m) (j : n), ‖A i j‖ ≤ r

Tactic:
simp_rw [norm_def, pi_norm_le_iff_of_nonneg hr]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Tactic/BVDecide/Bitblast/BVExpr/Basic.lean
theorem eval_eq : eval .eq = ((· == ·) : BitVec w → BitVec w → Bool)

Proof state:
w : Nat
⊢ eq.eval = fun x1 x2 => x1 == x2

Tactic:
rfl

Result:
no goals
-- Mathlib/Algebra/Polynomial/Reverse.lean
theorem reverse_mul {f g : R[X]} (fg : f.leadingCoeff * g.leadingCoeff ≠ 0) :
    reverse (f * g) = reverse f * reverse g

Proof state:
R : Type u_1
inst✝ : Semiring R
f g : R[X]
fg : f.leadingCoeff * g.leadingCoeff ≠ 0
⊢ reflect (f * g).natDegree (f * g) = reflect f.natDegree f * reflect g.natDegree g

Tactic:
rw [natDegree_mul' fg, reflect_mul f g rfl.le rfl.le]

Result:
no goals

Proof state:
R : Type u_1
inst✝ : Semiring R
f g : R[X]
fg : f.leadingCoeff * g.leadingCoeff ≠ 0
⊢ (f * g).reverse = f.reverse * g.reverse

Tactic:
unfold reverse

Result:
R : Type u_1
inst✝ : Semiring R
f g : R[X]
fg : f.leadingCoeff * g.leadingCoeff ≠ 0
⊢ reflect (f * g).natDegree (f * g) = reflect f.natDegree f * reflect g.natDegree g
-- Mathlib/Data/Finset/Lattice/Basic.lean
@[simp] lemma left_eq_union : s = s ∪ t ↔ t ⊆ s

Proof state:
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
⊢ s = s ∪ t ↔ t ⊆ s

Tactic:
rw [eq_comm, union_eq_left]

Result:
no goals
-- Mathlib/RingTheory/Ideal/Colon.lean
theorem colon_top {I : Ideal R} [I.IsTwoSided] : I.colon ⊤ = I

Proof state:
R : Type u_1
inst✝¹ : Semiring R
I : Ideal R
inst✝ : I.IsTwoSided
⊢ colon I ⊤ = I

Tactic:
simp_rw [SetLike.ext_iff, mem_colon, smul_eq_mul]

Result:
R : Type u_1
inst✝¹ : Semiring R
I : Ideal R
inst✝ : I.IsTwoSided
⊢ ∀ (x : R), (∀ p ∈ ⊤, x * p ∈ I) ↔ x ∈ I

Proof state:
R : Type u_1
inst✝¹ : Semiring R
I : Ideal R
inst✝ : I.IsTwoSided
⊢ ∀ (x : R), (∀ p ∈ ⊤, x * p ∈ I) ↔ x ∈ I

Tactic:
exact fun x ↦ ⟨fun h ↦ mul_one x ▸ h 1 trivial, fun h _ _ ↦ I.mul_mem_right _ h⟩

Result:
no goals
-- Mathlib/Data/ENNReal/Order.lean
theorem sub_add_eq_add_sub (hab : b ≤ a) (b_ne_top : b ≠ ∞) :
    a - b + c = a + c - b

Proof state:
a b c : ℝ≥0∞
hab : b ≤ a
b_ne_top : b ≠ ⊤
⊢ a - b + c = a + c - b

Tactic:
by_cases c_top : c = ∞

Result:
case pos
a b c : ℝ≥0∞
hab : b ≤ a
b_ne_top : b ≠ ⊤
c_top : c = ⊤
⊢ a - b + c = a + c - b

case neg
a b c : ℝ≥0∞
hab : b ≤ a
b_ne_top : b ≠ ⊤
c_top : ¬c = ⊤
⊢ a - b + c = a + c - b

Proof state:
case neg
a b c : ℝ≥0∞
hab : b ≤ a
b_ne_top : b ≠ ⊤
c_top : ¬c = ⊤
⊢ a - b + c = a + c - b

Tactic:
refine ENNReal.eq_sub_of_add_eq b_ne_top ?_

Result:
case neg
a b c : ℝ≥0∞
hab : b ≤ a
b_ne_top : b ≠ ⊤
c_top : ¬c = ⊤
⊢ a - b + c + b = a + c

Proof state:
case pos
a b c : ℝ≥0∞
hab : b ≤ a
b_ne_top : b ≠ ⊤
c_top : c = ⊤
⊢ a - b + c = a + c - b

Tactic:
simpa [c_top] using ENNReal.eq_sub_of_add_eq b_ne_top rfl

Result:
no goals

Proof state:
case neg
a b c : ℝ≥0∞
hab : b ≤ a
b_ne_top : b ≠ ⊤
c_top : ¬c = ⊤
⊢ a - b + c + b = a + c

Tactic:
simp only [add_assoc, add_comm c b]

Result:
case neg
a b c : ℝ≥0∞
hab : b ≤ a
b_ne_top : b ≠ ⊤
c_top : ¬c = ⊤
⊢ a - b + (b + c) = a + c

Proof state:
case neg
a b c : ℝ≥0∞
hab : b ≤ a
b_ne_top : b ≠ ⊤
c_top : ¬c = ⊤
⊢ a - b + (b + c) = a + c

Tactic:
simpa only [← add_assoc] using (add_left_inj c_top).mpr <| tsub_add_cancel_of_le hab

Result:
no goals
-- Mathlib/Analysis/InnerProductSpace/Orthogonal.lean
theorem mem_orthogonal_singleton_iff_inner_right {u v : E} : v ∈ (𝕜 ∙ u)ᗮ ↔ ⟪u, v⟫ = 0

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
u v : E
hv : inner u v = 0
w : E
hw : ∃ a, a • u = w
⊢ inner w v = 0

Tactic:
obtain ⟨c, rfl⟩ := hw

Result:
case intro
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
u v : E
hv : inner u v = 0
c : 𝕜
⊢ inner (c • u) v = 0

Proof state:
case intro
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
u v : E
hv : inner u v = 0
c : 𝕜
⊢ inner (c • u) v = 0

Tactic:
simp [inner_smul_left, hv]

Result:
no goals

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
u v : E
⊢ v ∈ (span 𝕜 {u})ᗮ ↔ inner u v = 0

Tactic:
refine ⟨inner_right_of_mem_orthogonal (mem_span_singleton_self u), ?_⟩

Result:
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
u v : E
⊢ inner u v = 0 → v ∈ (span 𝕜 {u})ᗮ

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
u v : E
hv : inner u v = 0
w : E
hw : w ∈ span 𝕜 {u}
⊢ inner w v = 0

Tactic:
rw [mem_span_singleton] at hw

Result:
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
u v : E
hv : inner u v = 0
w : E
hw : ∃ a, a • u = w
⊢ inner w v = 0

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
u v : E
⊢ inner u v = 0 → v ∈ (span 𝕜 {u})ᗮ

Tactic:
intro hv w hw

Result:
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
u v : E
hv : inner u v = 0
w : E
hw : w ∈ span 𝕜 {u}
⊢ inner w v = 0
-- Mathlib/Data/Real/EReal.lean
protected lemma neg_mul (x y : EReal) : -x * y = -(x * y)

Proof state:
case pos_bot
x✝ : ℝ
h : 0 < x✝
⊢ -↑x✝ * ⊥ = -(↑x✝ * ⊥)

Tactic:
rw [coe_mul_bot_of_pos h, neg_bot, ← coe_neg,
coe_mul_bot_of_neg (neg_neg_of_pos h)]

Result:
no goals

Proof state:
case zero_bot

⊢ -0 * ⊥ = -(0 * ⊥)

Tactic:
simp only [zero_mul, mul_zero, neg_zero]

Result:
no goals

Proof state:
case pos_top
x✝ : ℝ
h : 0 < x✝
⊢ -↑x✝ * ⊤ = -(↑x✝ * ⊤)

Tactic:
rw [coe_mul_top_of_pos h, neg_top, ← coe_neg,
coe_mul_top_of_neg (neg_neg_of_pos h)]

Result:
no goals

Proof state:
case top_pos
x✝ : ℝ
h : 0 < x✝
⊢ -⊤ * ↑x✝ = -(⊤ * ↑x✝)

Tactic:
rw [top_mul_coe_of_pos h, neg_top, bot_mul_coe_of_pos h]

Result:
no goals

Proof state:
x y : EReal
⊢ -x * y = -(x * y)

Tactic:
induction x, y using induction₂_neg_left with
| top_zero | zero_top | zero_bot => simp only [zero_mul, mul_zero, neg_zero]
| top_top | top_bot => rfl
| neg_left h => rw [h, neg_neg, neg_neg]
| coe_coe => norm_cast; exact neg_mul _ _
| top_pos _ h => rw [top_mul_coe_of_pos h, neg_top, bot_mul_coe_of_pos h]
| pos_top _ h => rw [coe_mul_top_of_pos h, neg_top, ← coe_neg,
  coe_mul_top_of_neg (neg_neg_of_pos h)]
| top_neg _ h => rw [top_mul_coe_of_neg h, neg_top, bot_mul_coe_of_neg h, neg_bot]
| pos_bot _ h => rw [coe_mul_bot_of_pos h, neg_bot, ← coe_neg,
  coe_mul_bot_of_neg (neg_neg_of_pos h)]

Result:
no goals

Proof state:
case top_bot

⊢ -⊤ * ⊥ = -(⊤ * ⊥)

Tactic:
rfl

Result:
no goals

Proof state:
case coe_coe
x✝ y✝ : ℝ
⊢ -x✝ * y✝ = -(x✝ * y✝)

Tactic:
exact neg_mul _ _

Result:
no goals

Proof state:
case coe_coe
x✝ y✝ : ℝ
⊢ -↑x✝ * ↑y✝ = -(↑x✝ * ↑y✝)

Tactic:
norm_cast

Result:
case coe_coe
x✝ y✝ : ℝ
⊢ -x✝ * y✝ = -(x✝ * y✝)

Proof state:
case neg_left
x✝ y✝ : EReal
h : -x✝ * y✝ = -(x✝ * y✝)
⊢ - -x✝ * y✝ = -(-x✝ * y✝)

Tactic:
rw [h, neg_neg, neg_neg]

Result:
no goals

Proof state:
case top_neg
x✝ : ℝ
h : x✝ < 0
⊢ -⊤ * ↑x✝ = -(⊤ * ↑x✝)

Tactic:
rw [top_mul_coe_of_neg h, neg_top, bot_mul_coe_of_neg h, neg_bot]

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Connectivity/WalkDecomp.lean
theorem takeUntil_copy {u v w v' w'} (p : G.Walk v w) (hv : v = v') (hw : w = w')
    (h : u ∈ (p.copy hv hw).support) :
    (p.copy hv hw).takeUntil u h = (p.takeUntil u (by subst_vars; exact h)).copy hv rfl

Proof state:
V : Type u
G : SimpleGraph V
inst✝ : DecidableEq V
u v w v' w' : V
p : G.Walk v w
hv : v = v'
hw : w = w'
h : u ∈ (p.copy hv hw).support
⊢ (p.copy hv hw).takeUntil u h = (p.takeUntil u ⋯).copy hv ⋯

Tactic:
subst_vars

Result:
V : Type u
G : SimpleGraph V
inst✝ : DecidableEq V
u v' w' : V
p : G.Walk v' w'
h : u ∈ (p.copy ⋯ ⋯).support
⊢ (p.copy ⋯ ⋯).takeUntil u h = (p.takeUntil u ⋯).copy ⋯ ⋯

Proof state:
V : Type u
G : SimpleGraph V
v✝ w✝ u✝ : V
inst✝ : DecidableEq V
u v w v' w' : V
p : G.Walk v w
hv : v = v'
hw : w = w'
h : u ∈ (p.copy hv hw).support
⊢ u ∈ p.support

Tactic:
subst_vars

Result:
V : Type u
G : SimpleGraph V
v w u✝ : V
inst✝ : DecidableEq V
u v' w' : V
p : G.Walk v' w'
h : u ∈ (p.copy ⋯ ⋯).support
⊢ u ∈ p.support

Proof state:
V : Type u
G : SimpleGraph V
inst✝ : DecidableEq V
u v' w' : V
p : G.Walk v' w'
h : u ∈ (p.copy ⋯ ⋯).support
⊢ (p.copy ⋯ ⋯).takeUntil u h = (p.takeUntil u ⋯).copy ⋯ ⋯

Tactic:
rfl

Result:
no goals

Proof state:
V : Type u
G : SimpleGraph V
v w u✝ : V
inst✝ : DecidableEq V
u v' w' : V
p : G.Walk v' w'
h : u ∈ (p.copy ⋯ ⋯).support
⊢ u ∈ p.support

Tactic:
exact h

Result:
no goals
-- Mathlib/NumberTheory/Padics/RingHoms.lean
theorem limNthHom_spec (r : R) :
    ∀ ε : ℝ, 0 < ε → ∃ N : ℕ, ∀ n ≥ N, ‖limNthHom f_compat r - nthHom f r n‖ < ε

Proof state:
R : Type u_1
inst✝ : NonAssocSemiring R
p : ℕ
f : (k : ℕ) → R →+* ZMod (p ^ k)
hp_prime : Fact (Nat.Prime p)
f_compat : ∀ (k1 k2 : ℕ) (hk : k1 ≤ k2), (ZMod.castHom ⋯ (ZMod (p ^ k1))).comp (f k2) = f k1
r : R
⊢ ∀ (ε : ℝ), 0 < ε → ∃ N, ∀ n ≥ N, ‖limNthHom f_compat r - ↑(nthHom f r n)‖ < ε

Tactic:
intro ε hε

Result:
R : Type u_1
inst✝ : NonAssocSemiring R
p : ℕ
f : (k : ℕ) → R →+* ZMod (p ^ k)
hp_prime : Fact (Nat.Prime p)
f_compat : ∀ (k1 k2 : ℕ) (hk : k1 ≤ k2), (ZMod.castHom ⋯ (ZMod (p ^ k1))).comp (f k2) = f k1
r : R
ε : ℝ
hε : 0 < ε
⊢ ∃ N, ∀ n ≥ N, ‖limNthHom f_compat r - ↑(nthHom f r n)‖ < ε
-- Mathlib/Order/CompleteLatticeIntervals.lean
theorem sInf_within_of_ordConnected {s : Set α} [hs : OrdConnected s] ⦃t : Set s⦄ (ht : t.Nonempty)
    (h_bdd : BddBelow t) : sInf ((↑) '' t : Set α) ∈ s

Proof state:
case intro.intro
α : Type u_2
inst✝ : ConditionallyCompleteLinearOrder α
s : Set α
hs : s.OrdConnected
t : Set ↑s
c : ↑s
hct : c ∈ t
B : ↑s
hB : B ∈ lowerBounds t
⊢ sInf (Subtype.val '' t) ∈ s

Tactic:
refine hs.out B.2 c.2 ⟨?_, ?_⟩

Result:
case intro.intro.refine_1
α : Type u_2
inst✝ : ConditionallyCompleteLinearOrder α
s : Set α
hs : s.OrdConnected
t : Set ↑s
c : ↑s
hct : c ∈ t
B : ↑s
hB : B ∈ lowerBounds t
⊢ ↑B ≤ sInf (Subtype.val '' t)

case intro.intro.refine_2
α : Type u_2
inst✝ : ConditionallyCompleteLinearOrder α
s : Set α
hs : s.OrdConnected
t : Set ↑s
c : ↑s
hct : c ∈ t
B : ↑s
hB : B ∈ lowerBounds t
⊢ sInf (Subtype.val '' t) ≤ ↑c

Proof state:
case intro
α : Type u_2
inst✝ : ConditionallyCompleteLinearOrder α
s : Set α
hs : s.OrdConnected
t : Set ↑s
h_bdd : BddBelow t
c : ↑s
hct : c ∈ t
⊢ sInf (Subtype.val '' t) ∈ s

Tactic:
obtain ⟨B, hB⟩ : ∃ B, B ∈ lowerBounds t := h_bdd

Result:
case intro.intro
α : Type u_2
inst✝ : ConditionallyCompleteLinearOrder α
s : Set α
hs : s.OrdConnected
t : Set ↑s
c : ↑s
hct : c ∈ t
B : ↑s
hB : B ∈ lowerBounds t
⊢ sInf (Subtype.val '' t) ∈ s

Proof state:
case intro.intro.refine_1
α : Type u_2
inst✝ : ConditionallyCompleteLinearOrder α
s : Set α
hs : s.OrdConnected
t : Set ↑s
c : ↑s
hct : c ∈ t
B : ↑s
hB : B ∈ lowerBounds t
⊢ ↑B ≤ sInf (Subtype.val '' t)

Tactic:
exact (Subtype.mono_coe s).le_csInf_image ⟨c, hct⟩ hB

Result:
no goals

Proof state:
case intro.intro.refine_2
α : Type u_2
inst✝ : ConditionallyCompleteLinearOrder α
s : Set α
hs : s.OrdConnected
t : Set ↑s
c : ↑s
hct : c ∈ t
B : ↑s
hB : B ∈ lowerBounds t
⊢ sInf (Subtype.val '' t) ≤ ↑c

Tactic:
exact (Subtype.mono_coe s).csInf_image_le hct ⟨B, hB⟩

Result:
no goals

Proof state:
α : Type u_2
inst✝ : ConditionallyCompleteLinearOrder α
s : Set α
hs : s.OrdConnected
t : Set ↑s
ht : t.Nonempty
h_bdd : BddBelow t
⊢ sInf (Subtype.val '' t) ∈ s

Tactic:
obtain ⟨c, hct⟩ : ∃ c, c ∈ t := ht

Result:
case intro
α : Type u_2
inst✝ : ConditionallyCompleteLinearOrder α
s : Set α
hs : s.OrdConnected
t : Set ↑s
h_bdd : BddBelow t
c : ↑s
hct : c ∈ t
⊢ sInf (Subtype.val '' t) ∈ s
-- Mathlib/AlgebraicGeometry/ProjectiveSpectrum/StructureSheaf.lean
theorem mul_mem' (U : (Opens (ProjectiveSpectrum.top 𝒜))ᵒᵖ) (a b : ∀ x : U.unop, at x.1)
    (ha : (isLocallyFraction 𝒜).pred a) (hb : (isLocallyFraction 𝒜).pred b) :
    (isLocallyFraction 𝒜).pred (a * b) := fun x => by
  rcases ha x with ⟨Va, ma, ia, ja, ⟨ra, ra_mem⟩, ⟨sa, sa_mem⟩, hwa, wa⟩
  rcases hb x with ⟨Vb, mb, ib, jb, ⟨rb, rb_mem⟩, ⟨sb, sb_mem⟩, hwb, wb⟩
  refine
    ⟨Va ⊓ Vb, ⟨ma, mb⟩, Opens.infLELeft _ _ ≫ ia, ja + jb,
      ⟨ra * rb, SetLike.mul_mem_graded ra_mem rb_mem⟩,
      ⟨sa * sb, SetLike.mul_mem_graded sa_mem sb_mem⟩, fun y =>
      y.1.asHomogeneousIdeal.toIdeal.primeCompl.mul_mem (hwa ⟨y.1, y.2.1⟩) (hwb ⟨y.1, y.2.2⟩), ?_⟩
  rintro ⟨y, hy⟩
  simp only [Subtype.forall, Opens.apply_mk] at wa wb
  simp [wa y hy.1, wb y hy.2, ext_iff_val, Localization.mk_mul]

Proof state:
case intro.intro.intro.intro.intro.mk.intro.mk.intro.intro.intro.intro.intro.intro.mk.intro.mk.intro.mk
R : Type u_1
A : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
𝒜 : ℕ → Submodule R A
inst✝ : GradedAlgebra 𝒜
U : (Opens ↑(ProjectiveSpectrum.top 𝒜))ᵒᵖ
a b : (x : ↥(unop U)) → at ↑x
ha : (isLocallyFraction 𝒜).pred a
hb : (isLocallyFraction 𝒜).pred b
x : ↥(unop U)
Va : Opens ↑(ProjectiveSpectrum.top 𝒜)
ma : ↑x ∈ Va
ia : Va ⟶ unop U
ja : ℕ
ra : A
ra_mem : ra ∈ 𝒜 ja
sa : A
sa_mem : sa ∈ 𝒜 ja
hwa : ∀ (x : ↥Va), ↑⟨sa, sa_mem⟩ ∉ (↑x).asHomogeneousIdeal
Vb : Opens ↑(ProjectiveSpectrum.top 𝒜)
mb : ↑x ∈ Vb
ib : Vb ⟶ unop U
jb : ℕ
rb : A
rb_mem : rb ∈ 𝒜 jb
sb : A
sb_mem : sb ∈ 𝒜 jb
hwb : ∀ (x : ↥Vb), ↑⟨sb, sb_mem⟩ ∉ (↑x).asHomogeneousIdeal
y : ↑(ProjectiveSpectrum.top 𝒜)
hy : y ∈ Va ⊓ Vb
wa :
  ∀ (a_1 : ↑(ProjectiveSpectrum.top 𝒜)) (b : a_1 ∈ Va),
    a ⟨a_1, ⋯⟩ = HomogeneousLocalization.mk { deg := ja, num := ⟨ra, ra_mem⟩, den := ⟨sa, sa_mem⟩, den_mem := ⋯ }
wb :
  ∀ (a : ↑(ProjectiveSpectrum.top 𝒜)) (b_1 : a ∈ Vb),
    b ⟨a, ⋯⟩ = HomogeneousLocalization.mk { deg := jb, num := ⟨rb, rb_mem⟩, den := ⟨sb, sb_mem⟩, den_mem := ⋯ }
⊢ (fun x => (a * b) ((Va.infLELeft Vb ≫ ia) x)) ⟨y, hy⟩ =
    HomogeneousLocalization.mk { deg := ja + jb, num := ⟨ra * rb, ⋯⟩, den := ⟨sa * sb, ⋯⟩, den_mem := ⋯ }

Tactic:
simp [wa y hy.1, wb y hy.2, ext_iff_val, Localization.mk_mul]

Result:
no goals
-- Mathlib/RingTheory/Polynomial/ScaleRoots.lean
theorem map_scaleRoots (p : R[X]) (x : R) (f : R →+* S) (h : f p.leadingCoeff ≠ 0) :
    (p.scaleRoots x).map f = (p.map f).scaleRoots (f x)

Proof state:
R : Type u_1
S : Type u_2
inst✝¹ : Semiring R
inst✝ : Semiring S
p : R[X]
x : R
f : R →+* S
h : f p.leadingCoeff ≠ 0
⊢ map f (p.scaleRoots x) = (map f p).scaleRoots (f x)

Tactic:
ext

Result:
case a
R : Type u_1
S : Type u_2
inst✝¹ : Semiring R
inst✝ : Semiring S
p : R[X]
x : R
f : R →+* S
h : f p.leadingCoeff ≠ 0
n✝ : ℕ
⊢ (map f (p.scaleRoots x)).coeff n✝ = ((map f p).scaleRoots (f x)).coeff n✝

Proof state:
case a
R : Type u_1
S : Type u_2
inst✝¹ : Semiring R
inst✝ : Semiring S
p : R[X]
x : R
f : R →+* S
h : f p.leadingCoeff ≠ 0
n✝ : ℕ
⊢ (map f (p.scaleRoots x)).coeff n✝ = ((map f p).scaleRoots (f x)).coeff n✝

Tactic:
simp [Polynomial.natDegree_map_of_leadingCoeff_ne_zero _ h]

Result:
no goals
-- Mathlib/.lake/packages/batteries/Batteries/Data/BinaryHeap.lean
theorem size_popMax (self : BinaryHeap α lt) :
    self.popMax.size = self.size - 1

Proof state:
α : Type u_1
lt : α → α → Bool
self : BinaryHeap α lt
⊢ self.popMax.size = self.size - 1

Tactic:
simp only [popMax, size]

Result:
α : Type u_1
lt : α → α → Bool
self : BinaryHeap α lt
⊢ (if h : self.arr.size = 0 then self
        else
          if h_1 : 0 < self.arr.size - 1 then
            { arr := (heapifyDown lt (self.vector.swap 0 (self.arr.size - 1) ⋯ ⋯).pop ⟨0, ⋯⟩).toArray }
          else { arr := (self.vector.swap 0 (self.arr.size - 1) ⋯ ⋯).pop.toArray }).arr.size =
    self.arr.size - 1

Proof state:
case isTrue
α : Type u_1
lt : α → α → Bool
self : BinaryHeap α lt
h✝ : self.arr.size = 0
⊢ self.arr.size = self.arr.size - 1

Tactic:
simp_arith [*]

Result:
no goals

Proof state:
case isFalse
α : Type u_1
lt : α → α → Bool
self : BinaryHeap α lt
h✝ : ¬self.arr.size = 0
⊢ (if h : 0 < self.arr.size - 1 then
          { arr := (heapifyDown lt (self.vector.swap 0 (self.arr.size - 1) ⋯ ⋯).pop ⟨0, ⋯⟩).toArray }
        else { arr := (self.vector.swap 0 (self.arr.size - 1) ⋯ ⋯).pop.toArray }).arr.size =
    self.arr.size - 1

Tactic:
split <;> simp_arith [*]

Result:
no goals

Proof state:
α : Type u_1
lt : α → α → Bool
self : BinaryHeap α lt
⊢ (if h : self.arr.size = 0 then self
        else
          if h_1 : 0 < self.arr.size - 1 then
            { arr := (heapifyDown lt (self.vector.swap 0 (self.arr.size - 1) ⋯ ⋯).pop ⟨0, ⋯⟩).toArray }
          else { arr := (self.vector.swap 0 (self.arr.size - 1) ⋯ ⋯).pop.toArray }).arr.size =
    self.arr.size - 1

Tactic:
split

Result:
case isTrue
α : Type u_1
lt : α → α → Bool
self : BinaryHeap α lt
h✝ : self.arr.size = 0
⊢ self.arr.size = self.arr.size - 1

case isFalse
α : Type u_1
lt : α → α → Bool
self : BinaryHeap α lt
h✝ : ¬self.arr.size = 0
⊢ (if h : 0 < self.arr.size - 1 then
          { arr := (heapifyDown lt (self.vector.swap 0 (self.arr.size - 1) ⋯ ⋯).pop ⟨0, ⋯⟩).toArray }
        else { arr := (self.vector.swap 0 (self.arr.size - 1) ⋯ ⋯).pop.toArray }).arr.size =
    self.arr.size - 1