harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Analysis/Quaternion.lean
theorem norm_piLp_equiv_symm_equivTuple (x : ℍ) :
    ‖(WithLp.equiv 2 (Fin 4 → _)).symm (equivTuple ℝ x)‖ = ‖x‖

Proof state:
x : ℍ
⊢ √(inner ((WithLp.equiv 2 (Fin 4 → ℝ)).symm ((equivTuple ℝ) x) 0)
              ((WithLp.equiv 2 (Fin 4 → ℝ)).symm ((equivTuple ℝ) x) 0) +
            inner ((WithLp.equiv 2 (Fin 4 → ℝ)).symm ((equivTuple ℝ) x) 1)
              ((WithLp.equiv 2 (Fin 4 → ℝ)).symm ((equivTuple ℝ) x) 1) +
          inner ((WithLp.equiv 2 (Fin 4 → ℝ)).symm ((equivTuple ℝ) x) 2)
            ((WithLp.equiv 2 (Fin 4 → ℝ)).symm ((equivTuple ℝ) x) 2) +
        inner ((WithLp.equiv 2 (Fin 4 → ℝ)).symm ((equivTuple ℝ) x) 3)
          ((WithLp.equiv 2 (Fin 4 → ℝ)).symm ((equivTuple ℝ) x) 3)) =
    √(x.re ^ 2 + x.imI ^ 2 + x.imJ ^ 2 + x.imK ^ 2)

Tactic:
simp_rw [RCLike.inner_apply, starRingEnd_apply, star_trivial, ← sq]

Result:
x : ℍ
⊢ √((WithLp.equiv 2 (Fin 4 → ℝ)).symm ((equivTuple ℝ) x) 0 ^ 2 +
            (WithLp.equiv 2 (Fin 4 → ℝ)).symm ((equivTuple ℝ) x) 1 ^ 2 +
          (WithLp.equiv 2 (Fin 4 → ℝ)).symm ((equivTuple ℝ) x) 2 ^ 2 +
        (WithLp.equiv 2 (Fin 4 → ℝ)).symm ((equivTuple ℝ) x) 3 ^ 2) =
    √(x.re ^ 2 + x.imI ^ 2 + x.imJ ^ 2 + x.imK ^ 2)

Proof state:
x : ℍ
⊢ √((WithLp.equiv 2 (Fin 4 → ℝ)).symm ((equivTuple ℝ) x) 0 ^ 2 +
            (WithLp.equiv 2 (Fin 4 → ℝ)).symm ((equivTuple ℝ) x) 1 ^ 2 +
          (WithLp.equiv 2 (Fin 4 → ℝ)).symm ((equivTuple ℝ) x) 2 ^ 2 +
        (WithLp.equiv 2 (Fin 4 → ℝ)).symm ((equivTuple ℝ) x) 3 ^ 2) =
    √(x.re ^ 2 + x.imI ^ 2 + x.imJ ^ 2 + x.imK ^ 2)

Tactic:
rfl

Result:
no goals

Proof state:
x : ℍ
⊢ ‖(WithLp.equiv 2 (Fin 4 → ℝ)).symm ((equivTuple ℝ) x)‖ = ‖x‖

Tactic:
rw [norm_eq_sqrt_real_inner, norm_eq_sqrt_real_inner, inner_self, normSq_def', PiLp.inner_apply,
  Fin.sum_univ_four]

Result:
x : ℍ
⊢ √(inner ((WithLp.equiv 2 (Fin 4 → ℝ)).symm ((equivTuple ℝ) x) 0)
              ((WithLp.equiv 2 (Fin 4 → ℝ)).symm ((equivTuple ℝ) x) 0) +
            inner ((WithLp.equiv 2 (Fin 4 → ℝ)).symm ((equivTuple ℝ) x) 1)
              ((WithLp.equiv 2 (Fin 4 → ℝ)).symm ((equivTuple ℝ) x) 1) +
          inner ((WithLp.equiv 2 (Fin 4 → ℝ)).symm ((equivTuple ℝ) x) 2)
            ((WithLp.equiv 2 (Fin 4 → ℝ)).symm ((equivTuple ℝ) x) 2) +
        inner ((WithLp.equiv 2 (Fin 4 → ℝ)).symm ((equivTuple ℝ) x) 3)
          ((WithLp.equiv 2 (Fin 4 → ℝ)).symm ((equivTuple ℝ) x) 3)) =
    √(x.re ^ 2 + x.imI ^ 2 + x.imJ ^ 2 + x.imK ^ 2)
-- Mathlib/NumberTheory/Harmonic/GammaDeriv.lean
lemma eulerMascheroniConstant_eq_neg_deriv : γ = -deriv Gamma 1

Proof state:
⊢ 1 = ↑0 + 1

Tactic:
simp

Result:
no goals

Proof state:
⊢ γ = -deriv Gamma 1

Tactic:
rw [show (1 : ℝ) = ↑(0 : ℕ) + 1 by simp, deriv_Gamma_nat 0]

Result:
⊢ γ = -(↑0! * (-γ + ↑(harmonic 0)))

Proof state:
⊢ γ = -(↑0! * (-γ + ↑(harmonic 0)))

Tactic:
simp

Result:
no goals
-- Mathlib/Topology/Algebra/UniformGroup/Defs.lean
theorem UniformContinuous.pow_const [UniformSpace β] {f : β → α} (hf : UniformContinuous f) :
    ∀ n : ℕ, UniformContinuous fun x => f x ^ n
  | 0 => by
    simp_rw [pow_zero]
    exact uniformContinuous_const
  | n + 1 => by
    simp_rw [pow_succ']
    exact hf.mul (hf.pow_const n)

Proof state:
α : Type u_1
β : Type u_2
inst✝³ : UniformSpace α
inst✝² : Group α
inst✝¹ : UniformGroup α
inst✝ : UniformSpace β
f : β → α
hf : UniformContinuous f
n : ℕ
⊢ UniformContinuous fun x => f x ^ (n + 1)

Tactic:
simp_rw [pow_succ']

Result:
α : Type u_1
β : Type u_2
inst✝³ : UniformSpace α
inst✝² : Group α
inst✝¹ : UniformGroup α
inst✝ : UniformSpace β
f : β → α
hf : UniformContinuous f
n : ℕ
⊢ UniformContinuous fun x => f x * f x ^ n

Proof state:
α : Type u_1
β : Type u_2
inst✝³ : UniformSpace α
inst✝² : Group α
inst✝¹ : UniformGroup α
inst✝ : UniformSpace β
f : β → α
hf : UniformContinuous f
⊢ UniformContinuous fun x => f x ^ 0

Tactic:
simp_rw [pow_zero]

Result:
α : Type u_1
β : Type u_2
inst✝³ : UniformSpace α
inst✝² : Group α
inst✝¹ : UniformGroup α
inst✝ : UniformSpace β
f : β → α
hf : UniformContinuous f
⊢ UniformContinuous fun x => 1

Proof state:
α : Type u_1
β : Type u_2
inst✝³ : UniformSpace α
inst✝² : Group α
inst✝¹ : UniformGroup α
inst✝ : UniformSpace β
f : β → α
hf : UniformContinuous f
n : ℕ
⊢ UniformContinuous fun x => f x * f x ^ n

Tactic:
exact hf.mul (hf.pow_const n)

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
inst✝³ : UniformSpace α
inst✝² : Group α
inst✝¹ : UniformGroup α
inst✝ : UniformSpace β
f : β → α
hf : UniformContinuous f
⊢ UniformContinuous fun x => 1

Tactic:
exact uniformContinuous_const

Result:
no goals
-- Mathlib/LinearAlgebra/Matrix/Permanent.lean
theorem permanent_diagonal {d : n → R} : permanent (diagonal d) = ∏ i, d i

Proof state:
n : Type u_1
inst✝² : DecidableEq n
inst✝¹ : Fintype n
R : Type u_2
inst✝ : CommSemiring R
d : n → R
σ : Perm n
x✝ : σ ∈ univ
hσ : σ ≠ 1
x : n
hx : ¬σ x = 1 x
⊢ ∏ i : n, diagonal d (σ i) i = 0

Tactic:
exact Finset.prod_eq_zero (mem_univ x) (if_neg hx)

Result:
no goals

Proof state:
n : Type u_1
inst✝² : DecidableEq n
inst✝¹ : Fintype n
R : Type u_2
inst✝ : CommSemiring R
d : n → R
⊢ (diagonal d).permanent = ∏ i : n, d i

Tactic:
refine (sum_eq_single 1 (fun σ _ hσ ↦ ?_) (fun h ↦ (h <| mem_univ _).elim)).trans ?_

Result:
case refine_1
n : Type u_1
inst✝² : DecidableEq n
inst✝¹ : Fintype n
R : Type u_2
inst✝ : CommSemiring R
d : n → R
σ : Perm n
x✝ : σ ∈ univ
hσ : σ ≠ 1
⊢ ∏ i : n, diagonal d (σ i) i = 0

case refine_2
n : Type u_1
inst✝² : DecidableEq n
inst✝¹ : Fintype n
R : Type u_2
inst✝ : CommSemiring R
d : n → R
⊢ ∏ i : n, diagonal d (1 i) i = ∏ i : n, d i

Proof state:
case refine_2
n : Type u_1
inst✝² : DecidableEq n
inst✝¹ : Fintype n
R : Type u_2
inst✝ : CommSemiring R
d : n → R
⊢ ∏ i : n, diagonal d (1 i) i = ∏ i : n, d i

Tactic:
simp only [Perm.one_apply, diagonal_apply_eq]

Result:
no goals

Proof state:
case refine_1
n : Type u_1
inst✝² : DecidableEq n
inst✝¹ : Fintype n
R : Type u_2
inst✝ : CommSemiring R
d : n → R
σ : Perm n
x✝ : σ ∈ univ
hσ : σ ≠ 1
⊢ ∏ i : n, diagonal d (σ i) i = 0

Tactic:
match not_forall.mp (mt Equiv.ext hσ) with
| ⟨x, hx⟩ => exact Finset.prod_eq_zero (mem_univ x) (if_neg hx)

Result:
no goals
-- Mathlib/Analysis/BoxIntegral/Partition/Split.lean
theorem sum_split_boxes {M : Type*} [AddCommMonoid M] (I : Box ι) (i : ι) (x : ℝ) (f : Box ι → M) :
    (∑ J ∈ (split I i x).boxes, f J) =
      (I.splitLower i x).elim' 0 f + (I.splitUpper i x).elim' 0 f

Proof state:
ι : Type u_1
M : Type u_3
inst✝ : AddCommMonoid M
I : Box ι
i : ι
x : ℝ
f : Box ι → M
⊢ ∑ J ∈ (split I i x).boxes, f J = Option.elim' 0 f (I.splitLower i x) + Option.elim' 0 f (I.splitUpper i x)

Tactic:
rw [split, sum_ofWithBot, Finset.sum_pair (I.splitLower_ne_splitUpper i x)]

Result:
no goals

Proof state:
ι : Type u_1
M : Type u_3
inst✝ : AddCommMonoid M
I : Box ι
i : ι
x : ℝ
f : Box ι → M
⊢ ∑ J ∈ (split I i x).boxes, f J = Option.elim' 0 f (I.splitLower i x) + Option.elim' 0 f (I.splitUpper i x)

Tactic:
classical
rw [split, sum_ofWithBot, Finset.sum_pair (I.splitLower_ne_splitUpper i x)]

Result:
no goals
-- Mathlib/Order/SupClosed.lean
@[simp] lemma supClosure_prod (s : Set α) (t : Set β) :
    supClosure (s ×ˢ t) = supClosure s ×ˢ supClosure t :=
  le_antisymm (supClosure_min (Set.prod_mono subset_supClosure subset_supClosure) <|
    supClosed_supClosure.prod supClosed_supClosure) <| by
      rintro ⟨_, _⟩ ⟨⟨u, hu, hus, rfl⟩, v, hv, hvt, rfl⟩
      refine ⟨u ×ˢ v, hu.product hv, ?_, ?_⟩
      · simpa only [coe_product] using Set.prod_mono hus hvt
      · simp [prodMk_sup'_sup']

Proof state:
α : Type u_3
β : Type u_4
inst✝¹ : SemilatticeSup α
inst✝ : SemilatticeSup β
s : Set α
t : Set β
⊢ supClosure s ×ˢ supClosure t ≤ supClosure (s ×ˢ t)

Tactic:
rintro ⟨_, _⟩ ⟨⟨u, hu, hus, rfl⟩, v, hv, hvt, rfl⟩

Result:
case mk.intro.intro.intro.intro.intro.intro.intro
α : Type u_3
β : Type u_4
inst✝¹ : SemilatticeSup α
inst✝ : SemilatticeSup β
s : Set α
t : Set β
u : Finset α
hu : u.Nonempty
hus : ↑u ⊆ s
v : Finset β
hv : v.Nonempty
hvt : ↑v ⊆ t
⊢ (u.sup' hu id, v.sup' hv id) ∈ supClosure (s ×ˢ t)

Proof state:
case mk.intro.intro.intro.intro.intro.intro.intro.refine_2
α : Type u_3
β : Type u_4
inst✝¹ : SemilatticeSup α
inst✝ : SemilatticeSup β
s : Set α
t : Set β
u : Finset α
hu : u.Nonempty
hus : ↑u ⊆ s
v : Finset β
hv : v.Nonempty
hvt : ↑v ⊆ t
⊢ (u ×ˢ v).sup' ⋯ id = (u.sup' hu id, v.sup' hv id)

Tactic:
simp [prodMk_sup'_sup']

Result:
no goals

Proof state:
case mk.intro.intro.intro.intro.intro.intro.intro.refine_1
α : Type u_3
β : Type u_4
inst✝¹ : SemilatticeSup α
inst✝ : SemilatticeSup β
s : Set α
t : Set β
u : Finset α
hu : u.Nonempty
hus : ↑u ⊆ s
v : Finset β
hv : v.Nonempty
hvt : ↑v ⊆ t
⊢ ↑(u ×ˢ v) ⊆ s ×ˢ t

Tactic:
simpa only [coe_product] using Set.prod_mono hus hvt

Result:
no goals

Proof state:
case mk.intro.intro.intro.intro.intro.intro.intro
α : Type u_3
β : Type u_4
inst✝¹ : SemilatticeSup α
inst✝ : SemilatticeSup β
s : Set α
t : Set β
u : Finset α
hu : u.Nonempty
hus : ↑u ⊆ s
v : Finset β
hv : v.Nonempty
hvt : ↑v ⊆ t
⊢ (u.sup' hu id, v.sup' hv id) ∈ supClosure (s ×ˢ t)

Tactic:
refine ⟨u ×ˢ v, hu.product hv, ?_, ?_⟩

Result:
case mk.intro.intro.intro.intro.intro.intro.intro.refine_1
α : Type u_3
β : Type u_4
inst✝¹ : SemilatticeSup α
inst✝ : SemilatticeSup β
s : Set α
t : Set β
u : Finset α
hu : u.Nonempty
hus : ↑u ⊆ s
v : Finset β
hv : v.Nonempty
hvt : ↑v ⊆ t
⊢ ↑(u ×ˢ v) ⊆ s ×ˢ t

case mk.intro.intro.intro.intro.intro.intro.intro.refine_2
α : Type u_3
β : Type u_4
inst✝¹ : SemilatticeSup α
inst✝ : SemilatticeSup β
s : Set α
t : Set β
u : Finset α
hu : u.Nonempty
hus : ↑u ⊆ s
v : Finset β
hv : v.Nonempty
hvt : ↑v ⊆ t
⊢ (u ×ˢ v).sup' ⋯ id = (u.sup' hu id, v.sup' hv id)
-- Mathlib/RingTheory/Polynomial/ScaleRoots.lean
theorem scaleRoots_ne_zero {p : R[X]} (hp : p ≠ 0) (s : R) : scaleRoots p s ≠ 0

Proof state:
R : Type u_1
inst✝ : Semiring R
p : R[X]
hp : p ≠ 0
s : R
h : p.scaleRoots s = 0
this✝ : p.coeff p.natDegree ≠ 0
this : (p.scaleRoots s).coeff p.natDegree = 0
⊢ False

Tactic:
rw [coeff_scaleRoots_natDegree] at this

Result:
R : Type u_1
inst✝ : Semiring R
p : R[X]
hp : p ≠ 0
s : R
h : p.scaleRoots s = 0
this✝ : p.coeff p.natDegree ≠ 0
this : p.leadingCoeff = 0
⊢ False

Proof state:
R : Type u_1
inst✝ : Semiring R
p : R[X]
hp : p ≠ 0
s : R
⊢ p.scaleRoots s ≠ 0

Tactic:
intro h

Result:
R : Type u_1
inst✝ : Semiring R
p : R[X]
hp : p ≠ 0
s : R
h : p.scaleRoots s = 0
⊢ False

Proof state:
R : Type u_1
inst✝ : Semiring R
p : R[X]
hp : p ≠ 0
s : R
h : p.scaleRoots s = 0
this✝ : p.coeff p.natDegree ≠ 0
this : p.leadingCoeff = 0
⊢ False

Tactic:
contradiction

Result:
no goals

Proof state:
R : Type u_1
inst✝ : Semiring R
p : R[X]
hp : p ≠ 0
s : R
h : p.scaleRoots s = 0
this : p.coeff p.natDegree ≠ 0
⊢ False

Tactic:
have : (scaleRoots p s).coeff p.natDegree = 0 :=
  congr_fun (congr_arg (coeff : R[X] → ℕ → R) h) p.natDegree

Result:
R : Type u_1
inst✝ : Semiring R
p : R[X]
hp : p ≠ 0
s : R
h : p.scaleRoots s = 0
this✝ : p.coeff p.natDegree ≠ 0
this : (p.scaleRoots s).coeff p.natDegree = 0
⊢ False

Proof state:
R : Type u_1
inst✝ : Semiring R
p : R[X]
hp : p ≠ 0
s : R
h : p.scaleRoots s = 0
⊢ False

Tactic:
have : p.coeff p.natDegree ≠ 0 := mt leadingCoeff_eq_zero.mp hp

Result:
R : Type u_1
inst✝ : Semiring R
p : R[X]
hp : p ≠ 0
s : R
h : p.scaleRoots s = 0
this : p.coeff p.natDegree ≠ 0
⊢ False
-- Mathlib/Tactic/CancelDenoms/Core.lean
theorem div_subst {α} [Field α] {n1 n2 k e1 e2 t1 : α}
    (h1 : n1 * e1 = t1) (h2 : n2 / e2 = 1) (h3 : n1 * n2 = k) : k * (e1 / e2) = t1

Proof state:
α : Type u_1
inst✝ : Field α
n1 n2 k e1 e2 t1 : α
h1 : n1 * e1 = t1
h2 : n2 / e2 = 1
h3 : n1 * n2 = k
⊢ k * (e1 / e2) = t1

Tactic:
rw [← h3, mul_assoc, mul_div_left_comm, h2, ← mul_assoc, h1, mul_comm, one_mul]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/RawLemmas.lean
theorem getKeyD_insertMany_empty_list_of_contains_eq_false [EquivBEq α] [LawfulHashable α]
    {l : List (α × β)} {k fallback : α}
    (h : (l.map Prod.fst).contains k = false) :
    (insertMany (empty : Raw₀ α (fun _ => β)) l).1.getKeyD k fallback = fallback

Proof state:
α : Type u
inst✝³ : BEq α
inst✝² : Hashable α
β : Type v
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
l : List (α × β)
k fallback : α
h : (List.map Prod.fst l).contains k = false
⊢ empty.getKeyD k fallback = fallback

Tactic:
apply getKeyD_empty

Result:
no goals

Proof state:
α : Type u
inst✝³ : BEq α
inst✝² : Hashable α
β : Type v
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
l : List (α × β)
k fallback : α
h : (List.map Prod.fst l).contains k = false
⊢ (insertMany empty l).val.getKeyD k fallback = fallback

Tactic:
rw [getKeyD_insertMany_list_of_contains_eq_false _ Raw.WF.empty₀ h]

Result:
α : Type u
inst✝³ : BEq α
inst✝² : Hashable α
β : Type v
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
l : List (α × β)
k fallback : α
h : (List.map Prod.fst l).contains k = false
⊢ empty.getKeyD k fallback = fallback
-- Mathlib/RingTheory/TensorProduct/Basic.lean
lemma comm_comp_map (f : A →ₐ[R] C) (g : B →ₐ[R] D) :
    (TensorProduct.comm R C D : C ⊗[R] D →ₐ[R] D ⊗[R] C).comp (Algebra.TensorProduct.map f g) =
    (Algebra.TensorProduct.map g f).comp (TensorProduct.comm R A B).toAlgHom

Proof state:
R : Type uR
A : Type uA
B : Type uB
C : Type uC
D : Type uD
inst✝⁸ : CommSemiring R
inst✝⁷ : Semiring A
inst✝⁶ : Algebra R A
inst✝⁵ : Semiring B
inst✝⁴ : Algebra R B
inst✝³ : Semiring C
inst✝² : Algebra R C
inst✝¹ : Semiring D
inst✝ : Algebra R D
f : A →ₐ[R] C
g : B →ₐ[R] D
⊢ (↑(TensorProduct.comm R C D)).comp (map f g) = (map g f).comp ↑(TensorProduct.comm R A B)

Tactic:
ext <;> rfl

Result:
no goals
-- Mathlib/MeasureTheory/Measure/SeparableMeasure.lean
theorem Measure.MeasureDense.fin_meas (h𝒜 : μ.MeasureDense 𝒜) :
    μ.MeasureDense {s | s ∈ 𝒜 ∧ μ s ≠ ∞} where
  measurable s h := h𝒜.measurable s h.1
  approx s ms hμs ε ε_pos

Proof state:
case intro.intro.intro
X : Type u_1
m : MeasurableSpace X
μ : Measure X
𝒜 : Set (Set X)
h𝒜 : μ.MeasureDense 𝒜
s : Set X
ms : MeasurableSet s
hμs : μ s ≠ ⊤
ε : ℝ
ε_pos : 0 < ε
t : Set X
t_mem : t ∈ 𝒜
hμt : μ t ≠ ⊤
hμst : μ (s ∆ t) < ENNReal.ofReal ε
⊢ ∃ t ∈ {s | s ∈ 𝒜 ∧ μ s ≠ ⊤}, μ (s ∆ t) < ENNReal.ofReal ε

Tactic:
exact ⟨t, ⟨t_mem, hμt⟩, hμst⟩

Result:
no goals

Proof state:
X : Type u_1
m : MeasurableSpace X
μ : Measure X
𝒜 : Set (Set X)
h𝒜 : μ.MeasureDense 𝒜
s : Set X
ms : MeasurableSet s
hμs : μ s ≠ ⊤
ε : ℝ
ε_pos : 0 < ε
⊢ ∃ t ∈ {s | s ∈ 𝒜 ∧ μ s ≠ ⊤}, μ (s ∆ t) < ENNReal.ofReal ε

Tactic:
rcases Measure.MeasureDense.fin_meas_approx h𝒜 ms hμs ε ε_pos with ⟨t, t_mem, hμt, hμst⟩

Result:
case intro.intro.intro
X : Type u_1
m : MeasurableSpace X
μ : Measure X
𝒜 : Set (Set X)
h𝒜 : μ.MeasureDense 𝒜
s : Set X
ms : MeasurableSet s
hμs : μ s ≠ ⊤
ε : ℝ
ε_pos : 0 < ε
t : Set X
t_mem : t ∈ 𝒜
hμt : μ t ≠ ⊤
hμst : μ (s ∆ t) < ENNReal.ofReal ε
⊢ ∃ t ∈ {s | s ∈ 𝒜 ∧ μ s ≠ ⊤}, μ (s ∆ t) < ENNReal.ofReal ε
-- Mathlib/Topology/UniformSpace/Equicontinuity.lean
lemma uniformEquicontinuousOn_univ (F : ι → β → α) :
    UniformEquicontinuousOn F univ ↔ UniformEquicontinuous F

Proof state:
ι : Type u_1
α : Type u_6
β : Type u_8
uα : UniformSpace α
uβ : UniformSpace β
F : ι → β → α
⊢ UniformEquicontinuousOn F univ ↔ UniformEquicontinuous F

Tactic:
simp [UniformEquicontinuousOn, UniformEquicontinuous]

Result:
no goals
-- Mathlib/Data/String/Lemmas.lean
lemma leftpad_suffix (n : ℕ) (c : Char) : ∀ s, IsSuffix s (leftpad n c s)
  | ⟨l⟩ => by simp only [IsSuffix, replicate, leftpad, String.length, List.leftpad_suffix]

Proof state:
n : ℕ
c : Char
l : List Char
⊢ { data := l }.IsSuffix (leftpad n c { data := l })

Tactic:
simp only [IsSuffix, replicate, leftpad, String.length, List.leftpad_suffix]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Tactic/BVDecide/LRAT/Internal/Formula/Lemmas.lean
theorem readyForRatAdd_delete {n : Nat} (f : DefaultFormula n) (arr : Array Nat) :
    ReadyForRatAdd f → ReadyForRatAdd (delete f arr)

Proof state:
n : Nat
f : DefaultFormula n
arr : Array Nat
h : f.ReadyForRatAdd
⊢ (f.delete arr).ReadyForRatAdd

Tactic:
constructor

Result:
case left
n : Nat
f : DefaultFormula n
arr : Array Nat
h : f.ReadyForRatAdd
⊢ (f.delete arr).ratUnits = #[]

case right
n : Nat
f : DefaultFormula n
arr : Array Nat
h : f.ReadyForRatAdd
⊢ (f.delete arr).ReadyForRupAdd

Proof state:
case left
n : Nat
f : DefaultFormula n
arr : Array Nat
h : f.ReadyForRatAdd
hb : f.ratUnits = #[]
⊢ (List.foldl (fun f id => f.deleteOne id) f arr.toList).ratUnits = #[]

Tactic:
have hl (acc : DefaultFormula n) (ih : acc.ratUnits = #[]) (id : Nat) (_id_in_arr : id ∈ arr.toList) :
  (deleteOne acc id).ratUnits = #[] := by rw [deleteOne_preserves_ratUnits, ih]

Result:
case left
n : Nat
f : DefaultFormula n
arr : Array Nat
h : f.ReadyForRatAdd
hb : f.ratUnits = #[]
hl : ∀ (acc : DefaultFormula n), acc.ratUnits = #[] → ∀ (id : Nat), id ∈ arr.toList → (acc.deleteOne id).ratUnits = #[]
⊢ (List.foldl (fun f id => f.deleteOne id) f arr.toList).ratUnits = #[]

Proof state:
case left
n : Nat
f : DefaultFormula n
arr : Array Nat
h : f.ReadyForRatAdd
hb : f.ratUnits = #[]
hl : ∀ (acc : DefaultFormula n), acc.ratUnits = #[] → ∀ (id : Nat), id ∈ arr.toList → (acc.deleteOne id).ratUnits = #[]
⊢ (List.foldl (fun f id => f.deleteOne id) f arr.toList).ratUnits = #[]

Tactic:
exact List.foldlRecOn arr.toList deleteOne f hb hl

Result:
no goals

Proof state:
case left
n : Nat
f : DefaultFormula n
arr : Array Nat
h : f.ReadyForRatAdd
⊢ (List.foldl (fun f id => f.deleteOne id) f arr.toList).ratUnits = #[]

Tactic:
have hb : f.ratUnits = #[] := h.1

Result:
case left
n : Nat
f : DefaultFormula n
arr : Array Nat
h : f.ReadyForRatAdd
hb : f.ratUnits = #[]
⊢ (List.foldl (fun f id => f.deleteOne id) f arr.toList).ratUnits = #[]

Proof state:
n : Nat
f : DefaultFormula n
arr : Array Nat
h : f.ReadyForRatAdd
hb : f.ratUnits = #[]
acc : DefaultFormula n
ih : acc.ratUnits = #[]
id : Nat
_id_in_arr : id ∈ arr.toList
⊢ (acc.deleteOne id).ratUnits = #[]

Tactic:
rw [deleteOne_preserves_ratUnits, ih]

Result:
no goals

Proof state:
case left
n : Nat
f : DefaultFormula n
arr : Array Nat
h : f.ReadyForRatAdd
⊢ (f.delete arr).ratUnits = #[]

Tactic:
rw [delete, ← Array.foldl_toList]

Result:
case left
n : Nat
f : DefaultFormula n
arr : Array Nat
h : f.ReadyForRatAdd
⊢ (List.foldl (fun f id => f.deleteOne id) f arr.toList).ratUnits = #[]

Proof state:
n : Nat
f : DefaultFormula n
arr : Array Nat
⊢ f.ReadyForRatAdd → (f.delete arr).ReadyForRatAdd

Tactic:
intro h

Result:
n : Nat
f : DefaultFormula n
arr : Array Nat
h : f.ReadyForRatAdd
⊢ (f.delete arr).ReadyForRatAdd

Proof state:
case right
n : Nat
f : DefaultFormula n
arr : Array Nat
h : f.ReadyForRatAdd
⊢ (f.delete arr).ReadyForRupAdd

Tactic:
exact readyForRupAdd_delete f arr h.2

Result:
no goals
-- Mathlib/Data/Matrix/Basic.lean
@[simp] lemma evalAddMonoidHom_comp_diagAddMonoidHom (i : m) :
    (Pi.evalAddMonoidHom _ i).comp (diagAddMonoidHom m α) = entryAddMonoidHom α i i

Proof state:
m : Type u_2
α : Type v
inst✝ : AddZeroClass α
i : m
⊢ (Pi.evalAddMonoidHom (fun i => α) i).comp (diagAddMonoidHom m α) = entryAddMonoidHom α i i

Tactic:
simp [AddMonoidHom.ext_iff]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/PropLemmas.lean
theorem exists_eq_right' : (∃ a, p a ∧ a' = a) ↔ p a'

Proof state:
α : Sort u_1
p : α → Prop
a' : α
⊢ (∃ a, p a ∧ a' = a) ↔ p a'

Tactic:
simp [@eq_comm _ a']

Result:
no goals
-- Mathlib/Data/Finset/Piecewise.lean
lemma piecewise_insert [DecidableEq ι] (j : ι) [∀ i, Decidable (i ∈ insert j s)] :
    (insert j s).piecewise f g = update (s.piecewise f g) j (f j)

Proof state:
ι : Type u_1
π : ι → Sort u_2
s : Finset ι
f g : (i : ι) → π i
inst✝² : (j : ι) → Decidable (j ∈ s)
inst✝¹ : DecidableEq ι
j : ι
inst✝ : (i : ι) → Decidable (i ∈ insert j s)
⊢ (↑(insert j s)).piecewise f g = (insert j ↑s).piecewise f g

Tactic:
ext

Result:
case h
ι : Type u_1
π : ι → Sort u_2
s : Finset ι
f g : (i : ι) → π i
inst✝² : (j : ι) → Decidable (j ∈ s)
inst✝¹ : DecidableEq ι
j : ι
inst✝ : (i : ι) → Decidable (i ∈ insert j s)
x✝ : ι
⊢ (↑(insert j s)).piecewise f g x✝ = (insert j ↑s).piecewise f g x✝

Proof state:
case h
ι : Type u_1
π : ι → Sort u_2
s : Finset ι
f g : (i : ι) → π i
inst✝² : (j : ι) → Decidable (j ∈ s)
inst✝¹ : DecidableEq ι
j : ι
inst✝ : (i : ι) → Decidable (i ∈ insert j s)
x✝ : ι
⊢ (↑(insert j s)).piecewise f g x✝ = (insert j ↑s).piecewise f g x✝

Tactic:
congr

Result:
case h.e_s
ι : Type u_1
π : ι → Sort u_2
s : Finset ι
f g : (i : ι) → π i
inst✝² : (j : ι) → Decidable (j ∈ s)
inst✝¹ : DecidableEq ι
j : ι
inst✝ : (i : ι) → Decidable (i ∈ insert j s)
x✝ : ι
⊢ ↑(insert j s) = insert j ↑s

Proof state:
ι : Type u_1
π : ι → Sort u_2
s : Finset ι
f g : (i : ι) → π i
inst✝² : (j : ι) → Decidable (j ∈ s)
inst✝¹ : DecidableEq ι
j : ι
inst✝ : (i : ι) → Decidable (i ∈ insert j s)
⊢ (insert j s).piecewise f g = update (s.piecewise f g) j (f j)

Tactic:
classical simp only [← piecewise_coe, coe_insert, ← Set.piecewise_insert]

Result:
ι : Type u_1
π : ι → Sort u_2
s : Finset ι
f g : (i : ι) → π i
inst✝² : (j : ι) → Decidable (j ∈ s)
inst✝¹ : DecidableEq ι
j : ι
inst✝ : (i : ι) → Decidable (i ∈ insert j s)
⊢ (↑(insert j s)).piecewise f g = (insert j ↑s).piecewise f g

Proof state:
ι : Type u_1
π : ι → Sort u_2
s : Finset ι
f g : (i : ι) → π i
inst✝² : (j : ι) → Decidable (j ∈ s)
inst✝¹ : DecidableEq ι
j : ι
inst✝ : (i : ι) → Decidable (i ∈ insert j s)
⊢ (insert j s).piecewise f g = update (s.piecewise f g) j (f j)

Tactic:
simp only [← piecewise_coe, coe_insert, ← Set.piecewise_insert]

Result:
ι : Type u_1
π : ι → Sort u_2
s : Finset ι
f g : (i : ι) → π i
inst✝² : (j : ι) → Decidable (j ∈ s)
inst✝¹ : DecidableEq ι
j : ι
inst✝ : (i : ι) → Decidable (i ∈ insert j s)
⊢ (↑(insert j s)).piecewise f g = (insert j ↑s).piecewise f g

Proof state:
case h.e_s
ι : Type u_1
π : ι → Sort u_2
s : Finset ι
f g : (i : ι) → π i
inst✝² : (j : ι) → Decidable (j ∈ s)
inst✝¹ : DecidableEq ι
j : ι
inst✝ : (i : ι) → Decidable (i ∈ insert j s)
x✝ : ι
⊢ ↑(insert j s) = insert j ↑s

Tactic:
simp

Result:
no goals
-- Mathlib/Algebra/Polynomial/Bivariate.lean
@[simp]
lemma evalEval_one (x y : R) : (1 : R[X][Y]).evalEval x y = 1

Proof state:
R : Type u_1
inst✝ : Semiring R
x y : R
⊢ evalEval x y 1 = 1

Tactic:
simp only [evalEval, eval_one]

Result:
no goals
-- Mathlib/SetTheory/ZFC/Basic.lean
theorem choice_mem (h : ∅ ∉ x) (y : ZFSet.{u}) (yx : y ∈ x) :
    (choice x ′ y : Class.{u}) ∈ (y : Class.{u})

Proof state:
x : ZFSet.{u}
h : ∅ ∉ x
y : ZFSet.{u}
yx : y ∈ x
⊢ ↑x.choice ′ ↑y ∈ ↑y

Tactic:
delta choice

Result:
x : ZFSet.{u}
h : ∅ ∉ x
y : ZFSet.{u}
yx : y ∈ x
⊢ ↑(map (fun y => Classical.epsilon fun z => z ∈ y) x) ′ ↑y ∈ ↑y

Proof state:
x : ZFSet.{u}
h : ∅ ∉ x
y : ZFSet.{u}
yx : y ∈ x
⊢ ↑(map (fun y => Classical.epsilon fun z => z ∈ y) x) ′ ↑y ∈ ↑y

Tactic:
rw [@map_fval _ (Classical.allZFSetDefinable _) x y yx, Class.coe_mem, Class.coe_apply]

Result:
x : ZFSet.{u}
h : ∅ ∉ x
y : ZFSet.{u}
yx : y ∈ x
⊢ (Classical.epsilon fun z => z ∈ y) ∈ y

Proof state:
x : ZFSet.{u}
h : ∅ ∉ x
y : ZFSet.{u}
yx : y ∈ x
⊢ (Classical.epsilon fun z => z ∈ y) ∈ y

Tactic:
exact choice_mem_aux x h y yx

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/ContinuousFunctionalCalculus/PosPart.lean
@[simp]
lemma posPart_one : (1 : A)⁺ = 1

Proof state:
A : Type u_1
inst✝⁵ : Ring A
inst✝⁴ : Algebra ℝ A
inst✝³ : StarRing A
inst✝² : TopologicalSpace A
inst✝¹ : ContinuousFunctionalCalculus ℝ IsSelfAdjoint
inst✝ : T2Space A
⊢ 1⁺ = 1

Tactic:
rw [CFC.posPart_def, cfcₙ_eq_cfc]

Result:
A : Type u_1
inst✝⁵ : Ring A
inst✝⁴ : Algebra ℝ A
inst✝³ : StarRing A
inst✝² : TopologicalSpace A
inst✝¹ : ContinuousFunctionalCalculus ℝ IsSelfAdjoint
inst✝ : T2Space A
⊢ cfc (fun x => x⁺) 1 = 1

Proof state:
A : Type u_1
inst✝⁵ : Ring A
inst✝⁴ : Algebra ℝ A
inst✝³ : StarRing A
inst✝² : TopologicalSpace A
inst✝¹ : ContinuousFunctionalCalculus ℝ IsSelfAdjoint
inst✝ : T2Space A
⊢ cfc (fun x => x⁺) 1 = 1

Tactic:
simp

Result:
no goals