harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Data/Matroid/Map.lean
@[simp] lemma mapEquiv_dep_iff {D : Set β} : (M.mapEquiv f).Dep D ↔ M.Dep (f.symm '' D)

Proof state:
α : Type u_1
β : Type u_2
M : Matroid α
f : α ≃ β
D : Set β
⊢ (M.mapEquiv f).Dep D ↔ M.Dep (⇑f.symm '' D)

Tactic:
rw [mapEquiv_eq_map, map_dep_iff]

Result:
α : Type u_1
β : Type u_2
M : Matroid α
f : α ≃ β
D : Set β
⊢ (∃ D₀, M.Dep D₀ ∧ D = ⇑f '' D₀) ↔ M.Dep (⇑f.symm '' D)

Proof state:
case intro.intro
α : Type u_1
β : Type u_2
M : Matroid α
f : α ≃ β
I : Set α
hI : M.Dep I
⊢ M.Dep (⇑f.symm '' (⇑f '' I))

Tactic:
simpa

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
M : Matroid α
f : α ≃ β
D : Set β
⊢ (∃ D₀, M.Dep D₀ ∧ D = ⇑f '' D₀) → M.Dep (⇑f.symm '' D)

Tactic:
rintro ⟨I, hI, rfl⟩

Result:
case intro.intro
α : Type u_1
β : Type u_2
M : Matroid α
f : α ≃ β
I : Set α
hI : M.Dep I
⊢ M.Dep (⇑f.symm '' (⇑f '' I))

Proof state:
α : Type u_1
β : Type u_2
M : Matroid α
f : α ≃ β
D : Set β
h : M.Dep (⇑f.symm '' D)
⊢ D = ⇑f '' (⇑f.symm '' D)

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
M : Matroid α
f : α ≃ β
D : Set β
⊢ (∃ D₀, M.Dep D₀ ∧ D = ⇑f '' D₀) ↔ M.Dep (⇑f.symm '' D)

Tactic:
exact ⟨by rintro ⟨I, hI, rfl⟩; simpa, fun h ↦ ⟨_, h, by simp⟩⟩

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Regularity/Bound.lean
theorem eps_pos (hPε : 100 ≤ (4 : ℝ) ^ #P.parts * ε ^ 5) : 0 < ε :=
  (Odd.pow_pos_iff (by decide)).mp (eps_pow_five_pos hPε)

Proof state:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
P : Finpartition univ
ε : ℝ
hPε : 100 ≤ 4 ^ #P.parts * ε ^ 5
⊢ Odd 5

Tactic:
decide

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem ofFn_succ (f : Fin (n+1) → α) :
    ofFn f = (ofFn (fun (i : Fin n) => f i.castSucc)).push (f ⟨n, by omega⟩)

Proof state:
n : Nat
α : Type ?u.463252
f : Fin (n + 1) → α
⊢ n < n + 1

Tactic:
omega

Result:
no goals

Proof state:
case h₂.isFalse.e_a.e_val
n : Nat
α : Type u_1
f : Fin (n + 1) → α
i : Nat
h₁ : i < (ofFn f).size
h₂ : i < ((ofFn fun i => f i.castSucc).push (f ⟨n, ⋯⟩)).size
h₃ : ¬i < n
⊢ i = n

Tactic:
simp at h₁ h₂

Result:
case h₂.isFalse.e_a.e_val
n : Nat
α : Type u_1
f : Fin (n + 1) → α
i : Nat
h₃ : ¬i < n
h₁ h₂ : i < n + 1
⊢ i = n

Proof state:
case h₂
n : Nat
α : Type u_1
f : Fin (n + 1) → α
i : Nat
h₁ : i < (ofFn f).size
h₂ : i < ((ofFn fun i => f i.castSucc).push (f ⟨n, ⋯⟩)).size
⊢ f ⟨i, ⋯⟩ = if h : i < n then f ⟨i, ⋯⟩ else f ⟨n, ⋯⟩

Tactic:
split <;> rename_i h₃

Result:
case h₂.isTrue
n : Nat
α : Type u_1
f : Fin (n + 1) → α
i : Nat
h₁ : i < (ofFn f).size
h₂ : i < ((ofFn fun i => f i.castSucc).push (f ⟨n, ⋯⟩)).size
h₃ : i < n
⊢ f ⟨i, ⋯⟩ = f ⟨i, ⋯⟩

case h₂.isFalse
n : Nat
α : Type u_1
f : Fin (n + 1) → α
i : Nat
h₁ : i < (ofFn f).size
h₂ : i < ((ofFn fun i => f i.castSucc).push (f ⟨n, ⋯⟩)).size
h₃ : ¬i < n
⊢ f ⟨i, ⋯⟩ = f ⟨n, ⋯⟩

Proof state:
case h₁
n : Nat
α : Type u_1
f : Fin (n + 1) → α
⊢ (ofFn f).size = ((ofFn fun i => f i.castSucc).push (f ⟨n, ⋯⟩)).size

Tactic:
simp

Result:
no goals

Proof state:
case h₂.isFalse
n : Nat
α : Type u_1
f : Fin (n + 1) → α
i : Nat
h₁ : i < (ofFn f).size
h₂ : i < ((ofFn fun i => f i.castSucc).push (f ⟨n, ⋯⟩)).size
h₃ : ¬i < n
⊢ f ⟨i, ⋯⟩ = f ⟨n, ⋯⟩

Tactic:
congr

Result:
case h₂.isFalse.e_a.e_val
n : Nat
α : Type u_1
f : Fin (n + 1) → α
i : Nat
h₁ : i < (ofFn f).size
h₂ : i < ((ofFn fun i => f i.castSucc).push (f ⟨n, ⋯⟩)).size
h₃ : ¬i < n
⊢ i = n

Proof state:
n : Nat
α : Type u_1
f : Fin (n + 1) → α
⊢ ofFn f = (ofFn fun i => f i.castSucc).push (f ⟨n, ⋯⟩)

Tactic:
ext i h₁ h₂

Result:
case h₁
n : Nat
α : Type u_1
f : Fin (n + 1) → α
⊢ (ofFn f).size = ((ofFn fun i => f i.castSucc).push (f ⟨n, ⋯⟩)).size

case h₂
n : Nat
α : Type u_1
f : Fin (n + 1) → α
i : Nat
h₁ : i < (ofFn f).size
h₂ : i < ((ofFn fun i => f i.castSucc).push (f ⟨n, ⋯⟩)).size
⊢ (ofFn f)[i] = ((ofFn fun i => f i.castSucc).push (f ⟨n, ⋯⟩))[i]

Proof state:
case h₂
n : Nat
α : Type u_1
f : Fin (n + 1) → α
i : Nat
h₁ : i < (ofFn f).size
h₂ : i < ((ofFn fun i => f i.castSucc).push (f ⟨n, ⋯⟩)).size
⊢ (ofFn f)[i] = ((ofFn fun i => f i.castSucc).push (f ⟨n, ⋯⟩))[i]

Tactic:
simp [getElem_push]

Result:
case h₂
n : Nat
α : Type u_1
f : Fin (n + 1) → α
i : Nat
h₁ : i < (ofFn f).size
h₂ : i < ((ofFn fun i => f i.castSucc).push (f ⟨n, ⋯⟩)).size
⊢ f ⟨i, ⋯⟩ = if h : i < n then f ⟨i, ⋯⟩ else f ⟨n, ⋯⟩

Proof state:
case h₂.isFalse.e_a.e_val
n : Nat
α : Type u_1
f : Fin (n + 1) → α
i : Nat
h₃ : ¬i < n
h₁ h₂ : i < n + 1
⊢ i = n

Tactic:
omega

Result:
no goals

Proof state:
case h₂.isTrue
n : Nat
α : Type u_1
f : Fin (n + 1) → α
i : Nat
h₁ : i < (ofFn f).size
h₂ : i < ((ofFn fun i => f i.castSucc).push (f ⟨n, ⋯⟩)).size
h₃ : i < n
⊢ f ⟨i, ⋯⟩ = f ⟨i, ⋯⟩

Tactic:
rfl

Result:
no goals
-- Mathlib/Algebra/Group/Subgroup/Ker.lean
theorem range_le_ker_iff (f : G →* G') (g : G' →* G'') : f.range ≤ g.ker ↔ g.comp f = 1 :=
  ⟨fun h => ext fun x => h ⟨x, rfl⟩, by rintro h _ ⟨y, rfl⟩; exact DFunLike.congr_fun h y⟩

Proof state:
case intro
G : Type u_1
G' : Type u_2
G'' : Type u_3
inst✝² : Group G
inst✝¹ : Group G'
inst✝ : Group G''
f : G →* G'
g : G' →* G''
h : g.comp f = 1
y : G
⊢ f y ∈ g.ker

Tactic:
exact DFunLike.congr_fun h y

Result:
no goals

Proof state:
G : Type u_1
G' : Type u_2
G'' : Type u_3
inst✝² : Group G
inst✝¹ : Group G'
inst✝ : Group G''
f : G →* G'
g : G' →* G''
⊢ g.comp f = 1 → f.range ≤ g.ker

Tactic:
rintro h _ ⟨y, rfl⟩

Result:
case intro
G : Type u_1
G' : Type u_2
G'' : Type u_3
inst✝² : Group G
inst✝¹ : Group G'
inst✝ : Group G''
f : G →* G'
g : G' →* G''
h : g.comp f = 1
y : G
⊢ f y ∈ g.ker
-- Mathlib/AlgebraicGeometry/OpenImmersion.lean
lemma image_iSup₂ {ι : Sort*} {κ : ι → Sort*} (s : (i : ι) → κ i → X.Opens) :
    (f ''ᵁ ⨆ (i : ι), ⨆ (j : κ i), s i j) = ⨆ (i : ι), ⨆ (j : κ i), f ''ᵁ s i j

Proof state:
X Y : Scheme
f : X.Hom Y
H : IsOpenImmersion f
ι : Sort u_1
κ : ι → Sort u_2
s : (i : ι) → κ i → X.Opens
⊢ f ''ᵁ ⨆ i, ⨆ j, s i j = ⨆ i, ⨆ j, f ''ᵁ s i j

Tactic:
ext : 1

Result:
case h
X Y : Scheme
f : X.Hom Y
H : IsOpenImmersion f
ι : Sort u_1
κ : ι → Sort u_2
s : (i : ι) → κ i → X.Opens
⊢ ↑(f ''ᵁ ⨆ i, ⨆ j, s i j) = ↑(⨆ i, ⨆ j, f ''ᵁ s i j)

Proof state:
case h
X Y : Scheme
f : X.Hom Y
H : IsOpenImmersion f
ι : Sort u_1
κ : ι → Sort u_2
s : (i : ι) → κ i → X.Opens
⊢ ↑(f ''ᵁ ⨆ i, ⨆ j, s i j) = ↑(⨆ i, ⨆ j, f ''ᵁ s i j)

Tactic:
simp [Set.image_iUnion₂]

Result:
no goals
-- Mathlib/Algebra/Algebra/NonUnitalSubalgebra.lean
theorem mem_sup_right {S T : NonUnitalSubalgebra R A} : ∀ {x : A}, x ∈ T → x ∈ S ⊔ T

Proof state:
R : Type u
A : Type v
inst✝⁴ : CommSemiring R
inst✝³ : NonUnitalNonAssocSemiring A
inst✝² : Module R A
inst✝¹ : IsScalarTower R A A
inst✝ : SMulCommClass R A A
S T : NonUnitalSubalgebra R A
⊢ ∀ {x : A}, x ∈ T → x ∈ S ⊔ T

Tactic:
rw [← SetLike.le_def]

Result:
R : Type u
A : Type v
inst✝⁴ : CommSemiring R
inst✝³ : NonUnitalNonAssocSemiring A
inst✝² : Module R A
inst✝¹ : IsScalarTower R A A
inst✝ : SMulCommClass R A A
S T : NonUnitalSubalgebra R A
⊢ T ≤ S ⊔ T

Proof state:
R : Type u
A : Type v
inst✝⁴ : CommSemiring R
inst✝³ : NonUnitalNonAssocSemiring A
inst✝² : Module R A
inst✝¹ : IsScalarTower R A A
inst✝ : SMulCommClass R A A
S T : NonUnitalSubalgebra R A
⊢ T ≤ S ⊔ T

Tactic:
exact le_sup_right

Result:
no goals
-- Mathlib/Data/Nat/Choose/Bounds.lean
theorem pow_le_choose (r n : ℕ) : ((n + 1 - r : ℕ) ^ r : α) / r ! ≤ n.choose r

Proof state:
α : Type u_1
inst✝ : LinearOrderedSemifield α
r n : ℕ
⊢ (n + 1 - r) ^ r ≤ n.descFactorial r

Tactic:
exact n.pow_sub_le_descFactorial r

Result:
no goals

Proof state:
α : Type u_1
inst✝ : LinearOrderedSemifield α
r n : ℕ
⊢ 0 < ↑r !

Tactic:
exact mod_cast r.factorial_pos

Result:
no goals

Proof state:
α : Type u_1
inst✝ : LinearOrderedSemifield α
r n : ℕ
⊢ ↑(n + 1 - r) ^ r / ↑r ! ≤ ↑(n.choose r)

Tactic:
rw [div_le_iff₀']

Result:
α : Type u_1
inst✝ : LinearOrderedSemifield α
r n : ℕ
⊢ ↑(n + 1 - r) ^ r ≤ ↑r ! * ↑(n.choose r)

α : Type u_1
inst✝ : LinearOrderedSemifield α
r n : ℕ
⊢ 0 < ↑r !

Proof state:
α : Type u_1
inst✝ : LinearOrderedSemifield α
r n : ℕ
⊢ ↑(n + 1 - r) ^ r ≤ ↑r ! * ↑(n.choose r)

Tactic:
norm_cast

Result:
α : Type u_1
inst✝ : LinearOrderedSemifield α
r n : ℕ
⊢ (n + 1 - r) ^ r ≤ r ! * n.choose r

Proof state:
α : Type u_1
inst✝ : LinearOrderedSemifield α
r n : ℕ
⊢ (n + 1 - r) ^ r ≤ r ! * n.choose r

Tactic:
rw [← Nat.descFactorial_eq_factorial_mul_choose]

Result:
α : Type u_1
inst✝ : LinearOrderedSemifield α
r n : ℕ
⊢ (n + 1 - r) ^ r ≤ n.descFactorial r
-- Mathlib/LinearAlgebra/RootSystem/Defs.lean
lemma pairing_smul_coroot_eq (k : ι) (hij : P.reflection_perm i = P.reflection_perm j) :
    P.pairing i k • P.coroot i = P.pairing j k • P.coroot j

Proof state:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
P : RootPairing ι R M N
i j k : ι
hij : P.reflection_perm i = P.reflection_perm j
⊢ P.pairing i k • P.coroot i = P.pairing j k • P.coroot j

Tactic:
have h : P.coreflection i (P.coroot k) = P.coreflection j (P.coroot k) := by
  simp only [← coroot_reflection_perm, hij]

Result:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
P : RootPairing ι R M N
i j k : ι
hij : P.reflection_perm i = P.reflection_perm j
h : (P.coreflection i) (P.coroot k) = (P.coreflection j) (P.coroot k)
⊢ P.pairing i k • P.coroot i = P.pairing j k • P.coroot j

Proof state:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
P : RootPairing ι R M N
i j k : ι
hij : P.reflection_perm i = P.reflection_perm j
⊢ (P.coreflection i) (P.coroot k) = (P.coreflection j) (P.coroot k)

Tactic:
simp only [← coroot_reflection_perm, hij]

Result:
no goals

Proof state:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
P : RootPairing ι R M N
i j k : ι
hij : P.reflection_perm i = P.reflection_perm j
h : (P.coreflection i) (P.coroot k) = (P.coreflection j) (P.coroot k)
⊢ P.pairing i k • P.coroot i = P.pairing j k • P.coroot j

Tactic:
simpa only [coreflection_apply_coroot, sub_right_inj] using h

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/AssocList/Lemmas.lean
theorem getD_eq {β : Type v} [BEq α] {l : AssocList α (fun _ => β)} {a : α} {fallback : β} :
    l.getD a fallback = getValueD a l.toList fallback

Proof state:
α : Type u
β : Type v
inst✝ : BEq α
l : AssocList α fun x => β
a : α
fallback : β
⊢ getD a fallback l = getValueD a l.toList fallback

Tactic:
induction l

Result:
case nil
α : Type u
β : Type v
inst✝ : BEq α
a : α
fallback : β
⊢ getD a fallback nil = getValueD a nil.toList fallback

case cons
α : Type u
β : Type v
inst✝ : BEq α
a : α
fallback : β
key✝ : α
value✝ : β
tail✝ : AssocList α fun x => β
tail_ih✝ : getD a fallback tail✝ = getValueD a tail✝.toList fallback
⊢ getD a fallback (cons key✝ value✝ tail✝) = getValueD a (cons key✝ value✝ tail✝).toList fallback

Proof state:
case nil
α : Type u
β : Type v
inst✝ : BEq α
a : α
fallback : β
⊢ getD a fallback nil = getValueD a nil.toList fallback

Tactic:
simp [getD, List.getValueD]

Result:
no goals

Proof state:
case cons
α : Type u
β : Type v
inst✝ : BEq α
a : α
fallback : β
key✝ : α
value✝ : β
tail✝ : AssocList α fun x => β
tail_ih✝ : getD a fallback tail✝ = getValueD a tail✝.toList fallback
⊢ getD a fallback (cons key✝ value✝ tail✝) = getValueD a (cons key✝ value✝ tail✝).toList fallback

Tactic:
simp_all [getD, List.getValueD, List.getValueD, List.getValue?_cons,
  Bool.apply_cond (fun x => Option.getD x fallback)]

Result:
no goals
-- Mathlib/Algebra/Polynomial/Derivative.lean
theorem iterate_derivative_eq_sum (p : R[X]) (k : ℕ) :
    derivative^[k] p =
      ∑ x ∈ (derivative^[k] p).support, C ((x + k).descFactorial k • p.coeff (x + k)) * X ^ x

Proof state:
R : Type u
inst✝ : Semiring R
p : R[X]
k : ℕ
⊢ ∑ i ∈ ((⇑derivative)^[k] p).support, C (((⇑derivative)^[k] p).coeff i) * X ^ i =
    ∑ x ∈ ((⇑derivative)^[k] p).support, C ((x + k).descFactorial k • p.coeff (x + k)) * X ^ x

Tactic:
refine sum_congr rfl fun i _ ↦ ?_

Result:
R : Type u
inst✝ : Semiring R
p : R[X]
k i : ℕ
x✝ : i ∈ ((⇑derivative)^[k] p).support
⊢ C (((⇑derivative)^[k] p).coeff i) * X ^ i = C ((i + k).descFactorial k • p.coeff (i + k)) * X ^ i

Proof state:
R : Type u
inst✝ : Semiring R
p : R[X]
k : ℕ
⊢ (⇑derivative)^[k] p = ∑ x ∈ ((⇑derivative)^[k] p).support, C ((x + k).descFactorial k • p.coeff (x + k)) * X ^ x

Tactic:
conv_lhs => rw [(derivative^[k] p).as_sum_support_C_mul_X_pow]

Result:
R : Type u
inst✝ : Semiring R
p : R[X]
k : ℕ
⊢ ∑ i ∈ ((⇑derivative)^[k] p).support, C (((⇑derivative)^[k] p).coeff i) * X ^ i =
    ∑ x ∈ ((⇑derivative)^[k] p).support, C ((x + k).descFactorial k • p.coeff (x + k)) * X ^ x

Proof state:
R : Type u
inst✝ : Semiring R
p : R[X]
k i : ℕ
x✝ : i ∈ ((⇑derivative)^[k] p).support
⊢ C (((⇑derivative)^[k] p).coeff i) * X ^ i = C ((i + k).descFactorial k • p.coeff (i + k)) * X ^ i

Tactic:
rw [coeff_iterate_derivative, Nat.descFactorial_eq_factorial_mul_choose]

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Walk.lean
theorem reverse_map : (p.map f).reverse = p.reverse.map f

Proof state:
V : Type u
V' : Type v
G : SimpleGraph V
G' : SimpleGraph V'
f : G →g G'
u v : V
p : G.Walk u v
⊢ (Walk.map f p).reverse = Walk.map f p.reverse

Tactic:
induction p <;> simp [map_append, *]

Result:
no goals
-- Mathlib/Topology/MetricSpace/HausdorffDistance.lean
theorem infEdist_le_hausdorffEdist_of_mem (h : x ∈ s) : infEdist x t ≤ hausdorffEdist s t

Proof state:
α : Type u
inst✝ : PseudoEMetricSpace α
x : α
s t : Set α
h : x ∈ s
⊢ infEdist x t ≤ (⨆ x ∈ s, infEdist x t) ⊔ ⨆ y ∈ t, infEdist y s

Tactic:
refine le_trans ?_ le_sup_left

Result:
α : Type u
inst✝ : PseudoEMetricSpace α
x : α
s t : Set α
h : x ∈ s
⊢ infEdist x t ≤ ⨆ x ∈ s, infEdist x t

Proof state:
α : Type u
inst✝ : PseudoEMetricSpace α
x : α
s t : Set α
h : x ∈ s
⊢ infEdist x t ≤ hausdorffEdist s t

Tactic:
rw [hausdorffEdist_def]

Result:
α : Type u
inst✝ : PseudoEMetricSpace α
x : α
s t : Set α
h : x ∈ s
⊢ infEdist x t ≤ (⨆ x ∈ s, infEdist x t) ⊔ ⨆ y ∈ t, infEdist y s

Proof state:
α : Type u
inst✝ : PseudoEMetricSpace α
x : α
s t : Set α
h : x ∈ s
⊢ infEdist x t ≤ ⨆ x ∈ s, infEdist x t

Tactic:
exact le_iSup₂ (α := ℝ≥0∞) x h

Result:
no goals
-- Mathlib/Data/Nat/MaxPowDiv.lean
theorem base_mul_eq_succ {p n : ℕ} (hp : 1 < p) (hn : 0 < n) :
    p.maxPowDiv (p*n) = p.maxPowDiv n + 1

Proof state:
p n : ℕ
hp : 1 < p
hn : 0 < n
this : 0 < p
⊢ p * n % p = 0

Tactic:
simp

Result:
no goals

Proof state:
case hc
p n : ℕ
hp : 1 < p
hn : 0 < n
this : 0 < p
⊢ 1 < p ∧ 0 < p * n ∧ p * n % p = 0

Tactic:
refine ⟨hp, ?_, by simp⟩

Result:
case hc
p n : ℕ
hp : 1 < p
hn : 0 < n
this : 0 < p
⊢ 0 < p * n

Proof state:
p n : ℕ
hp : 1 < p
hn : 0 < n
this : 0 < p
⊢ go 0 p (p * n) = go 0 p n + 1

Tactic:
rw [maxPowDiv.go, if_pos, mul_div_right _ this]

Result:
p n : ℕ
hp : 1 < p
hn : 0 < n
this : 0 < p
⊢ go (0 + 1) p n = go 0 p n + 1

case hc
p n : ℕ
hp : 1 < p
hn : 0 < n
this : 0 < p
⊢ 1 < p ∧ 0 < p * n ∧ p * n % p = 0

Proof state:
p n : ℕ
hp : 1 < p
hn : 0 < n
this : 0 < p
⊢ p.maxPowDiv (p * n) = p.maxPowDiv n + 1

Tactic:
dsimp [maxPowDiv]

Result:
p n : ℕ
hp : 1 < p
hn : 0 < n
this : 0 < p
⊢ go 0 p (p * n) = go 0 p n + 1

Proof state:
case hc
p n : ℕ
hp : 1 < p
hn : 0 < n
this : 0 < p
⊢ 0 < p * n

Tactic:
apply Nat.mul_pos this hn

Result:
no goals

Proof state:
p n : ℕ
hp : 1 < p
hn : 0 < n
⊢ p.maxPowDiv (p * n) = p.maxPowDiv n + 1

Tactic:
have : 0 < p := lt_trans (b := 1) (by simp) hp

Result:
p n : ℕ
hp : 1 < p
hn : 0 < n
this : 0 < p
⊢ p.maxPowDiv (p * n) = p.maxPowDiv n + 1

Proof state:
p n : ℕ
hp : 1 < p
hn : 0 < n
this : 0 < p
⊢ go (0 + 1) p n = go 0 p n + 1

Tactic:
apply go_succ

Result:
no goals

Proof state:
p n : ℕ
hp : 1 < p
hn : 0 < n
⊢ 0 < 1

Tactic:
simp

Result:
no goals
-- Mathlib/Algebra/Quaternion.lean
theorem star_add_self' : star a + a = ↑(2 * a.re + c₂ * a.imI)

Proof state:
R : Type u_3
c₁ c₂ c₃ : R
a : ℍ[R,c₁,c₂,c₃]
inst✝ : CommRing R
⊢ star a + a = ↑(2 * a.re + c₂ * a.imI)

Tactic:
rw [add_comm, self_add_star']

Result:
no goals
-- Mathlib/GroupTheory/Perm/Cycle/Basic.lean
theorem sameCycle_inv_apply_left : SameCycle f (f⁻¹ x) y ↔ SameCycle f x y

Proof state:
α : Type u_2
f : Perm α
x y : α
⊢ f.SameCycle (f⁻¹ x) y ↔ f.SameCycle x y

Tactic:
rw [← sameCycle_apply_left, apply_inv_self]

Result:
no goals
-- Mathlib/Order/Interval/Set/Basic.lean
theorem Icc_union_Ici' (h₁ : c ≤ b) : Icc a b ∪ Ici c = Ici (min a c)

Proof state:
case pos
α : Type u_1
inst✝ : LinearOrder α
a b c : α
h₁ : c ≤ b
x : α
hc : c ≤ x
⊢ a ≤ x ∧ x ≤ b ∨ c ≤ x ↔ a ≤ x ∨ c ≤ x

Tactic:
simp only [hc, or_true]

Result:
no goals

Proof state:
case h
α : Type u_1
inst✝ : LinearOrder α
a b c : α
h₁ : c ≤ b
x : α
⊢ x ∈ Icc a b ∪ Ici c ↔ x ∈ Ici (a ⊓ c)

Tactic:
simp_rw [mem_union, mem_Icc, mem_Ici, min_le_iff]

Result:
case h
α : Type u_1
inst✝ : LinearOrder α
a b c : α
h₁ : c ≤ b
x : α
⊢ a ≤ x ∧ x ≤ b ∨ c ≤ x ↔ a ≤ x ∨ c ≤ x

Proof state:
case neg
α : Type u_1
inst✝ : LinearOrder α
a b c : α
h₁ : c ≤ b
x : α
hc : ¬c ≤ x
hxb : x ≤ b
⊢ a ≤ x ∧ x ≤ b ∨ c ≤ x ↔ a ≤ x ∨ c ≤ x

Tactic:
simp only [hxb, and_true]

Result:
no goals

Proof state:
case h
α : Type u_1
inst✝ : LinearOrder α
a b c : α
h₁ : c ≤ b
x : α
⊢ a ≤ x ∧ x ≤ b ∨ c ≤ x ↔ a ≤ x ∨ c ≤ x

Tactic:
by_cases hc : c ≤ x

Result:
case pos
α : Type u_1
inst✝ : LinearOrder α
a b c : α
h₁ : c ≤ b
x : α
hc : c ≤ x
⊢ a ≤ x ∧ x ≤ b ∨ c ≤ x ↔ a ≤ x ∨ c ≤ x

case neg
α : Type u_1
inst✝ : LinearOrder α
a b c : α
h₁ : c ≤ b
x : α
hc : ¬c ≤ x
⊢ a ≤ x ∧ x ≤ b ∨ c ≤ x ↔ a ≤ x ∨ c ≤ x

Proof state:
case neg
α : Type u_1
inst✝ : LinearOrder α
a b c : α
h₁ : c ≤ b
x : α
hc : ¬c ≤ x
⊢ a ≤ x ∧ x ≤ b ∨ c ≤ x ↔ a ≤ x ∨ c ≤ x

Tactic:
have hxb : x ≤ b := (le_of_not_ge hc).trans h₁

Result:
case neg
α : Type u_1
inst✝ : LinearOrder α
a b c : α
h₁ : c ≤ b
x : α
hc : ¬c ≤ x
hxb : x ≤ b
⊢ a ≤ x ∧ x ≤ b ∨ c ≤ x ↔ a ≤ x ∨ c ≤ x

Proof state:
α : Type u_1
inst✝ : LinearOrder α
a b c : α
h₁ : c ≤ b
⊢ Icc a b ∪ Ici c = Ici (a ⊓ c)

Tactic:
ext1 x

Result:
case h
α : Type u_1
inst✝ : LinearOrder α
a b c : α
h₁ : c ≤ b
x : α
⊢ x ∈ Icc a b ∪ Ici c ↔ x ∈ Ici (a ⊓ c)
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Nat/Bitwise/Lemmas.lean
theorem and_le_right {n m : Nat} : n &&& m ≤ m :=
  le_of_testBit (by simp)

Proof state:
n m : Nat
⊢ ∀ (i : Nat), (n &&& m).testBit i = true → m.testBit i = true

Tactic:
simp

Result:
no goals
-- Mathlib/LinearAlgebra/Matrix/NonsingularInverse.lean
theorem inv_mul_eq_iff_eq_mul_of_invertible (A B C : Matrix n n α) [Invertible A] :
    A⁻¹ * B = C ↔ B = A * C :=
  ⟨fun h => by rw [← h, mul_inv_cancel_left_of_invertible],
   fun h => by rw [h, inv_mul_cancel_left_of_invertible]⟩

Proof state:
n : Type u'
α : Type v
inst✝³ : Fintype n
inst✝² : DecidableEq n
inst✝¹ : CommRing α
A B C : Matrix n n α
inst✝ : Invertible A
h : A⁻¹ * B = C
⊢ B = A * C

Tactic:
rw [← h, mul_inv_cancel_left_of_invertible]

Result:
no goals

Proof state:
n : Type u'
α : Type v
inst✝³ : Fintype n
inst✝² : DecidableEq n
inst✝¹ : CommRing α
A B C : Matrix n n α
inst✝ : Invertible A
h : B = A * C
⊢ A⁻¹ * B = C

Tactic:
rw [h, inv_mul_cancel_left_of_invertible]

Result:
no goals
-- Mathlib/Control/Traversable/Lemmas.lean
theorem naturality_pf (η : ApplicativeTransformation F G) (f : α → F β) :
    traverse (@η _ ∘ f) = @η _ ∘ (traverse f : t α → F (t β))

Proof state:
t : Type u → Type u
inst✝⁵ : Traversable t
inst✝⁴ : LawfulTraversable t
F G : Type u → Type u
inst✝³ : Applicative F
inst✝² : LawfulApplicative F
inst✝¹ : Applicative G
inst✝ : LawfulApplicative G
α β : Type u
η : ApplicativeTransformation F G
f : α → F β
⊢ traverse ((fun {α} => η.app α) ∘ f) = (fun {α} => η.app α) ∘ traverse f

Tactic:
ext

Result:
case h
t : Type u → Type u
inst✝⁵ : Traversable t
inst✝⁴ : LawfulTraversable t
F G : Type u → Type u
inst✝³ : Applicative F
inst✝² : LawfulApplicative F
inst✝¹ : Applicative G
inst✝ : LawfulApplicative G
α β : Type u
η : ApplicativeTransformation F G
f : α → F β
x✝ : t α
⊢ traverse ((fun {α} => η.app α) ∘ f) x✝ = ((fun {α} => η.app α) ∘ traverse f) x✝

Proof state:
case h
t : Type u → Type u
inst✝⁵ : Traversable t
inst✝⁴ : LawfulTraversable t
F G : Type u → Type u
inst✝³ : Applicative F
inst✝² : LawfulApplicative F
inst✝¹ : Applicative G
inst✝ : LawfulApplicative G
α β : Type u
η : ApplicativeTransformation F G
f : α → F β
x✝ : t α
⊢ traverse ((fun {α} => η.app α) ∘ f) x✝ = ((fun {α} => η.app α) ∘ traverse f) x✝

Tactic:
rw [comp_apply, naturality]

Result:
no goals
-- Mathlib/Analysis/Normed/Algebra/Spectrum.lean
lemma lt_nnreal_iff [Module ℝ A] [IsScalarTower ℝ A A] [SMulCommClass ℝ A A] {a : A}
    (ha : QuasispectrumRestricts a ContinuousMap.realToNNReal) {r : ℝ≥0} :
    (∀ x ∈ quasispectrum ℝ≥0 a, x < r) ↔ ∀ x ∈ quasispectrum ℝ a, x < r

Proof state:
A : Type u_3
inst✝³ : NonUnitalRing A
inst✝² : Module ℝ A
inst✝¹ : IsScalarTower ℝ A A
inst✝ : SMulCommClass ℝ A A
a : A
ha : QuasispectrumRestricts a ⇑ContinuousMap.realToNNReal
r : ℝ≥0
⊢ (∀ x ∈ σₙ ℝ≥0 a, x < r) ↔ ∀ x ∈ σₙ ℝ a, x < ↑r

Tactic:
simp [← ha.algebraMap_image]

Result:
no goals
-- Mathlib/Analysis/Asymptotics/SpecificAsymptotics.lean
theorem Asymptotics.isLittleO_sum_range_of_tendsto_zero {α : Type*} [NormedAddCommGroup α]
    {f : ℕ → α} (h : Tendsto f atTop (𝓝 0)) :
    (fun n => ∑ i ∈ range n, f i) =o[atTop] fun n => (n : ℝ)

Proof state:
α : Type u_1
inst✝ : NormedAddCommGroup α
f : ℕ → α
h : Tendsto f atTop (𝓝 0)
⊢ (fun n => ∑ i ∈ range n, f i) =o[atTop] fun n => ↑n

Tactic:
have := ((isLittleO_one_iff ℝ).2 h).sum_range fun i => zero_le_one

Result:
α : Type u_1
inst✝ : NormedAddCommGroup α
f : ℕ → α
h : Tendsto f atTop (𝓝 0)
this :
  Tendsto (fun n => ∑ i ∈ range n, 1) atTop atTop → (fun n => ∑ i ∈ range n, f i) =o[atTop] fun n => ∑ i ∈ range n, 1
⊢ (fun n => ∑ i ∈ range n, f i) =o[atTop] fun n => ↑n

Proof state:
α : Type u_1
inst✝ : NormedAddCommGroup α
f : ℕ → α
h : Tendsto f atTop (𝓝 0)
this : Tendsto (fun n => ↑n) atTop atTop → (fun n => ∑ i ∈ range n, f i) =o[atTop] fun n => ↑n
⊢ (fun n => ∑ i ∈ range n, f i) =o[atTop] fun n => ↑n

Tactic:
exact this tendsto_natCast_atTop_atTop

Result:
no goals

Proof state:
α : Type u_1
inst✝ : NormedAddCommGroup α
f : ℕ → α
h : Tendsto f atTop (𝓝 0)
this :
  Tendsto (fun n => ∑ i ∈ range n, 1) atTop atTop → (fun n => ∑ i ∈ range n, f i) =o[atTop] fun n => ∑ i ∈ range n, 1
⊢ (fun n => ∑ i ∈ range n, f i) =o[atTop] fun n => ↑n

Tactic:
simp only [sum_const, card_range, Nat.smul_one_eq_cast] at this

Result:
α : Type u_1
inst✝ : NormedAddCommGroup α
f : ℕ → α
h : Tendsto f atTop (𝓝 0)
this : Tendsto (fun n => ↑n) atTop atTop → (fun n => ∑ i ∈ range n, f i) =o[atTop] fun n => ↑n
⊢ (fun n => ∑ i ∈ range n, f i) =o[atTop] fun n => ↑n