harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Analysis/Calculus/FDeriv/Add.lean
theorem fderivWithin_add_const (c : F) :
    fderivWithin 𝕜 (fun y => f y + c) s x = fderivWithin 𝕜 f s x

Proof state:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
x : E
s : Set E
c : F
⊢ fderivWithin 𝕜 (fun y => f y + c) s x = fderivWithin 𝕜 f s x

Tactic:
simp [fderivWithin]

Result:
no goals

Proof state:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
x : E
s : Set E
c : F
⊢ fderivWithin 𝕜 (fun y => f y + c) s x = fderivWithin 𝕜 f s x

Tactic:
classical simp [fderivWithin]

Result:
no goals
-- Mathlib/RingTheory/Adjoin/Field.lean
theorem minpoly_algebraMap_sub_splits [Algebra K L] {x : L} (r : K)
    (g : (minpoly K x).Splits (algebraMap K L)) :
    (minpoly K (algebraMap K L r - x)).Splits (algebraMap K L)

Proof state:
K : Type u_2
L : Type u_3
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
x : L
r : K
g : Splits (algebraMap K L) (minpoly K x)
⊢ Splits (algebraMap K L) (minpoly K ((algebraMap K L) r - x))

Tactic:
simpa only [neg_sub] using minpoly_neg_splits (minpoly_sub_algebraMap_splits r g)

Result:
no goals
-- Mathlib/Data/Finset/Fold.lean
theorem fold_max_le : s.fold max b f ≤ c ↔ b ≤ c ∧ ∀ x ∈ s, f x ≤ c

Proof state:
α : Type u_1
β : Type u_2
f : α → β
b : β
s : Finset α
inst✝ : LinearOrder β
c : β
⊢ fold max b f s ≤ c ↔ b ≤ c ∧ ∀ x ∈ s, f x ≤ c

Tactic:
show _ ≥ _ ↔ _

Result:
α : Type u_1
β : Type u_2
f : α → β
b : β
s : Finset α
inst✝ : LinearOrder β
c : β
⊢ c ≥ fold max b f s ↔ b ≤ c ∧ ∀ x ∈ s, f x ≤ c

Proof state:
case hr
α : Type u_1
β : Type u_2
f : α → β
b : β
s : Finset α
inst✝ : LinearOrder β
c : β
⊢ ∀ {x y z : β}, x ≥ y ⊔ z ↔ x ≥ y ∧ x ≥ z

Tactic:
intro x y z

Result:
case hr
α : Type u_1
β : Type u_2
f : α → β
b : β
s : Finset α
inst✝ : LinearOrder β
c x y z : β
⊢ x ≥ y ⊔ z ↔ x ≥ y ∧ x ≥ z

Proof state:
case hr
α : Type u_1
β : Type u_2
f : α → β
b : β
s : Finset α
inst✝ : LinearOrder β
c x y z : β
⊢ y ⊔ z ≤ x ↔ x ≥ y ∧ x ≥ z

Tactic:
exact max_le_iff

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
f : α → β
b : β
s : Finset α
inst✝ : LinearOrder β
c : β
⊢ c ≥ fold max b f s ↔ b ≤ c ∧ ∀ x ∈ s, f x ≤ c

Tactic:
apply fold_op_rel_iff_and

Result:
case hr
α : Type u_1
β : Type u_2
f : α → β
b : β
s : Finset α
inst✝ : LinearOrder β
c : β
⊢ ∀ {x y z : β}, x ≥ y ⊔ z ↔ x ≥ y ∧ x ≥ z

Proof state:
case hr
α : Type u_1
β : Type u_2
f : α → β
b : β
s : Finset α
inst✝ : LinearOrder β
c x y z : β
⊢ x ≥ y ⊔ z ↔ x ≥ y ∧ x ≥ z

Tactic:
show _ ≤ _ ↔ _

Result:
case hr
α : Type u_1
β : Type u_2
f : α → β
b : β
s : Finset α
inst✝ : LinearOrder β
c x y z : β
⊢ y ⊔ z ≤ x ↔ x ≥ y ∧ x ≥ z
-- Mathlib/Analysis/Analytic/OfScalars.lean
theorem ofScalarsSum_unop [T2Space E] (x : Eᵐᵒᵖ) :
    ofScalarsSum c (MulOpposite.unop x) = MulOpposite.unop (ofScalarsSum c x)

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝⁵ : Field 𝕜
inst✝⁴ : Ring E
inst✝³ : Algebra 𝕜 E
inst✝² : TopologicalSpace E
inst✝¹ : IsTopologicalRing E
c : ℕ → 𝕜
inst✝ : T2Space E
x : Eᵐᵒᵖ
⊢ ofScalarsSum c (MulOpposite.unop x) = MulOpposite.unop (ofScalarsSum c x)

Tactic:
simp [ofScalars, ofScalars_sum_eq, ← MulOpposite.unop_pow, ← MulOpposite.unop_smul, tsum_unop]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/FinRange.lean
theorem finRange_succ (n) : finRange (n+1) = 0 :: (finRange n).map Fin.succ

Proof state:
case h
n : Nat
⊢ ∀ (i : Nat) (h₁ : i < (finRange (n + 1)).length) (h₂ : i < (0 :: map Fin.succ (finRange n)).length),
    (finRange (n + 1))[i] = (0 :: map Fin.succ (finRange n))[i]

Tactic:
intro i

Result:
case h
n i : Nat
⊢ ∀ (h₁ : i < (finRange (n + 1)).length) (h₂ : i < (0 :: map Fin.succ (finRange n)).length),
    (finRange (n + 1))[i] = (0 :: map Fin.succ (finRange n))[i]

Proof state:
case hl
n : Nat
⊢ (finRange (n + 1)).length = (0 :: map Fin.succ (finRange n)).length

case h
n : Nat
⊢ ∀ (i : Nat) (h₁ : i < (finRange (n + 1)).length) (h₂ : i < (0 :: map Fin.succ (finRange n)).length),
    (finRange (n + 1))[i] = (0 :: map Fin.succ (finRange n))[i]

Tactic:
simp

Result:
case h
n : Nat
⊢ ∀ (i : Nat) (h₁ : i < (finRange (n + 1)).length) (h₂ : i < (0 :: map Fin.succ (finRange n)).length),
    (finRange (n + 1))[i] = (0 :: map Fin.succ (finRange n))[i]

Proof state:
n : Nat
⊢ finRange (n + 1) = 0 :: map Fin.succ (finRange n)

Tactic:
apply List.ext_getElem

Result:
case hl
n : Nat
⊢ (finRange (n + 1)).length = (0 :: map Fin.succ (finRange n)).length

case h
n : Nat
⊢ ∀ (i : Nat) (h₁ : i < (finRange (n + 1)).length) (h₂ : i < (0 :: map Fin.succ (finRange n)).length),
    (finRange (n + 1))[i] = (0 :: map Fin.succ (finRange n))[i]

Proof state:
case h
n i : Nat
⊢ ∀ (h₁ : i < (finRange (n + 1)).length) (h₂ : i < (0 :: map Fin.succ (finRange n)).length),
    (finRange (n + 1))[i] = (0 :: map Fin.succ (finRange n))[i]

Tactic:
cases i <;> simp

Result:
no goals
-- Mathlib/Analysis/Normed/Group/Basic.lean
theorem preimage_mul_closedBall (a b : E) (r : ℝ) :
    (b * ·) ⁻¹' closedBall a r = closedBall (a / b) r

Proof state:
E : Type u_5
inst✝ : SeminormedCommGroup E
a b : E
r : ℝ
⊢ (fun x => b * x) ⁻¹' closedBall a r = closedBall (a / b) r

Tactic:
ext c

Result:
case h
E : Type u_5
inst✝ : SeminormedCommGroup E
a b : E
r : ℝ
c : E
⊢ c ∈ (fun x => b * x) ⁻¹' closedBall a r ↔ c ∈ closedBall (a / b) r

Proof state:
case h
E : Type u_5
inst✝ : SeminormedCommGroup E
a b : E
r : ℝ
c : E
⊢ c ∈ (fun x => b * x) ⁻¹' closedBall a r ↔ c ∈ closedBall (a / b) r

Tactic:
simp only [dist_eq_norm_div, Set.mem_preimage, mem_closedBall, div_div_eq_mul_div, mul_comm]

Result:
no goals
-- Mathlib/Data/Nat/Init.lean
lemma strongRecOn'_beta {P : ℕ → Sort*} {h} :
    (strongRecOn' n h : P n) = h n fun m _ ↦ (strongRecOn' m h : P m)

Proof state:
n : ℕ
P : ℕ → Sort u_1
h : (n : ℕ) → ((m : ℕ) → m < n → P m) → P n
⊢ n.strongRecOn' h = h n fun m x => m.strongRecOn' h

Tactic:
simp only [strongRecOn']

Result:
n : ℕ
P : ℕ → Sort u_1
h : (n : ℕ) → ((m : ℕ) → m < n → P m) → P n
⊢ Nat.strongRec' h n = h n fun m x => Nat.strongRec' h m

Proof state:
n : ℕ
P : ℕ → Sort u_1
h : (n : ℕ) → ((m : ℕ) → m < n → P m) → P n
⊢ Nat.strongRec' h n = h n fun m x => Nat.strongRec' h m

Tactic:
rw [Nat.strongRec']

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Pow/NNReal.lean
theorem _root_.Real.list_prod_map_rpow (l : List ℝ) (hl : ∀ x ∈ l, (0 : ℝ) ≤ x) (r : ℝ) :
    (l.map (· ^ r)).prod = l.prod ^ r

Proof state:
case intro
r : ℝ
l : List ℝ≥0
⊢ (List.map (fun x => x ^ r) (List.map toReal l)).prod = (List.map toReal l).prod ^ r

Tactic:
have := congr_arg ((↑) : ℝ≥0 → ℝ) (NNReal.list_prod_map_rpow l r)

Result:
case intro
r : ℝ
l : List ℝ≥0
this : ↑(List.map (fun x => x ^ r) l).prod = ↑(l.prod ^ r)
⊢ (List.map (fun x => x ^ r) (List.map toReal l)).prod = (List.map toReal l).prod ^ r

Proof state:
l : List ℝ
hl : ∀ x ∈ l, 0 ≤ x
r : ℝ
⊢ (List.map (fun x => x ^ r) l).prod = l.prod ^ r

Tactic:
lift l to List ℝ≥0 using hl

Result:
case intro
r : ℝ
l : List ℝ≥0
⊢ (List.map (fun x => x ^ r) (List.map toReal l)).prod = (List.map toReal l).prod ^ r

Proof state:
case intro
r : ℝ
l : List ℝ≥0
this : ↑(List.map (fun x => x ^ r) l).prod = ↑(l.prod ^ r)
⊢ (List.map (fun x => x ^ r) (List.map toReal l)).prod = (List.map toReal l).prod ^ r

Tactic:
push_cast at this

Result:
case intro
r : ℝ
l : List ℝ≥0
this : (List.map toReal (List.map (fun x => x ^ r) l)).prod = (List.map toReal l).prod ^ r
⊢ (List.map (fun x => x ^ r) (List.map toReal l)).prod = (List.map toReal l).prod ^ r

Proof state:
case intro
r : ℝ
l : List ℝ≥0
this : (List.map toReal (List.map (fun x => x ^ r) l)).prod = (List.map toReal l).prod ^ r
⊢ (List.map (fun x => x ^ r) (List.map toReal l)).prod = (List.map toReal l).prod ^ r

Tactic:
rw [List.map_map] at this ⊢

Result:
case intro
r : ℝ
l : List ℝ≥0
this : (List.map (toReal ∘ fun x => x ^ r) l).prod = (List.map toReal l).prod ^ r
⊢ (List.map ((fun x => x ^ r) ∘ toReal) l).prod = (List.map toReal l).prod ^ r

Proof state:
case intro
r : ℝ
l : List ℝ≥0
this : (List.map (toReal ∘ fun x => x ^ r) l).prod = (List.map toReal l).prod ^ r
⊢ (List.map ((fun x => x ^ r) ∘ toReal) l).prod = (List.map toReal l).prod ^ r

Tactic:
exact mod_cast this

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Sublist.lean
theorem isSuffixOf_iff_suffix [BEq α] [LawfulBEq α] {l₁ l₂ : List α} :
    l₁.isSuffixOf l₂ ↔ l₁ <:+ l₂

Proof state:
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
l₁ l₂ : List α
⊢ l₁.isSuffixOf l₂ = true ↔ l₁ <:+ l₂

Tactic:
simp [isSuffixOf]

Result:
no goals
-- Mathlib/Analysis/Calculus/Deriv/Add.lean
theorem HasDerivAtFilter.neg (h : HasDerivAtFilter f f' x L) :
    HasDerivAtFilter (fun x => -f x) (-f') x L

Proof state:
𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : 𝕜 → F
f' : F
x : 𝕜
L : Filter 𝕜
h : HasDerivAtFilter f f' x L
⊢ HasDerivAtFilter (fun x => -f x) (-f') x L

Tactic:
simpa using h.neg.hasDerivAtFilter

Result:
no goals
-- Mathlib/Data/Finset/Image.lean
theorem range_sdiff_zero {n : ℕ} : range (n + 1) \ {0} = (range n).image Nat.succ

Proof state:
case zero

⊢ range (0 + 1) \ {0} = image Nat.succ (range 0)

Tactic:
simp

Result:
no goals

Proof state:
case succ.h
k : ℕ
hk : range (k + 1) \ {0} = image Nat.succ (range k)
⊢ k + 1 ∉ {0}

Tactic:
simp

Result:
no goals

Proof state:
n : ℕ
⊢ range (n + 1) \ {0} = image Nat.succ (range n)

Tactic:
induction' n with k hk

Result:
case zero

⊢ range (0 + 1) \ {0} = image Nat.succ (range 0)

case succ
k : ℕ
hk : range (k + 1) \ {0} = image Nat.succ (range k)
⊢ range (k + 1 + 1) \ {0} = image Nat.succ (range (k + 1))

Proof state:
case succ
k : ℕ
hk : range (k + 1) \ {0} = image Nat.succ (range k)
⊢ range (k + 1 + 1) \ {0} = image Nat.succ (range (k + 1))

Tactic:
conv_rhs => rw [range_succ]

Result:
case succ
k : ℕ
hk : range (k + 1) \ {0} = image Nat.succ (range k)
⊢ range (k + 1 + 1) \ {0} = image Nat.succ (insert k (range k))

Proof state:
case succ
k : ℕ
hk : range (k + 1) \ {0} = image Nat.succ (range k)
⊢ range (k + 1 + 1) \ {0} = image Nat.succ (insert k (range k))

Tactic:
rw [range_succ, image_insert, ← hk, insert_sdiff_of_not_mem]

Result:
case succ.h
k : ℕ
hk : range (k + 1) \ {0} = image Nat.succ (range k)
⊢ k + 1 ∉ {0}
-- Mathlib/Algebra/Homology/Embedding/StupidTrunc.lean
@[simp]
lemma stupidTruncMap_id : stupidTruncMap (𝟙 K) e = 𝟙 _

Proof state:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst✝³ : Category.{u_4, u_3} C
inst✝² : HasZeroMorphisms C
inst✝¹ : HasZeroObject C
K : HomologicalComplex C c'
e : c.Embedding c'
inst✝ : e.IsRelIff
⊢ stupidTruncMap (𝟙 K) e = 𝟙 (K.stupidTrunc e)

Tactic:
simp [stupidTruncMap, stupidTrunc]

Result:
no goals
-- Mathlib/CategoryTheory/GradedObject.lean
@[ext]
lemma hom_ext {β : Type*} {X Y : GradedObject β C} (f g : X ⟶ Y) (h : ∀ x, f x = g x) : f = g

Proof state:
case h
C : Type u
inst✝ : Category.{v, u} C
β : Type u_1
X Y : GradedObject β C
f g : X ⟶ Y
h : ∀ (x : β), f x = g x
x✝ : β
⊢ f x✝ = g x✝

Tactic:
apply h

Result:
no goals

Proof state:
C : Type u
inst✝ : Category.{v, u} C
β : Type u_1
X Y : GradedObject β C
f g : X ⟶ Y
h : ∀ (x : β), f x = g x
⊢ f = g

Tactic:
funext

Result:
case h
C : Type u
inst✝ : Category.{v, u} C
β : Type u_1
X Y : GradedObject β C
f g : X ⟶ Y
h : ∀ (x : β), f x = g x
x✝ : β
⊢ f x✝ = g x✝
-- Mathlib/Algebra/Ring/Hom/Defs.lean
theorem zero_comp (f : α →ₙ+* β) : (0 : β →ₙ+* γ).comp f = 0

Proof state:
case a
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : NonUnitalNonAssocSemiring α
inst✝¹ : NonUnitalNonAssocSemiring β
inst✝ : NonUnitalNonAssocSemiring γ
f : α →ₙ+* β
x✝ : α
⊢ (comp 0 f) x✝ = 0 x✝

Tactic:
rfl

Result:
no goals

Proof state:
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : NonUnitalNonAssocSemiring α
inst✝¹ : NonUnitalNonAssocSemiring β
inst✝ : NonUnitalNonAssocSemiring γ
f : α →ₙ+* β
⊢ comp 0 f = 0

Tactic:
ext

Result:
case a
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : NonUnitalNonAssocSemiring α
inst✝¹ : NonUnitalNonAssocSemiring β
inst✝ : NonUnitalNonAssocSemiring γ
f : α →ₙ+* β
x✝ : α
⊢ (comp 0 f) x✝ = 0 x✝
-- Mathlib/Order/Filter/Lift.lean
theorem lift_neBot_iff (hm : Monotone g) : (NeBot (f.lift g)) ↔ ∀ s ∈ f, NeBot (g s)

Proof state:
α : Type u_1
β : Type u_2
f : Filter α
g : Set α → Filter β
hm : Monotone g
⊢ (f.lift g).NeBot ↔ ∀ s ∈ f, (g s).NeBot

Tactic:
simp only [neBot_iff, Ne, ← empty_mem_iff_bot, mem_lift_sets hm, not_exists, not_and]

Result:
no goals
-- Mathlib/Algebra/Order/Field/Basic.lean
theorem inv_antitoneOn_Icc_right (ha : 0 < a) :
    AntitoneOn (fun x : α ↦ x⁻¹) (Set.Icc a b)

Proof state:
α : Type u_2
inst✝ : LinearOrderedField α
a b : α
ha : 0 < a
⊢ AntitoneOn (fun x => x⁻¹) (Set.Icc a b)

Tactic:
convert sub_inv_antitoneOn_Icc_right ha

Result:
case h.e'_5.h.h.e'_3
α : Type u_2
inst✝ : LinearOrderedField α
a b : α
ha : 0 < a
x✝ : α
⊢ x✝ = x✝ - 0

Proof state:
case h.e'_5.h.h.e'_3
α : Type u_2
inst✝ : LinearOrderedField α
a b : α
ha : 0 < a
x✝ : α
⊢ x✝ = x✝ - 0

Tactic:
exact (sub_zero _).symm

Result:
no goals
-- Mathlib/Data/Nat/PartENat.lean
theorem get_le_get {x y : PartENat} {hx : x.Dom} {hy : y.Dom} : x.get hx ≤ y.get hy ↔ x ≤ y

Proof state:
x y : PartENat
hx : x.Dom
hy : y.Dom
⊢ x.get hx ≤ y.get hy ↔ x ≤ y

Tactic:
conv =>
  lhs
  rw [← coe_le_coe, natCast_get, natCast_get]

Result:
no goals
-- Mathlib/LinearAlgebra/Ray.lean
theorem neg_units_smul (u : Rˣ) (v : Module.Ray R M) : -u • v = -(u • v)

Proof state:
case h
R : Type u_1
inst✝² : StrictOrderedCommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
u : Rˣ
v✝ : M
hv✝ : v✝ ≠ 0
⊢ -u • rayOfNeZero R v✝ hv✝ = -(u • rayOfNeZero R v✝ hv✝)

Tactic:
simp only [smul_rayOfNeZero, Units.smul_def, Units.val_neg, neg_smul, neg_rayOfNeZero]

Result:
no goals

Proof state:
R : Type u_1
inst✝² : StrictOrderedCommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
u : Rˣ
v : Ray R M
⊢ -u • v = -(u • v)

Tactic:
induction v using Module.Ray.ind

Result:
case h
R : Type u_1
inst✝² : StrictOrderedCommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
u : Rˣ
v✝ : M
hv✝ : v✝ ≠ 0
⊢ -u • rayOfNeZero R v✝ hv✝ = -(u • rayOfNeZero R v✝ hv✝)
-- Mathlib/Algebra/Polynomial/GroupRingAction.lean
theorem eval_smul' [MulSemiringAction G S] (g : G) (f : S[X]) (x : S) :
    f.eval (g • x) = g • (g⁻¹ • f).eval x

Proof state:
S : Type u_3
inst✝² : CommSemiring S
G : Type u_4
inst✝¹ : Group G
inst✝ : MulSemiringAction G S
g : G
f : S[X]
x : S
⊢ eval (g • x) f = g • eval x (g⁻¹ • f)

Tactic:
rw [← smul_eval_smul, smul_inv_smul]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Log/Basic.lean
theorem log_mul (hx : x ≠ 0) (hy : y ≠ 0) : log (x * y) = log x + log y :=
  exp_injective <| by
    rw [exp_log_eq_abs (mul_ne_zero hx hy), exp_add, exp_log_eq_abs hx, exp_log_eq_abs hy, abs_mul]

Proof state:
x y : ℝ
hx : x ≠ 0
hy : y ≠ 0
⊢ rexp (log (x * y)) = rexp (log x + log y)

Tactic:
rw [exp_log_eq_abs (mul_ne_zero hx hy), exp_add, exp_log_eq_abs hx, exp_log_eq_abs hy, abs_mul]

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Operations.lean
/-- There is never an `s-t` edge in `G.replaceVertex s t`. -/
lemma not_adj_replaceVertex_same : ¬(G.replaceVertex s t).Adj s t

Proof state:
V : Type u_1
G : SimpleGraph V
s t : V
inst✝ : DecidableEq V
⊢ ¬(G.replaceVertex s t).Adj s t

Tactic:
simp [replaceVertex]

Result:
no goals
-- Mathlib/LinearAlgebra/Projectivization/Cardinality.lean
/-- Cardinality formula for the points of `ℙ k V` if `k` and `V` are finite expressed
as a fraction. -/
lemma card'' [Finite k] : Nat.card (ℙ k V) = (Nat.card V - 1) / (Nat.card k - 1)

Proof state:
case H
k : Type u_1
V : Type u_2
inst✝³ : Field k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : Finite k
this : 1 < Nat.card k
⊢ 0 < Nat.card k - 1

Tactic:
omega

Result:
no goals

Proof state:
k : Type u_1
V : Type u_2
inst✝³ : Field k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : Finite k
this : 1 < Nat.card k
⊢ Nat.card (ℙ k V) = (Nat.card V - 1) / (Nat.card k - 1)

Tactic:
rw [card k, Nat.mul_div_cancel]

Result:
case H
k : Type u_1
V : Type u_2
inst✝³ : Field k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : Finite k
this : 1 < Nat.card k
⊢ 0 < Nat.card k - 1

Proof state:
k : Type u_1
V : Type u_2
inst✝³ : Field k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : Finite k
⊢ Nat.card (ℙ k V) = (Nat.card V - 1) / (Nat.card k - 1)

Tactic:
have : 1 < Nat.card k := Finite.one_lt_card

Result:
k : Type u_1
V : Type u_2
inst✝³ : Field k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : Finite k
this : 1 < Nat.card k
⊢ Nat.card (ℙ k V) = (Nat.card V - 1) / (Nat.card k - 1)
-- Mathlib/Data/List/Chain.lean
theorem chain_iff_forall₂ :
    ∀ {a : α} {l : List α}, Chain R a l ↔ l = [] ∨ Forall₂ R (a :: dropLast l) l
  | a, [] => by simp
  | a, b :: l => by
    by_cases h : l = [] <;>
    simp [@chain_iff_forall₂ b l, dropLast, *]

Proof state:
α : Type u
R : α → α → Prop
a : α
⊢ Chain R a [] ↔ [] = [] ∨ Forall₂ R (a :: [].dropLast) []

Tactic:
simp

Result:
no goals

Proof state:
α : Type u
R : α → α → Prop
a b : α
l : List α
⊢ Chain R a (b :: l) ↔ b :: l = [] ∨ Forall₂ R (a :: (b :: l).dropLast) (b :: l)

Tactic:
by_cases h : l = [] <;>
simp [@chain_iff_forall₂ b l, dropLast, *]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Int/Lemmas.lean
theorem eq_one_of_mul_eq_self_left {a b : Int} (Hpos : a ≠ 0) (H : b * a = a) : b = 1 :=
  Int.eq_of_mul_eq_mul_right Hpos <| by rw [Int.one_mul, H]

Proof state:
a b : Int
Hpos : a ≠ 0
H : b * a = a
⊢ b * a = 1 * a

Tactic:
rw [Int.one_mul, H]

Result:
no goals
-- Mathlib/Geometry/Euclidean/Angle/Oriented/RightAngle.lean
theorem cos_oangle_add_right_of_oangle_eq_pi_div_two {x y : V} (h : o.oangle x y = ↑(π / 2)) :
    Real.Angle.cos (o.oangle x (x + y)) = ‖x‖ / ‖x + y‖

Proof state:
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
hd2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
h : o.oangle x y = ↑(π / 2)
⊢ (o.oangle x (x + y)).cos = ‖x‖ / ‖x + y‖

Tactic:
have hs : (o.oangle x (x + y)).sign = 1 := by
  rw [oangle_sign_add_right, h, Real.Angle.sign_coe_pi_div_two]

Result:
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
hd2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
h : o.oangle x y = ↑(π / 2)
hs : (o.oangle x (x + y)).sign = 1
⊢ (o.oangle x (x + y)).cos = ‖x‖ / ‖x + y‖

Proof state:
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
hd2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
h : o.oangle x y = ↑(π / 2)
hs : (o.oangle x (x + y)).sign = 1
⊢ (o.oangle x (x + y)).cos = ‖x‖ / ‖x + y‖

Tactic:
rw [o.oangle_eq_angle_of_sign_eq_one hs, Real.Angle.cos_coe,
  InnerProductGeometry.cos_angle_add_of_inner_eq_zero (o.inner_eq_zero_of_oangle_eq_pi_div_two h)]

Result:
no goals

Proof state:
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
hd2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
h : o.oangle x y = ↑(π / 2)
⊢ (o.oangle x (x + y)).sign = 1

Tactic:
rw [oangle_sign_add_right, h, Real.Angle.sign_coe_pi_div_two]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/RawLemmas.lean
theorem isEmpty_ofList [EquivBEq α] [LawfulHashable α]
    {l : List (α × β)} :
    (ofList l).isEmpty = l.isEmpty

Proof state:
α : Type u
inst✝³ : BEq α
inst✝² : Hashable α
β : Type v
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
l : List (α × β)
⊢ (ofList l).isEmpty = l.isEmpty

Tactic:
simp_to_raw using Raw₀.Const.isEmpty_insertMany_empty_list

Result:
no goals
-- Mathlib/Algebra/MvPolynomial/Equiv.lean
lemma isEmptyRingEquiv_eq_coeff_zero {σ R : Type*} [CommSemiring R] [IsEmpty σ] {x} :
    isEmptyRingEquiv R σ x = x.coeff 0

Proof state:
case intro
σ : Type u_2
R : Type u_3
inst✝¹ : CommSemiring R
inst✝ : IsEmpty σ
x : R
⊢ (isEmptyRingEquiv R σ) ((isEmptyRingEquiv R σ).symm x) = coeff 0 ((isEmptyRingEquiv R σ).symm x)

Tactic:
simp

Result:
no goals

Proof state:
σ : Type u_2
R : Type u_3
inst✝¹ : CommSemiring R
inst✝ : IsEmpty σ
x : MvPolynomial σ R
⊢ (isEmptyRingEquiv R σ) x = coeff 0 x

Tactic:
obtain ⟨x, rfl⟩ := (isEmptyRingEquiv R σ).symm.surjective x

Result:
case intro
σ : Type u_2
R : Type u_3
inst✝¹ : CommSemiring R
inst✝ : IsEmpty σ
x : R
⊢ (isEmptyRingEquiv R σ) ((isEmptyRingEquiv R σ).symm x) = coeff 0 ((isEmptyRingEquiv R σ).symm x)
-- Mathlib/Data/ENNReal/Basic.lean
theorem ofReal_one : ENNReal.ofReal (1 : ℝ) = (1 : ℝ≥0∞)

Proof state:
⊢ ENNReal.ofReal 1 = 1

Tactic:
simp [ENNReal.ofReal]

Result:
no goals
-- Mathlib/Computability/Reduce.lean
theorem le_refl (d : ManyOneDegree) : d ≤ d

Proof state:
d : ManyOneDegree
⊢ d ≤ d

Tactic:
induction d using ManyOneDegree.ind_on

Result:
case h
p✝ : Set ℕ
⊢ of p✝ ≤ of p✝

Proof state:
case h
p✝ : Set ℕ
⊢ p✝ ≤₀ p✝

Tactic:
rfl

Result:
no goals

Proof state:
case h
p✝ : Set ℕ
⊢ of p✝ ≤ of p✝

Tactic:
simp

Result:
case h
p✝ : Set ℕ
⊢ p✝ ≤₀ p✝
-- Mathlib/Topology/Basic.lean
theorem frontier_eq_inter_compl_interior :
    frontier s = (interior s)ᶜ ∩ (interior sᶜ)ᶜ

Proof state:
X : Type u
s : Set X
inst✝ : TopologicalSpace X
⊢ frontier s = (interior s)ᶜ ∩ (interior sᶜ)ᶜ

Tactic:
rw [← frontier_compl, ← closure_compl, ← diff_eq, closure_diff_interior]

Result:
no goals
-- Mathlib/Algebra/Algebra/Spectrum.lean
theorem mem_resolventSet_apply (φ : F) {a : A} {r : R} (h : r ∈ resolventSet R a) :
    r ∈ resolventSet R ((φ : A → B) a)

Proof state:
F : Type u_1
R : Type u_2
A : Type u_3
B : Type u_4
inst✝⁶ : CommSemiring R
inst✝⁵ : Ring A
inst✝⁴ : Algebra R A
inst✝³ : Ring B
inst✝² : Algebra R B
inst✝¹ : FunLike F A B
inst✝ : AlgHomClass F R A B
φ : F
a : A
r : R
h : r ∈ resolventSet R a
⊢ r ∈ resolventSet R (φ a)

Tactic:
simpa only [map_sub, AlgHomClass.commutes] using h.map φ

Result:
no goals
-- Mathlib/LinearAlgebra/Matrix/Charpoly/Coeff.lean
@[simp] lemma coeff_charpolyRev_eq_neg_trace (M : Matrix n n R) :
    coeff M.charpolyRev 1 = - trace M

Proof state:
case inl
R : Type u
inst✝² : CommRing R
n : Type v
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : Matrix n n R
a✝ : Nontrivial R
h✝ : IsEmpty n
⊢ M.charpolyRev.coeff 1 = -M.trace

Tactic:
simp [charpolyRev, coeff_one]

Result:
no goals

Proof state:
case inr
R : Type u
inst✝² : CommRing R
n : Type v
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : Matrix n n R
a✝ : Nontrivial R
h✝ : Nonempty n
⊢ M.charpolyRev.coeff 1 = -M.trace

Tactic:
simp [trace_eq_neg_charpoly_coeff M, ← M.reverse_charpoly, nextCoeff]

Result:
no goals

Proof state:
R : Type u
inst✝² : CommRing R
n : Type v
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : Matrix n n R
⊢ M.charpolyRev.coeff 1 = -M.trace

Tactic:
nontriviality R

Result:
R : Type u
inst✝² : CommRing R
n : Type v
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : Matrix n n R
a✝ : Nontrivial R
⊢ M.charpolyRev.coeff 1 = -M.trace

Proof state:
R : Type u
inst✝² : CommRing R
n : Type v
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : Matrix n n R
a✝ : Nontrivial R
⊢ M.charpolyRev.coeff 1 = -M.trace

Tactic:
cases isEmpty_or_nonempty n

Result:
case inl
R : Type u
inst✝² : CommRing R
n : Type v
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : Matrix n n R
a✝ : Nontrivial R
h✝ : IsEmpty n
⊢ M.charpolyRev.coeff 1 = -M.trace

case inr
R : Type u
inst✝² : CommRing R
n : Type v
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : Matrix n n R
a✝ : Nontrivial R
h✝ : Nonempty n
⊢ M.charpolyRev.coeff 1 = -M.trace
-- Mathlib/NumberTheory/LucasLehmer.lean
theorem card_eq : Fintype.card (X q) = q ^ 2

Proof state:
q : ℕ+
⊢ Fintype.card (ZMod ↑q × ZMod ↑q) = ↑q ^ 2

Tactic:
rw [Fintype.card_prod, ZMod.card q, sq]

Result:
no goals

Proof state:
q : ℕ+
⊢ Fintype.card (X q) = ↑q ^ 2

Tactic:
dsimp [X]

Result:
q : ℕ+
⊢ Fintype.card (ZMod ↑q × ZMod ↑q) = ↑q ^ 2
-- Mathlib/Data/Set/Lattice.lean
theorem image_iUnion₂ (f : α → β) (s : ∀ i, κ i → Set α) :
    (f '' ⋃ (i) (j), s i j) = ⋃ (i) (j), f '' s i j

Proof state:
α : Type u_1
β : Type u_2
ι : Sort u_5
κ : ι → Sort u_8
f : α → β
s : (i : ι) → κ i → Set α
⊢ f '' ⋃ i, ⋃ j, s i j = ⋃ i, ⋃ j, f '' s i j

Tactic:
simp_rw [image_iUnion]

Result:
no goals