harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Analysis/Normed/Ring/Units.lean
theorem inverse_add_norm_diff_nth_order (x : Rˣ) (n : ℕ) :
    (fun t : R => inverse (↑x + t) - (∑ i ∈ range n, (-↑x⁻¹ * t) ^ i) * ↑x⁻¹) =O[𝓝 (0 : R)]
      fun t => ‖t‖ ^ n

Proof state:
R : Type u_1
inst✝¹ : NormedRing R
inst✝ : HasSummableGeomSeries R
x : Rˣ
n : ℕ
⊢ (fun x_1 => (-↑x⁻¹ * x_1) ^ n) =O[𝓝 0] fun t => ‖t‖ ^ n

Tactic:
exact ((isBigO_refl _ _).norm_right.const_mul_left _).pow _

Result:
no goals

Proof state:
R : Type u_1
inst✝¹ : NormedRing R
inst✝ : HasSummableGeomSeries R
x : Rˣ
n : ℕ
⊢ (fun x_1 => (-↑x⁻¹ * x_1) ^ n * inverse (↑x + x_1)) =O[𝓝 0] fun t => ‖t‖ ^ n

Tactic:
refine ((isBigO_refl _ _).norm_right.mul (inverse_add_norm x)).trans ?_

Result:
R : Type u_1
inst✝¹ : NormedRing R
inst✝ : HasSummableGeomSeries R
x : Rˣ
n : ℕ
⊢ (fun x_1 => ‖(-↑x⁻¹ * x_1) ^ n‖ * 1) =O[𝓝 0] fun t => ‖t‖ ^ n

Proof state:
R : Type u_1
inst✝¹ : NormedRing R
inst✝ : HasSummableGeomSeries R
x : Rˣ
n : ℕ
⊢ (fun t => inverse (↑x + t) - (∑ i ∈ range n, (-↑x⁻¹ * t) ^ i) * ↑x⁻¹) =O[𝓝 0] fun t => ‖t‖ ^ n

Tactic:
refine EventuallyEq.trans_isBigO (.sub (inverse_add_nth_order x n) (.refl _ _)) ?_

Result:
R : Type u_1
inst✝¹ : NormedRing R
inst✝ : HasSummableGeomSeries R
x : Rˣ
n : ℕ
⊢ (fun x_1 =>
      (∑ i ∈ range n, (-↑x⁻¹ * x_1) ^ i) * ↑x⁻¹ + (-↑x⁻¹ * x_1) ^ n * inverse (↑x + x_1) -
        (∑ i ∈ range n, (-↑x⁻¹ * x_1) ^ i) * ↑x⁻¹) =O[𝓝 0]
    fun t => ‖t‖ ^ n

Proof state:
R : Type u_1
inst✝¹ : NormedRing R
inst✝ : HasSummableGeomSeries R
x : Rˣ
n : ℕ
⊢ (fun x_1 =>
      (∑ i ∈ range n, (-↑x⁻¹ * x_1) ^ i) * ↑x⁻¹ + (-↑x⁻¹ * x_1) ^ n * inverse (↑x + x_1) -
        (∑ i ∈ range n, (-↑x⁻¹ * x_1) ^ i) * ↑x⁻¹) =O[𝓝 0]
    fun t => ‖t‖ ^ n

Tactic:
simp only [add_sub_cancel_left]

Result:
R : Type u_1
inst✝¹ : NormedRing R
inst✝ : HasSummableGeomSeries R
x : Rˣ
n : ℕ
⊢ (fun x_1 => (-↑x⁻¹ * x_1) ^ n * inverse (↑x + x_1)) =O[𝓝 0] fun t => ‖t‖ ^ n

Proof state:
R : Type u_1
inst✝¹ : NormedRing R
inst✝ : HasSummableGeomSeries R
x : Rˣ
n : ℕ
⊢ (fun x_1 => ‖(-↑x⁻¹ * x_1) ^ n‖ * 1) =O[𝓝 0] fun t => ‖t‖ ^ n

Tactic:
simp only [mul_one, isBigO_norm_left]

Result:
R : Type u_1
inst✝¹ : NormedRing R
inst✝ : HasSummableGeomSeries R
x : Rˣ
n : ℕ
⊢ (fun x_1 => (-↑x⁻¹ * x_1) ^ n) =O[𝓝 0] fun t => ‖t‖ ^ n
-- Mathlib/NumberTheory/LegendreSymbol/JacobiSymbol.lean
theorem list_prod_right {a : ℤ} {l : List ℕ} (hl : ∀ n ∈ l, n ≠ 0) :
    J(a | l.prod) = (l.map fun n => J(a | n)).prod

Proof state:
case nil
a : ℤ
hl : ∀ n ∈ [], n ≠ 0
⊢ J(a | [].prod) = (List.map (fun n => J(a | n)) []).prod

Tactic:
simp only [List.prod_nil, one_right, List.map_nil]

Result:
no goals

Proof state:
a : ℤ
l : List ℕ
hl : ∀ n ∈ l, n ≠ 0
⊢ J(a | l.prod) = (List.map (fun n => J(a | n)) l).prod

Tactic:
induction l with
| nil => simp only [List.prod_nil, one_right, List.map_nil]
| cons n l' ih =>
  have hn := hl n (List.mem_cons_self n l')
  have hl' := List.prod_ne_zero fun hf => hl 0 (List.mem_cons_of_mem _ hf) rfl
  have h := fun m hm => hl m (List.mem_cons_of_mem _ hm)
  rw [List.map, List.prod_cons, List.prod_cons, mul_right' a hn hl', ih h]

Result:
no goals

Proof state:
case cons
a : ℤ
n : ℕ
l' : List ℕ
ih : (∀ n ∈ l', n ≠ 0) → J(a | l'.prod) = (List.map (fun n => J(a | n)) l').prod
hl : ∀ n_1 ∈ n :: l', n_1 ≠ 0
hn : n ≠ 0
hl' : l'.prod ≠ 0
h : ∀ m ∈ l', m ≠ 0
⊢ J(a | (n :: l').prod) = (List.map (fun n => J(a | n)) (n :: l')).prod

Tactic:
rw [List.map, List.prod_cons, List.prod_cons, mul_right' a hn hl', ih h]

Result:
no goals

Proof state:
case cons
a : ℤ
n : ℕ
l' : List ℕ
ih : (∀ n ∈ l', n ≠ 0) → J(a | l'.prod) = (List.map (fun n => J(a | n)) l').prod
hl : ∀ n_1 ∈ n :: l', n_1 ≠ 0
⊢ J(a | (n :: l').prod) = (List.map (fun n => J(a | n)) (n :: l')).prod

Tactic:
have hn := hl n (List.mem_cons_self n l')

Result:
case cons
a : ℤ
n : ℕ
l' : List ℕ
ih : (∀ n ∈ l', n ≠ 0) → J(a | l'.prod) = (List.map (fun n => J(a | n)) l').prod
hl : ∀ n_1 ∈ n :: l', n_1 ≠ 0
hn : n ≠ 0
⊢ J(a | (n :: l').prod) = (List.map (fun n => J(a | n)) (n :: l')).prod

Proof state:
case cons
a : ℤ
n : ℕ
l' : List ℕ
ih : (∀ n ∈ l', n ≠ 0) → J(a | l'.prod) = (List.map (fun n => J(a | n)) l').prod
hl : ∀ n_1 ∈ n :: l', n_1 ≠ 0
hn : n ≠ 0
⊢ J(a | (n :: l').prod) = (List.map (fun n => J(a | n)) (n :: l')).prod

Tactic:
have hl' := List.prod_ne_zero fun hf => hl 0 (List.mem_cons_of_mem _ hf) rfl

Result:
case cons
a : ℤ
n : ℕ
l' : List ℕ
ih : (∀ n ∈ l', n ≠ 0) → J(a | l'.prod) = (List.map (fun n => J(a | n)) l').prod
hl : ∀ n_1 ∈ n :: l', n_1 ≠ 0
hn : n ≠ 0
hl' : l'.prod ≠ 0
⊢ J(a | (n :: l').prod) = (List.map (fun n => J(a | n)) (n :: l')).prod

Proof state:
case cons
a : ℤ
n : ℕ
l' : List ℕ
ih : (∀ n ∈ l', n ≠ 0) → J(a | l'.prod) = (List.map (fun n => J(a | n)) l').prod
hl : ∀ n_1 ∈ n :: l', n_1 ≠ 0
hn : n ≠ 0
hl' : l'.prod ≠ 0
⊢ J(a | (n :: l').prod) = (List.map (fun n => J(a | n)) (n :: l')).prod

Tactic:
have h := fun m hm => hl m (List.mem_cons_of_mem _ hm)

Result:
case cons
a : ℤ
n : ℕ
l' : List ℕ
ih : (∀ n ∈ l', n ≠ 0) → J(a | l'.prod) = (List.map (fun n => J(a | n)) l').prod
hl : ∀ n_1 ∈ n :: l', n_1 ≠ 0
hn : n ≠ 0
hl' : l'.prod ≠ 0
h : ∀ m ∈ l', m ≠ 0
⊢ J(a | (n :: l').prod) = (List.map (fun n => J(a | n)) (n :: l')).prod
-- Mathlib/Data/Multiset/UnionInter.lean
theorem disjoint_iff_ne {s t : Multiset α} : Disjoint s t ↔ ∀ a ∈ s, ∀ b ∈ t, a ≠ b

Proof state:
α : Type u_1
s t : Multiset α
⊢ _root_.Disjoint s t ↔ ∀ a ∈ s, ∀ b ∈ t, a ≠ b

Tactic:
simp [disjoint_left, imp_not_comm]

Result:
no goals
-- Mathlib/Analysis/Calculus/FDeriv/Analytic.lean
theorem PartialHomeomorph.analyticAt_symm (f : PartialHomeomorph E F) {a : F}
    {i : E ≃L[𝕜] F} (h0 : a ∈ f.target) (h : AnalyticAt 𝕜 f (f.symm a))
    (h' : fderiv 𝕜 f (f.symm a) = i) :
    AnalyticAt 𝕜 f.symm a

Proof state:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : PartialHomeomorph E F
a : F
i : E ≃L[𝕜] F
h0 : a ∈ f.target
h : AnalyticAt 𝕜 (↑f) (↑f.symm a)
h' : fderiv 𝕜 (↑f) (↑f.symm a) = ↑i
this : a = ↑f (↑f.symm a)
⊢ AnalyticAt 𝕜 (↑f.symm) (↑f (↑f.symm a))

Tactic:
exact f.analyticAt_symm' (by simp [h0]) h h'

Result:
no goals

Proof state:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : PartialHomeomorph E F
a : F
i : E ≃L[𝕜] F
h0 : a ∈ f.target
h : AnalyticAt 𝕜 (↑f) (↑f.symm a)
h' : fderiv 𝕜 (↑f) (↑f.symm a) = ↑i
⊢ a = ↑f (↑f.symm a)

Tactic:
simp [h0]

Result:
no goals

Proof state:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : PartialHomeomorph E F
a : F
i : E ≃L[𝕜] F
h0 : a ∈ f.target
h : AnalyticAt 𝕜 (↑f) (↑f.symm a)
h' : fderiv 𝕜 (↑f) (↑f.symm a) = ↑i
this : a = ↑f (↑f.symm a)
⊢ ↑f.symm a ∈ f.source

Tactic:
simp [h0]

Result:
no goals

Proof state:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : PartialHomeomorph E F
a : F
i : E ≃L[𝕜] F
h0 : a ∈ f.target
h : AnalyticAt 𝕜 (↑f) (↑f.symm a)
h' : fderiv 𝕜 (↑f) (↑f.symm a) = ↑i
⊢ AnalyticAt 𝕜 (↑f.symm) a

Tactic:
have : a = f (f.symm a) := by simp [h0]

Result:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : PartialHomeomorph E F
a : F
i : E ≃L[𝕜] F
h0 : a ∈ f.target
h : AnalyticAt 𝕜 (↑f) (↑f.symm a)
h' : fderiv 𝕜 (↑f) (↑f.symm a) = ↑i
this : a = ↑f (↑f.symm a)
⊢ AnalyticAt 𝕜 (↑f.symm) a

Proof state:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : PartialHomeomorph E F
a : F
i : E ≃L[𝕜] F
h0 : a ∈ f.target
h : AnalyticAt 𝕜 (↑f) (↑f.symm a)
h' : fderiv 𝕜 (↑f) (↑f.symm a) = ↑i
this : a = ↑f (↑f.symm a)
⊢ AnalyticAt 𝕜 (↑f.symm) a

Tactic:
rw [this]

Result:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : PartialHomeomorph E F
a : F
i : E ≃L[𝕜] F
h0 : a ∈ f.target
h : AnalyticAt 𝕜 (↑f) (↑f.symm a)
h' : fderiv 𝕜 (↑f) (↑f.symm a) = ↑i
this : a = ↑f (↑f.symm a)
⊢ AnalyticAt 𝕜 (↑f.symm) (↑f (↑f.symm a))
-- Mathlib/Data/Set/MemPartition.lean
lemma disjoint_memPartition (f : ℕ → Set α) (n : ℕ) {u v : Set α}
    (hu : u ∈ memPartition f n) (hv : v ∈ memPartition f n) (huv : u ≠ v) :
    Disjoint u v

Proof state:
case succ
α : Type u_1
f : ℕ → Set α
n : ℕ
ih : ∀ {u v : Set α}, u ∈ memPartition f n → v ∈ memPartition f n → u ≠ v → Disjoint u v
u v : Set α
hu : u ∈ memPartition f (n + 1)
hv : v ∈ memPartition f (n + 1)
huv : u ≠ v
⊢ Disjoint u v

Tactic:
rw [memPartition_succ] at hu hv

Result:
case succ
α : Type u_1
f : ℕ → Set α
n : ℕ
ih : ∀ {u v : Set α}, u ∈ memPartition f n → v ∈ memPartition f n → u ≠ v → Disjoint u v
u v : Set α
hu : u ∈ {s | ∃ u ∈ memPartition f n, s = u ∩ f n ∨ s = u \ f n}
hv : v ∈ {s | ∃ u ∈ memPartition f n, s = u ∩ f n ∨ s = u \ f n}
huv : u ≠ v
⊢ Disjoint u v

Proof state:
case zero
α : Type u_1
f : ℕ → Set α
u v : Set α
huv : u ≠ v
hu : u = univ
hv : v = univ
⊢ Disjoint u v

Tactic:
rw [hu, hv] at huv

Result:
case zero
α : Type u_1
f : ℕ → Set α
u v : Set α
huv : univ ≠ univ
hu : u = univ
hv : v = univ
⊢ Disjoint u v
-- Mathlib/Algebra/BigOperators/Group/Finset/Basic.lean
theorem prod_toFinset {M : Type*} [DecidableEq α] [CommMonoid M] (f : α → M) :
    ∀ {l : List α} (_hl : l.Nodup), l.toFinset.prod f = (l.map f).prod
  | [], _ => by simp
  | a :: l, hl => by
    let ⟨not_mem, hl⟩ := List.nodup_cons.mp hl
    simp [Finset.prod_insert (mt List.mem_toFinset.mp not_mem), prod_toFinset _ hl]

Proof state:
α : Type u_3
M : Type u_6
inst✝¹ : DecidableEq α
inst✝ : CommMonoid M
f : α → M
a : α
l : List α
hl : (a :: l).Nodup
⊢ (a :: l).toFinset.prod f = (map f (a :: l)).prod

Tactic:
let ⟨not_mem, hl⟩ := List.nodup_cons.mp hl

Result:
α : Type u_3
M : Type u_6
inst✝¹ : DecidableEq α
inst✝ : CommMonoid M
f : α → M
a : α
l : List α
hl✝ : (a :: l).Nodup
not_mem : a ∉ l
hl : l.Nodup
⊢ (a :: l).toFinset.prod f = (map f (a :: l)).prod

Proof state:
α : Type u_3
M : Type u_6
inst✝¹ : DecidableEq α
inst✝ : CommMonoid M
f : α → M
a : α
l : List α
hl✝ : (a :: l).Nodup
not_mem : a ∉ l
hl : l.Nodup
⊢ (a :: l).toFinset.prod f = (map f (a :: l)).prod

Tactic:
simp [Finset.prod_insert (mt List.mem_toFinset.mp not_mem), prod_toFinset _ hl]

Result:
no goals

Proof state:
α : Type u_3
M : Type u_6
inst✝¹ : DecidableEq α
inst✝ : CommMonoid M
f : α → M
x✝ : [].Nodup
⊢ [].toFinset.prod f = (map f []).prod

Tactic:
simp

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem sub_le_sub_iff_le {x y z : BitVec w} (hxz : z ≤ x) (hyz : z ≤ y) :
    (x - z ≤ y - z) ↔ x ≤ y

Proof state:
w : Nat
x y z : BitVec w
hxz : z.toNat ≤ x.toNat
hyz : z.toNat ≤ y.toNat
⊢ x.toNat - z.toNat ≤ y.toNat - z.toNat ↔ x.toNat ≤ y.toNat

Tactic:
omega

Result:
no goals

Proof state:
w : Nat
x y z : BitVec w
hxz : z.toNat ≤ x.toNat
hyz : z.toNat ≤ y.toNat
⊢ z.toNat ≤ y.toNat

Tactic:
omega

Result:
no goals

Proof state:
w : Nat
x y z : BitVec w
hxz : z.toNat ≤ x.toNat
hyz : z.toNat ≤ y.toNat
⊢ z ≤ y

Tactic:
rw [BitVec.le_def]

Result:
w : Nat
x y z : BitVec w
hxz : z.toNat ≤ x.toNat
hyz : z.toNat ≤ y.toNat
⊢ z.toNat ≤ y.toNat

Proof state:
w : Nat
x y z : BitVec w
hxz : z.toNat ≤ x.toNat
hyz : z.toNat ≤ y.toNat
⊢ z ≤ x

Tactic:
rw [BitVec.le_def]

Result:
w : Nat
x y z : BitVec w
hxz : z.toNat ≤ x.toNat
hyz : z.toNat ≤ y.toNat
⊢ z.toNat ≤ x.toNat

Proof state:
w : Nat
x y z : BitVec w
hxz : z.toNat ≤ x.toNat
hyz : z.toNat ≤ y.toNat
⊢ (x - z).toNat ≤ (y - z).toNat ↔ x.toNat ≤ y.toNat

Tactic:
rw [BitVec.toNat_sub_of_le (by rw [BitVec.le_def]; omega),
  BitVec.toNat_sub_of_le (by rw [BitVec.le_def]; omega)]

Result:
w : Nat
x y z : BitVec w
hxz : z.toNat ≤ x.toNat
hyz : z.toNat ≤ y.toNat
⊢ x.toNat - z.toNat ≤ y.toNat - z.toNat ↔ x.toNat ≤ y.toNat

Proof state:
w : Nat
x y z : BitVec w
hxz : z ≤ x
hyz : z ≤ y
⊢ x - z ≤ y - z ↔ x ≤ y

Tactic:
simp_all only [BitVec.le_def]

Result:
w : Nat
x y z : BitVec w
hxz : z.toNat ≤ x.toNat
hyz : z.toNat ≤ y.toNat
⊢ (x - z).toNat ≤ (y - z).toNat ↔ x.toNat ≤ y.toNat

Proof state:
w : Nat
x y z : BitVec w
hxz : z.toNat ≤ x.toNat
hyz : z.toNat ≤ y.toNat
⊢ z.toNat ≤ x.toNat

Tactic:
omega

Result:
no goals
-- Mathlib/MeasureTheory/Function/LpSpace/Basic.lean
@[simp]
lemma norm_toLp (f : α → E) (hf : MemLp f p μ) : ‖hf.toLp f‖ = ENNReal.toReal (eLpNorm f p μ)

Proof state:
α : Type u_1
E : Type u_4
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : NormedAddCommGroup E
f : α → E
hf : MemLp f p μ
⊢ ‖MemLp.toLp f hf‖ = (eLpNorm f p μ).toReal

Tactic:
rw [norm_def, eLpNorm_congr_ae (MemLp.coeFn_toLp hf)]

Result:
no goals
-- Mathlib/SetTheory/Cardinal/Basic.lean
theorem mk_le_iff_forall_finset_subset_card_le {α : Type u} {n : ℕ} {t : Set α} :
    #t ≤ n ↔ ∀ s : Finset α, (s : Set α) ⊆ t → s.card ≤ n

Proof state:
α : Type u
n : ℕ
t : Set α
H : ∀ (s : Finset α), ↑s ⊆ t → s.card ≤ n
s : Finset ↑t
u : Finset α := Finset.image Subtype.val s
this : u.card = s.card
⊢ u.card ≤ n

Tactic:
apply H

Result:
case a
α : Type u
n : ℕ
t : Set α
H : ∀ (s : Finset α), ↑s ⊆ t → s.card ≤ n
s : Finset ↑t
u : Finset α := Finset.image Subtype.val s
this : u.card = s.card
⊢ ↑u ⊆ t

Proof state:
α : Type u
n : ℕ
t : Set α
H : ∀ (s : Finset α), ↑s ⊆ t → s.card ≤ n
s : Finset ↑t
u : Finset α := Finset.image Subtype.val s
⊢ s.card ≤ n

Tactic:
have : u.card = s.card := Finset.card_image_of_injOn Subtype.coe_injective.injOn

Result:
α : Type u
n : ℕ
t : Set α
H : ∀ (s : Finset α), ↑s ⊆ t → s.card ≤ n
s : Finset ↑t
u : Finset α := Finset.image Subtype.val s
this : u.card = s.card
⊢ s.card ≤ n

Proof state:
α : Type u
n : ℕ
t : Set α
H : ∀ (s : Finset α), ↑s ⊆ t → s.card ≤ n
s : Finset ↑t
⊢ s.card ≤ n

Tactic:
let u : Finset α := s.image Subtype.val

Result:
α : Type u
n : ℕ
t : Set α
H : ∀ (s : Finset α), ↑s ⊆ t → s.card ≤ n
s : Finset ↑t
u : Finset α := Finset.image Subtype.val s
⊢ s.card ≤ n

Proof state:
α : Type u
n : ℕ
t : Set α
⊢ #↑t ≤ ↑n ↔ ∀ (s : Finset α), ↑s ⊆ t → s.card ≤ n

Tactic:
refine ⟨fun H s hs ↦ by simpa using (mk_le_mk_of_subset hs).trans H, fun H ↦ ?_⟩

Result:
α : Type u
n : ℕ
t : Set α
H : ∀ (s : Finset α), ↑s ⊆ t → s.card ≤ n
⊢ #↑t ≤ ↑n

Proof state:
α : Type u
n : ℕ
t : Set α
H : ∀ (s : Finset α), ↑s ⊆ t → s.card ≤ n
s : Finset ↑t
⊢ s.card ≤ n

Tactic:
classical
let u : Finset α := s.image Subtype.val
have : u.card = s.card := Finset.card_image_of_injOn Subtype.coe_injective.injOn
rw [← this]
apply H
simp only [u, Finset.coe_image, image_subset_iff, Subtype.coe_preimage_self, subset_univ]

Result:
no goals

Proof state:
α : Type u
n : ℕ
t : Set α
H : ∀ (s : Finset α), ↑s ⊆ t → s.card ≤ n
s : Finset ↑t
u : Finset α := Finset.image Subtype.val s
this : u.card = s.card
⊢ s.card ≤ n

Tactic:
rw [← this]

Result:
α : Type u
n : ℕ
t : Set α
H : ∀ (s : Finset α), ↑s ⊆ t → s.card ≤ n
s : Finset ↑t
u : Finset α := Finset.image Subtype.val s
this : u.card = s.card
⊢ u.card ≤ n

Proof state:
α : Type u
n : ℕ
t : Set α
H : #↑t ≤ ↑n
s : Finset α
hs : ↑s ⊆ t
⊢ s.card ≤ n

Tactic:
simpa using (mk_le_mk_of_subset hs).trans H

Result:
no goals

Proof state:
α : Type u
n : ℕ
t : Set α
H : ∀ (s : Finset α), ↑s ⊆ t → s.card ≤ n
⊢ #↑t ≤ ↑n

Tactic:
apply card_le_of (fun s ↦ ?_)

Result:
α : Type u
n : ℕ
t : Set α
H : ∀ (s : Finset α), ↑s ⊆ t → s.card ≤ n
s : Finset ↑t
⊢ s.card ≤ n

Proof state:
case a
α : Type u
n : ℕ
t : Set α
H : ∀ (s : Finset α), ↑s ⊆ t → s.card ≤ n
s : Finset ↑t
u : Finset α := Finset.image Subtype.val s
this : u.card = s.card
⊢ ↑u ⊆ t

Tactic:
simp only [u, Finset.coe_image, image_subset_iff, Subtype.coe_preimage_self, subset_univ]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem toFin_allOnes : (allOnes w).toFin = Fin.ofNat' (2^w) (2^w - 1)

Proof state:
w : Nat
⊢ (allOnes w).toFin = Fin.ofNat' (2 ^ w) (2 ^ w - 1)

Tactic:
ext

Result:
case h
w : Nat
⊢ ↑(allOnes w).toFin = ↑(Fin.ofNat' (2 ^ w) (2 ^ w - 1))

Proof state:
case h
w : Nat
⊢ ↑(allOnes w).toFin = ↑(Fin.ofNat' (2 ^ w) (2 ^ w - 1))

Tactic:
simp

Result:
no goals
-- Mathlib/Order/WellFounded.lean
theorem Set.range_injOn_strictMono [WellFoundedLT β] :
    Set.InjOn Set.range { f : β → γ | StrictMono f }

Proof state:
case h.intro.inr.inr
β : Type u_2
γ : Type u_3
inst✝² : LinearOrder β
inst✝¹ : Preorder γ
inst✝ : WellFoundedLT β
f : β → γ
hf : f ∈ {f | StrictMono f}
g : β → γ
hg : g ∈ {f | StrictMono f}
hfg : range f = range g
a✝ a : β
IH : ∀ y < a, f y = g y
b : β
hb : g b = f a
h : a < b
⊢ f a = g a

Tactic:
obtain ⟨c, hc⟩ := hfg.symm ▸ mem_range_self a

Result:
case h.intro.inr.inr.intro
β : Type u_2
γ : Type u_3
inst✝² : LinearOrder β
inst✝¹ : Preorder γ
inst✝ : WellFoundedLT β
f : β → γ
hf : f ∈ {f | StrictMono f}
g : β → γ
hg : g ∈ {f | StrictMono f}
hfg : range f = range g
a✝ a : β
IH : ∀ y < a, f y = g y
b : β
hb : g b = f a
h : a < b
c : β
hc : f c = g a
⊢ f a = g a
-- Mathlib/RingTheory/LocalProperties/Basic.lean
theorem Ideal.localized'_eq_map (I : Ideal R) :
    Submodule.localized' S p (Algebra.linearMap R S) I = I.map (algebraMap R S)

Proof state:
R : Type u_1
S : Type u_2
inst✝³ : CommSemiring R
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
p : Submonoid R
inst✝ : IsLocalization p S
I : Ideal R
⊢ Submodule.localized' S p (Algebra.linearMap R S) I = map (algebraMap R S) I

Tactic:
rw [map, span, Submodule.localized'_eq_span, Algebra.coe_linearMap]

Result:
no goals
-- Mathlib/Algebra/Homology/ComplexShape.lean
theorem prev_eq' (c : ComplexShape ι) {i j : ι} (h : c.Rel i j) : c.prev j = i

Proof state:
ι : Type u_1
c : ComplexShape ι
i j : ι
h : c.Rel i j
⊢ c.prev j = i

Tactic:
apply c.prev_eq _ h

Result:
ι : Type u_1
c : ComplexShape ι
i j : ι
h : c.Rel i j
⊢ c.Rel (c.prev j) j

Proof state:
ι : Type u_1
c : ComplexShape ι
i j : ι
h : c.Rel i j
⊢ c.Rel (c.prev j) j

Tactic:
rw [prev, dif_pos]

Result:
ι : Type u_1
c : ComplexShape ι
i j : ι
h : c.Rel i j
⊢ c.Rel (Exists.choose ?hc) j

case hc
ι : Type u_1
c : ComplexShape ι
i j : ι
h : c.Rel i j
⊢ ∃ i, c.Rel i j

Proof state:
ι : Type u_1
c : ComplexShape ι
i j : ι
h : c.Rel i j
⊢ c.Rel (Exists.choose ?hc) j

case hc
ι : Type u_1
c : ComplexShape ι
i j : ι
h : c.Rel i j
⊢ ∃ i, c.Rel i j

Tactic:
exact Exists.choose_spec (⟨i, h⟩ : ∃ k, c.Rel k j)

Result:
no goals
-- Mathlib/Algebra/MvPolynomial/Degrees.lean
theorem degrees_pow_le {p : MvPolynomial σ R} {n : ℕ} : (p ^ n).degrees ≤ n • p.degrees

Proof state:
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
p : MvPolynomial σ R
n : ℕ
⊢ (p ^ n).degrees ≤ n • p.degrees

Tactic:
simpa using degrees_prod_le (s := .range n) (f := fun _ ↦ p)

Result:
no goals
-- Mathlib/SetTheory/Ordinal/Arithmetic.lean
theorem lt_mul_succ_div (a) {b : Ordinal} (h : b ≠ 0) : a < b * succ (a / b)

Proof state:
a b : Ordinal.{u_4}
h : b ≠ 0
⊢ a < b * succ (a / b)

Tactic:
rw [div_def a h]

Result:
a b : Ordinal.{u_4}
h : b ≠ 0
⊢ a < b * succ (sInf {o | a < b * succ o})

Proof state:
a b : Ordinal.{u_4}
h : b ≠ 0
⊢ a < b * succ (sInf {o | a < b * succ o})

Tactic:
exact csInf_mem (div_nonempty h)

Result:
no goals
-- Mathlib/MeasureTheory/Measure/Dirac.lean
theorem dirac_apply_of_mem {a : α} (h : a ∈ s) : dirac a s = 1

Proof state:
α : Type u_1
inst✝ : MeasurableSpace α
s : Set α
a : α
h : a ∈ s
this : ∀ (t : Set α), a ∈ t → t.indicator 1 a = 1
⊢ (dirac a) s ≤ univ.indicator 1 a

Tactic:
rw [← dirac_apply' a MeasurableSet.univ]

Result:
α : Type u_1
inst✝ : MeasurableSpace α
s : Set α
a : α
h : a ∈ s
this : ∀ (t : Set α), a ∈ t → t.indicator 1 a = 1
⊢ (dirac a) s ≤ (dirac a) univ

Proof state:
α : Type u_1
inst✝ : MeasurableSpace α
s : Set α
a : α
h : a ∈ s
this : ∀ (t : Set α), a ∈ t → t.indicator 1 a = 1
⊢ (dirac a) s ≤ (dirac a) univ

Tactic:
exact measure_mono (subset_univ s)

Result:
no goals

Proof state:
α : Type u_1
inst✝ : MeasurableSpace α
s : Set α
a : α
h : a ∈ s
this : ∀ (t : Set α), a ∈ t → t.indicator 1 a = 1
⊢ (dirac a) s = 1

Tactic:
refine le_antisymm (this univ trivial ▸ ?_) (this s h ▸ le_dirac_apply)

Result:
α : Type u_1
inst✝ : MeasurableSpace α
s : Set α
a : α
h : a ∈ s
this : ∀ (t : Set α), a ∈ t → t.indicator 1 a = 1
⊢ (dirac a) s ≤ univ.indicator 1 a

Proof state:
α : Type u_1
inst✝ : MeasurableSpace α
s : Set α
a : α
h : a ∈ s
⊢ (dirac a) s = 1

Tactic:
have : ∀ t : Set α, a ∈ t → t.indicator (1 : α → ℝ≥0∞) a = 1 := fun t ht => indicator_of_mem ht 1

Result:
α : Type u_1
inst✝ : MeasurableSpace α
s : Set α
a : α
h : a ∈ s
this : ∀ (t : Set α), a ∈ t → t.indicator 1 a = 1
⊢ (dirac a) s = 1
-- Mathlib/CategoryTheory/EqToHom.lean
theorem dcongr_arg {ι : Type*} {F G : ι → C} (α : ∀ i, F i ⟶ G i) {i j : ι} (h : i = j) :
    α i = eqToHom (congr_arg F h) ≫ α j ≫ eqToHom (congr_arg G h.symm)

Proof state:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
ι : Type u_2
F G : ι → C
α : (i : ι) → F i ⟶ G i
i j : ι
h : i = j
⊢ α i = eqToHom ⋯ ≫ α j ≫ eqToHom ⋯

Tactic:
subst h

Result:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
ι : Type u_2
F G : ι → C
α : (i : ι) → F i ⟶ G i
i : ι
⊢ α i = eqToHom ⋯ ≫ α i ≫ eqToHom ⋯

Proof state:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
ι : Type u_2
F G : ι → C
α : (i : ι) → F i ⟶ G i
i : ι
⊢ α i = eqToHom ⋯ ≫ α i ≫ eqToHom ⋯

Tactic:
simp

Result:
no goals
-- Mathlib/NumberTheory/Padics/PadicVal/Basic.lean
theorem padicValNat_self [Fact p.Prime] : padicValNat p p = 1

Proof state:
p : ℕ
inst✝ : Fact (Nat.Prime p)
⊢ multiplicity p p = 1

Tactic:
simp

Result:
no goals

Proof state:
p : ℕ
inst✝ : Fact (Nat.Prime p)
⊢ padicValNat p p = 1

Tactic:
rw [padicValNat_def (@Fact.out p.Prime).pos]

Result:
p : ℕ
inst✝ : Fact (Nat.Prime p)
⊢ multiplicity p p = 1
-- Mathlib/Data/Nat/Factorization/Basic.lean
theorem ordCompl_pos {n : ℕ} (p : ℕ) (hn : n ≠ 0) : 0 < ordCompl[p] n

Proof state:
n p : ℕ
hn : n ≠ 0
⊢ 0 < n / p ^ n.factorization p

Tactic:
if pp : p.Prime then
  exact Nat.div_pos (ordProj_le p hn) (ordProj_pos n p)
else
  simpa [Nat.factorization_eq_zero_of_non_prime n pp] using hn.bot_lt

Result:
no goals

Proof state:
n p : ℕ
hn : n ≠ 0
pp : ¬Prime p
⊢ 0 < n / p ^ n.factorization p

Tactic:
simpa [Nat.factorization_eq_zero_of_non_prime n pp] using hn.bot_lt

Result:
no goals

Proof state:
n p : ℕ
hn : n ≠ 0
pp : Prime p
⊢ 0 < n / p ^ n.factorization p

Tactic:
exact Nat.div_pos (ordProj_le p hn) (ordProj_pos n p)

Result:
no goals