harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/FieldTheory/KummerExtension.lean
lemma autEquivZmod_symm_apply_natCast [NeZero n] {ζ : K} (hζ : IsPrimitiveRoot ζ n) (m : ℕ) :
    (autEquivZmod H L hζ).symm (Multiplicative.ofAdd (m : ZMod n)) α = ζ ^ m • α

Proof state:
K : Type u
inst✝⁴ : Field K
n : ℕ
a : K
H : Irreducible (X ^ n - C a)
L : Type u_1
inst✝³ : Field L
inst✝² : Algebra K L
inst✝¹ : IsSplittingField K L (X ^ n - C a)
α : L
hα : α ^ n = (algebraMap K L) a
inst✝ : NeZero n
ζ : K
hζ : IsPrimitiveRoot ζ n
m : ℕ
⊢ ((autEquivZmod H L hζ).symm (Multiplicative.ofAdd ↑m)) α = ζ ^ m • α

Tactic:
simpa only [Int.cast_natCast, zpow_natCast] using autEquivZmod_symm_apply_intCast H L hα hζ m

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Zip.lean
theorem lt_size_left_of_zipWith {f : α → β → γ} {i : Nat} {l : Array α} {l' : Array β}
    (h : i < (zipWith f l l').size) : i < l.size

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
i : Nat
l : Array α
l' : Array β
h : i < min l.size l'.size
⊢ i < l.size

Tactic:
omega

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
i : Nat
l : Array α
l' : Array β
h : i < (zipWith f l l').size
⊢ i < l.size

Tactic:
rw [size_zipWith] at h

Result:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
i : Nat
l : Array α
l' : Array β
h : i < min l.size l'.size
⊢ i < l.size
-- Mathlib/SetTheory/Game/Basic.lean
/-- The right options of `x * y` are the left options of `x * (-y)` and of `(-x) * y` of the first
  kind, up to equivalence. -/
lemma rightMoves_mul_iff {x y : PGame} (P : Game → Prop) :
    (∀ k, P ⟦(x * y).moveRight k⟧) ↔
    (∀ i j, P (-⟦mulOption x (-y) i j⟧)) ∧ (∀ i j, P (-⟦mulOption (-x) y i j⟧))

Proof state:
case mk.mk.mp
P : Game → Prop
α✝¹ β✝¹ : Type u_1
a✝³ : α✝¹ → PGame
a✝² : β✝¹ → PGame
α✝ β✝ : Type u_1
a✝¹ : α✝ → PGame
a✝ : β✝ → PGame
h : ∀ (k : (mk α✝¹ β✝¹ a✝³ a✝² * mk α✝ β✝ a✝¹ a✝).RightMoves), P ⟦(mk α✝¹ β✝¹ a✝³ a✝² * mk α✝ β✝ a✝¹ a✝).moveRight k⟧
⊢ (∀ (i : (mk α✝¹ β✝¹ a✝³ a✝²).LeftMoves) (j : (-mk α✝ β✝ a✝¹ a✝).LeftMoves),
      P (-⟦(mk α✝¹ β✝¹ a✝³ a✝²).mulOption (-mk α✝ β✝ a✝¹ a✝) i j⟧)) ∧
    ∀ (i : (-mk α✝¹ β✝¹ a✝³ a✝²).LeftMoves) (j : (mk α✝ β✝ a✝¹ a✝).LeftMoves),
      P (-⟦(-mk α✝¹ β✝¹ a✝³ a✝²).mulOption (mk α✝ β✝ a✝¹ a✝) i j⟧)

case mk.mk.mpr
P : Game → Prop
α✝¹ β✝¹ : Type u_1
a✝³ : α✝¹ → PGame
a✝² : β✝¹ → PGame
α✝ β✝ : Type u_1
a✝¹ : α✝ → PGame
a✝ : β✝ → PGame
h :
  (∀ (i : (mk α✝¹ β✝¹ a✝³ a✝²).LeftMoves) (j : (-mk α✝ β✝ a✝¹ a✝).LeftMoves),
      P (-⟦(mk α✝¹ β✝¹ a✝³ a✝²).mulOption (-mk α✝ β✝ a✝¹ a✝) i j⟧)) ∧
    ∀ (i : (-mk α✝¹ β✝¹ a✝³ a✝²).LeftMoves) (j : (mk α✝ β✝ a✝¹ a✝).LeftMoves),
      P (-⟦(-mk α✝¹ β✝¹ a✝³ a✝²).mulOption (mk α✝ β✝ a✝¹ a✝) i j⟧)
⊢ ∀ (k : (mk α✝¹ β✝¹ a✝³ a✝² * mk α✝ β✝ a✝¹ a✝).RightMoves), P ⟦(mk α✝¹ β✝¹ a✝³ a✝² * mk α✝ β✝ a✝¹ a✝).moveRight k⟧

Tactic:
on_goal 1 =>
  constructor <;> intros i j
  on_goal 1 => convert h (Sum.inl (i, j))

Result:
case h.e'_1
P : Game → Prop
α✝¹ β✝¹ : Type u_1
a✝³ : α✝¹ → PGame
a✝² : β✝¹ → PGame
α✝ β✝ : Type u_1
a✝¹ : α✝ → PGame
a✝ : β✝ → PGame
h : ∀ (k : (mk α✝¹ β✝¹ a✝³ a✝² * mk α✝ β✝ a✝¹ a✝).RightMoves), P ⟦(mk α✝¹ β✝¹ a✝³ a✝² * mk α✝ β✝ a✝¹ a✝).moveRight k⟧
i : (mk α✝¹ β✝¹ a✝³ a✝²).LeftMoves
j : (-mk α✝ β✝ a✝¹ a✝).LeftMoves
⊢ -⟦(mk α✝¹ β✝¹ a✝³ a✝²).mulOption (-mk α✝ β✝ a✝¹ a✝) i j⟧ =
    ⟦(mk α✝¹ β✝¹ a✝³ a✝² * mk α✝ β✝ a✝¹ a✝).moveRight (Sum.inl (i, j))⟧

case mk.mk.mp.right
P : Game → Prop
α✝¹ β✝¹ : Type u_1
a✝³ : α✝¹ → PGame
a✝² : β✝¹ → PGame
α✝ β✝ : Type u_1
a✝¹ : α✝ → PGame
a✝ : β✝ → PGame
h : ∀ (k : (mk α✝¹ β✝¹ a✝³ a✝² * mk α✝ β✝ a✝¹ a✝).RightMoves), P ⟦(mk α✝¹ β✝¹ a✝³ a✝² * mk α✝ β✝ a✝¹ a✝).moveRight k⟧
i : (-mk α✝¹ β✝¹ a✝³ a✝²).LeftMoves
j : (mk α✝ β✝ a✝¹ a✝).LeftMoves
⊢ P (-⟦(-mk α✝¹ β✝¹ a✝³ a✝²).mulOption (mk α✝ β✝ a✝¹ a✝) i j⟧)

case mk.mk.mpr
P : Game → Prop
α✝¹ β✝¹ : Type u_1
a✝³ : α✝¹ → PGame
a✝² : β✝¹ → PGame
α✝ β✝ : Type u_1
a✝¹ : α✝ → PGame
a✝ : β✝ → PGame
h :
  (∀ (i : (mk α✝¹ β✝¹ a✝³ a✝²).LeftMoves) (j : (-mk α✝ β✝ a✝¹ a✝).LeftMoves),
      P (-⟦(mk α✝¹ β✝¹ a✝³ a✝²).mulOption (-mk α✝ β✝ a✝¹ a✝) i j⟧)) ∧
    ∀ (i : (-mk α✝¹ β✝¹ a✝³ a✝²).LeftMoves) (j : (mk α✝ β✝ a✝¹ a✝).LeftMoves),
      P (-⟦(-mk α✝¹ β✝¹ a✝³ a✝²).mulOption (mk α✝ β✝ a✝¹ a✝) i j⟧)
⊢ ∀ (k : (mk α✝¹ β✝¹ a✝³ a✝² * mk α✝ β✝ a✝¹ a✝).RightMoves), P ⟦(mk α✝¹ β✝¹ a✝³ a✝² * mk α✝ β✝ a✝¹ a✝).moveRight k⟧
-- Mathlib/SetTheory/Game/Basic.lean
/-- The right options of `x * y` are the left options of `x * (-y)` and of `(-x) * y` of the first
  kind, up to equivalence. -/
lemma rightMoves_mul_iff {x y : PGame} (P : Game → Prop) :
    (∀ k, P ⟦(x * y).moveRight k⟧) ↔
    (∀ i j, P (-⟦mulOption x (-y) i j⟧)) ∧ (∀ i j, P (-⟦mulOption (-x) y i j⟧))

Proof state:
case h.e'_1.e_a.e_a
P : Game → Prop
α✝¹ β✝¹ : Type u_1
a✝³ : α✝¹ → PGame
a✝² : β✝¹ → PGame
α✝ β✝ : Type u_1
a✝¹ : α✝ → PGame
a✝ : β✝ → PGame
h : ∀ (k : (mk α✝¹ β✝¹ a✝³ a✝² * mk α✝ β✝ a✝¹ a✝).RightMoves), P ⟦(mk α✝¹ β✝¹ a✝³ a✝² * mk α✝ β✝ a✝¹ a✝).moveRight k⟧
i : (mk α✝¹ β✝¹ a✝³ a✝²).LeftMoves
j : (-mk α✝ β✝ a✝¹ a✝).LeftMoves
⊢ -⟦a✝³ i * -mk α✝ β✝ a✝¹ a✝⟧ = ⟦a✝³ i * mk α✝ β✝ a✝¹ a✝⟧

case h.e'_1.e_a.e_a
P : Game → Prop
α✝¹ β✝¹ : Type u_1
a✝³ : α✝¹ → PGame
a✝² : β✝¹ → PGame
α✝ β✝ : Type u_1
a✝¹ : α✝ → PGame
a✝ : β✝ → PGame
h : ∀ (k : (mk α✝¹ β✝¹ a✝³ a✝² * mk α✝ β✝ a✝¹ a✝).RightMoves), P ⟦(mk α✝¹ β✝¹ a✝³ a✝² * mk α✝ β✝ a✝¹ a✝).moveRight k⟧
i : (mk α✝¹ β✝¹ a✝³ a✝²).LeftMoves
j : (-mk α✝ β✝ a✝¹ a✝).LeftMoves
⊢ -⟦mk α✝¹ β✝¹ a✝³ a✝² * -a✝ j⟧ = ⟦mk α✝¹ β✝¹ a✝³ a✝² * a✝ j⟧

case h.e'_1.e_a
P : Game → Prop
α✝¹ β✝¹ : Type u_1
a✝³ : α✝¹ → PGame
a✝² : β✝¹ → PGame
α✝ β✝ : Type u_1
a✝¹ : α✝ → PGame
a✝ : β✝ → PGame
h : ∀ (k : (mk α✝¹ β✝¹ a✝³ a✝² * mk α✝ β✝ a✝¹ a✝).RightMoves), P ⟦(mk α✝¹ β✝¹ a✝³ a✝² * mk α✝ β✝ a✝¹ a✝).moveRight k⟧
i : (mk α✝¹ β✝¹ a✝³ a✝²).LeftMoves
j : (-mk α✝ β✝ a✝¹ a✝).LeftMoves
⊢ -⟦a✝³ i * -a✝ j⟧ = ⟦a✝³ i * a✝ j⟧

case h.e'_1.e_a.e_a
P : Game → Prop
α✝¹ β✝¹ : Type u_1
a✝³ : α✝¹ → PGame
a✝² : β✝¹ → PGame
α✝ β✝ : Type u_1
a✝¹ : α✝ → PGame
a✝ : β✝ → PGame
h :
  (∀ (i : (mk α✝¹ β✝¹ a✝³ a✝²).LeftMoves) (j : (-mk α✝ β✝ a✝¹ a✝).LeftMoves),
      P (-⟦(mk α✝¹ β✝¹ a✝³ a✝²).mulOption (-mk α✝ β✝ a✝¹ a✝) i j⟧)) ∧
    ∀ (i : (-mk α✝¹ β✝¹ a✝³ a✝²).LeftMoves) (j : (mk α✝ β✝ a✝¹ a✝).LeftMoves),
      P (-⟦(-mk α✝¹ β✝¹ a✝³ a✝²).mulOption (mk α✝ β✝ a✝¹ a✝) i j⟧)
i : α✝¹
j : β✝
⊢ ⟦a✝³ i * mk α✝ β✝ a✝¹ a✝⟧ = -⟦a✝³ i * -mk α✝ β✝ a✝¹ a✝⟧

case h.e'_1.e_a.e_a
P : Game → Prop
α✝¹ β✝¹ : Type u_1
a✝³ : α✝¹ → PGame
a✝² : β✝¹ → PGame
α✝ β✝ : Type u_1
a✝¹ : α✝ → PGame
a✝ : β✝ → PGame
h :
  (∀ (i : (mk α✝¹ β✝¹ a✝³ a✝²).LeftMoves) (j : (-mk α✝ β✝ a✝¹ a✝).LeftMoves),
      P (-⟦(mk α✝¹ β✝¹ a✝³ a✝²).mulOption (-mk α✝ β✝ a✝¹ a✝) i j⟧)) ∧
    ∀ (i : (-mk α✝¹ β✝¹ a✝³ a✝²).LeftMoves) (j : (mk α✝ β✝ a✝¹ a✝).LeftMoves),
      P (-⟦(-mk α✝¹ β✝¹ a✝³ a✝²).mulOption (mk α✝ β✝ a✝¹ a✝) i j⟧)
i : α✝¹
j : β✝
⊢ ⟦mk α✝¹ β✝¹ a✝³ a✝² * a✝ j⟧ = -⟦mk α✝¹ β✝¹ a✝³ a✝² * -a✝ j⟧

case h.e'_1.e_a
P : Game → Prop
α✝¹ β✝¹ : Type u_1
a✝³ : α✝¹ → PGame
a✝² : β✝¹ → PGame
α✝ β✝ : Type u_1
a✝¹ : α✝ → PGame
a✝ : β✝ → PGame
h :
  (∀ (i : (mk α✝¹ β✝¹ a✝³ a✝²).LeftMoves) (j : (-mk α✝ β✝ a✝¹ a✝).LeftMoves),
      P (-⟦(mk α✝¹ β✝¹ a✝³ a✝²).mulOption (-mk α✝ β✝ a✝¹ a✝) i j⟧)) ∧
    ∀ (i : (-mk α✝¹ β✝¹ a✝³ a✝²).LeftMoves) (j : (mk α✝ β✝ a✝¹ a✝).LeftMoves),
      P (-⟦(-mk α✝¹ β✝¹ a✝³ a✝²).mulOption (mk α✝ β✝ a✝¹ a✝) i j⟧)
i : α✝¹
j : β✝
⊢ ⟦a✝³ i * a✝ j⟧ = -⟦a✝³ i * -a✝ j⟧

Tactic:
iterate 6 rw [quot_mul_neg, neg_neg]

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Clique.lean
lemma maximumIndepSet_exists [Fintype α] : ∃ (s : Finset α), G.IsMaximumIndepSet s

Proof state:
α : Type u_3
G : SimpleGraph α
inst✝ : Fintype α
⊢ ∃ s, G.IsMaximumIndepSet s

Tactic:
simp [← isMaximumClique_compl, maximumClique_exists]

Result:
no goals
-- Mathlib/Order/Interval/Set/Basic.lean
theorem Ioc_union_Ioc_union_Ioc_cycle :
    Ioc a b ∪ Ioc b c ∪ Ioc c a = Ioc (min a (min b c)) (max a (max b c))

Proof state:
α : Type u_1
inst✝ : LinearOrder α
a b c : α
⊢ Ioc a b ∪ Ioc b c ∪ Ioc c a = Ioc (a ⊓ (b ⊓ c)) (a ⊔ (b ⊔ c))

Tactic:
rw [Ioc_union_Ioc, Ioc_union_Ioc]

Result:
α : Type u_1
inst✝ : LinearOrder α
a b c : α
⊢ Ioc (a ⊓ b ⊓ c) (b ⊔ c ⊔ a) = Ioc (a ⊓ (b ⊓ c)) (a ⊔ (b ⊔ c))

case h₁
α : Type u_1
inst✝ : LinearOrder α
a b c : α
⊢ a ⊓ b ⊓ (b ⊔ c) ≤ c ⊔ a

case h₂
α : Type u_1
inst✝ : LinearOrder α
a b c : α
⊢ c ⊓ a ≤ a ⊓ b ⊔ (b ⊔ c)

case h₁
α : Type u_1
inst✝ : LinearOrder α
a b c : α
⊢ a ⊓ b ≤ b ⊔ c

case h₂
α : Type u_1
inst✝ : LinearOrder α
a b c : α
⊢ b ⊓ c ≤ a ⊔ b

Proof state:
case h₁
α : Type u_1
inst✝ : LinearOrder α
a b c : α
⊢ a ⊓ b ⊓ (b ⊔ c) ≤ c ⊔ a

case h₂
α : Type u_1
inst✝ : LinearOrder α
a b c : α
⊢ c ⊓ a ≤ a ⊓ b ⊔ (b ⊔ c)

case h₁
α : Type u_1
inst✝ : LinearOrder α
a b c : α
⊢ a ⊓ b ≤ b ⊔ c

case h₂
α : Type u_1
inst✝ : LinearOrder α
a b c : α
⊢ b ⊓ c ≤ a ⊔ b

Tactic:
all_goals
solve_by_elim (config := { maxDepth := 5 }) [min_le_of_left_le, min_le_of_right_le,
     le_max_of_le_left, le_max_of_le_right, le_refl]

Result:
no goals

Proof state:
case h₂
α : Type u_1
inst✝ : LinearOrder α
a b c : α
⊢ b ⊓ c ≤ a ⊔ b

Tactic:
solve_by_elim (config := { maxDepth := 5 }) [min_le_of_left_le, min_le_of_right_le,
     le_max_of_le_left, le_max_of_le_right, le_refl]

Result:
no goals

Proof state:
α : Type u_1
inst✝ : LinearOrder α
a b c : α
⊢ Ioc (a ⊓ b ⊓ c) (b ⊔ c ⊔ a) = Ioc (a ⊓ (b ⊓ c)) (a ⊔ (b ⊔ c))

Tactic:
ac_rfl

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Nat/TakeDrop.lean
theorem take_eq_dropLast {l : List α} {i : Nat} (h : i + 1 = l.length) :
    l.take i = l.dropLast

Proof state:
case cons.succ.nil
α : Type u_1
a : α
n✝ : Nat
ih : ∀ {i : Nat}, i + 1 = [].length → take i [] = [].dropLast
h : n✝ + 1 + 1 = [a].length
⊢ take (n✝ + 1) [a] = [a].dropLast

Tactic:
simp_all

Result:
no goals

Proof state:
case nil
α : Type u_1
i : Nat
h : i + 1 = [].length
⊢ take i [] = [].dropLast

Tactic:
simp

Result:
no goals

Proof state:
case cons.succ.cons
α : Type u_1
a : α
n✝ : Nat
b : α
bs : List α
ih : ∀ {i : Nat}, i + 1 = (b :: bs).length → take i (b :: bs) = (b :: bs).dropLast
h : n✝ + 1 + 1 = (a :: b :: bs).length
⊢ n✝ + 1 = (b :: bs).length

Tactic:
simpa using h

Result:
no goals

Proof state:
case cons.succ
α : Type u_1
a : α
as : List α
ih : ∀ {i : Nat}, i + 1 = as.length → take i as = as.dropLast
n✝ : Nat
h : n✝ + 1 + 1 = (a :: as).length
⊢ take (n✝ + 1) (a :: as) = (a :: as).dropLast

Tactic:
cases as with
| nil => simp_all
| cons b bs =>
  simp only [take_succ_cons, dropLast_cons₂]
  rw [ih]
  simpa using h

Result:
no goals

Proof state:
case cons.zero
α : Type u_1
a : α
as : List α
ih : ∀ {i : Nat}, i + 1 = as.length → take i as = as.dropLast
h : 0 + 1 = (a :: as).length
⊢ take 0 (a :: as) = (a :: as).dropLast

Tactic:
simp_all

Result:
no goals

Proof state:
case cons.succ.cons
α : Type u_1
a : α
n✝ : Nat
b : α
bs : List α
ih : ∀ {i : Nat}, i + 1 = (b :: bs).length → take i (b :: bs) = (b :: bs).dropLast
h : n✝ + 1 + 1 = (a :: b :: bs).length
⊢ take (n✝ + 1) (a :: b :: bs) = (a :: b :: bs).dropLast

Tactic:
simp only [take_succ_cons, dropLast_cons₂]

Result:
case cons.succ.cons
α : Type u_1
a : α
n✝ : Nat
b : α
bs : List α
ih : ∀ {i : Nat}, i + 1 = (b :: bs).length → take i (b :: bs) = (b :: bs).dropLast
h : n✝ + 1 + 1 = (a :: b :: bs).length
⊢ a :: take n✝ (b :: bs) = a :: (b :: bs).dropLast

Proof state:
case cons
α : Type u_1
a : α
as : List α
ih : ∀ {i : Nat}, i + 1 = as.length → take i as = as.dropLast
i : Nat
h : i + 1 = (a :: as).length
⊢ take i (a :: as) = (a :: as).dropLast

Tactic:
cases i

Result:
case cons.zero
α : Type u_1
a : α
as : List α
ih : ∀ {i : Nat}, i + 1 = as.length → take i as = as.dropLast
h : 0 + 1 = (a :: as).length
⊢ take 0 (a :: as) = (a :: as).dropLast

case cons.succ
α : Type u_1
a : α
as : List α
ih : ∀ {i : Nat}, i + 1 = as.length → take i as = as.dropLast
n✝ : Nat
h : n✝ + 1 + 1 = (a :: as).length
⊢ take (n✝ + 1) (a :: as) = (a :: as).dropLast

Proof state:
case cons.succ.cons
α : Type u_1
a : α
n✝ : Nat
b : α
bs : List α
ih : ∀ {i : Nat}, i + 1 = (b :: bs).length → take i (b :: bs) = (b :: bs).dropLast
h : n✝ + 1 + 1 = (a :: b :: bs).length
⊢ a :: take n✝ (b :: bs) = a :: (b :: bs).dropLast

Tactic:
rw [ih]

Result:
case cons.succ.cons
α : Type u_1
a : α
n✝ : Nat
b : α
bs : List α
ih : ∀ {i : Nat}, i + 1 = (b :: bs).length → take i (b :: bs) = (b :: bs).dropLast
h : n✝ + 1 + 1 = (a :: b :: bs).length
⊢ n✝ + 1 = (b :: bs).length
-- Mathlib/LinearAlgebra/Eigenspace/Semisimple.lean
lemma IsFinitelySemisimple.genEigenspace_eq_eigenspace
    (hf : f.IsFinitelySemisimple) (μ : R) {k : ℕ∞} (hk : 0 < k) :
    f.genEigenspace μ k = f.eigenspace μ

Proof state:
case refine_1
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : End R M
hf : f.IsFinitelySemisimple
μ : R
k : ℕ∞
hk : 0 < k
m : M
hm : m ∈ (f.genEigenspace μ) k
⊢ IsNilpotent (f - f)

Tactic:
simp

Result:
no goals

Proof state:
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : End R M
hf : f.IsFinitelySemisimple
μ : R
k : ℕ∞
hk : 0 < k
⊢ (f.genEigenspace μ) k = f.eigenspace μ

Tactic:
refine le_antisymm (fun m hm ↦ mem_eigenspace_iff.mpr ?_) (f.genEigenspace μ |>.mono ?_)

Result:
case refine_1
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : End R M
hf : f.IsFinitelySemisimple
μ : R
k : ℕ∞
hk : 0 < k
m : M
hm : m ∈ (f.genEigenspace μ) k
⊢ f m = μ • m

case refine_2
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : End R M
hf : f.IsFinitelySemisimple
μ : R
k : ℕ∞
hk : 0 < k
⊢ 1 ≤ k

Proof state:
case refine_1
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : End R M
hf : f.IsFinitelySemisimple
μ : R
k : ℕ∞
hk : 0 < k
m : M
hm : m ∈ (f.genEigenspace μ) k
⊢ f m = μ • m

Tactic:
apply apply_eq_of_mem_of_comm_of_isFinitelySemisimple_of_isNil hm rfl hf

Result:
case refine_1
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : End R M
hf : f.IsFinitelySemisimple
μ : R
k : ℕ∞
hk : 0 < k
m : M
hm : m ∈ (f.genEigenspace μ) k
⊢ IsNilpotent (f - f)

Proof state:
case refine_2
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : End R M
hf : f.IsFinitelySemisimple
μ : R
k : ℕ∞
hk : 0 < k
⊢ 1 ≤ k

Tactic:
exact Order.one_le_iff_pos.mpr hk

Result:
no goals
-- Mathlib/RingTheory/Polynomial/Nilpotent.lean
lemma isUnit_aeval_of_isUnit_aeval_of_isNilpotent_sub
    (hb : IsUnit (aeval b P)) (hab : IsNilpotent (a - b)) :
    IsUnit (aeval a P)

Proof state:
R : Type u_2
S : Type u_3
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
P : R[X]
a b : S
hb : IsUnit ((aeval b) P)
hab : IsNilpotent (a - b)
⊢ IsUnit ((aeval a) P)

Tactic:
rw [← add_sub_cancel (aeval b P) (aeval a P)]

Result:
R : Type u_2
S : Type u_3
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
P : R[X]
a b : S
hb : IsUnit ((aeval b) P)
hab : IsNilpotent (a - b)
⊢ IsUnit ((aeval b) P + ((aeval a) P - (aeval b) P))

Proof state:
R : Type u_2
S : Type u_3
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
P : R[X]
a b : S
hb : IsUnit ((aeval b) P)
hab : IsNilpotent (a - b)
⊢ IsUnit ((aeval b) P + ((aeval a) P - (aeval b) P))

Tactic:
refine IsNilpotent.isUnit_add_left_of_commute ?_ hb (Commute.all _ _)

Result:
R : Type u_2
S : Type u_3
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
P : R[X]
a b : S
hb : IsUnit ((aeval b) P)
hab : IsNilpotent (a - b)
⊢ IsNilpotent ((aeval a) P - (aeval b) P)

Proof state:
R : Type u_2
S : Type u_3
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
P : R[X]
a b : S
hb : IsUnit ((aeval b) P)
hab : IsNilpotent (a - b)
⊢ IsNilpotent ((aeval a) P - (aeval b) P)

Tactic:
exact isNilpotent_aeval_sub_of_isNilpotent_sub P hab

Result:
no goals
-- Mathlib/Geometry/Manifold/MFDeriv/FDeriv.lean
theorem mfderiv_eq_fderiv : mfderiv 𝓘(𝕜, E) 𝓘(𝕜, E') f x = fderiv 𝕜 f x

Proof state:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
E' : Type u_3
inst✝¹ : NormedAddCommGroup E'
inst✝ : NormedSpace 𝕜 E'
f : E → E'
x : E
⊢ mfderiv 𝓘(𝕜, E) 𝓘(𝕜, E') f x = fderiv 𝕜 f x

Tactic:
rw [← mfderivWithin_univ, ← fderivWithin_univ]

Result:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
E' : Type u_3
inst✝¹ : NormedAddCommGroup E'
inst✝ : NormedSpace 𝕜 E'
f : E → E'
x : E
⊢ mfderivWithin 𝓘(𝕜, E) 𝓘(𝕜, E') f Set.univ x = fderivWithin 𝕜 f Set.univ x

Proof state:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
E' : Type u_3
inst✝¹ : NormedAddCommGroup E'
inst✝ : NormedSpace 𝕜 E'
f : E → E'
x : E
⊢ mfderivWithin 𝓘(𝕜, E) 𝓘(𝕜, E') f Set.univ x = fderivWithin 𝕜 f Set.univ x

Tactic:
exact mfderivWithin_eq_fderivWithin

Result:
no goals
-- Mathlib/Data/BitVec.lean
@[simp] lemma ofFin_neg {x : Fin (2 ^ w)} : ofFin (-x) = -(ofFin x)

Proof state:
w : ℕ
x : Fin (2 ^ w)
⊢ { toFin := -x } = -{ toFin := x }

Tactic:
rfl

Result:
no goals
-- Mathlib/MeasureTheory/Integral/BochnerL1.lean
theorem weightedSMul_congr (s t : Set α) (hst : μ s = μ t) :
    (weightedSMul μ s : F →L[ℝ] F) = weightedSMul μ t

Proof state:
case h
α : Type u_1
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
s t : Set α
hst : μ s = μ t
x : F
⊢ (weightedSMul μ s) x = (weightedSMul μ t) x

Tactic:
simp_rw [weightedSMul_apply]

Result:
case h
α : Type u_1
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
s t : Set α
hst : μ s = μ t
x : F
⊢ (μ s).toReal • x = (μ t).toReal • x

Proof state:
case h
α : Type u_1
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
s t : Set α
hst : μ s = μ t
x : F
⊢ (μ s).toReal • x = (μ t).toReal • x

Tactic:
congr 2

Result:
no goals

Proof state:
α : Type u_1
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
s t : Set α
hst : μ s = μ t
⊢ weightedSMul μ s = weightedSMul μ t

Tactic:
ext1 x

Result:
case h
α : Type u_1
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
s t : Set α
hst : μ s = μ t
x : F
⊢ (weightedSMul μ s) x = (weightedSMul μ t) x
-- Mathlib/MeasureTheory/Function/LocallyIntegrable.lean
theorem MonotoneOn.memLp_isCompact [IsFiniteMeasureOnCompacts μ] (hs : IsCompact s)
    (hmono : MonotoneOn f s) : MemLp f p (μ.restrict s)

Proof state:
X : Type u_1
E : Type u_3
inst✝⁹ : MeasurableSpace X
inst✝⁸ : TopologicalSpace X
inst✝⁷ : NormedAddCommGroup E
f : X → E
μ : Measure X
s : Set X
inst✝⁶ : BorelSpace X
inst✝⁵ : ConditionallyCompleteLinearOrder X
inst✝⁴ : ConditionallyCompleteLinearOrder E
inst✝³ : OrderTopology X
inst✝² : OrderTopology E
inst✝¹ : SecondCountableTopology E
p : ℝ≥0∞
inst✝ : IsFiniteMeasureOnCompacts μ
hs : IsCompact s
hmono : MonotoneOn f s
⊢ MemLp f p (μ.restrict s)

Tactic:
obtain rfl | h := s.eq_empty_or_nonempty

Result:
case inl
X : Type u_1
E : Type u_3
inst✝⁹ : MeasurableSpace X
inst✝⁸ : TopologicalSpace X
inst✝⁷ : NormedAddCommGroup E
f : X → E
μ : Measure X
inst✝⁶ : BorelSpace X
inst✝⁵ : ConditionallyCompleteLinearOrder X
inst✝⁴ : ConditionallyCompleteLinearOrder E
inst✝³ : OrderTopology X
inst✝² : OrderTopology E
inst✝¹ : SecondCountableTopology E
p : ℝ≥0∞
inst✝ : IsFiniteMeasureOnCompacts μ
hs : IsCompact ∅
hmono : MonotoneOn f ∅
⊢ MemLp f p (μ.restrict ∅)

case inr
X : Type u_1
E : Type u_3
inst✝⁹ : MeasurableSpace X
inst✝⁸ : TopologicalSpace X
inst✝⁷ : NormedAddCommGroup E
f : X → E
μ : Measure X
s : Set X
inst✝⁶ : BorelSpace X
inst✝⁵ : ConditionallyCompleteLinearOrder X
inst✝⁴ : ConditionallyCompleteLinearOrder E
inst✝³ : OrderTopology X
inst✝² : OrderTopology E
inst✝¹ : SecondCountableTopology E
p : ℝ≥0∞
inst✝ : IsFiniteMeasureOnCompacts μ
hs : IsCompact s
hmono : MonotoneOn f s
h : s.Nonempty
⊢ MemLp f p (μ.restrict s)

Proof state:
case inr
X : Type u_1
E : Type u_3
inst✝⁹ : MeasurableSpace X
inst✝⁸ : TopologicalSpace X
inst✝⁷ : NormedAddCommGroup E
f : X → E
μ : Measure X
s : Set X
inst✝⁶ : BorelSpace X
inst✝⁵ : ConditionallyCompleteLinearOrder X
inst✝⁴ : ConditionallyCompleteLinearOrder E
inst✝³ : OrderTopology X
inst✝² : OrderTopology E
inst✝¹ : SecondCountableTopology E
p : ℝ≥0∞
inst✝ : IsFiniteMeasureOnCompacts μ
hs : IsCompact s
hmono : MonotoneOn f s
h : s.Nonempty
⊢ MemLp f p (μ.restrict s)

Tactic:
exact hmono.memLp_of_measure_ne_top (hs.isLeast_sInf h) (hs.isGreatest_sSup h)
  hs.measure_lt_top.ne hs.measurableSet

Result:
no goals

Proof state:
case inl
X : Type u_1
E : Type u_3
inst✝⁹ : MeasurableSpace X
inst✝⁸ : TopologicalSpace X
inst✝⁷ : NormedAddCommGroup E
f : X → E
μ : Measure X
inst✝⁶ : BorelSpace X
inst✝⁵ : ConditionallyCompleteLinearOrder X
inst✝⁴ : ConditionallyCompleteLinearOrder E
inst✝³ : OrderTopology X
inst✝² : OrderTopology E
inst✝¹ : SecondCountableTopology E
p : ℝ≥0∞
inst✝ : IsFiniteMeasureOnCompacts μ
hs : IsCompact ∅
hmono : MonotoneOn f ∅
⊢ MemLp f p (μ.restrict ∅)

Tactic:
simp

Result:
no goals
-- Mathlib/Data/Nat/Factorization/Defs.lean
theorem factorization_eq_zero_of_not_dvd {n p : ℕ} (h : ¬p ∣ n) : n.factorization p = 0

Proof state:
n p : ℕ
h : ¬p ∣ n
⊢ n.factorization p = 0

Tactic:
simp [factorization_eq_zero_iff, h]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Sum/Basic.lean
theorem liftRel_inl_inl : LiftRel r s (inl a) (inl c) ↔ r a c :=
  ⟨fun h => by cases h; assumption, LiftRel.inl⟩

Proof state:
α✝ : Type u_1
γ✝ : Type u_2
r : α✝ → γ✝ → Prop
β✝ : Type u_3
δ✝ : Type u_4
s : β✝ → δ✝ → Prop
a : α✝
c : γ✝
h : LiftRel r s (inl a) (inl c)
⊢ r a c

Tactic:
cases h

Result:
case inl
α✝ : Type u_1
γ✝ : Type u_2
r : α✝ → γ✝ → Prop
β✝ : Type u_3
δ✝ : Type u_4
s : β✝ → δ✝ → Prop
a : α✝
c : γ✝
a✝ : r a c
⊢ r a c

Proof state:
case inl
α✝ : Type u_1
γ✝ : Type u_2
r : α✝ → γ✝ → Prop
β✝ : Type u_3
δ✝ : Type u_4
s : β✝ → δ✝ → Prop
a : α✝
c : γ✝
a✝ : r a c
⊢ r a c

Tactic:
assumption

Result:
no goals
-- Mathlib/Algebra/BigOperators/Group/List/Basic.lean
theorem prod_hom_nonempty {l : List M} {F : Type*} [FunLike F M N] [MulHomClass F M N] (f : F)
    (hl : l ≠ []) : (l.map f).prod = f l.prod :=
  match l, hl with | x :: xs, hl => by induction xs generalizing x <;> aesop

Proof state:
M : Type u_4
N : Type u_5
inst✝³ : Monoid M
inst✝² : Monoid N
l : List M
F : Type u_8
inst✝¹ : FunLike F M N
inst✝ : MulHomClass F M N
f : F
hl✝ : l ≠ []
x : M
xs : List M
hl : x :: xs ≠ []
⊢ (map (⇑f) (x :: xs)).prod = f (x :: xs).prod

Tactic:
induction xs generalizing x <;> aesop

Result:
no goals
-- Mathlib/Analysis/Calculus/ContDiff/Defs.lean
theorem contDiffOn_succ_iff_fderiv_of_isOpen (hs : IsOpen s) :
    ContDiffOn 𝕜 (n + 1) f s ↔
      DifferentiableOn 𝕜 f s ∧ (n = ω → AnalyticOn 𝕜 f s) ∧
      ContDiffOn 𝕜 n (fderiv 𝕜 f) s

Proof state:
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
s : Set E
f : E → F
n : WithTop ℕ∞
hs : IsOpen s
⊢ ContDiffOn 𝕜 (n + 1) f s ↔ DifferentiableOn 𝕜 f s ∧ (n = ω → AnalyticOn 𝕜 f s) ∧ ContDiffOn 𝕜 n (fderiv 𝕜 f) s

Tactic:
rw [contDiffOn_succ_iff_fderivWithin hs.uniqueDiffOn,
  contDiffOn_congr fun x hx ↦ fderivWithin_of_isOpen hs hx]

Result:
no goals
-- Mathlib/RingTheory/WittVector/Basic.lean
theorem ghostFun_neg : ghostFun (-x) = -ghostFun x

Proof state:
p : ℕ
R : Type u_1
inst✝¹ : CommRing R
inst✝ : Fact (Nat.Prime p)
x : 𝕎 R
⊢ WittVector.ghostFun (-x) = -WittVector.ghostFun x

Tactic:
ghost_fun_tac -X 0, ![x.coeff]

Result:
no goals
-- Mathlib/Data/Sigma/Basic.lean
theorem mk.inj_iff {a₁ a₂ : α} {b₁ : β a₁} {b₂ : β a₂} :
    Sigma.mk a₁ b₁ = ⟨a₂, b₂⟩ ↔ a₁ = a₂ ∧ HEq b₁ b₂

Proof state:
α : Type u_1
β : α → Type u_4
a₁ a₂ : α
b₁ : β a₁
b₂ : β a₂
⊢ ⟨a₁, b₁⟩ = ⟨a₂, b₂⟩ ↔ a₁ = a₂ ∧ HEq b₁ b₂

Tactic:
simp

Result:
no goals