harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Order/TransfiniteIteration.lean
lemma transfiniteIterate_succ (i₀ : I) (j : J) (hj : ¬ IsMax j):
    transfiniteIterate φ (Order.succ j) i₀ =
      φ (transfiniteIterate φ j i₀)

Proof state:
I : Type u
inst✝³ : SupSet I
φ : I → I
J : Type w
inst✝² : LinearOrder J
inst✝¹ : SuccOrder J
inst✝ : WellFoundedLT J
i₀ : I
j : J
hj : ¬IsMax j
⊢ transfiniteIterate φ (Order.succ j) i₀ = φ (transfiniteIterate φ j i₀)

Tactic:
dsimp [transfiniteIterate]

Result:
I : Type u
inst✝³ : SupSet I
φ : I → I
J : Type w
inst✝² : LinearOrder J
inst✝¹ : SuccOrder J
inst✝ : WellFoundedLT J
i₀ : I
j : J
hj : ¬IsMax j
⊢ SuccOrder.limitRecOn (Order.succ j) (fun x x => id) (fun x x g => φ ∘ g) (fun y x h => ⨆ x, h ↑x ⋯) i₀ =
    φ (SuccOrder.limitRecOn j (fun x x => id) (fun x x g => φ ∘ g) (fun y x h => ⨆ x, h ↑x ⋯) i₀)

Proof state:
I : Type u
inst✝³ : SupSet I
φ : I → I
J : Type w
inst✝² : LinearOrder J
inst✝¹ : SuccOrder J
inst✝ : WellFoundedLT J
i₀ : I
j : J
hj : ¬IsMax j
⊢ (φ ∘ SuccOrder.limitRecOn j (fun x x => id) (fun x x g => φ ∘ g) fun y x h => ⨆ x, h ↑x ⋯) i₀ =
    φ (SuccOrder.limitRecOn j (fun x x => id) (fun x x g => φ ∘ g) (fun y x h => ⨆ x, h ↑x ⋯) i₀)

Tactic:
rfl

Result:
no goals

Proof state:
I : Type u
inst✝³ : SupSet I
φ : I → I
J : Type w
inst✝² : LinearOrder J
inst✝¹ : SuccOrder J
inst✝ : WellFoundedLT J
i₀ : I
j : J
hj : ¬IsMax j
⊢ SuccOrder.limitRecOn (Order.succ j) (fun x x => id) (fun x x g => φ ∘ g) (fun y x h => ⨆ x, h ↑x ⋯) i₀ =
    φ (SuccOrder.limitRecOn j (fun x x => id) (fun x x g => φ ∘ g) (fun y x h => ⨆ x, h ↑x ⋯) i₀)

Tactic:
rw [SuccOrder.limitRecOn_succ_of_not_isMax _ _ _ hj]

Result:
I : Type u
inst✝³ : SupSet I
φ : I → I
J : Type w
inst✝² : LinearOrder J
inst✝¹ : SuccOrder J
inst✝ : WellFoundedLT J
i₀ : I
j : J
hj : ¬IsMax j
⊢ (φ ∘ SuccOrder.limitRecOn j (fun x x => id) (fun x x g => φ ∘ g) fun y x h => ⨆ x, h ↑x ⋯) i₀ =
    φ (SuccOrder.limitRecOn j (fun x x => id) (fun x x g => φ ∘ g) (fun y x h => ⨆ x, h ↑x ⋯) i₀)
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Lemmas.lean
theorem getElem_eq_getElem?_get (a : Vector α n) (i : Nat) (h : i < n) :
    a[i] = a[i]?.get (by simp [getElem?_eq_getElem, h])

Proof state:
α : Type ?u.81346
n : Nat
a : Vector α n
i : Nat
h : i < n
⊢ a[i]?.isSome = true

Tactic:
simp [getElem?_eq_getElem, h]

Result:
no goals

Proof state:
α : Type u_1
n : Nat
a : Vector α n
i : Nat
h : i < n
⊢ a[i] = a[i]?.get ⋯

Tactic:
simp [getElem_eq_iff]

Result:
no goals
-- Mathlib/Data/Nat/Nth.lean
theorem nth_strictMono (hf : (setOf p).Infinite) : StrictMono (nth p)

Proof state:
p : ℕ → Prop
hf : (setOf p).Infinite
⊢ StrictMono (Subtype.val ∘ ⇑(Subtype.orderIsoOfNat (setOf p)))

Tactic:
exact (Subtype.strictMono_coe _).comp (OrderIso.strictMono _)

Result:
no goals

Proof state:
p : ℕ → Prop
hf : (setOf p).Infinite
⊢ StrictMono (nth p)

Tactic:
rw [nth_eq_orderIsoOfNat hf]

Result:
p : ℕ → Prop
hf : (setOf p).Infinite
⊢ StrictMono (Subtype.val ∘ ⇑(Subtype.orderIsoOfNat (setOf p)))
-- Mathlib/Data/List/Range.lean
theorem chain_range_succ (r : ℕ → ℕ → Prop) (n a : ℕ) :
    Chain r a (range n.succ) ↔ r a 0 ∧ ∀ m < n, r m m.succ

Proof state:
r : ℕ → ℕ → Prop
n a : ℕ
⊢ r a 0 → (Chain r 0 (map succ (range n)) ↔ Chain' r (0 :: map succ (range n)))

Tactic:
exact fun _ => Iff.rfl

Result:
no goals

Proof state:
r : ℕ → ℕ → Prop
n a : ℕ
⊢ Chain r a (range n.succ) ↔ r a 0 ∧ ∀ (m : ℕ), m < n → r m m.succ

Tactic:
rw [range_succ_eq_map, chain_cons, and_congr_right_iff, ← chain'_range_succ, range_succ_eq_map]

Result:
r : ℕ → ℕ → Prop
n a : ℕ
⊢ r a 0 → (Chain r 0 (map succ (range n)) ↔ Chain' r (0 :: map succ (range n)))
-- Mathlib/MeasureTheory/Function/LpSeminorm/Basic.lean
/-- See `eLpNorm_smul_measure_of_ne_zero` for a version with scalar multiplication by `ℝ≥0∞`. -/
lemma eLpNorm_smul_measure_of_ne_zero' {c : ℝ≥0} (hc : c ≠ 0) (f : α → F) (p : ℝ≥0∞)
    (μ : Measure α) : eLpNorm f p (c • μ) = c ^ p.toReal⁻¹ • eLpNorm f p μ :=
  (eLpNorm_smul_measure_of_ne_zero (ENNReal.coe_ne_zero.2 hc) ..).trans (by simp; norm_cast)

Proof state:
α : Type u_1
F : Type u_4
m0 : MeasurableSpace α
inst✝ : NormedAddCommGroup F
c : ℝ≥0
hc : c ≠ 0
f : α → F
p : ℝ≥0∞
μ : Measure α
⊢ ↑c ^ (1 / p).toReal • eLpNorm f p μ = c ^ p.toReal⁻¹ • eLpNorm f p μ

Tactic:
simp

Result:
α : Type u_1
F : Type u_4
m0 : MeasurableSpace α
inst✝ : NormedAddCommGroup F
c : ℝ≥0
hc : c ≠ 0
f : α → F
p : ℝ≥0∞
μ : Measure α
⊢ ↑c ^ p.toReal⁻¹ * eLpNorm f p μ = c ^ p.toReal⁻¹ • eLpNorm f p μ

Proof state:
α : Type u_1
F : Type u_4
m0 : MeasurableSpace α
inst✝ : NormedAddCommGroup F
c : ℝ≥0
hc : c ≠ 0
f : α → F
p : ℝ≥0∞
μ : Measure α
⊢ ↑c ^ p.toReal⁻¹ * eLpNorm f p μ = c ^ p.toReal⁻¹ • eLpNorm f p μ

Tactic:
norm_cast

Result:
no goals
-- Mathlib/LinearAlgebra/Span/Defs.lean
theorem mem_sup : x ∈ p ⊔ p' ↔ ∃ y ∈ p, ∃ z ∈ p', y + z = x :=
  ⟨fun h => by
    rw [← span_eq p, ← span_eq p', ← span_union] at h
    refine span_induction ?_ ?_ ?_ ?_ h
    · rintro y (h | h)
      · exact ⟨y, h, 0, by simp, by simp⟩
      · exact ⟨0, by simp, y, h, by simp⟩
    · exact ⟨0, by simp, 0, by simp⟩
    · rintro _ _ - - ⟨y₁, hy₁, z₁, hz₁, rfl⟩ ⟨y₂, hy₂, z₂, hz₂, rfl⟩
      exact ⟨_, add_mem hy₁ hy₂, _, add_mem hz₁ hz₂, by
        rw [add_assoc, add_assoc, ← add_assoc y₂, ← add_assoc z₁, add_comm y₂]⟩
    · rintro a - _ ⟨y, hy, z, hz, rfl⟩
      exact ⟨_, smul_mem _ a hy, _, smul_mem _ a hz, by simp [smul_add]⟩, by
    rintro ⟨y, hy, z, hz, rfl⟩
    exact add_mem ((le_sup_left : p ≤ p ⊔ p') hy) ((le_sup_right : p' ≤ p ⊔ p') hz)⟩

Proof state:
R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
x : M
p p' : Submodule R M
⊢ (∃ y ∈ p, ∃ z ∈ p', y + z = x) → x ∈ p ⊔ p'

Tactic:
rintro ⟨y, hy, z, hz, rfl⟩

Result:
case intro.intro.intro.intro
R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
p p' : Submodule R M
y : M
hy : y ∈ p
z : M
hz : z ∈ p'
⊢ y + z ∈ p ⊔ p'

Proof state:
R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
x : M
p p' : Submodule R M
h : x ∈ span R (↑p ∪ ↑p')
y₁ : M
hy₁ : y₁ ∈ p
z₁ : M
hz₁ : z₁ ∈ p'
y₂ : M
hy₂ : y₂ ∈ p
z₂ : M
hz₂ : z₂ ∈ p'
⊢ y₁ + y₂ + (z₁ + z₂) = y₁ + z₁ + (y₂ + z₂)

Tactic:
rw [add_assoc, add_assoc, ← add_assoc y₂, ← add_assoc z₁, add_comm y₂]

Result:
no goals

Proof state:
case refine_1.inr
R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
x : M
p p' : Submodule R M
h✝ : x ∈ span R (↑p ∪ ↑p')
y : M
h : y ∈ ↑p'
⊢ ∃ y_1 ∈ p, ∃ z ∈ p', y_1 + z = y

Tactic:
exact ⟨0, by simp, y, h, by simp⟩

Result:
no goals
-- Mathlib/Algebra/BigOperators/Group/List/Defs.lean
theorem prod_hom_rel (l : List ι) {r : M → N → Prop} {f : ι → M} {g : ι → N} (h₁ : r 1 1)
    (h₂ : ∀ ⦃i a b⦄, r a b → r (f i * a) (g i * b)) : r (l.map f).prod (l.map g).prod :=
  List.recOn l h₁ fun a l hl => by simp only [map_cons, prod_cons, h₂ hl]

Proof state:
ι : Type u_1
M : Type u_4
N : Type u_5
inst✝¹ : Monoid M
inst✝ : Monoid N
l✝ : List ι
r : M → N → Prop
f : ι → M
g : ι → N
h₁ : r 1 1
h₂ : ∀ ⦃i : ι⦄ ⦃a : M⦄ ⦃b : N⦄, r a b → r (f i * a) (g i * b)
a : ι
l : List ι
hl : r (map f l).prod (map g l).prod
⊢ r (map f (a :: l)).prod (map g (a :: l)).prod

Tactic:
simp only [map_cons, prod_cons, h₂ hl]

Result:
no goals
-- Mathlib/LinearAlgebra/QuadraticForm/Basic.lean
theorem polar_toQuadraticMap (x y : M) : polar (toQuadraticMap B) x y = B x y + B y x

Proof state:
R : Type u_3
M : Type u_4
N : Type u_5
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup N
inst✝¹ : Module R M
inst✝ : Module R N
B : BilinMap R M N
x y : M
⊢ polar (⇑B.toQuadraticMap) x y = (B x) y + (B y) x

Tactic:
simp only [polar, toQuadraticMap_apply, map_add, add_apply, add_assoc, add_comm (B y x) _,
  add_sub_cancel_left, sub_eq_add_neg _ (B y y), add_neg_cancel_left]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/RotateLeft.lean
theorem denote_blastRotateLeft (aig : AIG α) (target : ShiftTarget aig w)
    (assign : α → Bool) :
    ∀ (idx : Nat) (hidx : idx < w),
        ⟦
          (blastRotateLeft aig target).aig,
          (blastRotateLeft aig target).vec.get idx hidx,
          assign
        ⟧
          =
        if hidx2 : idx < target.distance % w then
          ⟦aig, target.vec.get (w - (target.distance % w) + idx) (by omega), assign⟧
        else
          ⟦aig, target.vec.get (idx - (target.distance % w)) (by omega), assign⟧

Proof state:
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
target : aig.ShiftTarget w
assign : α → Bool
⊢ ∀ (idx : Nat) (hidx : idx < w),
    ⟦assign, { aig := (blastRotateLeft aig target).aig, ref := (blastRotateLeft aig target).vec.get idx hidx }⟧ =
      if hidx2 : idx < target.distance % w then
        ⟦assign, { aig := aig, ref := target.vec.get (w - target.distance % w + idx) ⋯ }⟧
      else ⟦assign, { aig := aig, ref := target.vec.get (idx - target.distance % w) ⋯ }⟧

Tactic:
intros

Result:
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
target : aig.ShiftTarget w
assign : α → Bool
idx✝ : Nat
hidx✝ : idx✝ < w
⊢ ⟦assign, { aig := (blastRotateLeft aig target).aig, ref := (blastRotateLeft aig target).vec.get idx✝ hidx✝ }⟧ =
    if hidx2 : idx✝ < target.distance % w then
      ⟦assign, { aig := aig, ref := target.vec.get (w - target.distance % w + idx✝) ⋯ }⟧
    else ⟦assign, { aig := aig, ref := target.vec.get (idx✝ - target.distance % w) ⋯ }⟧
-- Mathlib/Algebra/Quaternion.lean
theorem mk_quaternionAlgebra : #(ℍ[R,c₁,c₂,c₃]) = #R ^ 4

Proof state:
R : Type u_1
c₁ c₂ c₃ : R
⊢ #ℍ[R,c₁,c₂,c₃] = #R ^ 4

Tactic:
rw [mk_congr (QuaternionAlgebra.equivProd c₁ c₂ c₃)]

Result:
R : Type u_1
c₁ c₂ c₃ : R
⊢ #(R × R × R × R) = #R ^ 4

Proof state:
R : Type u_1
c₁ c₂ c₃ : R
⊢ #(R × R × R × R) = #R ^ 4

Tactic:
simp only [mk_prod, lift_id]

Result:
R : Type u_1
c₁ c₂ c₃ : R
⊢ #R * (#R * (#R * #R)) = #R ^ 4

Proof state:
R : Type u_1
c₁ c₂ c₃ : R
⊢ #R * (#R * (#R * #R)) = #R ^ 4

Tactic:
ring

Result:
no goals
-- Mathlib/Analysis/NormedSpace/HahnBanach/Separation.lean
theorem geometric_hahn_banach_closed_compact (hs₁ : Convex ℝ s) (hs₂ : IsClosed s)
    (ht₁ : Convex ℝ t) (ht₂ : IsCompact t) (disj : Disjoint s t) :
    ∃ (f : E →L[𝕜] 𝕜) (u v : ℝ), (∀ a ∈ s, re (f a) < u) ∧ u < v ∧ ∀ b ∈ t, v < re (f b) :=
  let ⟨f, s, t, hs, st, ht⟩ := geometric_hahn_banach_compact_closed ht₁ ht₂ hs₁ hs₂ disj.symm
  ⟨-f, -t, -s, by simpa using ht, by simpa using st, by simpa using hs⟩

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝⁸ : TopologicalSpace E
inst✝⁷ : AddCommGroup E
inst✝⁶ : Module ℝ E
s✝ t✝ : Set E
inst✝⁵ : RCLike 𝕜
inst✝⁴ : Module 𝕜 E
inst✝³ : IsScalarTower ℝ 𝕜 E
inst✝² : IsTopologicalAddGroup E
inst✝¹ : ContinuousSMul 𝕜 E
inst✝ : LocallyConvexSpace ℝ E
hs₁ : Convex ℝ s✝
hs₂ : IsClosed s✝
ht₁ : Convex ℝ t✝
ht₂ : IsCompact t✝
disj : Disjoint s✝ t✝
f : E →L[𝕜] 𝕜
s t : ℝ
hs : ∀ a ∈ t✝, re (f a) < s
st : s < t
ht : ∀ b ∈ s✝, t < re (f b)
⊢ ∀ a ∈ s✝, re ((-f) a) < -t

Tactic:
simpa using ht

Result:
no goals

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝⁸ : TopologicalSpace E
inst✝⁷ : AddCommGroup E
inst✝⁶ : Module ℝ E
s✝ t✝ : Set E
inst✝⁵ : RCLike 𝕜
inst✝⁴ : Module 𝕜 E
inst✝³ : IsScalarTower ℝ 𝕜 E
inst✝² : IsTopologicalAddGroup E
inst✝¹ : ContinuousSMul 𝕜 E
inst✝ : LocallyConvexSpace ℝ E
hs₁ : Convex ℝ s✝
hs₂ : IsClosed s✝
ht₁ : Convex ℝ t✝
ht₂ : IsCompact t✝
disj : Disjoint s✝ t✝
f : E →L[𝕜] 𝕜
s t : ℝ
hs : ∀ a ∈ t✝, re (f a) < s
st : s < t
ht : ∀ b ∈ s✝, t < re (f b)
⊢ -t < -s

Tactic:
simpa using st

Result:
no goals

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝⁸ : TopologicalSpace E
inst✝⁷ : AddCommGroup E
inst✝⁶ : Module ℝ E
s✝ t✝ : Set E
inst✝⁵ : RCLike 𝕜
inst✝⁴ : Module 𝕜 E
inst✝³ : IsScalarTower ℝ 𝕜 E
inst✝² : IsTopologicalAddGroup E
inst✝¹ : ContinuousSMul 𝕜 E
inst✝ : LocallyConvexSpace ℝ E
hs₁ : Convex ℝ s✝
hs₂ : IsClosed s✝
ht₁ : Convex ℝ t✝
ht₂ : IsCompact t✝
disj : Disjoint s✝ t✝
f : E →L[𝕜] 𝕜
s t : ℝ
hs : ∀ a ∈ t✝, re (f a) < s
st : s < t
ht : ∀ b ∈ s✝, t < re (f b)
⊢ ∀ b ∈ t✝, -s < re ((-f) b)

Tactic:
simpa using hs

Result:
no goals
-- Mathlib/Algebra/Order/Sub/Basic.lean
theorem tsub_right_inj (ha : AddLECancellable a) (hb : AddLECancellable b)
    (hc : AddLECancellable c) (hba : b ≤ a) (hca : c ≤ a) : a - b = a - c ↔ b = c

Proof state:
α : Type u_1
inst✝⁴ : AddCommMonoid α
inst✝³ : PartialOrder α
inst✝² : CanonicallyOrderedAdd α
inst✝¹ : Sub α
inst✝ : OrderedSub α
a b c : α
ha : AddLECancellable a
hb : AddLECancellable b
hc : AddLECancellable c
hba : b ≤ a
hca : c ≤ a
⊢ a - b = a - c ↔ b = c

Tactic:
simp_rw [le_antisymm_iff, ha.tsub_le_tsub_iff_left hb hba, ha.tsub_le_tsub_iff_left hc hca,
  and_comm]

Result:
no goals
-- Mathlib/NumberTheory/PellMatiyasevic.lean
theorem isPell_pellZd : ∀ n : ℕ, IsPell (pellZd a1 n)
  | 0 => rfl
  | n + 1 => by
    let o := isPell_one a1
    simpa using Pell.isPell_mul (isPell_pellZd n) o

Proof state:
a : ℕ
a1 : 1 < a
n : ℕ
o : IsPell { re := ↑a, im := 1 } := isPell_one a1
⊢ IsPell (pellZd a1 (n + 1))

Tactic:
simpa using Pell.isPell_mul (isPell_pellZd n) o

Result:
no goals

Proof state:
a : ℕ
a1 : 1 < a
n : ℕ
⊢ IsPell (pellZd a1 (n + 1))

Tactic:
let o := isPell_one a1

Result:
a : ℕ
a1 : 1 < a
n : ℕ
o : IsPell { re := ↑a, im := 1 } := isPell_one a1
⊢ IsPell (pellZd a1 (n + 1))
-- Mathlib/RingTheory/MvPolynomial/MonomialOrder.lean
theorem degree_subsingleton [Subsingleton R] {f : MvPolynomial σ R} :
    m.degree f = 0

Proof state:
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝¹ : CommSemiring R
inst✝ : Subsingleton R
f : MvPolynomial σ R
⊢ m.degree f = 0

Tactic:
rw [Subsingleton.eq_zero f, degree_zero]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Integrals.lean
theorem integral_sin_pow :
    (∫ x in a..b, sin x ^ (n + 2)) =
      (sin a ^ (n + 1) * cos a - sin b ^ (n + 1) * cos b) / (n + 2) +
        (n + 1) / (n + 2) * ∫ x in a..b, sin x ^ n

Proof state:
case h.e'_2
a b : ℝ
n : ℕ
⊢ (∫ (x : ℝ) in a..b, sin x ^ (n + 2)) * (↑n + 2) =
    (∫ (x : ℝ) in a..b, sin x ^ (n + 2)) + (↑n + 1) * ∫ (x : ℝ) in a..b, sin x ^ (n + 2)

Tactic:
ring

Result:
no goals

Proof state:
a b : ℝ
n : ℕ
⊢ ∫ (x : ℝ) in a..b, sin x ^ (n + 2) =
    (sin a ^ (n + 1) * cos a - sin b ^ (n + 1) * cos b) / (↑n + 2) + (↑n + 1) / (↑n + 2) * ∫ (x : ℝ) in a..b, sin x ^ n

Tactic:
field_simp

Result:
a b : ℝ
n : ℕ
⊢ (∫ (x : ℝ) in a..b, sin x ^ (n + 2)) * (↑n + 2) =
    sin a ^ (n + 1) * cos a - sin b ^ (n + 1) * cos b + (↑n + 1) * ∫ (x : ℝ) in a..b, sin x ^ n

Proof state:
a b : ℝ
n : ℕ
⊢ (∫ (x : ℝ) in a..b, sin x ^ (n + 2)) * (↑n + 2) =
    sin a ^ (n + 1) * cos a - sin b ^ (n + 1) * cos b + (↑n + 1) * ∫ (x : ℝ) in a..b, sin x ^ n

Tactic:
convert eq_sub_iff_add_eq.mp (integral_sin_pow_aux n) using 1

Result:
case h.e'_2
a b : ℝ
n : ℕ
⊢ (∫ (x : ℝ) in a..b, sin x ^ (n + 2)) * (↑n + 2) =
    (∫ (x : ℝ) in a..b, sin x ^ (n + 2)) + (↑n + 1) * ∫ (x : ℝ) in a..b, sin x ^ (n + 2)
-- Mathlib/Data/Nat/Factorization/Defs.lean
theorem factorization_eq_primeFactorsList_multiset (n : ℕ) :
    n.factorization = Multiset.toFinsupp (n.primeFactorsList : Multiset ℕ)

Proof state:
n : ℕ
⊢ n.factorization = Multiset.toFinsupp ↑n.primeFactorsList

Tactic:
ext p

Result:
case h
n p : ℕ
⊢ n.factorization p = (Multiset.toFinsupp ↑n.primeFactorsList) p

Proof state:
case h
n p : ℕ
⊢ n.factorization p = (Multiset.toFinsupp ↑n.primeFactorsList) p

Tactic:
simp

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Bool.lean
theorem or_and_distrib_left  : ∀ (x y z : Bool), (x || y && z) = ((x || y) && (x || z))

Proof state:
⊢ ∀ (x y z : Bool), (x || y && z) = ((x || y) && (x || z))

Tactic:
decide

Result:
no goals
-- Mathlib/FieldTheory/Finite/GaloisField.lean
theorem card (h : n ≠ 0) : Nat.card (GaloisField p n) = p ^ n

Proof state:
p : ℕ
h_prime : Fact (Nat.Prime p)
n : ℕ
h : n ≠ 0
⊢ Nat.card (GaloisField p n) = p ^ n

Tactic:
let b := IsNoetherian.finsetBasis (ZMod p) (GaloisField p n)

Result:
p : ℕ
h_prime : Fact (Nat.Prime p)
n : ℕ
h : n ≠ 0
b : Basis { x // x ∈ IsNoetherian.finsetBasisIndex (ZMod p) (GaloisField p n) } (ZMod p) (GaloisField p n) :=
  IsNoetherian.finsetBasis (ZMod p) (GaloisField p n)
⊢ Nat.card (GaloisField p n) = p ^ n

Proof state:
p : ℕ
h_prime : Fact (Nat.Prime p)
n : ℕ
h : n ≠ 0
b : Basis { x // x ∈ IsNoetherian.finsetBasisIndex (ZMod p) (GaloisField p n) } (ZMod p) (GaloisField p n) :=
  IsNoetherian.finsetBasis (ZMod p) (GaloisField p n)
this : Fintype (GaloisField p n)
⊢ Nat.card (GaloisField p n) = p ^ n

Tactic:
rw [Nat.card_eq_fintype_card, Module.card_fintype b, ← Module.finrank_eq_card_basis b,
  ZMod.card, finrank p h]

Result:
no goals

Proof state:
p : ℕ
h_prime : Fact (Nat.Prime p)
n : ℕ
h : n ≠ 0
b : Basis { x // x ∈ IsNoetherian.finsetBasisIndex (ZMod p) (GaloisField p n) } (ZMod p) (GaloisField p n) :=
  IsNoetherian.finsetBasis (ZMod p) (GaloisField p n)
⊢ Nat.card (GaloisField p n) = p ^ n

Tactic:
haveI : Fintype (GaloisField p n) := Fintype.ofFinite (GaloisField p n)

Result:
p : ℕ
h_prime : Fact (Nat.Prime p)
n : ℕ
h : n ≠ 0
b : Basis { x // x ∈ IsNoetherian.finsetBasisIndex (ZMod p) (GaloisField p n) } (ZMod p) (GaloisField p n) :=
  IsNoetherian.finsetBasis (ZMod p) (GaloisField p n)
this : Fintype (GaloisField p n)
⊢ Nat.card (GaloisField p n) = p ^ n
-- Mathlib/Analysis/Calculus/FDeriv/Basic.lean
theorem hasFDerivAt_of_subsingleton [h : Subsingleton E] (f : E → F) (x : E) :
    HasFDerivAt f (0 : E →L[𝕜] F) x

Proof state:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
h : Subsingleton E
f : E → F
x : E
⊢ HasFDerivAt f 0 x

Tactic:
rw [← hasFDerivWithinAt_univ, subsingleton_univ.eq_singleton_of_mem (mem_univ x)]

Result:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
h : Subsingleton E
f : E → F
x : E
⊢ HasFDerivWithinAt f 0 {x} x

Proof state:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
h : Subsingleton E
f : E → F
x : E
⊢ HasFDerivWithinAt f 0 {x} x

Tactic:
exact hasFDerivWithinAt_singleton f x

Result:
no goals
-- Mathlib/RepresentationTheory/GroupCohomology/Functoriality.lean
theorem H2Map_comp {G H K : Type u} [Group G] [Group H] [Group K]
    {A : Rep k K} {B : Rep k H} {C : Rep k G} (f : H →* K) (g : G →* H)
    (φ : (Action.res _ f).obj A ⟶ B) (ψ : (Action.res _ g).obj B ⟶ C) :
    H2Map (f.comp g) ((Action.res _ g).map φ ≫ ψ) = H2Map f φ ≫ H2Map g ψ

Proof state:
k : Type u
inst✝³ : CommRing k
G H K : Type u
inst✝² : Group G
inst✝¹ : Group H
inst✝ : Group K
A : Rep k K
B : Rep k H
C : Rep k G
f : H →* K
g : G →* H
φ : (Action.res (ModuleCat k) f).obj A ⟶ B
ψ : (Action.res (ModuleCat k) g).obj B ⟶ C
⊢ H2Map (f.comp g) ((Action.res (ModuleCat k) g).map φ ≫ ψ) = H2Map f φ ≫ H2Map g ψ

Tactic:
simpa [H2Map, shortComplexH2, mapShortComplexH2_comp] using leftHomologyMap'_comp ..

Result:
no goals
-- Mathlib/Topology/DiscreteQuotient.lean
theorem isClopen_setOf_rel (x : X) : IsClopen (setOf (S.toSetoid x))

Proof state:
X : Type u_2
inst✝ : TopologicalSpace X
S : DiscreteQuotient X
x : X
⊢ IsClopen (setOf (S.toSetoid x))

Tactic:
rw [← fiber_eq]

Result:
X : Type u_2
inst✝ : TopologicalSpace X
S : DiscreteQuotient X
x : X
⊢ IsClopen (S.proj ⁻¹' {S.proj x})

Proof state:
X : Type u_2
inst✝ : TopologicalSpace X
S : DiscreteQuotient X
x : X
⊢ IsClopen (S.proj ⁻¹' {S.proj x})

Tactic:
apply isClopen_preimage

Result:
no goals
-- Mathlib/Order/Filter/AtTopBot/CountablyGenerated.lean
theorem subseq_tendsto_of_neBot {f : Filter α} [IsCountablyGenerated f] {u : ℕ → α}
    (hx : NeBot (f ⊓ map u atTop)) : ∃ θ : ℕ → ℕ, StrictMono θ ∧ Tendsto (u ∘ θ) atTop f

Proof state:
case intro
α : Type u_1
f : Filter α
inst✝ : f.IsCountablyGenerated
u : ℕ → α
hx : (comap u f ⊓ atTop).NeBot
φ : ℕ → ℕ
hφ : Tendsto (u ∘ φ) atTop f ∧ Tendsto φ atTop atTop
⊢ ∃ θ, StrictMono θ ∧ Tendsto (u ∘ θ) atTop f

Tactic:
obtain ⟨ψ, hψ, hψφ⟩ : ∃ ψ : ℕ → ℕ, StrictMono ψ ∧ StrictMono (φ ∘ ψ) :=
  strictMono_subseq_of_tendsto_atTop hφ.2

Result:
case intro.intro.intro
α : Type u_1
f : Filter α
inst✝ : f.IsCountablyGenerated
u : ℕ → α
hx : (comap u f ⊓ atTop).NeBot
φ : ℕ → ℕ
hφ : Tendsto (u ∘ φ) atTop f ∧ Tendsto φ atTop atTop
ψ : ℕ → ℕ
hψ : StrictMono ψ
hψφ : StrictMono (φ ∘ ψ)
⊢ ∃ θ, StrictMono θ ∧ Tendsto (u ∘ θ) atTop f

Proof state:
case intro.intro.intro
α : Type u_1
f : Filter α
inst✝ : f.IsCountablyGenerated
u : ℕ → α
hx : (comap u f ⊓ atTop).NeBot
φ : ℕ → ℕ
hφ : Tendsto (u ∘ φ) atTop f ∧ Tendsto φ atTop atTop
ψ : ℕ → ℕ
hψ : StrictMono ψ
hψφ : StrictMono (φ ∘ ψ)
⊢ ∃ θ, StrictMono θ ∧ Tendsto (u ∘ θ) atTop f

Tactic:
exact ⟨φ ∘ ψ, hψφ, hφ.1.comp hψ.tendsto_atTop⟩

Result:
no goals

Proof state:
case intro
α : Type u_1
f : Filter α
inst✝ : f.IsCountablyGenerated
u : ℕ → α
hx : (comap u f ⊓ atTop).NeBot
φ : ℕ → ℕ
hφ : Tendsto φ atTop (comap u f ⊓ atTop)
⊢ ∃ θ, StrictMono θ ∧ Tendsto (u ∘ θ) atTop f

Tactic:
rw [tendsto_inf, tendsto_comap_iff] at hφ

Result:
case intro
α : Type u_1
f : Filter α
inst✝ : f.IsCountablyGenerated
u : ℕ → α
hx : (comap u f ⊓ atTop).NeBot
φ : ℕ → ℕ
hφ : Tendsto (u ∘ φ) atTop f ∧ Tendsto φ atTop atTop
⊢ ∃ θ, StrictMono θ ∧ Tendsto (u ∘ θ) atTop f

Proof state:
α : Type u_1
f : Filter α
inst✝ : f.IsCountablyGenerated
u : ℕ → α
hx : (comap u f ⊓ atTop).NeBot
⊢ ∃ θ, StrictMono θ ∧ Tendsto (u ∘ θ) atTop f

Tactic:
rcases exists_seq_tendsto (comap u f ⊓ atTop) with ⟨φ, hφ⟩

Result:
case intro
α : Type u_1
f : Filter α
inst✝ : f.IsCountablyGenerated
u : ℕ → α
hx : (comap u f ⊓ atTop).NeBot
φ : ℕ → ℕ
hφ : Tendsto φ atTop (comap u f ⊓ atTop)
⊢ ∃ θ, StrictMono θ ∧ Tendsto (u ∘ θ) atTop f

Proof state:
α : Type u_1
f : Filter α
inst✝ : f.IsCountablyGenerated
u : ℕ → α
hx : (f ⊓ map u atTop).NeBot
⊢ ∃ θ, StrictMono θ ∧ Tendsto (u ∘ θ) atTop f

Tactic:
rw [← Filter.push_pull', map_neBot_iff] at hx

Result:
α : Type u_1
f : Filter α
inst✝ : f.IsCountablyGenerated
u : ℕ → α
hx : (comap u f ⊓ atTop).NeBot
⊢ ∃ θ, StrictMono θ ∧ Tendsto (u ∘ θ) atTop f
-- Mathlib/ModelTheory/PartialEquiv.lean
theorem symm_le_iff {f : M ≃ₚ[L] N} {g : N ≃ₚ[L] M} : f.symm ≤ g ↔ f ≤ g.symm :=
  ⟨by intro h; rw [← f.symm_symm]; exact monotone_symm h,
    by intro h; rw  [← g.symm_symm]; exact monotone_symm h⟩

Proof state:
L : Language
M : Type w
N : Type w'
inst✝¹ : L.Structure M
inst✝ : L.Structure N
f : M ≃ₚ[L] N
g : N ≃ₚ[L] M
h : f ≤ g.symm
⊢ f.symm ≤ g

Tactic:
rw  [← g.symm_symm]

Result:
L : Language
M : Type w
N : Type w'
inst✝¹ : L.Structure M
inst✝ : L.Structure N
f : M ≃ₚ[L] N
g : N ≃ₚ[L] M
h : f ≤ g.symm
⊢ f.symm ≤ g.symm.symm

Proof state:
L : Language
M : Type w
N : Type w'
inst✝¹ : L.Structure M
inst✝ : L.Structure N
f : M ≃ₚ[L] N
g : N ≃ₚ[L] M
h : f.symm ≤ g
⊢ f ≤ g.symm

Tactic:
rw [← f.symm_symm]

Result:
L : Language
M : Type w
N : Type w'
inst✝¹ : L.Structure M
inst✝ : L.Structure N
f : M ≃ₚ[L] N
g : N ≃ₚ[L] M
h : f.symm ≤ g
⊢ f.symm.symm ≤ g.symm

Proof state:
L : Language
M : Type w
N : Type w'
inst✝¹ : L.Structure M
inst✝ : L.Structure N
f : M ≃ₚ[L] N
g : N ≃ₚ[L] M
h : f.symm ≤ g
⊢ f.symm.symm ≤ g.symm

Tactic:
exact monotone_symm h

Result:
no goals

Proof state:
L : Language
M : Type w
N : Type w'
inst✝¹ : L.Structure M
inst✝ : L.Structure N
f : M ≃ₚ[L] N
g : N ≃ₚ[L] M
⊢ f ≤ g.symm → f.symm ≤ g

Tactic:
intro h

Result:
L : Language
M : Type w
N : Type w'
inst✝¹ : L.Structure M
inst✝ : L.Structure N
f : M ≃ₚ[L] N
g : N ≃ₚ[L] M
h : f ≤ g.symm
⊢ f.symm ≤ g

Proof state:
L : Language
M : Type w
N : Type w'
inst✝¹ : L.Structure M
inst✝ : L.Structure N
f : M ≃ₚ[L] N
g : N ≃ₚ[L] M
h : f ≤ g.symm
⊢ f.symm ≤ g.symm.symm

Tactic:
exact monotone_symm h

Result:
no goals

Proof state:
L : Language
M : Type w
N : Type w'
inst✝¹ : L.Structure M
inst✝ : L.Structure N
f : M ≃ₚ[L] N
g : N ≃ₚ[L] M
⊢ f.symm ≤ g → f ≤ g.symm

Tactic:
intro h

Result:
L : Language
M : Type w
N : Type w'
inst✝¹ : L.Structure M
inst✝ : L.Structure N
f : M ≃ₚ[L] N
g : N ≃ₚ[L] M
h : f.symm ≤ g
⊢ f ≤ g.symm