harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Topology/Algebra/Module/LinearMapPiProd.lean
theorem prod_ext_iff {f g : M × M₂ →L[R] M₃} :
    f = g ↔ f.comp (inl _ _ _) = g.comp (inl _ _ _) ∧ f.comp (inr _ _ _) = g.comp (inr _ _ _)

Proof state:
R : Type u_1
inst✝⁹ : Semiring R
M : Type u_2
inst✝⁸ : TopologicalSpace M
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R M
M₂ : Type u_3
inst✝⁵ : TopologicalSpace M₂
inst✝⁴ : AddCommMonoid M₂
inst✝³ : Module R M₂
M₃ : Type u_4
inst✝² : TopologicalSpace M₃
inst✝¹ : AddCommMonoid M₃
inst✝ : Module R M₃
f g : M × M₂ →L[R] M₃
⊢ f = g ↔ f.comp (inl R M M₂) = g.comp (inl R M M₂) ∧ f.comp (inr R M M₂) = g.comp (inr R M M₂)

Tactic:
simp only [← coe_inj, LinearMap.prod_ext_iff]

Result:
R : Type u_1
inst✝⁹ : Semiring R
M : Type u_2
inst✝⁸ : TopologicalSpace M
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R M
M₂ : Type u_3
inst✝⁵ : TopologicalSpace M₂
inst✝⁴ : AddCommMonoid M₂
inst✝³ : Module R M₂
M₃ : Type u_4
inst✝² : TopologicalSpace M₃
inst✝¹ : AddCommMonoid M₃
inst✝ : Module R M₃
f g : M × M₂ →L[R] M₃
⊢ ↑f ∘ₗ LinearMap.inl R M M₂ = ↑g ∘ₗ LinearMap.inl R M M₂ ∧ ↑f ∘ₗ LinearMap.inr R M M₂ = ↑g ∘ₗ LinearMap.inr R M M₂ ↔
    ↑(f.comp (inl R M M₂)) = ↑(g.comp (inl R M M₂)) ∧ ↑(f.comp (inr R M M₂)) = ↑(g.comp (inr R M M₂))

Proof state:
R : Type u_1
inst✝⁹ : Semiring R
M : Type u_2
inst✝⁸ : TopologicalSpace M
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R M
M₂ : Type u_3
inst✝⁵ : TopologicalSpace M₂
inst✝⁴ : AddCommMonoid M₂
inst✝³ : Module R M₂
M₃ : Type u_4
inst✝² : TopologicalSpace M₃
inst✝¹ : AddCommMonoid M₃
inst✝ : Module R M₃
f g : M × M₂ →L[R] M₃
⊢ ↑f ∘ₗ LinearMap.inl R M M₂ = ↑g ∘ₗ LinearMap.inl R M M₂ ∧ ↑f ∘ₗ LinearMap.inr R M M₂ = ↑g ∘ₗ LinearMap.inr R M M₂ ↔
    ↑(f.comp (inl R M M₂)) = ↑(g.comp (inl R M M₂)) ∧ ↑(f.comp (inr R M M₂)) = ↑(g.comp (inr R M M₂))

Tactic:
rfl

Result:
no goals
-- Mathlib/Algebra/Order/Interval/Set/Monoid.lean
theorem Icc_add_bij : BijOn (· + d) (Icc a b) (Icc (a + d) (b + d))

Proof state:
M : Type u_1
inst✝¹ : OrderedCancelAddCommMonoid M
inst✝ : ExistsAddOfLE M
a b d : M
⊢ BijOn (fun x => x + d) (Ici a ∩ Iic b) (Ici (a + d) ∩ Iic (b + d))

Tactic:
exact
  (Ici_add_bij a d).inter_mapsTo (fun x hx => add_le_add_right hx _) fun x hx =>
    le_of_add_le_add_right hx.2

Result:
no goals

Proof state:
M : Type u_1
inst✝¹ : OrderedCancelAddCommMonoid M
inst✝ : ExistsAddOfLE M
a b d : M
⊢ BijOn (fun x => x + d) (Icc a b) (Icc (a + d) (b + d))

Tactic:
rw [← Ici_inter_Iic, ← Ici_inter_Iic]

Result:
M : Type u_1
inst✝¹ : OrderedCancelAddCommMonoid M
inst✝ : ExistsAddOfLE M
a b d : M
⊢ BijOn (fun x => x + d) (Ici a ∩ Iic b) (Ici (a + d) ∩ Iic (b + d))
-- Mathlib/Algebra/Polynomial/Roots.lean
theorem roots_pow (p : R[X]) (n : ℕ) : (p ^ n).roots = n • p.roots

Proof state:
case succ.inl
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
n : ℕ
ihn : (0 ^ n).roots = n • roots 0
⊢ (0 ^ (n + 1)).roots = (n + 1) • roots 0

Tactic:
rw [zero_pow n.succ_ne_zero, roots_zero, smul_zero]

Result:
no goals

Proof state:
case succ.inr
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R[X]
n : ℕ
ihn : (p ^ n).roots = n • p.roots
hp : p ≠ 0
⊢ (p ^ (n + 1)).roots = (n + 1) • p.roots

Tactic:
rw [pow_succ, roots_mul (mul_ne_zero (pow_ne_zero _ hp) hp), ihn, add_smul, one_smul]

Result:
no goals

Proof state:
case succ
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R[X]
n : ℕ
ihn : (p ^ n).roots = n • p.roots
⊢ (p ^ (n + 1)).roots = (n + 1) • p.roots

Tactic:
rcases eq_or_ne p 0 with (rfl | hp)

Result:
case succ.inl
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
n : ℕ
ihn : (0 ^ n).roots = n • roots 0
⊢ (0 ^ (n + 1)).roots = (n + 1) • roots 0

case succ.inr
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R[X]
n : ℕ
ihn : (p ^ n).roots = n • p.roots
hp : p ≠ 0
⊢ (p ^ (n + 1)).roots = (n + 1) • p.roots

Proof state:
case zero
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R[X]
⊢ (p ^ 0).roots = 0 • p.roots

Tactic:
rw [pow_zero, roots_one, zero_smul, empty_eq_zero]

Result:
no goals
-- Mathlib/Data/Complex/Exponential.lean
lemma norm_exp_sub_sum_le_norm_mul_exp (x : ℂ) (n : ℕ) :
    ‖exp x - ∑ m ∈ range n, x ^ m / m.factorial‖ ≤ ‖x‖ ^ n * Real.exp ‖x‖

Proof state:
x : ℂ
n j : ℕ
hj : j ≥ n
⊢ ↑(cauSeqNorm (exp' x - const norm (∑ m ∈ range n, x ^ m / ↑m.factorial))) j ≤ ↑(const abs (‖x‖ ^ n * Real.exp ‖x‖)) j

Tactic:
show ‖(∑ m ∈ range j, x ^ m / m.factorial) - ∑ m ∈ range n, x ^ m / m.factorial‖ ≤ _

Result:
x : ℂ
n j : ℕ
hj : j ≥ n
⊢ ‖∑ m ∈ range j, x ^ m / ↑m.factorial - ∑ m ∈ range n, x ^ m / ↑m.factorial‖ ≤ ↑(const abs (‖x‖ ^ n * Real.exp ‖x‖)) j

Proof state:
case e_a.refine_3.refine_2
x : ℂ
n j : ℕ
hj : j ≥ n
b : ℕ
hb : b < j ∧ n ≤ b
⊢ b - n + n = b

Tactic:
rw [tsub_add_cancel_of_le hb.2]

Result:
no goals

Proof state:
case e_a.refine_3
x : ℂ
n j : ℕ
hj : j ≥ n
⊢ ∀ b ∈ filter (fun m => n ≤ m) (range j), ∃ a, ∃ (ha : a ∈ range (j - n)), (fun m hm => m + n) a ha = b

Tactic:
intro b hb

Result:
case e_a.refine_3
x : ℂ
n j : ℕ
hj : j ≥ n
b : ℕ
hb : b ∈ filter (fun m => n ≤ m) (range j)
⊢ ∃ a, ∃ (ha : a ∈ range (j - n)), (fun m hm => m + n) a ha = b

Proof state:
case e_a.refine_2
x : ℂ
n j : ℕ
hj : j ≥ n
a : ℕ
ha : a ∈ range (j - n)
b : ℕ
hb : b ∈ range (j - n)
hab : (fun m hm => m + n) a ha = (fun m hm => m + n) b hb
⊢ a = b

Tactic:
simpa using hab

Result:
no goals

Proof state:
x : ℂ
n j : ℕ
hj : j ≥ n
⊢ ‖∑ m ∈ filter (fun m => n ≤ m) (range j), x ^ m / ↑m.factorial‖ =
    ‖∑ m ∈ filter (fun m => n ≤ m) (range j), x ^ n * (x ^ (m - n) / ↑m.factorial)‖

Tactic:
refine congr_arg norm (sum_congr rfl fun m hm => ?_)

Result:
x : ℂ
n j : ℕ
hj : j ≥ n
m : ℕ
hm : m ∈ filter (fun m => n ≤ m) (range j)
⊢ x ^ m / ↑m.factorial = x ^ n * (x ^ (m - n) / ↑m.factorial)

Proof state:
case e_a.refine_1
x : ℂ
n j : ℕ
hj : j ≥ n
a : ℕ
ha : a ∈ range (j - n)
⊢ a + n < j

Tactic:
simp only [mem_range] at ha

Result:
case e_a.refine_1
x : ℂ
n j : ℕ
hj : j ≥ n
a : ℕ
ha : a < j - n
⊢ a + n < j

Proof state:
case e_a.refine_1
x : ℂ
n j : ℕ
hj : j ≥ n
a : ℕ
ha : a < j - n
⊢ a + n < j

Tactic:
rwa [← lt_tsub_iff_right]

Result:
no goals

Proof state:
x : ℂ
n j : ℕ
hj : j ≥ n
m : ℕ
hm : m < j ∧ n ≤ m
⊢ x ^ m / ↑m.factorial = x ^ n * (x ^ (m - n) / ↑m.factorial)

Tactic:
rw [← mul_div_assoc, ← pow_add, add_tsub_cancel_of_le hm.2]

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

Proof state:
case inr
d : ℤ
a b : Solution₁ d
ha : 0 < a.x
hb : 0 < b.x
h : d < 0
⊢ 0 < 1 + d * 0 ^ 2 + d * 0 ^ 2

Tactic:
simp

Result:
no goals

Proof state:
d : ℤ
a b : Solution₁ d
ha : 0 < a.x
hb : 0 < b.x
⊢ 0 < a.x * b.x + d * (a.y * b.y)

Tactic:
refine neg_lt_iff_pos_add'.mp (abs_lt.mp ?_).1

Result:
d : ℤ
a b : Solution₁ d
ha : 0 < a.x
hb : 0 < b.x
⊢ |d * (a.y * b.y)| < a.x * b.x

Proof state:
d : ℤ
a b : Solution₁ d
ha : 0 < a.x
hb : 0 < b.x
⊢ 0 < (1 + d * a.y ^ 2) * (1 + d * b.y ^ 2) - (d * (a.y * b.y)) ^ 2

Tactic:
ring_nf

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

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

Tactic:
rcases le_or_lt 0 d with h | h

Result:
case inl
d : ℤ
a b : Solution₁ d
ha : 0 < a.x
hb : 0 < b.x
h : 0 ≤ d
⊢ 0 < 1 + d * a.y ^ 2 + d * b.y ^ 2

case inr
d : ℤ
a b : Solution₁ d
ha : 0 < a.x
hb : 0 < b.x
h : d < 0
⊢ 0 < 1 + d * a.y ^ 2 + d * b.y ^ 2

Proof state:
d : ℤ
a b : Solution₁ d
ha : 0 < a.x
hb : 0 < b.x
⊢ |d * (a.y * b.y)| < a.x * b.x

Tactic:
rw [← abs_of_pos ha, ← abs_of_pos hb, ← abs_mul, ← sq_lt_sq, mul_pow a.x, a.prop_x, b.prop_x, ←
  sub_pos]

Result:
d : ℤ
a b : Solution₁ d
ha : 0 < a.x
hb : 0 < b.x
⊢ 0 < (1 + d * a.y ^ 2) * (1 + d * b.y ^ 2) - (d * (a.y * b.y)) ^ 2

Proof state:
case inl
d : ℤ
a b : Solution₁ d
ha : 0 < a.x
hb : 0 < b.x
h : 0 ≤ d
⊢ 0 < 1 + d * a.y ^ 2 + d * b.y ^ 2

Tactic:
positivity

Result:
no goals

Proof state:
case inr
d : ℤ
a b : Solution₁ d
ha : 0 < a.x
hb : 0 < b.x
h : d < 0
⊢ 0 < 1 + d * a.y ^ 2 + d * b.y ^ 2

Tactic:
rw [(eq_zero_of_d_neg h a).resolve_left ha.ne', (eq_zero_of_d_neg h b).resolve_left hb.ne']

Result:
case inr
d : ℤ
a b : Solution₁ d
ha : 0 < a.x
hb : 0 < b.x
h : d < 0
⊢ 0 < 1 + d * 0 ^ 2 + d * 0 ^ 2

Proof state:
d : ℤ
a b : Solution₁ d
ha : 0 < a.x
hb : 0 < b.x
⊢ 0 < (a * b).x

Tactic:
simp only [x_mul]

Result:
d : ℤ
a b : Solution₁ d
ha : 0 < a.x
hb : 0 < b.x
⊢ 0 < a.x * b.x + d * (a.y * b.y)
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/ToArray.lean
theorem zipWithAux_toArray_succ' (as : List α) (bs : List β) (f : α → β → γ) (i : Nat) (cs : Array γ) :
    zipWithAux as.toArray bs.toArray f (i + 1) cs = zipWithAux (as.drop (i+1)).toArray (bs.drop (i+1)).toArray f 0 cs

Proof state:
case succ
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
i : Nat
ih :
  ∀ (as : List α) (bs : List β) (cs : Array γ),
    as.toArray.zipWithAux bs.toArray f (i + 1) cs =
      (drop (i + 1) as).toArray.zipWithAux (drop (i + 1) bs).toArray f 0 cs
as : List α
bs : List β
cs : Array γ
⊢ (drop (i + 1) as.tail).toArray.zipWithAux (drop (i + 1) bs.tail).toArray f 0 cs =
    (drop (i + 1 + 1) as).toArray.zipWithAux (drop (i + 1 + 1) bs).toArray f 0 cs

Tactic:
simp

Result:
no goals

Proof state:
case zero
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
as : List α
bs : List β
cs : Array γ
⊢ as.toArray.zipWithAux bs.toArray f (0 + 1) cs = (drop (0 + 1) as).toArray.zipWithAux (drop (0 + 1) bs).toArray f 0 cs

Tactic:
simp [zipWithAux_toArray_succ]

Result:
no goals

Proof state:
case succ
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
i : Nat
ih :
  ∀ (as : List α) (bs : List β) (cs : Array γ),
    as.toArray.zipWithAux bs.toArray f (i + 1) cs =
      (drop (i + 1) as).toArray.zipWithAux (drop (i + 1) bs).toArray f 0 cs
as : List α
bs : List β
cs : Array γ
⊢ as.toArray.zipWithAux bs.toArray f (i + 1 + 1) cs =
    (drop (i + 1 + 1) as).toArray.zipWithAux (drop (i + 1 + 1) bs).toArray f 0 cs

Tactic:
rw [zipWithAux_toArray_succ, ih]

Result:
case succ
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
i : Nat
ih :
  ∀ (as : List α) (bs : List β) (cs : Array γ),
    as.toArray.zipWithAux bs.toArray f (i + 1) cs =
      (drop (i + 1) as).toArray.zipWithAux (drop (i + 1) bs).toArray f 0 cs
as : List α
bs : List β
cs : Array γ
⊢ (drop (i + 1) as.tail).toArray.zipWithAux (drop (i + 1) bs.tail).toArray f 0 cs =
    (drop (i + 1 + 1) as).toArray.zipWithAux (drop (i + 1 + 1) bs).toArray f 0 cs

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
as : List α
bs : List β
f : α → β → γ
i : Nat
cs : Array γ
⊢ as.toArray.zipWithAux bs.toArray f (i + 1) cs = (drop (i + 1) as).toArray.zipWithAux (drop (i + 1) bs).toArray f 0 cs

Tactic:
induction i generalizing as bs cs with
| zero => simp [zipWithAux_toArray_succ]
| succ i ih =>
  rw [zipWithAux_toArray_succ, ih]
  simp

Result:
no goals
-- Mathlib/Data/Nat/Choose/Basic.lean
theorem multichoose_two (k : ℕ) : multichoose 2 k = k + 1

Proof state:
k : ℕ
⊢ multichoose 2 k = k + 1

Tactic:
induction' k with k IH

Result:
case zero

⊢ multichoose 2 0 = 0 + 1

case succ
k : ℕ
IH : multichoose 2 k = k + 1
⊢ multichoose 2 (k + 1) = k + 1 + 1

Proof state:
case zero

⊢ multichoose 2 0 = 0 + 1

Tactic:
simp

Result:
no goals

Proof state:
case succ
k : ℕ
IH : multichoose 2 k = k + 1
⊢ multichoose 1 (k + 1) + (k + 1) = k + 1 + 1

Tactic:
simp [Nat.add_comm]

Result:
no goals

Proof state:
case succ
k : ℕ
IH : multichoose 2 k = k + 1
⊢ multichoose 2 (k + 1) = k + 1 + 1

Tactic:
rw [multichoose, IH]

Result:
case succ
k : ℕ
IH : multichoose 2 k = k + 1
⊢ multichoose 1 (k + 1) + (k + 1) = k + 1 + 1
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Bitblast.lean
theorem bit_not_add_self (x : BitVec w) :
  ((iunfoldr (fun (i : Fin w) c => (c, !(x.getLsbD i)))) ()).snd + x  = -1

Proof state:
w : Nat
x : BitVec w
⊢ (iunfoldr (fun i c => (c, !x.getLsbD ↑i)) ()).snd + x = -1

Tactic:
simp only [add_eq_adc]

Result:
w : Nat
x : BitVec w
⊢ ((iunfoldr (fun i c => (c, !x.getLsbD ↑i)) ()).snd.adc x false).snd = -1

Proof state:
w : Nat
x : BitVec w
⊢ ∀ (i : Fin w),
    adcb ((iunfoldr (fun i c => (c, !x.getLsbD ↑i)) ()).snd.getLsbD ↑i) (x.getLsbD ↑i) false = (false, (-1).getLsbD ↑i)

Tactic:
intro i

Result:
w : Nat
x : BitVec w
i : Fin w
⊢ adcb ((iunfoldr (fun i c => (c, !x.getLsbD ↑i)) ()).snd.getLsbD ↑i) (x.getLsbD ↑i) false = (false, (-1).getLsbD ↑i)

Proof state:
w : Nat
x : BitVec w
i : Fin w
⊢ (((iunfoldr (fun i c => (c, !x.getLsbD ↑i)) ()).snd.getLsbD ↑i).atLeastTwo (x.getLsbD ↑i) false,
      (iunfoldr (fun i c => (c, !x.getLsbD ↑i)) ()).snd.getLsbD ↑i ^^ (x.getLsbD ↑i ^^ false)) =
    (false, (-1).getLsbD ↑i)

Tactic:
rw [iunfoldr_replace_snd (fun _ => ()) (((iunfoldr (fun i c => (c, !(x.getLsbD i)))) ()).snd)]
<;> simp [bit_not_testBit, negOne_eq_allOnes, getLsbD_allOnes]

Result:
no goals

Proof state:
w : Nat
x : BitVec w
i : Fin w
⊢ adcb ((iunfoldr (fun i c => (c, !x.getLsbD ↑i)) ()).snd.getLsbD ↑i) (x.getLsbD ↑i) false = (false, (-1).getLsbD ↑i)

Tactic:
simp only [ BitVec.not, adcb, testBit_toNat]

Result:
w : Nat
x : BitVec w
i : Fin w
⊢ (((iunfoldr (fun i c => (c, !x.getLsbD ↑i)) ()).snd.getLsbD ↑i).atLeastTwo (x.getLsbD ↑i) false,
      (iunfoldr (fun i c => (c, !x.getLsbD ↑i)) ()).snd.getLsbD ↑i ^^ (x.getLsbD ↑i ^^ false)) =
    (false, (-1).getLsbD ↑i)

Proof state:
w : Nat
x : BitVec w
⊢ ((iunfoldr (fun i c => (c, !x.getLsbD ↑i)) ()).snd.adc x false).snd = -1

Tactic:
apply iunfoldr_replace_snd (fun _ => false) (-1) false rfl

Result:
w : Nat
x : BitVec w
⊢ ∀ (i : Fin w),
    adcb ((iunfoldr (fun i c => (c, !x.getLsbD ↑i)) ()).snd.getLsbD ↑i) (x.getLsbD ↑i) false = (false, (-1).getLsbD ↑i)
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/List/Associative.lean
theorem isEmpty_replaceEntry [BEq α] {l : List ((a : α) × β a)} {k : α} {v : β k} :
    (replaceEntry k v l).isEmpty = l.isEmpty

Proof state:
case cons
α : Type u
β : α → Type v
inst✝ : BEq α
k : α
v : β k
k✝ : α
v✝ : β k✝
tail✝ : List ((a : α) × β a)
a✝ : (replaceEntry k v tail✝).isEmpty = tail✝.isEmpty
⊢ (if (k✝ == k) = true then ⟨k, v⟩ :: tail✝ else ⟨k✝, v✝⟩ :: replaceEntry k v tail✝).isEmpty = false

Tactic:
split <;> simp

Result:
no goals

Proof state:
case cons
α : Type u
β : α → Type v
inst✝ : BEq α
k : α
v : β k
k✝ : α
v✝ : β k✝
tail✝ : List ((a : α) × β a)
a✝ : (replaceEntry k v tail✝).isEmpty = tail✝.isEmpty
⊢ (replaceEntry k v (⟨k✝, v✝⟩ :: tail✝)).isEmpty = (⟨k✝, v✝⟩ :: tail✝).isEmpty

Tactic:
simp only [replaceEntry_cons, cond_eq_if, List.isEmpty_cons]

Result:
case cons
α : Type u
β : α → Type v
inst✝ : BEq α
k : α
v : β k
k✝ : α
v✝ : β k✝
tail✝ : List ((a : α) × β a)
a✝ : (replaceEntry k v tail✝).isEmpty = tail✝.isEmpty
⊢ (if (k✝ == k) = true then ⟨k, v⟩ :: tail✝ else ⟨k✝, v✝⟩ :: replaceEntry k v tail✝).isEmpty = false

Proof state:
case nil
α : Type u
β : α → Type v
inst✝ : BEq α
k : α
v : β k
⊢ (replaceEntry k v []).isEmpty = [].isEmpty

Tactic:
simp

Result:
no goals

Proof state:
α : Type u
β : α → Type v
inst✝ : BEq α
l : List ((a : α) × β a)
k : α
v : β k
⊢ (replaceEntry k v l).isEmpty = l.isEmpty

Tactic:
induction l using assoc_induction

Result:
case nil
α : Type u
β : α → Type v
inst✝ : BEq α
k : α
v : β k
⊢ (replaceEntry k v []).isEmpty = [].isEmpty

case cons
α : Type u
β : α → Type v
inst✝ : BEq α
k : α
v : β k
k✝ : α
v✝ : β k✝
tail✝ : List ((a : α) × β a)
a✝ : (replaceEntry k v tail✝).isEmpty = tail✝.isEmpty
⊢ (replaceEntry k v (⟨k✝, v✝⟩ :: tail✝)).isEmpty = (⟨k✝, v✝⟩ :: tail✝).isEmpty
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/BasicAux.lean
theorem append_cancel_right_eq (as bs cs : List α) : (as ++ bs = cs ++ bs) = (as = cs)

Proof state:
α : Type u_1
as bs cs : List α
⊢ (as ++ bs = cs ++ bs) = (as = cs)

Tactic:
apply propext

Result:
case a
α : Type u_1
as bs cs : List α
⊢ as ++ bs = cs ++ bs ↔ as = cs

Proof state:
case a.mpr
α : Type u_1
as bs cs : List α
⊢ as = cs → as ++ bs = cs ++ bs

Tactic:
next => intro h; simp [h]

Result:
no goals

Proof state:
α : Type u_1
as bs cs : List α
⊢ as = cs → as ++ bs = cs ++ bs

Tactic:
intro h

Result:
α : Type u_1
as bs cs : List α
h : as = cs
⊢ as ++ bs = cs ++ bs

Proof state:
α : Type u_1
as bs cs : List α
h : as = cs
⊢ as ++ bs = cs ++ bs

Tactic:
simp [h]

Result:
no goals

Proof state:
case a
α : Type u_1
as bs cs : List α
⊢ as ++ bs = cs ++ bs ↔ as = cs

Tactic:
apply Iff.intro

Result:
case a.mp
α : Type u_1
as bs cs : List α
⊢ as ++ bs = cs ++ bs → as = cs

case a.mpr
α : Type u_1
as bs cs : List α
⊢ as = cs → as ++ bs = cs ++ bs

Proof state:
α : Type u_1
as bs cs : List α
⊢ as ++ bs = cs ++ bs → as = cs

Tactic:
apply append_cancel_right

Result:
no goals

Proof state:
case a.mp
α : Type u_1
as bs cs : List α
⊢ as ++ bs = cs ++ bs → as = cs

case a.mpr
α : Type u_1
as bs cs : List α
⊢ as = cs → as ++ bs = cs ++ bs

Tactic:
next => apply append_cancel_right

Result:
case a.mpr
α : Type u_1
as bs cs : List α
⊢ as = cs → as ++ bs = cs ++ bs
-- Mathlib/Analysis/SpecialFunctions/Trigonometric/Angle.lean
theorem neg_pi_div_two_ne_zero : ((-π / 2 : ℝ) : Angle) ≠ 0

Proof state:
⊢ ↑(-π / 2) ≠ 0

Tactic:
rw [← toReal_injective.ne_iff, toReal_neg_pi_div_two, toReal_zero]

Result:
⊢ -π / 2 ≠ 0

Proof state:
⊢ -π / 2 ≠ 0

Tactic:
exact div_ne_zero (neg_ne_zero.2 Real.pi_ne_zero) two_ne_zero

Result:
no goals
-- Mathlib/Topology/Category/Profinite/Nobeling.lean
theorem projRestricts_eq_id : ProjRestricts C (fun i (h : J i) ↦ h) = id

Proof state:
case h.mk.intro.intro.a.h
I : Type u
C : Set (I → Bool)
J : I → Prop
inst✝ : (i : I) → Decidable (J i)
y : I → Bool
hy : y ∈ C
i : I
⊢ ↑(ProjRestricts C ⋯ ⟨Proj J y, ⋯⟩) i = ↑(id ⟨Proj J y, ⋯⟩) i

Tactic:
simp +contextual only [π, Proj, ProjRestricts_coe, id_eq, if_true]

Result:
no goals

Proof state:
I : Type u
C : Set (I → Bool)
J : I → Prop
inst✝ : (i : I) → Decidable (J i)
⊢ ProjRestricts C ⋯ = id

Tactic:
ext ⟨x, y, hy, rfl⟩ i

Result:
case h.mk.intro.intro.a.h
I : Type u
C : Set (I → Bool)
J : I → Prop
inst✝ : (i : I) → Decidable (J i)
y : I → Bool
hy : y ∈ C
i : I
⊢ ↑(ProjRestricts C ⋯ ⟨Proj J y, ⋯⟩) i = ↑(id ⟨Proj J y, ⋯⟩) i
-- Mathlib/.lake/packages/batteries/Batteries/Data/AssocList.lean
theorem toList_eq_toListTR : @toList = @toListTR

Proof state:
⊢ @toList = @toListTR

Tactic:
funext α β as

Result:
case h.h.h
α : Type u_2
β : Type u_1
as : AssocList α β
⊢ as.toList = as.toListTR

Proof state:
case h.h.h
α : Type u_2
β : Type u_1
as : AssocList α β
⊢ as.toList = as.toListTR

Tactic:
simp [toListTR]

Result:
case h.h.h
α : Type u_2
β : Type u_1
as : AssocList α β
⊢ as.toList = (List.foldl (fun d x => d.push (x.fst, x.snd)) #[] as.toList).toList

Proof state:
case h.h.h
α : Type u_2
β : Type u_1
as : AssocList α β
⊢ as.toList = (List.foldl (fun d x => d.push (x.fst, x.snd)) #[] as.toList).toList

Tactic:
exact .symm <| (Array.foldl_toList_eq_map (toList as) _ id).trans (List.map_id _)

Result:
no goals
-- Mathlib/Probability/Kernel/Disintegration/StandardBorel.lean
lemma compProd_fst_condKernelReal (κ : Kernel α (γ × ℝ)) [IsFiniteKernel κ] :
    fst κ ⊗ₖ condKernelReal κ = κ

Proof state:
α : Type u_1
γ : Type u_3
mα : MeasurableSpace α
mγ : MeasurableSpace γ
inst✝¹ : CountablyGenerated γ
κ : Kernel α (γ × ℝ)
inst✝ : IsFiniteKernel κ
⊢ κ.fst ⊗ₖ κ.condKernelReal = κ

Tactic:
rw [condKernelReal, compProd_toKernel]

Result:
no goals
-- Mathlib/Algebra/ContinuedFractions/Computation/CorrectnessTerminating.lean
theorem compExactValue_correctness_of_stream_eq_some :
    ∀ {ifp_n : IntFractPair K}, IntFractPair.stream v n = some ifp_n →
      v = compExactValue ((of v).contsAux n) ((of v).contsAux <| n + 1) ifp_n.fr

Proof state:
case zero.inl
K : Type u_1
inst✝¹ : LinearOrderedField K
v : K
n : ℕ
inst✝ : FloorRing K
g : GenContFract K := of v
stream_zero_eq : IntFractPair.stream v 0 = some (IntFractPair.of v)
fract_eq_zero : Int.fract v = 0
⊢ v = ↑⌊v⌋

Tactic:
calc
  v = Int.fract v + ⌊v⌋ := by rw [Int.fract_add_floor]
  _ = ⌊v⌋ := by simp [fract_eq_zero]

Result:
no goals

Proof state:
K : Type u_1
inst✝¹ : LinearOrderedField K
v : K
n✝ : ℕ
inst✝ : FloorRing K
g : GenContFract K := of v
n : ℕ
ifp_n : IntFractPair K
nth_stream_eq : IntFractPair.stream v n = some ifp_n
nth_fract_ne_zero : ifp_n.fr ≠ 0
conts : Pair K := g.contsAux (n + 2)
pconts : Pair K := g.contsAux (n + 1)
pconts_eq : pconts = g.contsAux (n + 1)
ppconts : Pair K := g.contsAux n
IH : ∀ {ifp_n : IntFractPair K}, IntFractPair.stream v n = some ifp_n → v = compExactValue ppconts pconts ifp_n.fr
ppconts_eq : ppconts = g.contsAux n
nth_stream_eq' : IntFractPair.stream v n = some ifp_n
ifp_n_fract_ne_zero : ifp_n.fr ≠ 0
succ_nth_stream_eq : IntFractPair.stream v (n + 1) = some (IntFractPair.of ifp_n.fr⁻¹)
ifp_succ_n_fr_ne_zero : (IntFractPair.of ifp_n.fr⁻¹).fr ≠ 0
s_nth_eq : g.s.get? n = some { a := 1, b := ↑⌊ifp_n.fr⁻¹⌋ }
ppA : K := ppconts.a
ppB : K := ppconts.b
pA : K := pconts.a
pB : K := pconts.b
this : compExactValue ppconts pconts ifp_n.fr = (ppA + ifp_n.fr⁻¹ * pA) / (ppB + ifp_n.fr⁻¹ * pB)
tmp_calc :
  (↑⌊1 / ifp_n.fr⌋ * pA + ppA) / Int.fract (1 / ifp_n.fr) + pA = (pA * (1 / ifp_n.fr) + ppA) / Int.fract (1 / ifp_n.fr)
tmp_calc' :
  (↑⌊1 / ifp_n.fr⌋ * pB + ppB) / Int.fract (1 / ifp_n.fr) + pB = (pB * (1 / ifp_n.fr) + ppB) / Int.fract (1 / ifp_n.fr)
f : K := Int.fract (1 / ifp_n.fr)
f_ne_zero : f ≠ 0
hA : ↑⌊1 / ifp_n.fr⌋ * pA + ppA + pA * f = pA * (1 / ifp_n.fr) + ppA
hB : ↑⌊1 / ifp_n.fr⌋ * pB + ppB + pB * f = pB * (1 / ifp_n.fr) + ppB
hfr : (IntFractPair.of (1 / ifp_n.fr)).fr = f
⊢ ¬(IntFractPair.of ifp_n.fr⁻¹).fr = 0

Tactic:
rwa [inv_eq_one_div, hfr]

Result:
no goals

Proof state:
K : Type u_1
inst✝¹ : LinearOrderedField K
v : K
n : ℕ
inst✝ : FloorRing K
g : GenContFract K := of v
ifp_zero : IntFractPair K
stream_zero_eq : IntFractPair.stream v 0 = some ifp_zero
this : IntFractPair.stream v 0 = some (IntFractPair.of v)
⊢ IntFractPair.of v = ifp_zero

Tactic:
simpa only [this, Option.some.injEq] using stream_zero_eq

Result:
no goals
-- Mathlib/Analysis/Calculus/FDeriv/Analytic.lean
theorem AnalyticAt.fderiv [CompleteSpace F] (h : AnalyticAt 𝕜 f x) :
    AnalyticAt 𝕜 (fderiv 𝕜 f) x

Proof state:
𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
F : Type v
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
f : E → F
x : E
inst✝ : CompleteSpace F
h : AnalyticAt 𝕜 f x
⊢ AnalyticAt 𝕜 (fderiv 𝕜 f) x

Tactic:
rcases h with ⟨p, r, hp⟩

Result:
case intro.intro
𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
F : Type v
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
f : E → F
x : E
inst✝ : CompleteSpace F
p : FormalMultilinearSeries 𝕜 E F
r : ℝ≥0∞
hp : HasFPowerSeriesOnBall f p x r
⊢ AnalyticAt 𝕜 (fderiv 𝕜 f) x

Proof state:
case intro.intro
𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
F : Type v
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
f : E → F
x : E
inst✝ : CompleteSpace F
p : FormalMultilinearSeries 𝕜 E F
r : ℝ≥0∞
hp : HasFPowerSeriesOnBall f p x r
⊢ AnalyticAt 𝕜 (fderiv 𝕜 f) x

Tactic:
exact hp.fderiv.analyticAt

Result:
no goals