harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/BasicAux.lean
theorem get_last {as : List α} {i : Fin (length (as ++ [a]))} (h : ¬ i.1 < as.length) : (as ++ [a] : List _).get i = a

Proof state:
case mk.cons
α : Type u_1
a✝ a : α
as : List α
ih : ∀ (i : Nat) (h' : i < (as ++ [a✝]).length), ¬↑⟨i, h'⟩ < as.length → (as ++ [a✝]).get ⟨i, h'⟩ = a✝
i : Nat
h' : i < (a :: as ++ [a✝]).length
h : ¬↑⟨i, h'⟩ < (a :: as).length
⊢ (a :: as ++ [a✝]).get ⟨i, h'⟩ = a✝

Tactic:
cases i with simp at h
| succ i => apply ih; simp [h]

Result:
no goals

Proof state:
case mk
α : Type u_1
a : α
as : List α
val✝ : Nat
isLt✝ : val✝ < (as ++ [a]).length
h : ¬↑⟨val✝, isLt✝⟩ < as.length
⊢ (as ++ [a]).get ⟨val✝, isLt✝⟩ = a

Tactic:
rename_i i h'

Result:
case mk
α : Type u_1
a : α
as : List α
i : Nat
h' : i < (as ++ [a]).length
h : ¬↑⟨i, h'⟩ < as.length
⊢ (as ++ [a]).get ⟨i, h'⟩ = a

Proof state:
case mk.nil.succ
α : Type u_1
a : α
n✝ : Nat
h' : n✝ + 1 < ([] ++ [a]).length
h : ¬↑⟨n✝ + 1, h'⟩ < [].length
⊢ ([] ++ [a]).get ⟨n✝ + 1, h'⟩ = a

Tactic:
simp_arith at h'

Result:
no goals

Proof state:
case mk
α : Type u_1
a : α
as : List α
i : Nat
h' : i < (as ++ [a]).length
h : ¬↑⟨i, h'⟩ < as.length
⊢ (as ++ [a]).get ⟨i, h'⟩ = a

Tactic:
induction as generalizing i with
| nil => cases i with
  | zero => simp [List.get]
  | succ => simp_arith at h'
| cons a as ih =>
  cases i with simp at h
  | succ i => apply ih; simp [h]

Result:
no goals

Proof state:
α : Type u_1
a : α
as : List α
i : Fin (as ++ [a]).length
h : ¬↑i < as.length
⊢ (as ++ [a]).get i = a

Tactic:
cases i

Result:
case mk
α : Type u_1
a : α
as : List α
val✝ : Nat
isLt✝ : val✝ < (as ++ [a]).length
h : ¬↑⟨val✝, isLt✝⟩ < as.length
⊢ (as ++ [a]).get ⟨val✝, isLt✝⟩ = a

Proof state:
case mk.nil
α : Type u_1
a : α
i : Nat
h' : i < ([] ++ [a]).length
h : ¬↑⟨i, h'⟩ < [].length
⊢ ([] ++ [a]).get ⟨i, h'⟩ = a

Tactic:
cases i with
| zero => simp [List.get]
| succ => simp_arith at h'

Result:
no goals

Proof state:
case mk.nil.zero
α : Type u_1
a : α
h' : 0 < ([] ++ [a]).length
h : ¬↑⟨0, h'⟩ < [].length
⊢ ([] ++ [a]).get ⟨0, h'⟩ = a

Tactic:
simp [List.get]

Result:
no goals

Proof state:
case mk.cons.succ
α : Type u_1
a✝ a : α
as : List α
ih : ∀ (i : Nat) (h' : i < (as ++ [a✝]).length), ¬↑⟨i, h'⟩ < as.length → (as ++ [a✝]).get ⟨i, h'⟩ = a✝
i : Nat
h' : i + 1 < (a :: as ++ [a✝]).length
h : as.length ≤ i
⊢ (a :: as ++ [a✝]).get ⟨i + 1, h'⟩ = a✝

Tactic:
apply ih

Result:
case mk.cons.succ.h
α : Type u_1
a✝ a : α
as : List α
ih : ∀ (i : Nat) (h' : i < (as ++ [a✝]).length), ¬↑⟨i, h'⟩ < as.length → (as ++ [a✝]).get ⟨i, h'⟩ = a✝
i : Nat
h' : i + 1 < (a :: as ++ [a✝]).length
h : as.length ≤ i
⊢ ¬↑⟨i, ⋯⟩ < as.length

Proof state:
case mk.cons.succ.h
α : Type u_1
a✝ a : α
as : List α
ih : ∀ (i : Nat) (h' : i < (as ++ [a✝]).length), ¬↑⟨i, h'⟩ < as.length → (as ++ [a✝]).get ⟨i, h'⟩ = a✝
i : Nat
h' : i + 1 < (a :: as ++ [a✝]).length
h : as.length ≤ i
⊢ ¬↑⟨i, ⋯⟩ < as.length

Tactic:
simp [h]

Result:
no goals
-- Mathlib/Data/Nat/Factorization/Root.lean
/-- The RHS is a noncomputable version of `Nat.ceilRoot` with better order theoretical
properties. -/
lemma ceilRoot_def :
    ceilRoot n a = if n = 0 ∨ a = 0 then 0 else (a.factorization ⌈/⌉ n).prod (· ^ ·)

Proof state:
a n : ℕ
⊢ n.ceilRoot a = if n = 0 ∨ a = 0 then 0 else (a.factorization ⌈/⌉ n).prod fun x1 x2 => x1 ^ x2

Tactic:
unfold ceilRoot

Result:
a n : ℕ
⊢ (if n = 0 ∨ a = 0 then 0 else a.factorization.prod fun p k => p ^ ((k + n - 1) / n)) =
    if n = 0 ∨ a = 0 then 0 else (a.factorization ⌈/⌉ n).prod fun x1 x2 => x1 ^ x2

Proof state:
a n : ℕ
⊢ (if n = 0 ∨ a = 0 then 0 else a.factorization.prod fun p k => p ^ ((k + n - 1) / n)) =
    if n = 0 ∨ a = 0 then 0 else (a.factorization ⌈/⌉ n).prod fun x1 x2 => x1 ^ x2

Tactic:
split_ifs with h <;>
  simp [Finsupp.ceilDiv_def, prod_mapRange_index pow_zero, Nat.ceilDiv_eq_add_pred_div]

Result:
no goals
-- Mathlib/NumberTheory/LSeries/HurwitzZetaEven.lean
/-- Formula for `cosZeta` as a Dirichlet series in the convergence range, with sum over `ℤ`. -/
lemma hasSum_int_cosZeta (a : ℝ) {s : ℂ} (hs : 1 < re s) :
    HasSum (fun n : ℤ ↦ cexp (2 * π * I * a * n) / ↑|n| ^ s / 2) (cosZeta a s)

Proof state:
a : ℝ
s : ℂ
hs : 1 < s.re
n : ℤ
⊢ cexp (2 * ↑π * I * ↑a * ↑n) / ↑|n| ^ s / 2 = s.Gammaℝ * cexp (2 * ↑π * I * ↑a * ↑n) / ↑|n| ^ s / 2 / s.Gammaℝ

Tactic:
rw [mul_div_assoc _ (cexp _), div_right_comm _ (2 : ℂ),
  mul_div_cancel_left₀ _ (Gammaℝ_ne_zero_of_re_pos (zero_lt_one.trans hs))]

Result:
no goals

Proof state:
a : ℝ
s : ℂ
hs : 1 < s.re
⊢ HasSum (fun n => cexp (2 * ↑π * I * ↑a * ↑n) / ↑|n| ^ s / 2) (cosZeta (↑a) s)

Tactic:
rw [cosZeta, Function.update_of_ne (ne_zero_of_one_lt_re hs)]

Result:
a : ℝ
s : ℂ
hs : 1 < s.re
⊢ HasSum (fun n => cexp (2 * ↑π * I * ↑a * ↑n) / ↑|n| ^ s / 2) (completedCosZeta (↑a) s / s.Gammaℝ)

Proof state:
a : ℝ
s : ℂ
hs : 1 < s.re
⊢ HasSum (fun n => cexp (2 * ↑π * I * ↑a * ↑n) / ↑|n| ^ s / 2) (completedCosZeta (↑a) s / s.Gammaℝ)

Tactic:
refine ((hasSum_int_completedCosZeta a hs).div_const (Gammaℝ s)).congr_fun fun n ↦ ?_

Result:
a : ℝ
s : ℂ
hs : 1 < s.re
n : ℤ
⊢ cexp (2 * ↑π * I * ↑a * ↑n) / ↑|n| ^ s / 2 = s.Gammaℝ * cexp (2 * ↑π * I * ↑a * ↑n) / ↑|n| ^ s / 2 / s.Gammaℝ
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Nat/Lemmas.lean
theorem pow_le_pow_of_le {a n m : Nat} (h : 1 < a) (w : n ≤ m) : a ^ n ≤ a ^ m

Proof state:
case inl
a n m : Nat
h : 1 < a
w : n ≤ m
h✝ : n < m
⊢ a ^ n ≤ a ^ m

case inr
a n m : Nat
h : 1 < a
w : n ≤ m
h✝ : n = m
⊢ a ^ n ≤ a ^ m

Tactic:
case inl lt =>
  exact Nat.le_of_lt (Nat.pow_lt_pow_of_lt h lt)

Result:
case inr
a n m : Nat
h : 1 < a
w : n ≤ m
h✝ : n = m
⊢ a ^ n ≤ a ^ m

Proof state:
case inr
a n m : Nat
h : 1 < a
w : n ≤ m
h✝ : n = m
⊢ a ^ n ≤ a ^ m

Tactic:
case inr eq =>
  subst eq
  exact Nat.le_refl _

Result:
no goals

Proof state:
a n m : Nat
h : 1 < a
w : n ≤ m
eq : n = m
⊢ a ^ n ≤ a ^ m

Tactic:
subst eq

Result:
a n : Nat
h : 1 < a
w : n ≤ n
⊢ a ^ n ≤ a ^ n

Proof state:
a n m : Nat
h : 1 < a
w : n ≤ m
lt : n < m
⊢ a ^ n ≤ a ^ m

Tactic:
exact Nat.le_of_lt (Nat.pow_lt_pow_of_lt h lt)

Result:
no goals

Proof state:
a n : Nat
h : 1 < a
w : n ≤ n
⊢ a ^ n ≤ a ^ n

Tactic:
exact Nat.le_refl _

Result:
no goals

Proof state:
a n m : Nat
h : 1 < a
w : n ≤ m
⊢ a ^ n ≤ a ^ m

Tactic:
cases Nat.lt_or_eq_of_le w

Result:
case inl
a n m : Nat
h : 1 < a
w : n ≤ m
h✝ : n < m
⊢ a ^ n ≤ a ^ m

case inr
a n m : Nat
h : 1 < a
w : n ≤ m
h✝ : n = m
⊢ a ^ n ≤ a ^ m
-- Mathlib/Data/ZMod/Basic.lean
@[simp]
lemma nsmul_zmod_val_inv_nsmul (hn : (Nat.card α).Coprime n) (a : α) :
    n • (n⁻¹ : ZMod (Nat.card α)).val • a = a

Proof state:
α : Type u_1
inst✝ : AddGroup α
n : ℕ
hn : (Nat.card α).Coprime n
a : α
⊢ n • (↑n)⁻¹.val • a = a

Tactic:
rw [← mul_nsmul', ← mod_natCard_nsmul, ← ZMod.val_natCast, Nat.cast_mul,
  ZMod.mul_val_inv hn.symm, ZMod.val_one_eq_one_mod, mod_natCard_nsmul, one_nsmul]

Result:
no goals
-- Mathlib/Data/Set/Lattice.lean
theorem biUnion_diff_biUnion_subset (s₁ s₂ : Set α) :
    ((⋃ x ∈ s₁, t x) \ ⋃ x ∈ s₂, t x) ⊆ ⋃ x ∈ s₁ \ s₂, t x

Proof state:
α : Type u_1
β : Type u_2
t : α → Set β
s₁ s₂ : Set α
⊢ (⋃ x ∈ s₁, t x) \ ⋃ x ∈ s₂, t x ⊆ ⋃ x ∈ s₁ \ s₂, t x

Tactic:
simp only [diff_subset_iff, ← biUnion_union]

Result:
α : Type u_1
β : Type u_2
t : α → Set β
s₁ s₂ : Set α
⊢ ⋃ x ∈ s₁, t x ⊆ ⋃ x ∈ s₂ ∪ s₁ \ s₂, t x

Proof state:
case h
α : Type u_1
β : Type u_2
t : α → Set β
s₁ s₂ : Set α
⊢ s₁ ⊆ s₂ ∪ s₁ \ s₂

Tactic:
rw [union_diff_self]

Result:
case h
α : Type u_1
β : Type u_2
t : α → Set β
s₁ s₂ : Set α
⊢ s₁ ⊆ s₂ ∪ s₁

Proof state:
case h
α : Type u_1
β : Type u_2
t : α → Set β
s₁ s₂ : Set α
⊢ s₁ ⊆ s₂ ∪ s₁

Tactic:
apply subset_union_right

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
t : α → Set β
s₁ s₂ : Set α
⊢ ⋃ x ∈ s₁, t x ⊆ ⋃ x ∈ s₂ ∪ s₁ \ s₂, t x

Tactic:
apply biUnion_subset_biUnion_left

Result:
case h
α : Type u_1
β : Type u_2
t : α → Set β
s₁ s₂ : Set α
⊢ s₁ ⊆ s₂ ∪ s₁ \ s₂
-- Mathlib/Algebra/Polynomial/Eval/Degree.lean
/-- Variant of `natDegree_map_lt` that assumes `0 < natDegree p` instead of `map f p ≠ 0`. -/
lemma natDegree_map_lt' (hp : f p.leadingCoeff = 0) (hp₀ : 0 < natDegree p) :
    (p.map f).natDegree < p.natDegree

Proof state:
case neg
R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
f : R →+* S
p : R[X]
hp : f p.leadingCoeff = 0
hp₀ : 0 < p.natDegree
H : ¬map f p = 0
⊢ (map f p).natDegree < p.natDegree

Tactic:
exact natDegree_map_lt hp H

Result:
no goals

Proof state:
R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
f : R →+* S
p : R[X]
hp : f p.leadingCoeff = 0
hp₀ : 0 < p.natDegree
⊢ (map f p).natDegree < p.natDegree

Tactic:
by_cases H : map f p = 0

Result:
case pos
R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
f : R →+* S
p : R[X]
hp : f p.leadingCoeff = 0
hp₀ : 0 < p.natDegree
H : map f p = 0
⊢ (map f p).natDegree < p.natDegree

case neg
R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
f : R →+* S
p : R[X]
hp : f p.leadingCoeff = 0
hp₀ : 0 < p.natDegree
H : ¬map f p = 0
⊢ (map f p).natDegree < p.natDegree

Proof state:
case pos
R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
f : R →+* S
p : R[X]
hp : f p.leadingCoeff = 0
hp₀ : 0 < p.natDegree
H : map f p = 0
⊢ (map f p).natDegree < p.natDegree

Tactic:
rwa [H, natDegree_zero]

Result:
no goals
-- Mathlib/RingTheory/Localization/Defs.lean
theorem injective (hM : M ≤ nonZeroDivisors R) : Injective (algebraMap R S)

Proof state:
R : Type u_1
inst✝³ : CommRing R
M : Submonoid R
S : Type u_2
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
hM : M ≤ nonZeroDivisors R
⊢ ∀ (a : R), (algebraMap R S) a = 0 → a = 0

Tactic:
intro a ha

Result:
R : Type u_1
inst✝³ : CommRing R
M : Submonoid R
S : Type u_2
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
hM : M ≤ nonZeroDivisors R
a : R
ha : (algebraMap R S) a = 0
⊢ a = 0

Proof state:
R : Type u_1
inst✝³ : CommRing R
M : Submonoid R
S : Type u_2
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
hM : M ≤ nonZeroDivisors R
⊢ Injective ⇑(algebraMap R S)

Tactic:
rw [injective_iff_map_eq_zero (algebraMap R S)]

Result:
R : Type u_1
inst✝³ : CommRing R
M : Submonoid R
S : Type u_2
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
hM : M ≤ nonZeroDivisors R
⊢ ∀ (a : R), (algebraMap R S) a = 0 → a = 0

Proof state:
R : Type u_1
inst✝³ : CommRing R
M : Submonoid R
S : Type u_2
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
hM : M ≤ nonZeroDivisors R
a : R
ha : (algebraMap R S) a = 0
⊢ a = 0

Tactic:
rwa [to_map_eq_zero_iff S hM] at ha

Result:
no goals
-- Mathlib/Topology/MetricSpace/GromovHausdorffRealized.lean
theorem candidates_nonneg (fA : f ∈ candidates X Y) : 0 ≤ f (x, y)

Proof state:
X : Type u
Y : Type v
inst✝¹ : MetricSpace X
inst✝ : MetricSpace Y
f : GromovHausdorff.ProdSpaceFun X Y
x y : X ⊕ Y
fA : f ∈ candidates X Y
⊢ 0 ≤ f (x, y)

Tactic:
have : 0 ≤ 2 * f (x, y) :=
  calc
    0 = f (x, x) := (candidates_refl fA).symm
    _ ≤ f (x, y) + f (y, x) := candidates_triangle fA
    _ = f (x, y) + f (x, y) := by rw [candidates_symm fA]
    _ = 2 * f (x, y) := by ring

Result:
X : Type u
Y : Type v
inst✝¹ : MetricSpace X
inst✝ : MetricSpace Y
f : GromovHausdorff.ProdSpaceFun X Y
x y : X ⊕ Y
fA : f ∈ candidates X Y
this : 0 ≤ 2 * f (x, y)
⊢ 0 ≤ f (x, y)

Proof state:
X : Type u
Y : Type v
inst✝¹ : MetricSpace X
inst✝ : MetricSpace Y
f : GromovHausdorff.ProdSpaceFun X Y
x y : X ⊕ Y
fA : f ∈ candidates X Y
this : 0 ≤ 2 * f (x, y)
⊢ 0 ≤ f (x, y)

Tactic:
linarith

Result:
no goals

Proof state:
X : Type u
Y : Type v
inst✝¹ : MetricSpace X
inst✝ : MetricSpace Y
f : GromovHausdorff.ProdSpaceFun X Y
x y : X ⊕ Y
fA : f ∈ candidates X Y
⊢ f (x, y) + f (y, x) = f (x, y) + f (x, y)

Tactic:
rw [candidates_symm fA]

Result:
no goals

Proof state:
X : Type u
Y : Type v
inst✝¹ : MetricSpace X
inst✝ : MetricSpace Y
f : GromovHausdorff.ProdSpaceFun X Y
x y : X ⊕ Y
fA : f ∈ candidates X Y
⊢ f (x, y) + f (x, y) = 2 * f (x, y)

Tactic:
ring

Result:
no goals
-- Mathlib/Analysis/Calculus/Implicit.lean
theorem implicitToPartialHomeomorphOfComplemented_self (hf : HasStrictFDerivAt f f' a)
    (hf' : range f' = ⊤) (hker : (ker f').ClosedComplemented) :
    hf.implicitToPartialHomeomorphOfComplemented f f' hf' hker a = (f a, 0)

Proof state:
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : CompleteSpace E
F : Type u_3
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
inst✝ : CompleteSpace F
f : E → F
f' : E →L[𝕜] F
a : E
hf : HasStrictFDerivAt f f' a
hf' : range f' = ⊤
hker : (LinearMap.ker f').ClosedComplemented
⊢ ↑(implicitToPartialHomeomorphOfComplemented f f' hf hf' hker) a = (f a, 0)

Tactic:
simp [hf.implicitToPartialHomeomorphOfComplemented_apply]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Sublist.lean
theorem prefix_of_prefix_length_le :
    ∀ {l₁ l₂ l₃ : List α}, l₁ <+: l₃ → l₂ <+: l₃ → length l₁ ≤ length l₂ → l₁ <+: l₂
  | [], _, _, _, _, _ => nil_prefix
  | _ :: _, b :: _, _, ⟨_, rfl⟩, ⟨_, e⟩, ll => by
    injection e with _ e'; subst b
    rcases prefix_of_prefix_length_le ⟨_, rfl⟩ ⟨_, e'⟩ (le_of_succ_le_succ ll) with ⟨r₃, rfl⟩
    exact ⟨r₃, rfl⟩

Proof state:
α : Type u_1
head✝ : α
tail✝¹ : List α
b : α
tail✝ w✝¹ w✝ : List α
e : b :: tail✝ ++ w✝ = head✝ :: tail✝¹ ++ w✝¹
ll : (head✝ :: tail✝¹).length ≤ (b :: tail✝).length
⊢ head✝ :: tail✝¹ <+: b :: tail✝

Tactic:
injection e with _ e'

Result:
α : Type u_1
head✝ : α
tail✝¹ : List α
b : α
tail✝ w✝¹ w✝ : List α
ll : (head✝ :: tail✝¹).length ≤ (b :: tail✝).length
head_eq✝ : b = head✝
e' : tail✝.append w✝ = tail✝¹.append w✝¹
⊢ head✝ :: tail✝¹ <+: b :: tail✝

Proof state:
case intro
α : Type u_1
head✝ : α
tail✝ w✝¹ w✝ r₃ : List α
e' : (tail✝ ++ r₃).append w✝ = tail✝.append w✝¹
ll : (head✝ :: tail✝).length ≤ (head✝ :: (tail✝ ++ r₃)).length
⊢ head✝ :: tail✝ <+: head✝ :: (tail✝ ++ r₃)

Tactic:
exact ⟨r₃, rfl⟩

Result:
no goals

Proof state:
α : Type u_1
head✝ : α
tail✝¹ : List α
b : α
tail✝ w✝¹ w✝ : List α
ll : (head✝ :: tail✝¹).length ≤ (b :: tail✝).length
head_eq✝ : b = head✝
e' : tail✝.append w✝ = tail✝¹.append w✝¹
⊢ head✝ :: tail✝¹ <+: b :: tail✝

Tactic:
subst b

Result:
α : Type u_1
head✝ : α
tail✝¹ tail✝ w✝¹ w✝ : List α
e' : tail✝.append w✝ = tail✝¹.append w✝¹
ll : (head✝ :: tail✝¹).length ≤ (head✝ :: tail✝).length
⊢ head✝ :: tail✝¹ <+: head✝ :: tail✝

Proof state:
α : Type u_1
head✝ : α
tail✝¹ tail✝ w✝¹ w✝ : List α
e' : tail✝.append w✝ = tail✝¹.append w✝¹
ll : (head✝ :: tail✝¹).length ≤ (head✝ :: tail✝).length
⊢ head✝ :: tail✝¹ <+: head✝ :: tail✝

Tactic:
rcases prefix_of_prefix_length_le ⟨_, rfl⟩ ⟨_, e'⟩ (le_of_succ_le_succ ll) with ⟨r₃, rfl⟩

Result:
case intro
α : Type u_1
head✝ : α
tail✝ w✝¹ w✝ r₃ : List α
e' : (tail✝ ++ r₃).append w✝ = tail✝.append w✝¹
ll : (head✝ :: tail✝).length ≤ (head✝ :: (tail✝ ++ r₃)).length
⊢ head✝ :: tail✝ <+: head✝ :: (tail✝ ++ r₃)
-- Mathlib/CategoryTheory/Monoidal/Category.lean
theorem inv_hom_whiskerRight {X Y : C} (f : X ≅ Y) (Z : C) :
    f.inv ▷ Z ≫ f.hom ▷ Z = 𝟙 (Y ⊗ Z)

Proof state:
C : Type u
𝒞 : Category.{v, u} C
inst✝ : MonoidalCategory C
X Y : C
f : X ≅ Y
Z : C
⊢ f.inv ▷ Z ≫ f.hom ▷ Z = 𝟙 (Y ⊗ Z)

Tactic:
rw [← comp_whiskerRight, inv_hom_id, id_whiskerRight]

Result:
no goals
-- Mathlib/Analysis/InnerProductSpace/EuclideanDist.lean
theorem nhds_basis_closedBall {x : E} : (𝓝 x).HasBasis (fun r : ℝ => 0 < r) (closedBall x)

Proof state:
E : Type u_1
inst✝⁶ : AddCommGroup E
inst✝⁵ : TopologicalSpace E
inst✝⁴ : IsTopologicalAddGroup E
inst✝³ : T2Space E
inst✝² : Module ℝ E
inst✝¹ : ContinuousSMul ℝ E
inst✝ : FiniteDimensional ℝ E
x : E
⊢ (𝓝 x).HasBasis (fun r => 0 < r) (closedBall x)

Tactic:
rw [toEuclidean.toHomeomorph.nhds_eq_comap x]

Result:
E : Type u_1
inst✝⁶ : AddCommGroup E
inst✝⁵ : TopologicalSpace E
inst✝⁴ : IsTopologicalAddGroup E
inst✝³ : T2Space E
inst✝² : Module ℝ E
inst✝¹ : ContinuousSMul ℝ E
inst✝ : FiniteDimensional ℝ E
x : E
⊢ (Filter.comap (⇑toEuclidean.toHomeomorph) (𝓝 (toEuclidean.toHomeomorph x))).HasBasis (fun r => 0 < r) (closedBall x)

Proof state:
E : Type u_1
inst✝⁶ : AddCommGroup E
inst✝⁵ : TopologicalSpace E
inst✝⁴ : IsTopologicalAddGroup E
inst✝³ : T2Space E
inst✝² : Module ℝ E
inst✝¹ : ContinuousSMul ℝ E
inst✝ : FiniteDimensional ℝ E
x : E
⊢ (Filter.comap (⇑toEuclidean.toHomeomorph) (𝓝 (toEuclidean.toHomeomorph x))).HasBasis (fun r => 0 < r) (closedBall x)

Tactic:
exact Metric.nhds_basis_closedBall.comap _

Result:
no goals
-- Mathlib/Data/Nat/Squarefree.lean
theorem squarefree_pow_iff {n k : ℕ} (hn : n ≠ 1) (hk : k ≠ 0) :
    Squarefree (n ^ k) ↔ Squarefree n ∧ k = 1

Proof state:
n k : ℕ
hn : n ≠ 1
hk : k ≠ 0
⊢ Squarefree (n ^ k) ↔ Squarefree n ∧ k = 1

Tactic:
refine ⟨fun h => ?_, by rintro ⟨hn, rfl⟩; simpa⟩

Result:
n k : ℕ
hn : n ≠ 1
hk : k ≠ 0
h : Squarefree (n ^ k)
⊢ Squarefree n ∧ k = 1

Proof state:
case inr
n k : ℕ
hn : n ≠ 1
hk : k ≠ 0
h : Squarefree (n ^ k)
h₁ : ¬k = 1
this : 2 ≤ k
⊢ False

Tactic:
apply hn (Nat.isUnit_iff.1 (h _ _))

Result:
n k : ℕ
hn : n ≠ 1
hk : k ≠ 0
h : Squarefree (n ^ k)
h₁ : ¬k = 1
this : 2 ≤ k
⊢ n * n ∣ n ^ k

Proof state:
n k : ℕ
hn : n ≠ 1
hk : k ≠ 0
⊢ Squarefree n ∧ k = 1 → Squarefree (n ^ k)

Tactic:
rintro ⟨hn, rfl⟩

Result:
case intro
n : ℕ
hn✝ : n ≠ 1
hn : Squarefree n
hk : 1 ≠ 0
⊢ Squarefree (n ^ 1)

Proof state:
case inr
n k : ℕ
hn : n ≠ 1
hk : k ≠ 0
h : Squarefree (n ^ k)
⊢ Squarefree n ∧ k = 1

Tactic:
refine ⟨h.squarefree_of_dvd (dvd_pow_self _ hk), by_contradiction fun h₁ => ?_⟩

Result:
case inr
n k : ℕ
hn : n ≠ 1
hk : k ≠ 0
h : Squarefree (n ^ k)
h₁ : ¬k = 1
⊢ False

Proof state:
case intro
n : ℕ
hn✝ : n ≠ 1
hn : Squarefree n
hk : 1 ≠ 0
⊢ Squarefree (n ^ 1)

Tactic:
simpa

Result:
no goals

Proof state:
n k : ℕ
hn : n ≠ 1
hk : k ≠ 0
h : Squarefree (n ^ k)
h₁ : ¬k = 1
this : 2 ≤ k
⊢ n * n ∣ n ^ k

Tactic:
rw [← sq]

Result:
n k : ℕ
hn : n ≠ 1
hk : k ≠ 0
h : Squarefree (n ^ k)
h₁ : ¬k = 1
this : 2 ≤ k
⊢ n ^ 2 ∣ n ^ k

Proof state:
case inl
k : ℕ
hk : k ≠ 0
hn : 0 ≠ 1
h : Squarefree (0 ^ k)
⊢ Squarefree 0 ∧ k = 1

Tactic:
simp [zero_pow hk] at h

Result:
no goals

Proof state:
n k : ℕ
hn : n ≠ 1
hk : k ≠ 0
h : Squarefree (n ^ k)
h₁ : ¬k = 1
this : 2 ≤ k
⊢ n ^ 2 ∣ n ^ k

Tactic:
exact pow_dvd_pow _ this

Result:
no goals

Proof state:
n k : ℕ
hn : n ≠ 1
hk : k ≠ 0
h : Squarefree (n ^ k)
⊢ Squarefree n ∧ k = 1

Tactic:
rcases eq_or_ne n 0 with (rfl | -)

Result:
case inl
k : ℕ
hk : k ≠ 0
hn : 0 ≠ 1
h : Squarefree (0 ^ k)
⊢ Squarefree 0 ∧ k = 1

case inr
n k : ℕ
hn : n ≠ 1
hk : k ≠ 0
h : Squarefree (n ^ k)
⊢ Squarefree n ∧ k = 1

Proof state:
case inr
n k : ℕ
hn : n ≠ 1
hk : k ≠ 0
h : Squarefree (n ^ k)
h₁ : ¬k = 1
⊢ False

Tactic:
have : 2 ≤ k := k.two_le_iff.mpr ⟨hk, h₁⟩

Result:
case inr
n k : ℕ
hn : n ≠ 1
hk : k ≠ 0
h : Squarefree (n ^ k)
h₁ : ¬k = 1
this : 2 ≤ k
⊢ False
-- Mathlib/Geometry/Manifold/Instances/Real.lean
lemma IccLeftChart_extend_interior_pos {p : Set.Icc x y} (hp : x < p.val ∧ p.val < y) :
    0 < (IccLeftChart x y).extend (𝓡∂ 1) p 0

Proof state:
x y : ℝ
hxy : Fact (x < y)
p : ↑(Icc x y)
hp : x < ↑p ∧ ↑p < y
⊢ 0 < ↑((IccLeftChart x y).extend (𝓡∂ 1)) p 0

Tactic:
simp_rw [iccLeftChart_extend_zero]

Result:
x y : ℝ
hxy : Fact (x < y)
p : ↑(Icc x y)
hp : x < ↑p ∧ ↑p < y
⊢ 0 < ↑p - x

Proof state:
x y : ℝ
hxy : Fact (x < y)
p : ↑(Icc x y)
hp : x < ↑p ∧ ↑p < y
⊢ 0 < ↑p - x

Tactic:
norm_num [hp.1]

Result:
no goals
-- Mathlib/FieldTheory/IntermediateField/Adjoin/Basic.lean
theorem adjoin_rank_le_of_isAlgebraic (L : IntermediateField F K)
    (halg : Algebra.IsAlgebraic F E ∨ Algebra.IsAlgebraic F L) :
    Module.rank E (adjoin E (L : Set K)) ≤ Module.rank F L

Proof state:
F : Type u_1
inst✝⁶ : Field F
E : Type u_2
inst✝⁵ : Field E
inst✝⁴ : Algebra F E
K : Type u_3
inst✝³ : Field K
inst✝² : Algebra F K
inst✝¹ : Algebra E K
inst✝ : IsScalarTower F E K
L : IntermediateField F K
halg : Algebra.IsAlgebraic F E ∨ Algebra.IsAlgebraic F ↥L
⊢ Module.rank E ↥(adjoin E ↑L) ≤ Module.rank F ↥L

Tactic:
have h : (adjoin E (L.toSubalgebra : Set K)).toSubalgebra =
    Algebra.adjoin E (L.toSubalgebra : Set K) :=
  L.adjoin_toSubalgebra_of_isAlgebraic E halg

Result:
F : Type u_1
inst✝⁶ : Field F
E : Type u_2
inst✝⁵ : Field E
inst✝⁴ : Algebra F E
K : Type u_3
inst✝³ : Field K
inst✝² : Algebra F K
inst✝¹ : Algebra E K
inst✝ : IsScalarTower F E K
L : IntermediateField F K
halg : Algebra.IsAlgebraic F E ∨ Algebra.IsAlgebraic F ↥L
h : (adjoin E ↑L.toSubalgebra).toSubalgebra = Algebra.adjoin E ↑L.toSubalgebra
⊢ Module.rank E ↥(adjoin E ↑L) ≤ Module.rank F ↥L

Proof state:
F : Type u_1
inst✝⁶ : Field F
E : Type u_2
inst✝⁵ : Field E
inst✝⁴ : Algebra F E
K : Type u_3
inst✝³ : Field K
inst✝² : Algebra F K
inst✝¹ : Algebra E K
inst✝ : IsScalarTower F E K
L : IntermediateField F K
halg : Algebra.IsAlgebraic F E ∨ Algebra.IsAlgebraic F ↥L
h : (adjoin E ↑L.toSubalgebra).toSubalgebra = Algebra.adjoin E ↑L.toSubalgebra
this : Module.rank E ↥(Algebra.adjoin E ↑L.toSubalgebra) ≤ Module.rank F ↥L.toSubalgebra
⊢ Module.rank E ↥(adjoin E ↑L) ≤ Module.rank F ↥L

Tactic:
rwa [(Subalgebra.equivOfEq _ _ h).symm.toLinearEquiv.rank_eq] at this

Result:
no goals

Proof state:
F : Type u_1
inst✝⁶ : Field F
E : Type u_2
inst✝⁵ : Field E
inst✝⁴ : Algebra F E
K : Type u_3
inst✝³ : Field K
inst✝² : Algebra F K
inst✝¹ : Algebra E K
inst✝ : IsScalarTower F E K
L : IntermediateField F K
halg : Algebra.IsAlgebraic F E ∨ Algebra.IsAlgebraic F ↥L
h : (adjoin E ↑L.toSubalgebra).toSubalgebra = Algebra.adjoin E ↑L.toSubalgebra
⊢ Module.rank E ↥(adjoin E ↑L) ≤ Module.rank F ↥L

Tactic:
have := L.toSubalgebra.adjoin_rank_le E

Result:
F : Type u_1
inst✝⁶ : Field F
E : Type u_2
inst✝⁵ : Field E
inst✝⁴ : Algebra F E
K : Type u_3
inst✝³ : Field K
inst✝² : Algebra F K
inst✝¹ : Algebra E K
inst✝ : IsScalarTower F E K
L : IntermediateField F K
halg : Algebra.IsAlgebraic F E ∨ Algebra.IsAlgebraic F ↥L
h : (adjoin E ↑L.toSubalgebra).toSubalgebra = Algebra.adjoin E ↑L.toSubalgebra
this : Module.rank E ↥(Algebra.adjoin E ↑L.toSubalgebra) ≤ Module.rank F ↥L.toSubalgebra
⊢ Module.rank E ↥(adjoin E ↑L) ≤ Module.rank F ↥L
-- Mathlib/CategoryTheory/Iso.lean
theorem cancel_iso_inv_right {X Y Z : C} (f f' : X ⟶ Y) (g : Z ≅ Y) :
    f ≫ g.inv = f' ≫ g.inv ↔ f = f'

Proof state:
C : Type u
inst✝ : Category.{v, u} C
X Y Z : C
f f' : X ⟶ Y
g : Z ≅ Y
⊢ f ≫ g.inv = f' ≫ g.inv ↔ f = f'

Tactic:
simp only [cancel_mono]

Result:
no goals
-- Mathlib/Data/Vector/Defs.lean
theorem toList_take {n m : ℕ} (v : Vector α m) : toList (take n v) = List.take n (toList v)

Proof state:
α : Type u_1
n m : ℕ
v : Vector α m
⊢ (take n v).toList = List.take n v.toList

Tactic:
cases v

Result:
case mk
α : Type u_1
n m : ℕ
val✝ : List α
property✝ : val✝.length = m
⊢ (take n ⟨val✝, property✝⟩).toList = List.take n (toList ⟨val✝, property✝⟩)

Proof state:
case mk
α : Type u_1
n m : ℕ
val✝ : List α
property✝ : val✝.length = m
⊢ (take n ⟨val✝, property✝⟩).toList = List.take n (toList ⟨val✝, property✝⟩)

Tactic:
rfl

Result:
no goals
-- Mathlib/Analysis/Convex/Deriv.lean
lemma le_slope_of_hasDerivWithinAt_Iio (hfc : ConcaveOn ℝ S f)
    (hx : x ∈ S) (hy : y ∈ S) (hxy : x < y) (hf' : HasDerivWithinAt f f' (Iio y) y) :
    f' ≤ slope f x y

Proof state:
S : Set ℝ
f : ℝ → ℝ
x y f' : ℝ
hfc : ConcaveOn ℝ S f
hx : x ∈ S
hy : y ∈ S
hxy : x < y
hf' : HasDerivWithinAt f f' (Iio y) y
⊢ f' ≤ slope f x y

Tactic:
simpa only [neg_neg, Pi.neg_def, slope_neg] using
  neg_le_neg (hfc.neg.slope_le_of_hasDerivWithinAt_Iio hx hy hxy hf'.neg)

Result:
no goals
-- Mathlib/MeasureTheory/Decomposition/RadonNikodym.lean
lemma integrableOn_toReal_rnDeriv {s : Set α} (hμs : μ s ≠ ∞) :
    IntegrableOn (fun x ↦ (μ.rnDeriv ν x).toReal) s ν

Proof state:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
s : Set α
hμs : μ s ≠ ⊤
⊢ ∫⁻ (x : α) in s, μ.rnDeriv ν x ∂ν ≠ ⊤

Tactic:
exact ((setLIntegral_rnDeriv_le _).trans_lt hμs.lt_top).ne

Result:
no goals

Proof state:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
s : Set α
hμs : μ s ≠ ⊤
⊢ IntegrableOn (fun x => (μ.rnDeriv ν x).toReal) s ν

Tactic:
refine integrable_toReal_of_lintegral_ne_top (Measure.measurable_rnDeriv _ _).aemeasurable ?_

Result:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
s : Set α
hμs : μ s ≠ ⊤
⊢ ∫⁻ (x : α) in s, μ.rnDeriv ν x ∂ν ≠ ⊤