harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/RingTheory/Ideal/Operations.lean
theorem IsPrime.pow_le_iff {I P : Ideal R} [hP : P.IsPrime] {n : ℕ} (hn : n ≠ 0) :
    I ^ n ≤ P ↔ I ≤ P

Proof state:
R : Type u
inst✝ : CommSemiring R
I P : Ideal R
hP : P.IsPrime
n : ℕ
hn : n ≠ 0
h : (Multiset.replicate n I).prod ≤ P ↔ ∃ I_1 ∈ Multiset.replicate n I, I_1 ≤ P
⊢ I ^ n ≤ P ↔ I ≤ P

Tactic:
simp_rw [Multiset.prod_replicate, Multiset.mem_replicate, ne_eq, hn, not_false_eq_true,
  true_and, exists_eq_left] at h

Result:
R : Type u
inst✝ : CommSemiring R
I P : Ideal R
hP : P.IsPrime
n : ℕ
hn : n ≠ 0
h : I ^ n ≤ P ↔ I ≤ P
⊢ I ^ n ≤ P ↔ I ≤ P

Proof state:
R : Type u
inst✝ : CommSemiring R
I P : Ideal R
hP : P.IsPrime
n : ℕ
hn : n ≠ 0
h : I ^ n ≤ P ↔ I ≤ P
⊢ I ^ n ≤ P ↔ I ≤ P

Tactic:
exact h

Result:
no goals

Proof state:
R : Type u
inst✝ : CommSemiring R
I P : Ideal R
hP : P.IsPrime
n : ℕ
hn : n ≠ 0
⊢ I ^ n ≤ P ↔ I ≤ P

Tactic:
have h : (Multiset.replicate n I).prod ≤ P ↔ _ := hP.multiset_prod_le

Result:
R : Type u
inst✝ : CommSemiring R
I P : Ideal R
hP : P.IsPrime
n : ℕ
hn : n ≠ 0
h : (Multiset.replicate n I).prod ≤ P ↔ ∃ I_1 ∈ Multiset.replicate n I, I_1 ≤ P
⊢ I ^ n ≤ P ↔ I ≤ P
-- Mathlib/Data/Nat/Choose/Sum.lean
theorem sum_antidiagonal_choose_add (d n : ℕ) :
    (∑ ij ∈ antidiagonal n, (d + ij.2).choose d) = (d + n + 1).choose (d + 1)

Proof state:
case succ
d n : ℕ
hn : ∑ ij ∈ antidiagonal n, (d + ij.2).choose d = (d + n + 1).choose (d + 1)
⊢ ∑ ij ∈ antidiagonal (n + 1), (d + ij.2).choose d = (d + (n + 1) + 1).choose (d + 1)

Tactic:
rw [Nat.sum_antidiagonal_succ, hn, Nat.choose_succ_succ (d + (n + 1)), ← add_assoc]

Result:
no goals

Proof state:
case zero
d : ℕ
⊢ ∑ ij ∈ antidiagonal 0, (d + ij.2).choose d = (d + 0 + 1).choose (d + 1)

Tactic:
simp

Result:
no goals

Proof state:
d n : ℕ
⊢ ∑ ij ∈ antidiagonal n, (d + ij.2).choose d = (d + n + 1).choose (d + 1)

Tactic:
induction n with
| zero => simp
| succ n hn => rw [Nat.sum_antidiagonal_succ, hn, Nat.choose_succ_succ (d + (n + 1)), ← add_assoc]

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Finite.lean
theorem card_commonNeighbors_le_degree_right [DecidableRel G.Adj] (v w : V) :
    Fintype.card (G.commonNeighbors v w) ≤ G.degree w

Proof state:
V : Type u_1
G : SimpleGraph V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
v w : V
⊢ Fintype.card ↑(G.commonNeighbors v w) ≤ G.degree w

Tactic:
simp_rw [commonNeighbors_symm _ v w, card_commonNeighbors_le_degree_left]

Result:
no goals
-- Mathlib/Analysis/Complex/AbsMax.lean
theorem norm_max_aux₂ {f : ℂ → F} {z w : ℂ} (hd : DiffContOnCl ℂ f (ball z (dist w z)))
    (hz : IsMaxOn (norm ∘ f) (closedBall z (dist w z)) z) : ‖f w‖ = ‖f z‖

Proof state:
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℂ F
f : ℂ → F
z w : ℂ
hd : DiffContOnCl ℂ f (ball z (dist w z))
e : F →L[ℂ] F̂ := UniformSpace.Completion.toComplL
he : ∀ (x : F), ‖e x‖ = ‖x‖
hz : IsMaxOn (norm ∘ ⇑e ∘ f) (closedBall z (dist w z)) z
⊢ ‖f w‖ = ‖f z‖

Tactic:
simpa only [he, Function.comp_def]
  using norm_max_aux₁ (e.differentiable.comp_diffContOnCl hd) hz

Result:
no goals

Proof state:
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℂ F
f : ℂ → F
z w : ℂ
hd : DiffContOnCl ℂ f (ball z (dist w z))
hz : IsMaxOn (norm ∘ f) (closedBall z (dist w z)) z
e : F →L[ℂ] F̂ := UniformSpace.Completion.toComplL
⊢ ‖f w‖ = ‖f z‖

Tactic:
have he : ∀ x, ‖e x‖ = ‖x‖ := UniformSpace.Completion.norm_coe

Result:
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℂ F
f : ℂ → F
z w : ℂ
hd : DiffContOnCl ℂ f (ball z (dist w z))
hz : IsMaxOn (norm ∘ f) (closedBall z (dist w z)) z
e : F →L[ℂ] F̂ := UniformSpace.Completion.toComplL
he : ∀ (x : F), ‖e x‖ = ‖x‖
⊢ ‖f w‖ = ‖f z‖

Proof state:
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℂ F
f : ℂ → F
z w : ℂ
hd : DiffContOnCl ℂ f (ball z (dist w z))
hz : IsMaxOn (norm ∘ f) (closedBall z (dist w z)) z
e : F →L[ℂ] F̂ := UniformSpace.Completion.toComplL
he : ∀ (x : F), ‖e x‖ = ‖x‖
⊢ IsMaxOn (norm ∘ ⇑e ∘ f) (closedBall z (dist w z)) z

Tactic:
simpa only [IsMaxOn, Function.comp_def, he] using hz

Result:
no goals

Proof state:
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℂ F
f : ℂ → F
z w : ℂ
hd : DiffContOnCl ℂ f (ball z (dist w z))
hz : IsMaxOn (norm ∘ f) (closedBall z (dist w z)) z
⊢ ‖f w‖ = ‖f z‖

Tactic:
set e : F →L[ℂ] F̂ := UniformSpace.Completion.toComplL

Result:
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℂ F
f : ℂ → F
z w : ℂ
hd : DiffContOnCl ℂ f (ball z (dist w z))
hz : IsMaxOn (norm ∘ f) (closedBall z (dist w z)) z
e : F →L[ℂ] F̂ := UniformSpace.Completion.toComplL
⊢ ‖f w‖ = ‖f z‖

Proof state:
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℂ F
f : ℂ → F
z w : ℂ
hd : DiffContOnCl ℂ f (ball z (dist w z))
hz : IsMaxOn (norm ∘ f) (closedBall z (dist w z)) z
e : F →L[ℂ] F̂ := UniformSpace.Completion.toComplL
he : ∀ (x : F), ‖e x‖ = ‖x‖
⊢ ‖f w‖ = ‖f z‖

Tactic:
replace hz : IsMaxOn (norm ∘ e ∘ f) (closedBall z (dist w z)) z := by
  simpa only [IsMaxOn, Function.comp_def, he] using hz

Result:
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℂ F
f : ℂ → F
z w : ℂ
hd : DiffContOnCl ℂ f (ball z (dist w z))
e : F →L[ℂ] F̂ := UniformSpace.Completion.toComplL
he : ∀ (x : F), ‖e x‖ = ‖x‖
hz : IsMaxOn (norm ∘ ⇑e ∘ f) (closedBall z (dist w z)) z
⊢ ‖f w‖ = ‖f z‖
-- Mathlib/MeasureTheory/Measure/Prod.lean
theorem AEMeasurable.prod_swap [SFinite μ] [SFinite ν] {f : β × α → γ}
    (hf : AEMeasurable f (ν.prod μ)) : AEMeasurable (fun z : α × β => f z.swap) (μ.prod ν)

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝⁴ : MeasurableSpace α
inst✝³ : MeasurableSpace β
inst✝² : MeasurableSpace γ
μ : Measure α
ν : Measure β
inst✝¹ : SFinite μ
inst✝ : SFinite ν
f : β × α → γ
hf : AEMeasurable f (map Prod.swap (μ.prod ν))
⊢ AEMeasurable (fun z => f z.swap) (μ.prod ν)

Tactic:
exact hf.comp_measurable measurable_swap

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝⁴ : MeasurableSpace α
inst✝³ : MeasurableSpace β
inst✝² : MeasurableSpace γ
μ : Measure α
ν : Measure β
inst✝¹ : SFinite μ
inst✝ : SFinite ν
f : β × α → γ
hf : AEMeasurable f (ν.prod μ)
⊢ AEMeasurable (fun z => f z.swap) (μ.prod ν)

Tactic:
rw [← Measure.prod_swap] at hf

Result:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝⁴ : MeasurableSpace α
inst✝³ : MeasurableSpace β
inst✝² : MeasurableSpace γ
μ : Measure α
ν : Measure β
inst✝¹ : SFinite μ
inst✝ : SFinite ν
f : β × α → γ
hf : AEMeasurable f (map Prod.swap (μ.prod ν))
⊢ AEMeasurable (fun z => f z.swap) (μ.prod ν)
-- Mathlib/NumberTheory/NumberField/Embeddings.lean
lemma isUnramified_iff_stabilizer_eq_bot [IsGalois k K] : IsUnramified k w ↔ Stab w = ⊥

Proof state:
k : Type u_1
inst✝³ : Field k
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra k K
w : InfinitePlace K
inst✝ : IsGalois k K
⊢ IsUnramified k w ↔ Stab w = ⊥

Tactic:
rw [← mk_embedding w, isUnramified_mk_iff_forall_isConj]

Result:
k : Type u_1
inst✝³ : Field k
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra k K
w : InfinitePlace K
inst✝ : IsGalois k K
⊢ (∀ (σ : K ≃ₐ[k] K), ComplexEmbedding.IsConj w.embedding σ → σ = 1) ↔ Stab (mk w.embedding) = ⊥

Proof state:
k : Type u_1
inst✝³ : Field k
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra k K
w : InfinitePlace K
inst✝ : IsGalois k K
⊢ (∀ (σ : K ≃ₐ[k] K), ComplexEmbedding.IsConj w.embedding σ → σ = 1) ↔ Stab (mk w.embedding) = ⊥

Tactic:
simp only [eq_bot_iff, SetLike.le_def, mem_stabilizer_mk_iff,
  Subgroup.mem_bot, forall_eq_or_imp, true_and]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem toList_filter' (p : α → Bool) (l : Array α) (h : stop = l.size) :
    (l.filter p 0 stop).toList = l.toList.filter p

Proof state:
α : Type u_1
stop : Nat
p : α → Bool
l : Array α
h : stop = l.size
⊢ (filter p l 0 stop).toList = List.filter p l.toList

Tactic:
subst h

Result:
α : Type u_1
p : α → Bool
l : Array α
⊢ (filter p l).toList = List.filter p l.toList

Proof state:
case cons
α : Type u_1
p : α → Bool
l : Array α
head✝ : α
tail✝ : List α
tail_ih✝ :
  ∀ (a : Array α),
    (List.foldl (fun r a => if p a = true then r.push a else r) a tail✝).toList = a.toList ++ List.filter p tail✝
⊢ ∀ (a : Array α),
    (List.foldl (fun r a => if p a = true then r.push a else r) (if p head✝ = true then a.push head✝ else a)
          tail✝).toList =
      a.toList ++ List.filter p (head✝ :: tail✝)

Tactic:
split <;> simp [*]

Result:
no goals

Proof state:
α : Type u_1
p : α → Bool
l : Array α
⊢ (filter p l).toList = List.filter p l.toList

Tactic:
dsimp only [filter]

Result:
α : Type u_1
p : α → Bool
l : Array α
⊢ (foldl (fun r a => if p a = true then r.push a else r) #[] l).toList = List.filter p l.toList

Proof state:
α : Type u_1
p : α → Bool
l : Array α
⊢ (List.foldl (fun r a => if p a = true then r.push a else r) #[] l.toList).toList = List.filter p l.toList

Tactic:
generalize l.toList = l

Result:
α : Type u_1
p : α → Bool
l✝ : Array α
l : List α
⊢ (List.foldl (fun r a => if p a = true then r.push a else r) #[] l).toList = List.filter p l

Proof state:
α : Type u_1
p : α → Bool
l✝ : Array α
l : List α
this :
  ∀ (a : Array α), (List.foldl (fun r a => if p a = true then r.push a else r) a l).toList = a.toList ++ List.filter p l
⊢ (List.foldl (fun r a => if p a = true then r.push a else r) #[] l).toList = List.filter p l

Tactic:
simpa using this #[]

Result:
no goals

Proof state:
α : Type u_1
p : α → Bool
l : Array α
⊢ (foldl (fun r a => if p a = true then r.push a else r) #[] l).toList = List.filter p l.toList

Tactic:
rw [← foldl_toList]

Result:
α : Type u_1
p : α → Bool
l : Array α
⊢ (List.foldl (fun r a => if p a = true then r.push a else r) #[] l.toList).toList = List.filter p l.toList

Proof state:
α : Type u_1
p : α → Bool
l✝ : Array α
l : List α
⊢ ∀ (a : Array α), (List.foldl (fun r a => if p a = true then r.push a else r) a l).toList = a.toList ++ List.filter p l

Tactic:
induction l with simp
| cons => split <;> simp [*]

Result:
no goals

Proof state:
α : Type u_1
p : α → Bool
l✝ : Array α
l : List α
⊢ (List.foldl (fun r a => if p a = true then r.push a else r) #[] l).toList = List.filter p l

Tactic:
suffices ∀ a, (List.foldl (fun r a => if p a = true then push r a else r) a l).toList =
    a.toList ++ List.filter p l by
  simpa using this #[]

Result:
α : Type u_1
p : α → Bool
l✝ : Array α
l : List α
⊢ ∀ (a : Array α), (List.foldl (fun r a => if p a = true then r.push a else r) a l).toList = a.toList ++ List.filter p l
-- Mathlib/LinearAlgebra/Matrix/Hermitian.lean
theorem isHermitian_transpose_iff (A : Matrix n n α) : Aᵀ.IsHermitian ↔ A.IsHermitian :=
  ⟨by intro h; rw [← transpose_transpose A]; exact IsHermitian.transpose h, IsHermitian.transpose⟩

Proof state:
α : Type u_1
n : Type u_4
inst✝ : Star α
A : Matrix n n α
h : Aᵀ.IsHermitian
⊢ Aᵀᵀ.IsHermitian

Tactic:
exact IsHermitian.transpose h

Result:
no goals

Proof state:
α : Type u_1
n : Type u_4
inst✝ : Star α
A : Matrix n n α
h : Aᵀ.IsHermitian
⊢ A.IsHermitian

Tactic:
rw [← transpose_transpose A]

Result:
α : Type u_1
n : Type u_4
inst✝ : Star α
A : Matrix n n α
h : Aᵀ.IsHermitian
⊢ Aᵀᵀ.IsHermitian

Proof state:
α : Type u_1
n : Type u_4
inst✝ : Star α
A : Matrix n n α
⊢ Aᵀ.IsHermitian → A.IsHermitian

Tactic:
intro h

Result:
α : Type u_1
n : Type u_4
inst✝ : Star α
A : Matrix n n α
h : Aᵀ.IsHermitian
⊢ A.IsHermitian
-- Mathlib/Algebra/BigOperators/Group/List/Lemmas.lean
theorem neg_one_mem_of_prod_eq_neg_one {l : List ℤ} (h : l.prod = -1) : (-1 : ℤ) ∈ l

Proof state:
case intro.intro
l : List ℤ
h : l.prod = -1
x : ℤ
h₁ : x ∈ l
h₂ : x ≠ 1
⊢ -1 ∈ l

Tactic:
exact Or.resolve_left
  (Int.isUnit_iff.mp (prod_isUnit_iff.mp
    (h.symm ▸ ⟨⟨-1, -1, by decide, by decide⟩, rfl⟩ : IsUnit l.prod) x h₁)) h₂ ▸ h₁

Result:
no goals

Proof state:
l : List ℤ
h : l.prod = -1
x : ℤ
h₁ : x ∈ l
h₂ : x ≠ 1
⊢ -1 * -1 = 1

Tactic:
decide

Result:
no goals

Proof state:
l : List ℤ
h : l.prod = -1
⊢ -1 ≠ 1

Tactic:
decide

Result:
no goals

Proof state:
l : List ℤ
h : l.prod = -1
⊢ -1 ∈ l

Tactic:
obtain ⟨x, h₁, h₂⟩ := exists_mem_ne_one_of_prod_ne_one (ne_of_eq_of_ne h (by decide))

Result:
case intro.intro
l : List ℤ
h : l.prod = -1
x : ℤ
h₁ : x ∈ l
h₂ : x ≠ 1
⊢ -1 ∈ l
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Attach.lean
theorem toList_attach {α : Type _} {l : Vector α n} :
    l.attach.toList = l.toList.attachWith (· ∈ l) (by simp)

Proof state:
n : Nat
α : Type u_1
l : Vector α n
⊢ l.attach.toList = l.toList.attachWith (fun x => x ∈ l) ⋯

Tactic:
simp [attach]

Result:
no goals

Proof state:
n : Nat
α : Type ?u.6031
l : Vector α n
⊢ ∀ (x : α), x ∈ l.toList → (fun x => x ∈ l) x

Tactic:
simp

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Complex/Arg.lean
theorem arg_mul_coe_angle {x y : ℂ} (hx : x ≠ 0) (hy : y ≠ 0) :
    (arg (x * y) : Real.Angle) = arg x + arg y

Proof state:
x y : ℂ
hx : x ≠ 0
hy : y ≠ 0
⊢ ↑(x * y).arg = ↑x.arg + ↑y.arg

Tactic:
convert arg_mul_cos_add_sin_mul_I_coe_angle (mul_pos (norm_pos_iff.mpr hx) (norm_pos_iff.mpr hy))
    (arg x + arg y : Real.Angle) using 3

Result:
case h.e'_2.h.e'_1.h.e'_1
x y : ℂ
hx : x ≠ 0
hy : y ≠ 0
⊢ x * y = ↑(‖x‖ * ‖y‖) * (↑(↑x.arg + ↑y.arg).cos + ↑(↑x.arg + ↑y.arg).sin * I)

Proof state:
case h.e'_2.h.e'_1.h.e'_1
x y : ℂ
hx : x ≠ 0
hy : y ≠ 0
⊢ x * y = ↑(‖x‖ * ‖y‖) * (↑(↑x.arg + ↑y.arg).cos + ↑(↑x.arg + ↑y.arg).sin * I)

Tactic:
simp_rw [← Real.Angle.coe_add, Real.Angle.sin_coe, Real.Angle.cos_coe, ofReal_cos, ofReal_sin,
  cos_add_sin_I, ofReal_add, add_mul, exp_add, ofReal_mul]

Result:
case h.e'_2.h.e'_1.h.e'_1
x y : ℂ
hx : x ≠ 0
hy : y ≠ 0
⊢ x * y = ↑‖x‖ * ↑‖y‖ * (cexp (↑x.arg * I) * cexp (↑y.arg * I))

Proof state:
case h.e'_2.h.e'_1.h.e'_1
x y : ℂ
hx : x ≠ 0
hy : y ≠ 0
⊢ x * y = ↑‖x‖ * ↑‖y‖ * (cexp (↑x.arg * I) * cexp (↑y.arg * I))

Tactic:
rw [mul_assoc, mul_comm (exp _), ← mul_assoc (‖y‖ : ℂ), norm_mul_exp_arg_mul_I, mul_comm y, ←
  mul_assoc, norm_mul_exp_arg_mul_I]

Result:
no goals
-- Mathlib/Algebra/Group/Indicator.lean
theorem mulIndicator_mul_compl_eq_piecewise [DecidablePred (· ∈ s)] (f g : α → M) :
    s.mulIndicator f * sᶜ.mulIndicator g = s.piecewise f g

Proof state:
α : Type u_1
M : Type u_3
inst✝¹ : MulOneClass M
s : Set α
inst✝ : DecidablePred fun x => x ∈ s
f g : α → M
⊢ s.mulIndicator f * sᶜ.mulIndicator g = s.piecewise f g

Tactic:
ext x

Result:
case h
α : Type u_1
M : Type u_3
inst✝¹ : MulOneClass M
s : Set α
inst✝ : DecidablePred fun x => x ∈ s
f g : α → M
x : α
⊢ (s.mulIndicator f * sᶜ.mulIndicator g) x = s.piecewise f g x

Proof state:
case pos
α : Type u_1
M : Type u_3
inst✝¹ : MulOneClass M
s : Set α
inst✝ : DecidablePred fun x => x ∈ s
f g : α → M
x : α
h : x ∈ s
⊢ (s.mulIndicator f * sᶜ.mulIndicator g) x = s.piecewise f g x

Tactic:
rw [piecewise_eq_of_mem _ _ _ h, Pi.mul_apply, Set.mulIndicator_of_mem h,
  Set.mulIndicator_of_not_mem (Set.not_mem_compl_iff.2 h), mul_one]

Result:
no goals

Proof state:
case neg
α : Type u_1
M : Type u_3
inst✝¹ : MulOneClass M
s : Set α
inst✝ : DecidablePred fun x => x ∈ s
f g : α → M
x : α
h : x ∉ s
⊢ (s.mulIndicator f * sᶜ.mulIndicator g) x = s.piecewise f g x

Tactic:
rw [piecewise_eq_of_not_mem _ _ _ h, Pi.mul_apply, Set.mulIndicator_of_not_mem h,
  Set.mulIndicator_of_mem (Set.mem_compl h), one_mul]

Result:
no goals

Proof state:
case h
α : Type u_1
M : Type u_3
inst✝¹ : MulOneClass M
s : Set α
inst✝ : DecidablePred fun x => x ∈ s
f g : α → M
x : α
⊢ (s.mulIndicator f * sᶜ.mulIndicator g) x = s.piecewise f g x

Tactic:
by_cases h : x ∈ s

Result:
case pos
α : Type u_1
M : Type u_3
inst✝¹ : MulOneClass M
s : Set α
inst✝ : DecidablePred fun x => x ∈ s
f g : α → M
x : α
h : x ∈ s
⊢ (s.mulIndicator f * sᶜ.mulIndicator g) x = s.piecewise f g x

case neg
α : Type u_1
M : Type u_3
inst✝¹ : MulOneClass M
s : Set α
inst✝ : DecidablePred fun x => x ∈ s
f g : α → M
x : α
h : x ∉ s
⊢ (s.mulIndicator f * sᶜ.mulIndicator g) x = s.piecewise f g x
-- Mathlib/.lake/packages/lean4/src/lean/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/SignExtend.lean
theorem go_get (aig : AIG α) (w : Nat) (hw : 0 < w) (input : RefVec aig w) (newWidth : Nat)
    (curr : Nat) (hcurr : curr ≤ newWidth) (s : RefVec aig curr) :
    ∀ (idx : Nat) (hidx1 : idx < newWidth),
        curr ≤ idx
          →
        (go w hw input newWidth curr hcurr s).get idx hidx1
          =
        if hidx2 : idx < w then
          input.get idx (by omega)
        else
          input.get (w - 1) (by omega)

Proof state:
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
w : Nat
hw : 0 < w
input : aig.RefVec w
newWidth curr : Nat
hcurr✝ : curr ≤ newWidth
s : aig.RefVec curr
idx : Nat
hidx1 : idx < newWidth
hcurr : curr ≤ idx
⊢ (if hcurr1 : curr < newWidth then
          if hcurr2 : curr < w then
            let s := s.push (input.get curr hcurr2);
            go w hw input newWidth (curr + 1) ⋯ s
          else
            let s := s.push (input.get (w - 1) ⋯);
            go w hw input newWidth (curr + 1) ⋯ s
        else
          let_fun hcurr := ⋯;
          hcurr ▸ s).get
      idx hidx1 =
    if hidx2 : idx < w then input.get idx ⋯ else input.get (w - 1) ⋯

Tactic:
have : curr < newWidth := by omega

Result:
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
w : Nat
hw : 0 < w
input : aig.RefVec w
newWidth curr : Nat
hcurr✝ : curr ≤ newWidth
s : aig.RefVec curr
idx : Nat
hidx1 : idx < newWidth
hcurr : curr ≤ idx
this : curr < newWidth
⊢ (if hcurr1 : curr < newWidth then
          if hcurr2 : curr < w then
            let s := s.push (input.get curr hcurr2);
            go w hw input newWidth (curr + 1) ⋯ s
          else
            let s := s.push (input.get (w - 1) ⋯);
            go w hw input newWidth (curr + 1) ⋯ s
        else
          let_fun hcurr := ⋯;
          hcurr ▸ s).get
      idx hidx1 =
    if hidx2 : idx < w then input.get idx ⋯ else input.get (w - 1) ⋯
-- Mathlib/Data/BitVec.lean
theorem ofFin_intCast (z : ℤ) : ofFin (z : Fin (2^w)) = ↑z

Proof state:
z : ℤ
w : ℕ
⊢ {
      toFin :=
        (fun x =>
            match x with
            | Int.ofNat n => ↑n
            | Int.negSucc n => -↑(n + 1))
          z } =
    BitVec.ofInt (w + 1) z

Tactic:
rcases z with z | z

Result:
case ofNat
w z : ℕ
⊢ {
      toFin :=
        (fun x =>
            match x with
            | Int.ofNat n => ↑n
            | Int.negSucc n => -↑(n + 1))
          (Int.ofNat z) } =
    BitVec.ofInt (w + 1) (Int.ofNat z)

case negSucc
w z : ℕ
⊢ {
      toFin :=
        (fun x =>
            match x with
            | Int.ofNat n => ↑n
            | Int.negSucc n => -↑(n + 1))
          (Int.negSucc z) } =
    BitVec.ofInt (w + 1) (Int.negSucc z)

Proof state:
z : ℤ
w : ℕ
⊢ { toFin := Int.castDef z } = BitVec.ofInt (w + 1) z

Tactic:
unfold Int.castDef

Result:
z : ℤ
w : ℕ
⊢ {
      toFin :=
        (fun x =>
            match x with
            | Int.ofNat n => ↑n
            | Int.negSucc n => -↑(n + 1))
          z } =
    BitVec.ofInt (w + 1) z

Proof state:
case negSucc
w z : ℕ
⊢ {
      toFin :=
        (fun x =>
            match x with
            | Int.ofNat n => ↑n
            | Int.negSucc n => -↑(n + 1))
          (Int.negSucc z) } =
    BitVec.ofInt (w + 1) (Int.negSucc z)

Tactic:
rw [ofInt_negSucc_eq_not_ofNat]

Result:
case negSucc
w z : ℕ
⊢ {
      toFin :=
        (fun x =>
            match x with
            | Int.ofNat n => ↑n
            | Int.negSucc n => -↑(n + 1))
          (Int.negSucc z) } =
    ~~~BitVec.ofNat (w + 1) z

Proof state:
z : ℤ
⊢ { toFin := ↑z } = ↑z

Tactic:
simp only [eq_nil]

Result:
no goals

Proof state:
case negSucc
w z : ℕ
⊢ {
      toFin :=
        (fun x =>
            match x with
            | Int.ofNat n => ↑n
            | Int.negSucc n => -↑(n + 1))
          (Int.negSucc z) } =
    ~~~BitVec.ofNat (w + 1) z

Tactic:
simp only [Nat.cast_add, Nat.cast_one, neg_add_rev]

Result:
case negSucc
w z : ℕ
⊢ { toFin := -1 + -↑z } = ~~~BitVec.ofNat (w + 1) z

Proof state:
w : ℕ
z : ℤ
⊢ { toFin := ↑z } = ↑z

Tactic:
cases w

Result:
case zero
z : ℤ
⊢ { toFin := ↑z } = ↑z

case succ
z : ℤ
n✝ : ℕ
⊢ { toFin := ↑z } = ↑z

Proof state:
case negSucc
w z : ℕ
⊢ { toFin := -1 + -↑z } = ~~~BitVec.ofNat (w + 1) z

Tactic:
rw [← add_ofFin, ofFin_neg, ofFin_ofNat, ofNat_eq_ofNat, ofFin_neg, ofFin_natCast,
  natCast_eq_ofNat, negOne_eq_allOnes, ← sub_toAdd, allOnes_sub_eq_not]

Result:
no goals

Proof state:
case ofNat
w z : ℕ
⊢ {
      toFin :=
        (fun x =>
            match x with
            | Int.ofNat n => ↑n
            | Int.negSucc n => -↑(n + 1))
          (Int.ofNat z) } =
    BitVec.ofInt (w + 1) (Int.ofNat z)

Tactic:
rfl

Result:
no goals

Proof state:
case zero
z : ℤ
⊢ { toFin := ↑z } = ↑z

case succ
z : ℤ
n✝ : ℕ
⊢ { toFin := ↑z } = ↑z

Tactic:
case zero =>
  simp only [eq_nil]

Result:
case succ
z : ℤ
n✝ : ℕ
⊢ { toFin := ↑z } = ↑z

Proof state:
z : ℤ
w : ℕ
⊢ { toFin := ↑z } = ↑z

Tactic:
simp only [Int.cast, IntCast.intCast]

Result:
z : ℤ
w : ℕ
⊢ { toFin := Int.castDef z } = BitVec.ofInt (w + 1) z
-- Mathlib/Topology/Compactness/Compact.lean
theorem disjoint_cocompact_left (f : Filter X) :
    Disjoint (Filter.cocompact X) f ↔ ∃ K ∈ f, IsCompact K

Proof state:
X : Type u
inst✝ : TopologicalSpace X
f : Filter X
⊢ Disjoint (cocompact X) f ↔ ∃ K ∈ f, IsCompact K

Tactic:
simp_rw [hasBasis_cocompact.disjoint_iff_left, compl_compl]

Result:
X : Type u
inst✝ : TopologicalSpace X
f : Filter X
⊢ (∃ i, IsCompact i ∧ i ∈ f) ↔ ∃ K ∈ f, IsCompact K

Proof state:
X : Type u
inst✝ : TopologicalSpace X
f : Filter X
⊢ (∃ i, IsCompact i ∧ i ∈ f) ↔ ∃ K ∈ f, IsCompact K

Tactic:
tauto

Result:
no goals
-- Mathlib/Algebra/Polynomial/RingDivision.lean
theorem rootMultiplicity_eq_rootMultiplicity {p : R[X]} {t : R} :
    p.rootMultiplicity t = (p.comp (X + C t)).rootMultiplicity 0

Proof state:
case e_e
R : Type u
inst✝ : CommRing R
p : R[X]
t : R
⊢ multiplicity (X - C t) p = multiplicity X (p.comp (X + C t))

Tactic:
convert (multiplicity_map_eq <| algEquivAevalXAddC t).symm using 2

Result:
case h.e'_3.h.e'_3
R : Type u
inst✝ : CommRing R
p : R[X]
t : R
⊢ X = (algEquivAevalXAddC t) (X - C t)

Proof state:
R : Type u
inst✝ : CommRing R
p : R[X]
t : R
⊢ rootMultiplicity t p = rootMultiplicity 0 (p.comp (X + C t))

Tactic:
simp_rw [rootMultiplicity_eq_multiplicity, comp_X_add_C_eq_zero_iff]

Result:
R : Type u
inst✝ : CommRing R
p : R[X]
t : R
⊢ (if p = 0 then 0 else multiplicity (X - C t) p) = if p = 0 then 0 else multiplicity (X - C 0) (p.comp (X + C t))

Proof state:
case e_e
R : Type u
inst✝ : CommRing R
p : R[X]
t : R
⊢ multiplicity (X - C t) p = multiplicity (X - C 0) (p.comp (X + C t))

Tactic:
rw [C_0, sub_zero]

Result:
case e_e
R : Type u
inst✝ : CommRing R
p : R[X]
t : R
⊢ multiplicity (X - C t) p = multiplicity X (p.comp (X + C t))

Proof state:
R : Type u
inst✝ : CommRing R
p : R[X]
t : R
⊢ (if p = 0 then 0 else multiplicity (X - C t) p) = if p = 0 then 0 else multiplicity (X - C 0) (p.comp (X + C t))

Tactic:
congr 1

Result:
case e_e
R : Type u
inst✝ : CommRing R
p : R[X]
t : R
⊢ multiplicity (X - C t) p = multiplicity (X - C 0) (p.comp (X + C t))

Proof state:
R : Type u
inst✝ : CommRing R
p : R[X]
t : R
⊢ rootMultiplicity t p = rootMultiplicity 0 (p.comp (X + C t))

Tactic:
classical
simp_rw [rootMultiplicity_eq_multiplicity, comp_X_add_C_eq_zero_iff]
congr 1
rw [C_0, sub_zero]
convert (multiplicity_map_eq <| algEquivAevalXAddC t).symm using 2
simp [C_eq_algebraMap]

Result:
no goals

Proof state:
case h.e'_3.h.e'_3
R : Type u
inst✝ : CommRing R
p : R[X]
t : R
⊢ X = (algEquivAevalXAddC t) (X - C t)

Tactic:
simp [C_eq_algebraMap]

Result:
no goals
-- Mathlib/Analysis/Seminorm.lean
theorem absorbent_ball (hx : ‖x‖ < r) : Absorbent 𝕜 (Metric.ball x r)

Proof state:
𝕜 : Type u_3
E : Type u_7
inst✝² : NormedField 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
r : ℝ
x : E
hx : ‖x‖ < r
⊢ Absorbent 𝕜 ((normSeminorm 𝕜 E).ball x r)

Tactic:
exact (normSeminorm _ _).absorbent_ball hx

Result:
no goals

Proof state:
𝕜 : Type u_3
E : Type u_7
inst✝² : NormedField 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
r : ℝ
x : E
hx : ‖x‖ < r
⊢ Absorbent 𝕜 (Metric.ball x r)

Tactic:
rw [← ball_normSeminorm 𝕜]

Result:
𝕜 : Type u_3
E : Type u_7
inst✝² : NormedField 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
r : ℝ
x : E
hx : ‖x‖ < r
⊢ Absorbent 𝕜 ((normSeminorm 𝕜 E).ball x r)