harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Computability/AkraBazzi/AkraBazzi.lean
lemma isLittleO_self_div_log_id :
    (fun (n : ℕ) => n / log n ^ 2) =o[atTop] (fun (n : ℕ) => (n : ℝ))

Proof state:
⊢ (fun n => 1) = fun x => 1 ^ 2

Tactic:
simp

Result:
no goals

Proof state:
⊢ (fun n => ↑n * 1⁻¹) = fun n => ↑n

Tactic:
ext

Result:
case h
x✝ : ℕ
⊢ ↑x✝ * 1⁻¹ = ↑x✝

Proof state:
⊢ 0 < 2

Tactic:
norm_num

Result:
no goals

Proof state:
⊢ (fun n => ↑n * (log ↑n ^ 2)⁻¹) =o[atTop] fun n => ↑n * 1⁻¹

Tactic:
refine IsBigO.mul_isLittleO (isBigO_refl _ _) ?_

Result:
⊢ (fun n => (log ↑n ^ 2)⁻¹) =o[atTop] fun n => 1⁻¹

Proof state:
case main

⊢ (fun n => 1) =o[atTop] fun n => log ↑n ^ 2

case zero

⊢ ∀ᶠ (x : ℕ) in atTop, 1 = 0 → log ↑x ^ 2 = 0

Tactic:
case zero => simp

Result:
case main

⊢ (fun n => 1) =o[atTop] fun n => log ↑n ^ 2

Proof state:
⊢ ∀ᶠ (x : ℕ) in atTop, 1 = 0 → log ↑x ^ 2 = 0

Tactic:
simp

Result:
no goals

Proof state:
⊢ (fun n => ↑n / log ↑n ^ 2) = fun n => ↑n * (log ↑n ^ 2)⁻¹

Tactic:
simp_rw [div_eq_mul_inv]

Result:
no goals

Proof state:
⊢ (fun n => ↑n / log ↑n ^ 2) =o[atTop] fun n => ↑n

Tactic:
calc (fun (n : ℕ) => (n : ℝ) / log n ^ 2) = fun (n : ℕ) => (n : ℝ) * ((log n) ^ 2)⁻¹ := by
                simp_rw [div_eq_mul_inv]
       _ =o[atTop] fun (n : ℕ) => (n : ℝ) * 1⁻¹ := by
                refine IsBigO.mul_isLittleO (isBigO_refl _ _) ?_
                refine IsLittleO.inv_rev ?main ?zero
                case zero => simp
                case main => calc
                  _ = (fun (_ : ℕ) => ((1 : ℝ) ^ 2))     := by simp
                  _ =o[atTop] (fun (n : ℕ) => (log n)^2) :=
                        IsLittleO.pow (IsLittleO.natCast_atTop
                          <| isLittleO_const_log_atTop) (by norm_num)
       _ = (fun (n : ℕ) => (n : ℝ)) := by ext; simp

Result:
no goals

Proof state:
⊢ (fun n => (log ↑n ^ 2)⁻¹) =o[atTop] fun n => 1⁻¹

Tactic:
refine IsLittleO.inv_rev ?main ?zero

Result:
case main

⊢ (fun n => 1) =o[atTop] fun n => log ↑n ^ 2

case zero

⊢ ∀ᶠ (x : ℕ) in atTop, 1 = 0 → log ↑x ^ 2 = 0

Proof state:
case main

⊢ (fun n => 1) =o[atTop] fun n => log ↑n ^ 2

Tactic:
case main => calc
  _ = (fun (_ : ℕ) => ((1 : ℝ) ^ 2))     := by simp
  _ =o[atTop] (fun (n : ℕ) => (log n)^2) :=
        IsLittleO.pow (IsLittleO.natCast_atTop
          <| isLittleO_const_log_atTop) (by norm_num)

Result:
no goals

Proof state:
case h
x✝ : ℕ
⊢ ↑x✝ * 1⁻¹ = ↑x✝

Tactic:
simp

Result:
no goals

Proof state:
⊢ (fun n => 1) =o[atTop] fun n => log ↑n ^ 2

Tactic:
calc
_ = (fun (_ : ℕ) => ((1 : ℝ) ^ 2))     := by simp
_ =o[atTop] (fun (n : ℕ) => (log n)^2) :=
IsLittleO.pow (IsLittleO.natCast_atTop
<| isLittleO_const_log_atTop) (by norm_num)

Result:
no goals
-- Mathlib/MeasureTheory/Measure/LevyProkhorovMetric.lean
lemma left_measure_le_of_levyProkhorovEDist_lt {μ ν : Measure Ω} {c : ℝ≥0∞}
    (h : levyProkhorovEDist μ ν < c) {B : Set Ω} (B_mble : MeasurableSet B) :
    μ B ≤ ν (thickening c.toReal B) + c

Proof state:
Ω : Type u_1
inst✝¹ : MeasurableSpace Ω
inst✝ : PseudoEMetricSpace Ω
μ ν : Measure Ω
c : ℝ≥0∞
h : levyProkhorovEDist μ ν < c
B : Set Ω
B_mble : MeasurableSet B
⊢ μ B ≤ ν (thickening c.toReal B) + c

Tactic:
obtain ⟨c', ⟨hc', lt_c⟩⟩ := sInf_lt_iff.mp h

Result:
case intro.intro
Ω : Type u_1
inst✝¹ : MeasurableSpace Ω
inst✝ : PseudoEMetricSpace Ω
μ ν : Measure Ω
c : ℝ≥0∞
h : levyProkhorovEDist μ ν < c
B : Set Ω
B_mble : MeasurableSet B
c' : ℝ≥0∞
hc' :
  c' ∈ {ε | ∀ (B : Set Ω), MeasurableSet B → μ B ≤ ν (thickening ε.toReal B) + ε ∧ ν B ≤ μ (thickening ε.toReal B) + ε}
lt_c : c' < c
⊢ μ B ≤ ν (thickening c.toReal B) + c

Proof state:
case intro.intro
Ω : Type u_1
inst✝¹ : MeasurableSpace Ω
inst✝ : PseudoEMetricSpace Ω
μ ν : Measure Ω
c : ℝ≥0∞
h : levyProkhorovEDist μ ν < c
B : Set Ω
B_mble : MeasurableSet B
c' : ℝ≥0∞
hc' :
  c' ∈ {ε | ∀ (B : Set Ω), MeasurableSet B → μ B ≤ ν (thickening ε.toReal B) + ε ∧ ν B ≤ μ (thickening ε.toReal B) + ε}
lt_c : c' < c
⊢ μ B ≤ ν (thickening c.toReal B) + c

Tactic:
exact meas_le_of_le_of_forall_le_meas_thickening_add μ ν lt_c.le (hc' B B_mble).1

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Tactic/BVDecide/Normalize/BitVec.lean
theorem BitVec.not_lt_zero (a : BitVec n) : (BitVec.ult a 0#n) = false

Proof state:
n : Nat
a : BitVec n
⊢ a.ult 0#n = false

Tactic:
rfl

Result:
no goals
-- Mathlib/Topology/DenseEmbedding.lean
theorem dense_image (di : IsDenseInducing i) {s : Set α} : Dense (i '' s) ↔ Dense s

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
i : α → β
di : IsDenseInducing i
s : Set α
H : Dense (i '' s)
x : α
⊢ x ∈ univ

Tactic:
trivial

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
i : α → β
di : IsDenseInducing i
s : Set α
⊢ Dense (i '' s) ↔ Dense s

Tactic:
refine ⟨fun H x => ?_, di.dense.dense_image di.continuous⟩

Result:
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
i : α → β
di : IsDenseInducing i
s : Set α
H : Dense (i '' s)
x : α
⊢ x ∈ closure s

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
i : α → β
di : IsDenseInducing i
s : Set α
H : Dense (i '' s)
x : α
⊢ x ∈ closure s

Tactic:
rw [di.isInducing.closure_eq_preimage_closure_image, H.closure_eq, preimage_univ]

Result:
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
i : α → β
di : IsDenseInducing i
s : Set α
H : Dense (i '' s)
x : α
⊢ x ∈ univ
-- Mathlib/Algebra/BigOperators/Fin.lean
theorem prod_Ioi_zero {M : Type*} [CommMonoid M] {n : ℕ} {v : Fin n.succ → M} :
    ∏ i ∈ Ioi 0, v i = ∏ j : Fin n, v j.succ

Proof state:
M : Type u_3
inst✝ : CommMonoid M
n : ℕ
v : Fin n.succ → M
⊢ ∏ i ∈ Ioi 0, v i = ∏ j : Fin n, v j.succ

Tactic:
rw [Ioi_zero_eq_map, Finset.prod_map, val_succEmb]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Nat/Lemmas.lean
theorem one_le_two_pow : 1 ≤ 2 ^ n :=
  if h : n = 0 then
    by subst h; simp
  else
    Nat.le_of_lt (Nat.one_lt_two_pow h)

Proof state:
n : Nat
h : n = 0
⊢ 1 ≤ 2 ^ n

Tactic:
subst h

Result:
⊢ 1 ≤ 2 ^ 0

Proof state:
⊢ 1 ≤ 2 ^ 0

Tactic:
simp

Result:
no goals
-- Mathlib/Analysis/Convolution.lean
theorem _root_.HasCompactSupport.hasDerivAt_convolution_right (hf : LocallyIntegrable f₀ μ)
    (hcg : HasCompactSupport g₀) (hg : ContDiff 𝕜 1 g₀) (x₀ : 𝕜) :
    HasDerivAt (f₀ ⋆[L, μ] g₀) ((f₀ ⋆[L, μ] deriv g₀) x₀) x₀

Proof state:
𝕜 : Type u𝕜
E : Type uE
E' : Type uE'
F : Type uF
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedAddCommGroup E'
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : RCLike 𝕜
inst✝⁵ : NormedSpace 𝕜 E
inst✝⁴ : NormedSpace 𝕜 E'
inst✝³ : NormedSpace ℝ F
inst✝² : NormedSpace 𝕜 F
f₀ : 𝕜 → E
g₀ : 𝕜 → E'
L : E →L[𝕜] E' →L[𝕜] F
μ : Measure 𝕜
inst✝¹ : μ.IsAddLeftInvariant
inst✝ : SFinite μ
hf : LocallyIntegrable f₀ μ
hcg : HasCompactSupport g₀
hg : ContDiff 𝕜 1 g₀
x₀ : 𝕜
⊢ HasDerivAt (f₀ ⋆[L, μ] g₀) ((f₀ ⋆[L, μ] deriv g₀) x₀) x₀

Tactic:
convert (hcg.hasFDerivAt_convolution_right L hf hg x₀).hasDerivAt using 1

Result:
case h.e'_9
𝕜 : Type u𝕜
E : Type uE
E' : Type uE'
F : Type uF
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedAddCommGroup E'
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : RCLike 𝕜
inst✝⁵ : NormedSpace 𝕜 E
inst✝⁴ : NormedSpace 𝕜 E'
inst✝³ : NormedSpace ℝ F
inst✝² : NormedSpace 𝕜 F
f₀ : 𝕜 → E
g₀ : 𝕜 → E'
L : E →L[𝕜] E' →L[𝕜] F
μ : Measure 𝕜
inst✝¹ : μ.IsAddLeftInvariant
inst✝ : SFinite μ
hf : LocallyIntegrable f₀ μ
hcg : HasCompactSupport g₀
hg : ContDiff 𝕜 1 g₀
x₀ : 𝕜
⊢ (f₀ ⋆[L, μ] deriv g₀) x₀ = ((f₀ ⋆[precompR 𝕜 L, μ] fderiv 𝕜 g₀) x₀) 1

Proof state:
case h.e'_9
𝕜 : Type u𝕜
E : Type uE
E' : Type uE'
F : Type uF
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedAddCommGroup E'
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : RCLike 𝕜
inst✝⁵ : NormedSpace 𝕜 E
inst✝⁴ : NormedSpace 𝕜 E'
inst✝³ : NormedSpace ℝ F
inst✝² : NormedSpace 𝕜 F
f₀ : 𝕜 → E
g₀ : 𝕜 → E'
L : E →L[𝕜] E' →L[𝕜] F
μ : Measure 𝕜
inst✝¹ : μ.IsAddLeftInvariant
inst✝ : SFinite μ
hf : LocallyIntegrable f₀ μ
hcg : HasCompactSupport g₀
hg : ContDiff 𝕜 1 g₀
x₀ : 𝕜
⊢ (f₀ ⋆[L, μ] deriv g₀) x₀ = (f₀ ⋆[L, μ] fun a => (fderiv 𝕜 g₀ a) 1) x₀

Tactic:
rfl

Result:
no goals

Proof state:
case h.e'_9
𝕜 : Type u𝕜
E : Type uE
E' : Type uE'
F : Type uF
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedAddCommGroup E'
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : RCLike 𝕜
inst✝⁵ : NormedSpace 𝕜 E
inst✝⁴ : NormedSpace 𝕜 E'
inst✝³ : NormedSpace ℝ F
inst✝² : NormedSpace 𝕜 F
f₀ : 𝕜 → E
g₀ : 𝕜 → E'
L : E →L[𝕜] E' →L[𝕜] F
μ : Measure 𝕜
inst✝¹ : μ.IsAddLeftInvariant
inst✝ : SFinite μ
hf : LocallyIntegrable f₀ μ
hcg : HasCompactSupport g₀
hg : ContDiff 𝕜 1 g₀
x₀ : 𝕜
⊢ (f₀ ⋆[L, μ] deriv g₀) x₀ = ((f₀ ⋆[precompR 𝕜 L, μ] fderiv 𝕜 g₀) x₀) 1

Tactic:
rw [convolution_precompR_apply L hf (hcg.fderiv 𝕜) (hg.continuous_fderiv le_rfl)]

Result:
case h.e'_9
𝕜 : Type u𝕜
E : Type uE
E' : Type uE'
F : Type uF
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedAddCommGroup E'
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : RCLike 𝕜
inst✝⁵ : NormedSpace 𝕜 E
inst✝⁴ : NormedSpace 𝕜 E'
inst✝³ : NormedSpace ℝ F
inst✝² : NormedSpace 𝕜 F
f₀ : 𝕜 → E
g₀ : 𝕜 → E'
L : E →L[𝕜] E' →L[𝕜] F
μ : Measure 𝕜
inst✝¹ : μ.IsAddLeftInvariant
inst✝ : SFinite μ
hf : LocallyIntegrable f₀ μ
hcg : HasCompactSupport g₀
hg : ContDiff 𝕜 1 g₀
x₀ : 𝕜
⊢ (f₀ ⋆[L, μ] deriv g₀) x₀ = (f₀ ⋆[L, μ] fun a => (fderiv 𝕜 g₀ a) 1) x₀
-- Mathlib/Data/Matrix/Block.lean
theorem fromBlocks_neg [Neg R] (A : Matrix n l R) (B : Matrix n m R) (C : Matrix o l R)
    (D : Matrix o m R) : -fromBlocks A B C D = fromBlocks (-A) (-B) (-C) (-D)

Proof state:
case a
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
R : Type u_10
inst✝ : Neg R
A : Matrix n l R
B : Matrix n m R
C : Matrix o l R
D : Matrix o m R
i : n ⊕ o
j : l ⊕ m
⊢ (-fromBlocks A B C D) i j = fromBlocks (-A) (-B) (-C) (-D) i j

Tactic:
cases i <;> cases j <;> simp [fromBlocks]

Result:
no goals

Proof state:
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
R : Type u_10
inst✝ : Neg R
A : Matrix n l R
B : Matrix n m R
C : Matrix o l R
D : Matrix o m R
⊢ -fromBlocks A B C D = fromBlocks (-A) (-B) (-C) (-D)

Tactic:
ext i j

Result:
case a
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
R : Type u_10
inst✝ : Neg R
A : Matrix n l R
B : Matrix n m R
C : Matrix o l R
D : Matrix o m R
i : n ⊕ o
j : l ⊕ m
⊢ (-fromBlocks A B C D) i j = fromBlocks (-A) (-B) (-C) (-D) i j
-- Mathlib/RingTheory/Ideal/Span.lean
theorem mem_span_singleton {x y : α} : x ∈ span ({y} : Set α) ↔ y ∣ x :=
  mem_span_singleton'.trans <| exists_congr fun _ => by rw [eq_comm, mul_comm]

Proof state:
α : Type u
inst✝ : CommSemiring α
x y x✝ : α
⊢ x✝ * y = x ↔ x = y * x✝

Tactic:
rw [eq_comm, mul_comm]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/RawLemmas.lean
theorem get!_insertMany_list_of_mem [EquivBEq α] [LawfulHashable α] [Inhabited β] (h : m.WF)
    {l : List (α × β)} {k k' : α} (k_beq : k == k') {v : β}
    (distinct : l.Pairwise (fun a b => (a.1 == b.1) = false)) (mem : ⟨k, v⟩ ∈ l) :
    get! (insertMany m l) k' = v

Proof state:
α : Type u
inst✝⁴ : BEq α
inst✝³ : Hashable α
β : Type v
m : Raw α fun x => β
inst✝² : EquivBEq α
inst✝¹ : LawfulHashable α
inst✝ : Inhabited β
h : m.WF
l : List (α × β)
k k' : α
k_beq : (k == k') = true
v : β
distinct : List.Pairwise (fun a b => (a.fst == b.fst) = false) l
mem : (k, v) ∈ l
⊢ get! (insertMany m l) k' = v

Tactic:
simp_to_raw using Raw₀.Const.get!_insertMany_list_of_mem

Result:
no goals
-- Mathlib/Algebra/MvPolynomial/Division.lean
theorem X_dvd_X [Nontrivial R] {i j : σ} :
    (X i : MvPolynomial σ R) ∣ (X j : MvPolynomial σ R) ↔ i = j

Proof state:
σ : Type u_1
R : Type u_2
inst✝¹ : CommSemiring R
inst✝ : Nontrivial R
i j : σ
⊢ X i ∣ X j ↔ i = j

Tactic:
refine monomial_one_dvd_monomial_one.trans ?_

Result:
σ : Type u_1
R : Type u_2
inst✝¹ : CommSemiring R
inst✝ : Nontrivial R
i j : σ
⊢ Finsupp.single i 1 ≤ Finsupp.single j 1 ↔ i = j

Proof state:
σ : Type u_1
R : Type u_2
inst✝¹ : CommSemiring R
inst✝ : Nontrivial R
i j : σ
⊢ Finsupp.single i 1 ≤ Finsupp.single j 1 ↔ i = j

Tactic:
simp_rw [Finsupp.single_le_iff, Nat.one_le_iff_ne_zero, Finsupp.single_apply_ne_zero,
  ne_eq, reduceCtorEq,not_false_eq_true, and_true]

Result:
no goals
-- Mathlib/LinearAlgebra/Matrix/PosDef.lean
@[simp]
lemma sqrt_mul_self : hA.sqrt * hA.sqrt = A

Proof state:
n : Type u_2
𝕜 : Type u_4
inst✝² : Fintype n
inst✝¹ : RCLike 𝕜
inst✝ : DecidableEq n
A : Matrix n n 𝕜
hA : A.PosSemidef
⊢ hA.sqrt * hA.sqrt = A

Tactic:
rw [← pow_two, sq_sqrt]

Result:
no goals
-- Mathlib/Topology/MetricSpace/Pseudo/Pi.lean
lemma dist_pi_le_iff' [Nonempty β] {f g : ∀ b, π b} {r : ℝ} :
    dist f g ≤ r ↔ ∀ b, dist (f b) (g b) ≤ r

Proof state:
case pos
β : Type u_2
π : β → Type u_3
inst✝² : Fintype β
inst✝¹ : (b : β) → PseudoMetricSpace (π b)
inst✝ : Nonempty β
f g : (b : β) → π b
r : ℝ
hr : 0 ≤ r
⊢ dist f g ≤ r ↔ ∀ (b : β), dist (f b) (g b) ≤ r

Tactic:
exact dist_pi_le_iff hr

Result:
no goals

Proof state:
β : Type u_2
π : β → Type u_3
inst✝² : Fintype β
inst✝¹ : (b : β) → PseudoMetricSpace (π b)
inst✝ : Nonempty β
f g : (b : β) → π b
r : ℝ
⊢ dist f g ≤ r ↔ ∀ (b : β), dist (f b) (g b) ≤ r

Tactic:
by_cases hr : 0 ≤ r

Result:
case pos
β : Type u_2
π : β → Type u_3
inst✝² : Fintype β
inst✝¹ : (b : β) → PseudoMetricSpace (π b)
inst✝ : Nonempty β
f g : (b : β) → π b
r : ℝ
hr : 0 ≤ r
⊢ dist f g ≤ r ↔ ∀ (b : β), dist (f b) (g b) ≤ r

case neg
β : Type u_2
π : β → Type u_3
inst✝² : Fintype β
inst✝¹ : (b : β) → PseudoMetricSpace (π b)
inst✝ : Nonempty β
f g : (b : β) → π b
r : ℝ
hr : ¬0 ≤ r
⊢ dist f g ≤ r ↔ ∀ (b : β), dist (f b) (g b) ≤ r

Proof state:
case neg
β : Type u_2
π : β → Type u_3
inst✝² : Fintype β
inst✝¹ : (b : β) → PseudoMetricSpace (π b)
inst✝ : Nonempty β
f g : (b : β) → π b
r : ℝ
hr : ¬0 ≤ r
⊢ dist f g ≤ r ↔ ∀ (b : β), dist (f b) (g b) ≤ r

Tactic:
exact iff_of_false (fun h => hr <| dist_nonneg.trans h) fun h =>
  hr <| dist_nonneg.trans <| h <| Classical.arbitrary _

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Perm.lean
theorem Perm.insert (a : α) {l₁ l₂ : List α} (p : l₁ ~ l₂) :
    l₁.insert a ~ l₂.insert a

Proof state:
α : Type u_1
inst✝ : DecidableEq α
a : α
l₁ l₂ : List α
p : l₁ ~ l₂
h : a ∈ l₁
⊢ List.insert a l₁ ~ List.insert a l₂

Tactic:
simp [h, p.subset h, p]

Result:
no goals

Proof state:
α : Type u_1
inst✝ : DecidableEq α
a : α
l₁ l₂ : List α
p : l₁ ~ l₂
h : ¬a ∈ l₁
this : a :: l₁ ~ a :: l₂
⊢ List.insert a l₁ ~ List.insert a l₂

Tactic:
simpa [h, mt p.mem_iff.2 h] using this

Result:
no goals

Proof state:
α : Type u_1
inst✝ : DecidableEq α
a : α
l₁ l₂ : List α
p : l₁ ~ l₂
h : ¬a ∈ l₁
⊢ List.insert a l₁ ~ List.insert a l₂

Tactic:
have := p.cons a

Result:
α : Type u_1
inst✝ : DecidableEq α
a : α
l₁ l₂ : List α
p : l₁ ~ l₂
h : ¬a ∈ l₁
this : a :: l₁ ~ a :: l₂
⊢ List.insert a l₁ ~ List.insert a l₂

Proof state:
α : Type u_1
inst✝ : DecidableEq α
a : α
l₁ l₂ : List α
p : l₁ ~ l₂
⊢ List.insert a l₁ ~ List.insert a l₂

Tactic:
if h : a ∈ l₁ then
  simp [h, p.subset h, p]
else
  have := p.cons a
  simpa [h, mt p.mem_iff.2 h] using this

Result:
no goals
-- Mathlib/CategoryTheory/Limits/FunctorCategory/Shapes/Pullbacks.lean
theorem pullbackObjIso_hom_comp_snd (f : F ⟶ H) (g : G ⟶ H) (d : D) :
    (pullbackObjIso f g d).hom ≫ pullback.snd (f.app d) (g.app d) = (pullback.snd f g).app d

Proof state:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F G H : D ⥤ C
inst✝ : HasPullbacks C
f : F ⟶ H
g : G ⟶ H
d : D
⊢ (pullbackObjIso f g d).hom ≫ pullback.snd (f.app d) (g.app d) = (pullback.snd f g).app d

Tactic:
simp [pullbackObjIso]

Result:
no goals
-- Mathlib/CategoryTheory/MorphismProperty/Limits.lean
@[simp]
lemma coproducts_le_iff {P Q : MorphismProperty C} [IsStableUnderCoproducts.{w} Q] :
    coproducts.{w} P ≤ Q ↔ P ≤ Q

Proof state:
case mpr
C : Type u
inst✝¹ : Category.{v, u} C
P Q : MorphismProperty C
inst✝ : IsStableUnderCoproducts.{w, v, u} Q
⊢ P ≤ Q → coproducts.{w, v, u} P ≤ Q

Tactic:
intro h

Result:
case mpr
C : Type u
inst✝¹ : Category.{v, u} C
P Q : MorphismProperty C
inst✝ : IsStableUnderCoproducts.{w, v, u} Q
h : P ≤ Q
⊢ coproducts.{w, v, u} P ≤ Q

Proof state:
case mpr
C : Type u
inst✝¹ : Category.{v, u} C
P Q : MorphismProperty C
inst✝ : IsStableUnderCoproducts.{w, v, u} Q
h : P ≤ Q
⊢ coproducts.{w, v, u} P ≤ Q

Tactic:
exact le_trans (coproducts_monotone h) Q.coproducts_le

Result:
no goals

Proof state:
case mp
C : Type u
inst✝¹ : Category.{v, u} C
P Q : MorphismProperty C
inst✝ : IsStableUnderCoproducts.{w, v, u} Q
⊢ coproducts.{w, v, u} P ≤ Q → P ≤ Q

Tactic:
exact le_trans P.le_coproducts

Result:
no goals

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
P Q : MorphismProperty C
inst✝ : IsStableUnderCoproducts.{w, v, u} Q
⊢ coproducts.{w, v, u} P ≤ Q ↔ P ≤ Q

Tactic:
constructor

Result:
case mp
C : Type u
inst✝¹ : Category.{v, u} C
P Q : MorphismProperty C
inst✝ : IsStableUnderCoproducts.{w, v, u} Q
⊢ coproducts.{w, v, u} P ≤ Q → P ≤ Q

case mpr
C : Type u
inst✝¹ : Category.{v, u} C
P Q : MorphismProperty C
inst✝ : IsStableUnderCoproducts.{w, v, u} Q
⊢ P ≤ Q → coproducts.{w, v, u} P ≤ Q
-- Mathlib/CategoryTheory/Limits/Shapes/Pullback/Cospan.lean
theorem cospanExt_app_right : (cospanExt iX iY iZ wf wg).app WalkingCospan.right = iY

Proof state:
C : Type u
inst✝ : Category.{v, u} C
X Y Z X' Y' Z' : C
iX : X ≅ X'
iY : Y ≅ Y'
iZ : Z ≅ Z'
f : X ⟶ Z
g : Y ⟶ Z
f' : X' ⟶ Z'
g' : Y' ⟶ Z'
wf : iX.hom ≫ f' = f ≫ iZ.hom
wg : iY.hom ≫ g' = g ≫ iZ.hom
⊢ (cospanExt iX iY iZ wf wg).app WalkingCospan.right = iY

Tactic:
dsimp [cospanExt]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Int/Lemmas.lean
theorem toNat_sub (m n : Nat) : toNat (m - n) = m - n

Proof state:
m n : Nat
⊢ (↑m - ↑n).toNat = m - n

Tactic:
rw [← Int.subNatNat_eq_coe]

Result:
m n : Nat
⊢ (subNatNat m n).toNat = m - n

Proof state:
case refine_2
m n✝ i n : Nat
⊢ (fun m n i => i.toNat = m - n) n (n + i + 1) -[i+1]

Tactic:
dsimp

Result:
case refine_2
m n✝ i n : Nat
⊢ -[i+1].toNat = n - (n + i + 1)

Proof state:
case refine_2
m n✝ i n : Nat
⊢ -[i+1].toNat = 0

Tactic:
rfl

Result:
no goals

Proof state:
case refine_1
m n✝ i n : Nat
⊢ (fun m n i => i.toNat = m - n) (n + i) n ↑i

Tactic:
exact (Nat.add_sub_cancel_left ..).symm

Result:
no goals

Proof state:
m n : Nat
⊢ (subNatNat m n).toNat = m - n

Tactic:
refine subNatNat_elim m n (fun m n i => toNat i = m - n) (fun i n => ?_) (fun i n => ?_)

Result:
case refine_1
m n✝ i n : Nat
⊢ (fun m n i => i.toNat = m - n) (n + i) n ↑i

case refine_2
m n✝ i n : Nat
⊢ (fun m n i => i.toNat = m - n) n (n + i + 1) -[i+1]

Proof state:
case refine_2
m n✝ i n : Nat
⊢ -[i+1].toNat = n - (n + i + 1)

Tactic:
rw [Nat.add_assoc, Nat.sub_eq_zero_of_le (Nat.le_add_right ..)]

Result:
case refine_2
m n✝ i n : Nat
⊢ -[i+1].toNat = 0
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/RawLemmas.lean
theorem getKey?_empty {a : α} {c} :
    (empty c : Raw α β).getKey? a = none

Proof state:
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : Hashable α
a : α
c : Nat
⊢ (empty c).getKey? a = none

Tactic:
simp_to_raw using Raw₀.getKey?_empty

Result:
no goals
-- Mathlib/NumberTheory/FLT/Basic.lean
lemma FermatLastTheoremFor.mono (hmn : m ∣ n) (hm : FermatLastTheoremFor m) :
    FermatLastTheoremFor n

Proof state:
m n : ℕ
hmn : m ∣ n
hm : FermatLastTheoremFor m
⊢ FermatLastTheoremFor n

Tactic:
exact FermatLastTheoremWith.mono hmn hm

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Nat/Bitwise/Basic.lean
theorem shiftRight_eq_div_pow (m : Nat) : ∀ n, m >>> n = m / 2 ^ n
  | 0 => (Nat.div_one _).symm
  | k + 1 => by
    rw [shiftRight_add, shiftRight_eq_div_pow m k]
    simp [Nat.div_div_eq_div_mul, ← Nat.pow_succ, shiftRight_succ]

Proof state:
m k : Nat
⊢ (m / 2 ^ k) >>> 1 = m / 2 ^ (k + 1)

Tactic:
simp [Nat.div_div_eq_div_mul, ← Nat.pow_succ, shiftRight_succ]

Result:
no goals

Proof state:
m k : Nat
⊢ m >>> (k + 1) = m / 2 ^ (k + 1)

Tactic:
rw [shiftRight_add, shiftRight_eq_div_pow m k]

Result:
m k : Nat
⊢ (m / 2 ^ k) >>> 1 = m / 2 ^ (k + 1)
-- Mathlib/Analysis/Normed/Group/Ultra.lean
/--
Generalised ultrametric triangle inequality for finite products in commutative groups with
an ultrametric norm.
-/
@[to_additive "Generalised ultrametric triangle inequality for finite sums in additive commutative
groups with an ultrametric norm."]
lemma norm_prod_le_of_forall_le_of_nonneg {s : Finset ι} {f : ι → M} {C : ℝ}
    (h_nonneg : 0 ≤ C) (hC : ∀ i ∈ s, ‖f i‖ ≤ C) : ‖∏ i ∈ s, f i‖ ≤ C

Proof state:
M : Type u_1
ι : Type u_2
inst✝¹ : SeminormedCommGroup M
inst✝ : IsUltrametricDist M
s : Finset ι
f : ι → M
C : ℝ
h_nonneg : 0 ≤ C
hC : ∀ i ∈ s, ‖f i‖ ≤ C
⊢ ‖∏ i ∈ s, f i‖ ≤ C

Tactic:
lift C to NNReal using h_nonneg

Result:
case intro
M : Type u_1
ι : Type u_2
inst✝¹ : SeminormedCommGroup M
inst✝ : IsUltrametricDist M
s : Finset ι
f : ι → M
C : ℝ≥0
hC : ∀ i ∈ s, ‖f i‖ ≤ ↑C
⊢ ‖∏ i ∈ s, f i‖ ≤ ↑C

Proof state:
case intro
M : Type u_1
ι : Type u_2
inst✝¹ : SeminormedCommGroup M
inst✝ : IsUltrametricDist M
s : Finset ι
f : ι → M
C : ℝ≥0
hC : ∀ i ∈ s, ‖f i‖ ≤ ↑C
⊢ ‖∏ i ∈ s, f i‖ ≤ ↑C

Tactic:
exact nnnorm_prod_le_of_forall_le hC

Result:
no goals
-- Mathlib/Topology/UniformSpace/Defs.lean
theorem lift_nhds_right {x : α} {g : Set α → Filter β} (hg : Monotone g) :
    (𝓝 x).lift g = (𝓤 α).lift fun s : Set (α × α) => g { y | (y, x) ∈ s }

Proof state:
α : Type ua
β : Type ub
inst✝ : UniformSpace α
x : α
g : Set α → Filter β
hg : Monotone g
⊢ (𝓤 α).lift (g ∘ preimage fun y => (y, x)) = (𝓤 α).lift fun s => g {y | (y, x) ∈ s}

Tactic:
simp_rw [Function.comp_def, preimage]

Result:
no goals

Proof state:
α : Type ua
β : Type ub
inst✝ : UniformSpace α
x : α
g : Set α → Filter β
hg : Monotone g
⊢ (𝓝 x).lift g = (𝓤 α).lift fun s => g {y | (y, x) ∈ s}

Tactic:
rw [nhds_eq_comap_uniformity', comap_lift_eq2 hg]

Result:
α : Type ua
β : Type ub
inst✝ : UniformSpace α
x : α
g : Set α → Filter β
hg : Monotone g
⊢ (𝓤 α).lift (g ∘ preimage fun y => (y, x)) = (𝓤 α).lift fun s => g {y | (y, x) ∈ s}
-- Mathlib/Data/List/Indexes.lean
theorem oldMapIdx_append : ∀ (f : ℕ → α → β) (l : List α) (e : α),
    List.oldMapIdx f (l ++ [e]) = List.oldMapIdx f l ++ [f l.length e]

Proof state:
α : Type u
β : Type v
f : ℕ → α → β
l : List α
e : α
⊢ List.oldMapIdxCore f 0 l ++ List.oldMapIdxCore f (0 + l.length) [e] = List.oldMapIdxCore f 0 l ++ [f l.length e]

Tactic:
simp only [Nat.zero_add]

Result:
α : Type u
β : Type v
f : ℕ → α → β
l : List α
e : α
⊢ List.oldMapIdxCore f 0 l ++ List.oldMapIdxCore f l.length [e] = List.oldMapIdxCore f 0 l ++ [f l.length e]

Proof state:
α : Type u
β : Type v
f : ℕ → α → β
l : List α
e : α
⊢ List.oldMapIdx f (l ++ [e]) = List.oldMapIdx f l ++ [f l.length e]

Tactic:
unfold List.oldMapIdx

Result:
α : Type u
β : Type v
f : ℕ → α → β
l : List α
e : α
⊢ List.oldMapIdxCore f 0 (l ++ [e]) = List.oldMapIdxCore f 0 l ++ [f l.length e]

Proof state:
α : Type u
β : Type v
⊢ ∀ (f : ℕ → α → β) (l : List α) (e : α), List.oldMapIdx f (l ++ [e]) = List.oldMapIdx f l ++ [f l.length e]

Tactic:
intros f l e

Result:
α : Type u
β : Type v
f : ℕ → α → β
l : List α
e : α
⊢ List.oldMapIdx f (l ++ [e]) = List.oldMapIdx f l ++ [f l.length e]

Proof state:
α : Type u
β : Type v
f : ℕ → α → β
l : List α
e : α
⊢ List.oldMapIdxCore f 0 (l ++ [e]) = List.oldMapIdxCore f 0 l ++ [f l.length e]

Tactic:
rw [List.oldMapIdxCore_append f 0 l [e]]

Result:
α : Type u
β : Type v
f : ℕ → α → β
l : List α
e : α
⊢ List.oldMapIdxCore f 0 l ++ List.oldMapIdxCore f (0 + l.length) [e] = List.oldMapIdxCore f 0 l ++ [f l.length e]

Proof state:
α : Type u
β : Type v
f : ℕ → α → β
l : List α
e : α
⊢ List.oldMapIdxCore f 0 l ++ List.oldMapIdxCore f l.length [e] = List.oldMapIdxCore f 0 l ++ [f l.length e]

Tactic:
rfl

Result:
no goals
-- Mathlib/Data/ZMod/Units.lean
lemma not_isUnit_of_mem_primeFactors {n p : ℕ} (h : p ∈ n.primeFactors) :
    ¬ IsUnit (p : ZMod n)

Proof state:
n p : ℕ
h : p ∈ n.primeFactors
⊢ ¬IsUnit ↑p

Tactic:
rw [isUnit_iff_coprime]

Result:
n p : ℕ
h : p ∈ n.primeFactors
⊢ ¬p.Coprime n

Proof state:
n p : ℕ
h : p ∈ n.primeFactors
⊢ ¬p.Coprime n

Tactic:
exact (Prime.dvd_iff_not_coprime <| prime_of_mem_primeFactors h).mp <| dvd_of_mem_primeFactors h

Result:
no goals