harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Analysis/InnerProductSpace/OfNorm.lean
theorem rat_prop (r : ℚ) : innerProp' E (r : 𝕜)

Proof state:
𝕜 : Type u_1
inst✝³ : RCLike 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : InnerProductSpaceable E
r : ℚ
x y : E
⊢ inner_ 𝕜 (↑r • x) y = (starRingEnd 𝕜) ↑r * inner_ 𝕜 x y

Tactic:
let hom : 𝕜 →ₗ[ℚ] 𝕜 := AddMonoidHom.toRatLinearMap <|
  AddMonoidHom.mk' (fun r ↦ inner_ 𝕜 (r • x) y) <| fun a b ↦ by
    simpa [add_smul] using add_left (a • x) (b • x) y

Result:
𝕜 : Type u_1
inst✝³ : RCLike 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : InnerProductSpaceable E
r : ℚ
x y : E
hom : 𝕜 →ₗ[ℚ] 𝕜 := (AddMonoidHom.mk' (fun r => inner_ 𝕜 (r • x) y) ⋯).toRatLinearMap
⊢ inner_ 𝕜 (↑r • x) y = (starRingEnd 𝕜) ↑r * inner_ 𝕜 x y

Proof state:
𝕜 : Type u_1
inst✝³ : RCLike 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : InnerProductSpaceable E
r : ℚ
x y : E
hom : 𝕜 →ₗ[ℚ] 𝕜 := (AddMonoidHom.mk' (fun r => inner_ 𝕜 (r • x) y) ⋯).toRatLinearMap
⊢ inner_ 𝕜 (↑r • x) y = (starRingEnd 𝕜) ↑r * inner_ 𝕜 x y

Tactic:
simpa [hom, Rat.smul_def] using map_smul hom r 1

Result:
no goals

Proof state:
𝕜 : Type u_1
inst✝³ : RCLike 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : InnerProductSpaceable E
r : ℚ
x y : E
a b : 𝕜
⊢ (fun r => inner_ 𝕜 (r • x) y) (a + b) = (fun r => inner_ 𝕜 (r • x) y) a + (fun r => inner_ 𝕜 (r • x) y) b

Tactic:
simpa [add_smul] using add_left (a • x) (b • x) y

Result:
no goals

Proof state:
𝕜 : Type u_1
inst✝³ : RCLike 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : InnerProductSpaceable E
r : ℚ
⊢ InnerProductSpaceable.innerProp' E ↑r

Tactic:
intro x y

Result:
𝕜 : Type u_1
inst✝³ : RCLike 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : InnerProductSpaceable E
r : ℚ
x y : E
⊢ inner_ 𝕜 (↑r • x) y = (starRingEnd 𝕜) ↑r * inner_ 𝕜 x y
-- Mathlib/AlgebraicGeometry/EllipticCurve/Affine.lean
@[simp]
lemma slope_of_Y_ne {x₁ x₂ y₁ y₂ : F} (hx : x₁ = x₂) (hy : y₁ ≠ W.negY x₂ y₂) :
    W.slope x₁ x₂ y₁ y₂ =
      (3 * x₁ ^ 2 + 2 * W.a₂ * x₁ + W.a₄ - W.a₁ * y₁) / (y₁ - W.negY x₁ y₁)

Proof state:
F : Type u
inst✝ : Field F
W : Affine F
x₁ x₂ y₁ y₂ : F
hx : x₁ = x₂
hy : y₁ ≠ W.negY x₂ y₂
⊢ W.slope x₁ x₂ y₁ y₂ = (3 * x₁ ^ 2 + 2 * W.a₂ * x₁ + W.a₄ - W.a₁ * y₁) / (y₁ - W.negY x₁ y₁)

Tactic:
rw [slope, if_pos hx, if_neg hy]

Result:
no goals
-- Mathlib/Combinatorics/SetFamily/Compression/UV.lean
theorem compress_idem (u v a : α) : compress u v (compress u v a) = compress u v a

Proof state:
α : Type u_1
inst✝² : GeneralizedBooleanAlgebra α
inst✝¹ : DecidableRel Disjoint
inst✝ : DecidableRel fun x1 x2 => x1 ≤ x2
u v a : α
⊢ compress u v (compress u v a) = compress u v a

Tactic:
unfold compress

Result:
α : Type u_1
inst✝² : GeneralizedBooleanAlgebra α
inst✝¹ : DecidableRel Disjoint
inst✝ : DecidableRel fun x1 x2 => x1 ≤ x2
u v a : α
⊢ (if
        Disjoint u (if Disjoint u a ∧ v ≤ a then (a ⊔ u) \ v else a) ∧
          v ≤ if Disjoint u a ∧ v ≤ a then (a ⊔ u) \ v else a then
      ((if Disjoint u a ∧ v ≤ a then (a ⊔ u) \ v else a) ⊔ u) \ v
    else if Disjoint u a ∧ v ≤ a then (a ⊔ u) \ v else a) =
    if Disjoint u a ∧ v ≤ a then (a ⊔ u) \ v else a

Proof state:
case neg
α : Type u_1
inst✝² : GeneralizedBooleanAlgebra α
inst✝¹ : DecidableRel Disjoint
inst✝ : DecidableRel fun x1 x2 => x1 ≤ x2
u v a : α
h : Disjoint u a ∧ v ≤ a
h' : ¬(Disjoint u ((a ⊔ u) \ v) ∧ v ≤ (a ⊔ u) \ v)
⊢ (a ⊔ u) \ v = (a ⊔ u) \ v

Tactic:
rfl

Result:
no goals

Proof state:
case neg
α : Type u_1
inst✝² : GeneralizedBooleanAlgebra α
inst✝¹ : DecidableRel Disjoint
inst✝ : DecidableRel fun x1 x2 => x1 ≤ x2
u v a : α
h : ¬(Disjoint u a ∧ v ≤ a)
⊢ a = a

Tactic:
rfl

Result:
no goals

Proof state:
case pos
α : Type u_1
inst✝² : GeneralizedBooleanAlgebra α
inst✝¹ : DecidableRel Disjoint
inst✝ : DecidableRel fun x1 x2 => x1 ≤ x2
u v a : α
h : Disjoint u a ∧ v ≤ a
h' : Disjoint u ((a ⊔ u) \ v) ∧ v ≤ (a ⊔ u) \ v
⊢ ((a ⊔ u) \ v ⊔ u) \ v = (a ⊔ u) \ v

Tactic:
rw [le_sdiff_right.1 h'.2, sdiff_bot, sdiff_bot, sup_assoc, sup_idem]

Result:
no goals

Proof state:
α : Type u_1
inst✝² : GeneralizedBooleanAlgebra α
inst✝¹ : DecidableRel Disjoint
inst✝ : DecidableRel fun x1 x2 => x1 ≤ x2
u v a : α
⊢ (if
        Disjoint u (if Disjoint u a ∧ v ≤ a then (a ⊔ u) \ v else a) ∧
          v ≤ if Disjoint u a ∧ v ≤ a then (a ⊔ u) \ v else a then
      ((if Disjoint u a ∧ v ≤ a then (a ⊔ u) \ v else a) ⊔ u) \ v
    else if Disjoint u a ∧ v ≤ a then (a ⊔ u) \ v else a) =
    if Disjoint u a ∧ v ≤ a then (a ⊔ u) \ v else a

Tactic:
split_ifs with h h'

Result:
case pos
α : Type u_1
inst✝² : GeneralizedBooleanAlgebra α
inst✝¹ : DecidableRel Disjoint
inst✝ : DecidableRel fun x1 x2 => x1 ≤ x2
u v a : α
h : Disjoint u a ∧ v ≤ a
h' : Disjoint u ((a ⊔ u) \ v) ∧ v ≤ (a ⊔ u) \ v
⊢ ((a ⊔ u) \ v ⊔ u) \ v = (a ⊔ u) \ v

case neg
α : Type u_1
inst✝² : GeneralizedBooleanAlgebra α
inst✝¹ : DecidableRel Disjoint
inst✝ : DecidableRel fun x1 x2 => x1 ≤ x2
u v a : α
h : Disjoint u a ∧ v ≤ a
h' : ¬(Disjoint u ((a ⊔ u) \ v) ∧ v ≤ (a ⊔ u) \ v)
⊢ (a ⊔ u) \ v = (a ⊔ u) \ v

case neg
α : Type u_1
inst✝² : GeneralizedBooleanAlgebra α
inst✝¹ : DecidableRel Disjoint
inst✝ : DecidableRel fun x1 x2 => x1 ≤ x2
u v a : α
h : ¬(Disjoint u a ∧ v ≤ a)
⊢ a = a
-- Mathlib/Control/Traversable/Lemmas.lean
theorem traverse_id : traverse pure = (pure : t α → Id (t α))

Proof state:
t : Type u → Type u
inst✝¹ : Traversable t
inst✝ : LawfulTraversable t
α : Type u
⊢ traverse pure = pure

Tactic:
ext

Result:
case h
t : Type u → Type u
inst✝¹ : Traversable t
inst✝ : LawfulTraversable t
α : Type u
x✝ : t α
⊢ traverse pure x✝ = pure x✝

Proof state:
case h
t : Type u → Type u
inst✝¹ : Traversable t
inst✝ : LawfulTraversable t
α : Type u
x✝ : t α
⊢ traverse pure x✝ = pure x✝

Tactic:
exact id_traverse _

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem filter_append {p : α → Bool} (l₁ l₂ : Array α) :
    filter p (l₁ ++ l₂) = filter p l₁ ++ filter p l₂

Proof state:
α : Type u_1
p : α → Bool
l₁ l₂ : Array α
⊢ filter p (l₁ ++ l₂) = filter p l₁ ++ filter p l₂

Tactic:
rcases l₁ with ⟨l₁⟩

Result:
case mk
α : Type u_1
p : α → Bool
l₂ : Array α
l₁ : List α
⊢ filter p ({ toList := l₁ } ++ l₂) = filter p { toList := l₁ } ++ filter p l₂

Proof state:
case mk
α : Type u_1
p : α → Bool
l₂ : Array α
l₁ : List α
⊢ filter p ({ toList := l₁ } ++ l₂) = filter p { toList := l₁ } ++ filter p l₂

Tactic:
rcases l₂ with ⟨l₂⟩

Result:
case mk.mk
α : Type u_1
p : α → Bool
l₁ l₂ : List α
⊢ filter p ({ toList := l₁ } ++ { toList := l₂ }) = filter p { toList := l₁ } ++ filter p { toList := l₂ }

Proof state:
case mk.mk
α : Type u_1
p : α → Bool
l₁ l₂ : List α
⊢ filter p ({ toList := l₁ } ++ { toList := l₂ }) = filter p { toList := l₁ } ++ filter p { toList := l₂ }

Tactic:
simp [List.filter_append]

Result:
no goals
-- Mathlib/GroupTheory/SpecificGroups/Quaternion.lean
theorem a_one_pow (k : ℕ) : (a 1 : QuaternionGroup n) ^ k = a k

Proof state:
case zero
n : ℕ
⊢ a 1 ^ 0 = a ↑0

Tactic:
rw [Nat.cast_zero]

Result:
case zero
n : ℕ
⊢ a 1 ^ 0 = a 0

Proof state:
case zero
n : ℕ
⊢ a 1 ^ 0 = a 0

Tactic:
rfl

Result:
no goals

Proof state:
case succ
n k : ℕ
IH : a 1 ^ k = a ↑k
⊢ a (↑k + 1) = a ↑(k + 1)

Tactic:
congr 1

Result:
case succ.e_a
n k : ℕ
IH : a 1 ^ k = a ↑k
⊢ ↑k + 1 = ↑(k + 1)

Proof state:
case succ.e_a
n k : ℕ
IH : a 1 ^ k = a ↑k
⊢ ↑k + 1 = ↑(k + 1)

Tactic:
norm_cast

Result:
no goals

Proof state:
n k : ℕ
⊢ a 1 ^ k = a ↑k

Tactic:
induction' k with k IH

Result:
case zero
n : ℕ
⊢ a 1 ^ 0 = a ↑0

case succ
n k : ℕ
IH : a 1 ^ k = a ↑k
⊢ a 1 ^ (k + 1) = a ↑(k + 1)

Proof state:
case succ
n k : ℕ
IH : a 1 ^ k = a ↑k
⊢ a 1 ^ (k + 1) = a ↑(k + 1)

Tactic:
rw [pow_succ, IH, a_mul_a]

Result:
case succ
n k : ℕ
IH : a 1 ^ k = a ↑k
⊢ a (↑k + 1) = a ↑(k + 1)
-- Mathlib/MeasureTheory/Integral/RieszMarkovKakutani/Basic.lean
theorem rieszContentAux_sup_le (K1 K2 : Compacts X) :
    rieszContentAux Λ (K1 ⊔ K2) ≤ rieszContentAux Λ K1 + rieszContentAux Λ K2

Proof state:
X : Type u_1
inst✝² : TopologicalSpace X
Λ : (X →C_c ℝ≥0) →ₗ[ℝ≥0] ℝ≥0
inst✝¹ : T2Space X
inst✝ : LocallyCompactSpace X
K1 K2 : Compacts X
ε : ℝ≥0
εpos : 0 < ε
f1 : X →C_c ℝ≥0
f_test_function_K1 : (∀ x ∈ K1, 1 ≤ f1 x) ∧ Λ f1 < rieszContentAux Λ K1 + ε / 2
f2 : X →C_c ℝ≥0
f_test_function_K2 : (∀ x ∈ K2, 1 ≤ f2 x) ∧ Λ f2 < rieszContentAux Λ K2 + ε / 2
f_test_function_union : ∀ x ∈ K1 ⊔ K2, 1 ≤ (f1 + f2) x
⊢ Λ f1 + Λ f2 < rieszContentAux Λ K1 + rieszContentAux Λ K2 + ε

Tactic:
apply lt_of_lt_of_le (_root_.add_lt_add f_test_function_K1.right f_test_function_K2.right)
  (le_of_eq _)

Result:
X : Type u_1
inst✝² : TopologicalSpace X
Λ : (X →C_c ℝ≥0) →ₗ[ℝ≥0] ℝ≥0
inst✝¹ : T2Space X
inst✝ : LocallyCompactSpace X
K1 K2 : Compacts X
ε : ℝ≥0
εpos : 0 < ε
f1 : X →C_c ℝ≥0
f_test_function_K1 : (∀ x ∈ K1, 1 ≤ f1 x) ∧ Λ f1 < rieszContentAux Λ K1 + ε / 2
f2 : X →C_c ℝ≥0
f_test_function_K2 : (∀ x ∈ K2, 1 ≤ f2 x) ∧ Λ f2 < rieszContentAux Λ K2 + ε / 2
f_test_function_union : ∀ x ∈ K1 ⊔ K2, 1 ≤ (f1 + f2) x
⊢ rieszContentAux Λ K1 + ε / 2 + (rieszContentAux Λ K2 + ε / 2) = rieszContentAux Λ K1 + rieszContentAux Λ K2 + ε

Proof state:
case h.intro
X : Type u_1
inst✝² : TopologicalSpace X
Λ : (X →C_c ℝ≥0) →ₗ[ℝ≥0] ℝ≥0
inst✝¹ : T2Space X
inst✝ : LocallyCompactSpace X
K1 K2 : Compacts X
ε : ℝ≥0
εpos : 0 < ε
f1 : X →C_c ℝ≥0
f_test_function_K1 : (∀ x ∈ K1, 1 ≤ f1 x) ∧ Λ f1 < rieszContentAux Λ K1 + ε / 2
⊢ rieszContentAux Λ (K1 ⊔ K2) ≤ rieszContentAux Λ K1 + rieszContentAux Λ K2 + ε

Tactic:
obtain ⟨f2, f_test_function_K2⟩ := exists_lt_rieszContentAux_add_pos Λ K2 (half_pos εpos)

Result:
case h.intro.intro
X : Type u_1
inst✝² : TopologicalSpace X
Λ : (X →C_c ℝ≥0) →ₗ[ℝ≥0] ℝ≥0
inst✝¹ : T2Space X
inst✝ : LocallyCompactSpace X
K1 K2 : Compacts X
ε : ℝ≥0
εpos : 0 < ε
f1 : X →C_c ℝ≥0
f_test_function_K1 : (∀ x ∈ K1, 1 ≤ f1 x) ∧ Λ f1 < rieszContentAux Λ K1 + ε / 2
f2 : X →C_c ℝ≥0
f_test_function_K2 : (∀ x ∈ K2, 1 ≤ f2 x) ∧ Λ f2 < rieszContentAux Λ K2 + ε / 2
⊢ rieszContentAux Λ (K1 ⊔ K2) ≤ rieszContentAux Λ K1 + rieszContentAux Λ K2 + ε
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/RawLemmas.lean
theorem get_alter (h : m.1.WF) {k k' : α} {f : Option β → Option β}
    (hc : (Const.alter m k f).contains k') :
    Const.get (Const.alter m k f) k' hc =
      if heq : k == k' then
        haveI h' : (f (Const.get? m k)).isSome

Proof state:
α : Type u
β✝ : α → Type v
m✝ : Raw₀ α β✝
inst✝³ : BEq α
inst✝² : Hashable α
β : Type v
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
m : Raw₀ α fun x => β
h : m.val.WF
k k' : α
f : Option β → Option β
hc : (alter m k f).contains k' = true
heq : ¬(k == k') = true
⊢ m.contains k' = true

Tactic:
rwa [contains_alter _ h, if_neg heq] at hc

Result:
no goals

Proof state:
α : Type u
inst✝³ : BEq α
inst✝² : Hashable α
β : Type v
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
m : Raw₀ α fun x => β
h : m.val.WF
k k' : α
f : Option β → Option β
hc : (alter m k f).contains k' = true
⊢ get (alter m k f) k' hc = if heq : (k == k') = true then (f (get? m k)).get ⋯ else get m k' ⋯

Tactic:
simp_to_model [Const.alter] using List.Const.getValue_alterKey

Result:
no goals

Proof state:
α : Type u
β✝ : α → Type v
m✝ : Raw₀ α β✝
inst✝³ : BEq α
inst✝² : Hashable α
β : Type v
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
m : Raw₀ α fun x => β
h : m.val.WF
k k' : α
f : Option β → Option β
hc : (alter m k f).contains k' = true
heq : (k == k') = true
⊢ (f (get? m k)).isSome = true

Tactic:
rwa [contains_alter _ h, if_pos heq] at hc

Result:
no goals
-- Mathlib/MeasureTheory/Measure/AddContent.lean
/-- An `addContent C` on a `SetSemiring C` is sub-additive. -/
lemma addContent_sUnion_le_sum {m : AddContent C} (hC : IsSetSemiring C)
    (J : Finset (Set α)) (h_ss : ↑J ⊆ C) (h_mem : ⋃₀ ↑J ∈ C) :
    m (⋃₀ ↑J) ≤ ∑ u ∈ J, m u

Proof state:
α : Type u_1
C : Set (Set α)
m : AddContent C
hC : IsSetSemiring C
J : Finset (Set α)
h_ss : ↑J ⊆ C
h_mem : ⋃₀ ↑J ∈ C
h1 : ↑(J.disjiUnion (hC.disjointOfUnion h_ss) ⋯) ⊆ C
h2 : (↑(J.disjiUnion (hC.disjointOfUnion h_ss) ⋯)).PairwiseDisjoint id
⊢ m (⋃₀ ↑J) ≤ ∑ u ∈ J, m u

Tactic:
have h3 : ⋃₀ J = ⋃₀ ((disjiUnion J (hC.disjointOfUnion h_ss)
    (hC.pairwiseDisjoint_disjointOfUnion h_ss)) : Set (Set α)) := by
  simp only [disjiUnion_eq_biUnion, coe_biUnion, mem_coe]
  exact (Exists.choose_spec (hC.disjointOfUnion_props h_ss)).2.2.2.2.2

Result:
α : Type u_1
C : Set (Set α)
m : AddContent C
hC : IsSetSemiring C
J : Finset (Set α)
h_ss : ↑J ⊆ C
h_mem : ⋃₀ ↑J ∈ C
h1 : ↑(J.disjiUnion (hC.disjointOfUnion h_ss) ⋯) ⊆ C
h2 : (↑(J.disjiUnion (hC.disjointOfUnion h_ss) ⋯)).PairwiseDisjoint id
h3 : ⋃₀ ↑J = ⋃₀ ↑(J.disjiUnion (hC.disjointOfUnion h_ss) ⋯)
⊢ m (⋃₀ ↑J) ≤ ∑ u ∈ J, m u

Proof state:
α : Type u_1
C : Set (Set α)
m : AddContent C
hC : IsSetSemiring C
J : Finset (Set α)
h_ss : ↑J ⊆ C
h_mem : ⋃₀ ↑J ∈ C
h1 : ↑(J.disjiUnion (hC.disjointOfUnion h_ss) ⋯) ⊆ C
⊢ (↑(J.disjiUnion (hC.disjointOfUnion h_ss) ⋯)).PairwiseDisjoint id

Tactic:
simp only [disjiUnion_eq_biUnion, coe_biUnion, mem_coe]

Result:
α : Type u_1
C : Set (Set α)
m : AddContent C
hC : IsSetSemiring C
J : Finset (Set α)
h_ss : ↑J ⊆ C
h_mem : ⋃₀ ↑J ∈ C
h1 : ↑(J.disjiUnion (hC.disjointOfUnion h_ss) ⋯) ⊆ C
⊢ (⋃ x ∈ J, ↑(hC.disjointOfUnion h_ss x)).PairwiseDisjoint id

Proof state:
α : Type u_1
C : Set (Set α)
m : AddContent C
hC : IsSetSemiring C
J : Finset (Set α)
h_ss : ↑J ⊆ C
h_mem : ⋃₀ ↑J ∈ C
⊢ ∀ i ∈ J, ↑(hC.disjointOfUnion h_ss i) ⊆ C

Tactic:
exact fun _ x ↦ hC.disjointOfUnion_subset h_ss x

Result:
no goals
-- Mathlib/RingTheory/PrincipalIdealDomain.lean
theorem exists_gcd_eq_mul_add_mul (a b : R) : ∃ x y, gcd a b = a * x + b * y

Proof state:
R : Type u
inst✝³ : CommRing R
inst✝² : IsBezout R
inst✝¹ : IsDomain R
inst✝ : GCDMonoid R
a b : R
⊢ ∃ x y, gcd a b = a * x + b * y

Tactic:
rw [← gcd_dvd_iff_exists]

Result:
no goals
-- Mathlib/Data/Nat/Init.lean
lemma le_succ_iff : m ≤ n.succ ↔ m ≤ n ∨ m = n.succ

Proof state:
m n : ℕ
⊢ m ≤ n.succ ↔ m ≤ n ∨ m = n.succ

Tactic:
refine ⟨fun hmn ↦ (Nat.lt_or_eq_of_le hmn).imp_left le_of_lt_succ, ?_⟩

Result:
m n : ℕ
⊢ m ≤ n ∨ m = n.succ → m ≤ n.succ

Proof state:
case inl
m n : ℕ
hmn : m ≤ n
⊢ m ≤ n.succ

Tactic:
exact le_succ_of_le hmn

Result:
no goals

Proof state:
case inr
n : ℕ
⊢ n.succ ≤ n.succ

Tactic:
exact Nat.le_refl _

Result:
no goals

Proof state:
m n : ℕ
⊢ m ≤ n ∨ m = n.succ → m ≤ n.succ

Tactic:
rintro (hmn | rfl)

Result:
case inl
m n : ℕ
hmn : m ≤ n
⊢ m ≤ n.succ

case inr
n : ℕ
⊢ n.succ ≤ n.succ
-- Mathlib/Data/List/Basic.lean
theorem forall_mem_iff_getElem {l : List α} {p : α → Prop} :
    (∀ x ∈ l, p x) ↔ ∀ (i : ℕ) (_ : i < l.length), p l[i]

Proof state:
α : Type u
l : List α
p : α → Prop
⊢ (∀ (x : α), x ∈ l → p x) ↔ ∀ (i : ℕ) (x : i < l.length), p l[i]

Tactic:
simp [mem_iff_getElem, @forall_swap α]

Result:
no goals
-- Mathlib/Topology/MetricSpace/Pseudo/Constructions.lean
@[simp]
lemma NNReal.nndist_zero_eq_val' (z : ℝ≥0) : nndist z 0 = z

Proof state:
z : ℝ≥0
⊢ nndist z 0 = z

Tactic:
rw [nndist_comm]

Result:
z : ℝ≥0
⊢ nndist 0 z = z

Proof state:
z : ℝ≥0
⊢ nndist 0 z = z

Tactic:
exact NNReal.nndist_zero_eq_val z

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Nat/Linear.lean
theorem Poly.denote_mul (ctx : Context) (k : Nat) (p : Poly) : (p.mul k).denote ctx = k * p.denote ctx

Proof state:
ctx : Context
k : Nat
p : Poly
⊢ denote ctx (bif k == 0 then [] else bif k == 1 then p else mul.go k p) = k * denote ctx p

Tactic:
by_cases h : k == 0 <;> simp [h]

Result:
case pos
ctx : Context
k : Nat
p : Poly
h : (k == 0) = true
⊢ 0 = k * denote ctx p

case neg
ctx : Context
k : Nat
p : Poly
h : ¬(k == 0) = true
⊢ denote ctx (bif k == 1 then p else mul.go k p) = k * denote ctx p

Proof state:
case neg.cons
ctx : Context
k : Nat
h✝ : ¬(k == 0) = true
h : ¬(k == 1) = true
kv : Nat × Var
m : List (Nat × Var)
ih : denote ctx (mul.go k m) = k * denote ctx m
⊢ denote ctx (mul.go k (kv :: m)) = k * denote ctx (kv :: m)

Tactic:
cases kv with | _ k' v => simp [ih]

Result:
no goals

Proof state:
case neg.cons.mk
ctx : Context
k : Nat
h✝ : ¬(k == 0) = true
h : ¬(k == 1) = true
m : List (Nat × Var)
ih : denote ctx (mul.go k m) = k * denote ctx m
k' : Nat
v : Var
⊢ denote ctx (mul.go k ((k', v) :: m)) = k * denote ctx ((k', v) :: m)

Tactic:
simp [ih]

Result:
no goals

Proof state:
ctx : Context
k : Nat
p : Poly
⊢ denote ctx (mul k p) = k * denote ctx p

Tactic:
simp

Result:
ctx : Context
k : Nat
p : Poly
⊢ denote ctx (bif k == 0 then [] else bif k == 1 then p else mul.go k p) = k * denote ctx p

Proof state:
case pos
ctx : Context
k : Nat
p : Poly
h : (k == 0) = true
⊢ 0 = k * denote ctx p

case neg
ctx : Context
k : Nat
p : Poly
h : ¬(k == 0) = true
⊢ denote ctx (bif k == 1 then p else mul.go k p) = k * denote ctx p

Tactic:
simp [eq_of_beq h]

Result:
case neg
ctx : Context
k : Nat
p : Poly
h : ¬(k == 0) = true
⊢ denote ctx (bif k == 1 then p else mul.go k p) = k * denote ctx p

Proof state:
case pos
ctx : Context
k : Nat
p : Poly
h✝ : ¬(k == 0) = true
h : (k == 1) = true
⊢ denote ctx p = k * denote ctx p

case neg
ctx : Context
k : Nat
p : Poly
h✝ : ¬(k == 0) = true
h : ¬(k == 1) = true
⊢ denote ctx (mul.go k p) = k * denote ctx p

Tactic:
simp [eq_of_beq h]

Result:
case neg
ctx : Context
k : Nat
p : Poly
h✝ : ¬(k == 0) = true
h : ¬(k == 1) = true
⊢ denote ctx (mul.go k p) = k * denote ctx p

Proof state:
case neg
ctx : Context
k : Nat
p : Poly
h✝ : ¬(k == 0) = true
h : ¬(k == 1) = true
⊢ denote ctx (mul.go k p) = k * denote ctx p

Tactic:
induction p with
| nil  => simp
| cons kv m ih => cases kv with | _ k' v => simp [ih]

Result:
no goals

Proof state:
case neg
ctx : Context
k : Nat
p : Poly
h : ¬(k == 0) = true
⊢ denote ctx (bif k == 1 then p else mul.go k p) = k * denote ctx p

Tactic:
by_cases h : k == 1 <;> simp [h]

Result:
case pos
ctx : Context
k : Nat
p : Poly
h✝ : ¬(k == 0) = true
h : (k == 1) = true
⊢ denote ctx p = k * denote ctx p

case neg
ctx : Context
k : Nat
p : Poly
h✝ : ¬(k == 0) = true
h : ¬(k == 1) = true
⊢ denote ctx (mul.go k p) = k * denote ctx p

Proof state:
case neg.nil
ctx : Context
k : Nat
h✝ : ¬(k == 0) = true
h : ¬(k == 1) = true
⊢ denote ctx (mul.go k []) = k * denote ctx []

Tactic:
simp

Result:
no goals
-- Mathlib/Algebra/Module/Submodule/Lattice.lean
theorem subsingleton_iff : Subsingleton (Submodule R M) ↔ Subsingleton M :=
  have h : Subsingleton (Submodule R M) ↔ Subsingleton (AddSubmonoid M)

Proof state:
R : Type u_1
M : Type u_3
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
⊢ Subsingleton (Submodule R M) ↔ Subsingleton (AddSubmonoid M)

Tactic:
rw [← subsingleton_iff_bot_eq_top, ← subsingleton_iff_bot_eq_top, ← toAddSubmonoid_inj,
  bot_toAddSubmonoid, top_toAddSubmonoid]

Result:
no goals
-- Mathlib/RingTheory/Henselian.lean
theorem HenselianLocalRing.TFAE (R : Type u) [CommRing R] [IsLocalRing R] :
    TFAE
      [HenselianLocalRing R,
        ∀ f : R[X], f.Monic → ∀ a₀ : ResidueField R, aeval a₀ f = 0 →
          aeval a₀ (derivative f) ≠ 0 → ∃ a : R, f.IsRoot a ∧ residue R a = a₀,
        ∀ {K : Type u} [Field K],
          ∀ (φ : R →+* K), Surjective φ → ∀ f : R[X], f.Monic → ∀ a₀ : K,
            f.eval₂ φ a₀ = 0 → f.derivative.eval₂ φ a₀ ≠ 0 → ∃ a : R, f.IsRoot a ∧ φ a = a₀]

Proof state:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsLocalRing R
⊢ [HenselianLocalRing R,
      ∀ (f : R[X]),
        f.Monic →
          ∀ (a₀ : ResidueField R),
            (aeval a₀) f = 0 → (aeval a₀) (derivative f) ≠ 0 → ∃ a, f.IsRoot a ∧ (residue R) a = a₀,
      ∀ {K : Type u} [inst : Field K] (φ : R →+* K),
        Surjective ⇑φ →
          ∀ (f : R[X]),
            f.Monic → ∀ (a₀ : K), eval₂ φ a₀ f = 0 → eval₂ φ a₀ (derivative f) ≠ 0 → ∃ a, f.IsRoot a ∧ φ a = a₀].TFAE

Tactic:
tfae_have 3 → 2
| H => H (residue R) Ideal.Quotient.mk_surjective

Result:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsLocalRing R
tfae_3_to_2 :
  (∀ {K : Type u} [inst : Field K] (φ : R →+* K),
      Surjective ⇑φ →
        ∀ (f : R[X]),
          f.Monic → ∀ (a₀ : K), eval₂ φ a₀ f = 0 → eval₂ φ a₀ (derivative f) ≠ 0 → ∃ a, f.IsRoot a ∧ φ a = a₀) →
    ∀ (f : R[X]),
      f.Monic →
        ∀ (a₀ : ResidueField R), (aeval a₀) f = 0 → (aeval a₀) (derivative f) ≠ 0 → ∃ a, f.IsRoot a ∧ (residue R) a = a₀
⊢ [HenselianLocalRing R,
      ∀ (f : R[X]),
        f.Monic →
          ∀ (a₀ : ResidueField R),
            (aeval a₀) f = 0 → (aeval a₀) (derivative f) ≠ 0 → ∃ a, f.IsRoot a ∧ (residue R) a = a₀,
      ∀ {K : Type u} [inst : Field K] (φ : R →+* K),
        Surjective ⇑φ →
          ∀ (f : R[X]),
            f.Monic → ∀ (a₀ : K), eval₂ φ a₀ f = 0 → eval₂ φ a₀ (derivative f) ≠ 0 → ∃ a, f.IsRoot a ∧ φ a = a₀].TFAE
-- Mathlib/RingTheory/WittVector/Verschiebung.lean
theorem aeval_verschiebung_poly' (x : 𝕎 R) (n : ℕ) :
    aeval x.coeff (verschiebungPoly n) = (verschiebungFun x).coeff n

Proof state:
case succ
p : ℕ
R : Type u_1
inst✝ : CommRing R
x : 𝕎 R
n : ℕ
⊢ (aeval x.coeff) (verschiebungPoly (n + 1)) = x.verschiebungFun.coeff (n + 1)

Tactic:
rw [verschiebungPoly, verschiebungFun_coeff_succ, if_neg n.succ_ne_zero, aeval_X,
  add_tsub_cancel_right]

Result:
no goals

Proof state:
p : ℕ
R : Type u_1
inst✝ : CommRing R
x : 𝕎 R
n : ℕ
⊢ (aeval x.coeff) (verschiebungPoly n) = x.verschiebungFun.coeff n

Tactic:
rcases n with - | n

Result:
case zero
p : ℕ
R : Type u_1
inst✝ : CommRing R
x : 𝕎 R
⊢ (aeval x.coeff) (verschiebungPoly 0) = x.verschiebungFun.coeff 0

case succ
p : ℕ
R : Type u_1
inst✝ : CommRing R
x : 𝕎 R
n : ℕ
⊢ (aeval x.coeff) (verschiebungPoly (n + 1)) = x.verschiebungFun.coeff (n + 1)

Proof state:
case zero
p : ℕ
R : Type u_1
inst✝ : CommRing R
x : 𝕎 R
⊢ (aeval x.coeff) (verschiebungPoly 0) = x.verschiebungFun.coeff 0

Tactic:
simp only [verschiebungPoly, ite_true, map_zero, verschiebungFun_coeff_zero]

Result:
no goals
-- Mathlib/SetTheory/Ordinal/Arithmetic.lean
theorem mul_mod (x y : Ordinal) : x * y % x = 0

Proof state:
x y : Ordinal.{u_4}
⊢ x * y % x = 0

Tactic:
simpa using mul_add_mod_self x y 0

Result:
no goals
-- Mathlib/RingTheory/Polynomial/Dickson.lean
theorem dickson_two_one_eq_chebyshev_S : ∀ n, dickson 2 (1 : R) n = Chebyshev.S R n
  | 0 => by
    simp only [Chebyshev.S_zero, mul_one, one_comp, dickson_zero]
    norm_num
  | 1 => by
    rw [dickson_one, Nat.cast_one, Chebyshev.S_one]
  | n + 2 => by
    rw [dickson_add_two, C_1, Nat.cast_add, Nat.cast_two, Chebyshev.S_add_two,
      dickson_two_one_eq_chebyshev_S (n + 1), dickson_two_one_eq_chebyshev_S n]
    push_cast
    ring

Proof state:
R : Type u_1
inst✝ : CommRing R
n : ℕ
⊢ dickson 2 1 (n + 2) = Chebyshev.S R ↑(n + 2)

Tactic:
rw [dickson_add_two, C_1, Nat.cast_add, Nat.cast_two, Chebyshev.S_add_two,
  dickson_two_one_eq_chebyshev_S (n + 1), dickson_two_one_eq_chebyshev_S n]

Result:
R : Type u_1
inst✝ : CommRing R
n : ℕ
⊢ X * Chebyshev.S R ↑(n + 1) - 1 * Chebyshev.S R ↑n = X * Chebyshev.S R (↑n + 1) - Chebyshev.S R ↑n

Proof state:
R : Type u_1
inst✝ : CommRing R
⊢ dickson 2 1 1 = Chebyshev.S R ↑1

Tactic:
rw [dickson_one, Nat.cast_one, Chebyshev.S_one]

Result:
no goals

Proof state:
R : Type u_1
inst✝ : CommRing R
n : ℕ
⊢ X * Chebyshev.S R ↑(n + 1) - 1 * Chebyshev.S R ↑n = X * Chebyshev.S R (↑n + 1) - Chebyshev.S R ↑n

Tactic:
push_cast

Result:
R : Type u_1
inst✝ : CommRing R
n : ℕ
⊢ X * Chebyshev.S R (↑n + 1) - 1 * Chebyshev.S R ↑n = X * Chebyshev.S R (↑n + 1) - Chebyshev.S R ↑n

Proof state:
R : Type u_1
inst✝ : CommRing R
⊢ 3 - ↑2 = Chebyshev.S R ↑0

Tactic:
norm_num

Result:
no goals

Proof state:
R : Type u_1
inst✝ : CommRing R
n : ℕ
⊢ X * Chebyshev.S R (↑n + 1) - 1 * Chebyshev.S R ↑n = X * Chebyshev.S R (↑n + 1) - Chebyshev.S R ↑n

Tactic:
ring

Result:
no goals

Proof state:
R : Type u_1
inst✝ : CommRing R
⊢ dickson 2 1 0 = Chebyshev.S R ↑0

Tactic:
simp only [Chebyshev.S_zero, mul_one, one_comp, dickson_zero]

Result:
R : Type u_1
inst✝ : CommRing R
⊢ 3 - ↑2 = Chebyshev.S R ↑0