harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Algebra/Order/BigOperators/Group/List.lean
@[to_additive] lemma monotone_prod_take (L : List M) : Monotone fun i => (L.take i).prod

Proof state:
case inl
M : Type u_3
inst✝¹ : OrderedCommMonoid M
inst✝ : CanonicallyOrderedMul M
L : List M
n : ℕ
h : n < L.length
⊢ (take n L).prod ≤ (take n L).prod * L[n]

Tactic:
exact le_self_mul

Result:
no goals

Proof state:
M : Type u_3
inst✝¹ : OrderedCommMonoid M
inst✝ : CanonicallyOrderedMul M
L : List M
⊢ Monotone fun i => (take i L).prod

Tactic:
refine monotone_nat_of_le_succ fun n => ?_

Result:
M : Type u_3
inst✝¹ : OrderedCommMonoid M
inst✝ : CanonicallyOrderedMul M
L : List M
n : ℕ
⊢ (take n L).prod ≤ (take (n + 1) L).prod

Proof state:
case inr
M : Type u_3
inst✝¹ : OrderedCommMonoid M
inst✝ : CanonicallyOrderedMul M
L : List M
n : ℕ
h : L.length ≤ n
⊢ (take n L).prod ≤ (take (n + 1) L).prod

Tactic:
simp [take_of_length_le h, take_of_length_le (le_trans h (Nat.le_succ _))]

Result:
no goals

Proof state:
case inl
M : Type u_3
inst✝¹ : OrderedCommMonoid M
inst✝ : CanonicallyOrderedMul M
L : List M
n : ℕ
h : n < L.length
⊢ (take n L).prod ≤ (take (n + 1) L).prod

Tactic:
rw [prod_take_succ _ _ h]

Result:
case inl
M : Type u_3
inst✝¹ : OrderedCommMonoid M
inst✝ : CanonicallyOrderedMul M
L : List M
n : ℕ
h : n < L.length
⊢ (take n L).prod ≤ (take n L).prod * L[n]

Proof state:
M : Type u_3
inst✝¹ : OrderedCommMonoid M
inst✝ : CanonicallyOrderedMul M
L : List M
n : ℕ
⊢ (take n L).prod ≤ (take (n + 1) L).prod

Tactic:
rcases lt_or_le n L.length with h | h

Result:
case inl
M : Type u_3
inst✝¹ : OrderedCommMonoid M
inst✝ : CanonicallyOrderedMul M
L : List M
n : ℕ
h : n < L.length
⊢ (take n L).prod ≤ (take (n + 1) L).prod

case inr
M : Type u_3
inst✝¹ : OrderedCommMonoid M
inst✝ : CanonicallyOrderedMul M
L : List M
n : ℕ
h : L.length ≤ n
⊢ (take n L).prod ≤ (take (n + 1) L).prod
-- Mathlib/GroupTheory/GroupAction/Period.lean
theorem period_inv (g : G) (a : α) : period g⁻¹ a = period g a

Proof state:
α : Type v
G : Type u
inst✝¹ : Group G
inst✝ : MulAction G α
g : G
a : α
⊢ period g⁻¹ a = period g a

Tactic:
simp only [period_eq_minimalPeriod, Function.minimalPeriod_eq_minimalPeriod_iff,
  isPeriodicPt_smul_iff]

Result:
α : Type v
G : Type u
inst✝¹ : Group G
inst✝ : MulAction G α
g : G
a : α
⊢ ∀ (n : ℕ), g⁻¹ ^ n • a = a ↔ g ^ n • a = a

Proof state:
α : Type v
G : Type u
inst✝¹ : Group G
inst✝ : MulAction G α
g : G
a : α
n : ℕ
⊢ g⁻¹ ^ n • a = a ↔ g ^ n • a = a

Tactic:
rw [smul_eq_iff_eq_inv_smul, eq_comm, ← zpow_natCast, inv_zpow, inv_inv, zpow_natCast]

Result:
no goals

Proof state:
α : Type v
G : Type u
inst✝¹ : Group G
inst✝ : MulAction G α
g : G
a : α
⊢ ∀ (n : ℕ), g⁻¹ ^ n • a = a ↔ g ^ n • a = a

Tactic:
intro n

Result:
α : Type v
G : Type u
inst✝¹ : Group G
inst✝ : MulAction G α
g : G
a : α
n : ℕ
⊢ g⁻¹ ^ n • a = a ↔ g ^ n • a = a
-- Mathlib/Analysis/SpecialFunctions/Trigonometric/Deriv.lean
theorem one_lt_cosh : 1 < cosh x ↔ x ≠ 0 :=
  cosh_zero ▸ cosh_lt_cosh.trans (by simp only [_root_.abs_zero, abs_pos])

Proof state:
x : ℝ
⊢ |0| < |x| ↔ x ≠ 0

Tactic:
simp only [_root_.abs_zero, abs_pos]

Result:
no goals
-- Mathlib/Data/Complex/Trigonometric.lean
theorem cosh_add_aux {a b c d : ℂ} :
    (a + b) * (c + d) + (a - b) * (c - d) = 2 * (a * c + b * d)

Proof state:
a b c d : ℂ
⊢ (a + b) * (c + d) + (a - b) * (c - d) = 2 * (a * c + b * d)

Tactic:
ring

Result:
no goals
-- Mathlib/AlgebraicGeometry/EllipticCurve/Affine.lean
lemma map_polynomial : (W'.map f).toAffine.polynomial = W'.polynomial.map (mapRingHom f)

Proof state:
R : Type r
S : Type s
inst✝¹ : CommRing R
inst✝ : CommRing S
W' : Affine R
f : R →+* S
⊢ Y ^ 2 + C (C (map W' f).toAffine.a₁ * X + C (map W' f).toAffine.a₃) * Y -
      C (X ^ 3 + C (map W' f).toAffine.a₂ * X ^ 2 + C (map W' f).toAffine.a₄ * X + C (map W' f).toAffine.a₆) =
    Polynomial.map (mapRingHom f)
      (Y ^ 2 + C (C W'.a₁ * X + C W'.a₃) * Y - C (X ^ 3 + C W'.a₂ * X ^ 2 + C W'.a₄ * X + C W'.a₆))

Tactic:
map_simp

Result:
no goals

Proof state:
R : Type r
S : Type s
inst✝¹ : CommRing R
inst✝ : CommRing S
W' : Affine R
f : R →+* S
⊢ (map W' f).toAffine.polynomial = Polynomial.map (mapRingHom f) W'.polynomial

Tactic:
simp only [polynomial]

Result:
R : Type r
S : Type s
inst✝¹ : CommRing R
inst✝ : CommRing S
W' : Affine R
f : R →+* S
⊢ Y ^ 2 + C (C (map W' f).toAffine.a₁ * X + C (map W' f).toAffine.a₃) * Y -
      C (X ^ 3 + C (map W' f).toAffine.a₂ * X ^ 2 + C (map W' f).toAffine.a₄ * X + C (map W' f).toAffine.a₆) =
    Polynomial.map (mapRingHom f)
      (Y ^ 2 + C (C W'.a₁ * X + C W'.a₃) * Y - C (X ^ 3 + C W'.a₂ * X ^ 2 + C W'.a₄ * X + C W'.a₆))
-- Mathlib/Algebra/ModEq.lean
theorem sub_iff_left :
    a₁ ≡ b₁ [PMOD p] → (a₁ - a₂ ≡ b₁ - b₂ [PMOD p] ↔ a₂ ≡ b₂ [PMOD p]) := fun ⟨m, hm⟩ =>
  (Equiv.subLeft m).symm.exists_congr_left.trans <| by simp [sub_sub_sub_comm, hm, sub_smul, ModEq]

Proof state:
α : Type u_1
inst✝ : AddCommGroup α
p a₁ a₂ b₁ b₂ : α
x✝ : a₁ ≡ b₁ [PMOD p]
m : ℤ
hm : b₁ - a₁ = m • p
⊢ (∃ b, b₁ - b₂ - (a₁ - a₂) = (Equiv.subLeft m).symm.symm b • p) ↔ a₂ ≡ b₂ [PMOD p]

Tactic:
simp [sub_sub_sub_comm, hm, sub_smul, ModEq]

Result:
no goals
-- Mathlib/Data/Fin/Basic.lean
theorem castSucc_lt_succ_iff {a b : Fin n} : castSucc a < succ b ↔ a ≤ b

Proof state:
n : ℕ
a b : Fin n
⊢ a.castSucc < b.succ ↔ a ≤ b

Tactic:
rw [castSucc_lt_iff_succ_le, succ_le_succ_iff]

Result:
no goals
-- Mathlib/Algebra/Order/Ring/Unbundled/Basic.lean
lemma mul_neg_iff [PosMulStrictMono α] [MulPosStrictMono α]
    [AddLeftReflectLT α] [AddLeftStrictMono α] :
    a * b < 0 ↔ 0 < a ∧ b < 0 ∨ a < 0 ∧ 0 < b

Proof state:
α : Type u
inst✝⁵ : Ring α
inst✝⁴ : LinearOrder α
a b : α
inst✝³ : PosMulStrictMono α
inst✝² : MulPosStrictMono α
inst✝¹ : AddLeftReflectLT α
inst✝ : AddLeftStrictMono α
⊢ a * b < 0 ↔ 0 < a ∧ b < 0 ∨ a < 0 ∧ 0 < b

Tactic:
rw [← neg_pos, neg_mul_eq_mul_neg, mul_pos_iff (α := α), neg_pos, neg_lt_zero]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/List/Associative.lean
theorem getValue?_append {β : Type v} [BEq α] {l l' : List ((_ : α) × β)} {a : α} :
    getValue? a (l ++ l') = (getValue? a l).or (getValue? a l')

Proof state:
α : Type u
β : Type v
inst✝ : BEq α
l l' : List ((_ : α) × β)
a : α
⊢ getValue? a (l ++ l') = (getValue? a l).or (getValue? a l')

Tactic:
simp [getValue?_eq_getEntry?, Option.map_or']

Result:
no goals
-- Mathlib/Data/Nat/Dist.lean
theorem dist_pos_of_ne {i j : Nat} : i ≠ j → 0 < dist i j := fun hne =>
  ltByCases i j
    (fun h : i < j => by rw [dist_eq_sub_of_le (le_of_lt h)]; apply tsub_pos_of_lt h)
    (fun h : i = j => by contradiction) fun h : i > j => by
    rw [dist_eq_sub_of_le_right (le_of_lt h)]; apply tsub_pos_of_lt h

Proof state:
i j : ℕ
hne : i ≠ j
h : i < j
⊢ 0 < i.dist j

Tactic:
rw [dist_eq_sub_of_le (le_of_lt h)]

Result:
i j : ℕ
hne : i ≠ j
h : i < j
⊢ 0 < j - i

Proof state:
i j : ℕ
hne : i ≠ j
h : i = j
⊢ 0 < i.dist j

Tactic:
contradiction

Result:
no goals

Proof state:
i j : ℕ
hne : i ≠ j
h : i < j
⊢ 0 < j - i

Tactic:
apply tsub_pos_of_lt h

Result:
no goals

Proof state:
i j : ℕ
hne : i ≠ j
h : i > j
⊢ 0 < i - j

Tactic:
apply tsub_pos_of_lt h

Result:
no goals

Proof state:
i j : ℕ
hne : i ≠ j
h : i > j
⊢ 0 < i.dist j

Tactic:
rw [dist_eq_sub_of_le_right (le_of_lt h)]

Result:
i j : ℕ
hne : i ≠ j
h : i > j
⊢ 0 < i - j
-- Mathlib/Combinatorics/SimpleGraph/Basic.lean
@[simp] lemma edgeSet_nonempty : G.edgeSet.Nonempty ↔ G ≠ ⊥

Proof state:
V : Type u
G : SimpleGraph V
⊢ G.edgeSet.Nonempty ↔ G ≠ ⊥

Tactic:
rw [Set.nonempty_iff_ne_empty, edgeSet_eq_empty.ne]

Result:
no goals
-- Mathlib/RingTheory/Int/Basic.lean
theorem eq_pow_of_mul_eq_pow_odd_left {a b c : ℤ} (hab : IsCoprime a b) {k : ℕ} (hk : Odd k)
    (h : a * b = c ^ k) : ∃ d, a = d ^ k

Proof state:
case intro
a b c : ℤ
hab : IsCoprime a b
k : ℕ
hk : Odd k
h : a * b = c ^ k
d : ℤ
hd : Associated a (d ^ k)
⊢ ∃ d, a = d ^ k

Tactic:
rw [associated_iff_natAbs, natAbs_eq_natAbs_iff, ← hk.neg_pow] at hd

Result:
case intro
a b c : ℤ
hab : IsCoprime a b
k : ℕ
hk : Odd k
h : a * b = c ^ k
d : ℤ
hd : a = d ^ k ∨ a = (-d) ^ k
⊢ ∃ d, a = d ^ k

Proof state:
case intro
a b c : ℤ
hab : IsCoprime a b
k : ℕ
hk : Odd k
h : a * b = c ^ k
d : ℤ
hd : Associated (d ^ k) a
⊢ ∃ d, a = d ^ k

Tactic:
replace hd := hd.symm

Result:
case intro
a b c : ℤ
hab : IsCoprime a b
k : ℕ
hk : Odd k
h : a * b = c ^ k
d : ℤ
hd : Associated a (d ^ k)
⊢ ∃ d, a = d ^ k

Proof state:
case intro
a b c : ℤ
hab : IsCoprime a b
k : ℕ
hk : Odd k
h : a * b = c ^ k
d : ℤ
hd : a = d ^ k ∨ a = (-d) ^ k
⊢ ∃ d, a = d ^ k

Tactic:
obtain rfl | rfl := hd <;> exact ⟨_, rfl⟩

Result:
no goals

Proof state:
a b c : ℤ
hab : IsCoprime a b
k : ℕ
hk : Odd k
h : a * b = c ^ k
⊢ ∃ d, a = d ^ k

Tactic:
obtain ⟨d, hd⟩ := exists_associated_pow_of_mul_eq_pow' hab h

Result:
case intro
a b c : ℤ
hab : IsCoprime a b
k : ℕ
hk : Odd k
h : a * b = c ^ k
d : ℤ
hd : Associated (d ^ k) a
⊢ ∃ d, a = d ^ k
-- Mathlib/NumberTheory/Pell.lean
theorem x_mul (a b : Solution₁ d) : (a * b).x = a.x * b.x + d * (a.y * b.y)

Proof state:
d : ℤ
a b : Solution₁ d
⊢ (a * b).x = a.x * b.x + d * a.y * b.y

Tactic:
rfl

Result:
no goals

Proof state:
d : ℤ
a b : Solution₁ d
⊢ (a * b).x = a.x * b.x + d * (a.y * b.y)

Tactic:
rw [← mul_assoc]

Result:
d : ℤ
a b : Solution₁ d
⊢ (a * b).x = a.x * b.x + d * a.y * b.y
-- Mathlib/Algebra/Module/ZLattice/Basic.lean
lemma fundamentalDomain_pi_basisFun [Fintype ι] :
    fundamentalDomain (Pi.basisFun ℝ ι) = Set.pi Set.univ fun _ : ι ↦ Set.Ico (0 : ℝ) 1

Proof state:
ι : Type u_2
inst✝ : Fintype ι
⊢ fundamentalDomain (Pi.basisFun ℝ ι) = Set.univ.pi fun x => Set.Ico 0 1

Tactic:
ext

Result:
case h
ι : Type u_2
inst✝ : Fintype ι
x✝ : ι → ℝ
⊢ x✝ ∈ fundamentalDomain (Pi.basisFun ℝ ι) ↔ x✝ ∈ Set.univ.pi fun x => Set.Ico 0 1

Proof state:
case h
ι : Type u_2
inst✝ : Fintype ι
x✝ : ι → ℝ
⊢ x✝ ∈ fundamentalDomain (Pi.basisFun ℝ ι) ↔ x✝ ∈ Set.univ.pi fun x => Set.Ico 0 1

Tactic:
simp

Result:
no goals
-- Mathlib/Algebra/BigOperators/Pi.lean
@[to_additive (attr := elab_as_elim) existing]
lemma Pi.mulSingle_induction [CommMonoid M] (p : (ι → M) → Prop) (f : ι → M)
    (one : p 1) (mul : ∀ f g, p f → p g → p (f * g))
    (mulSingle : ∀ i m, p (Pi.mulSingle i m)) : p f

Proof state:
ι : Type u_1
inst✝² : Finite ι
inst✝¹ : DecidableEq ι
M : Type u_4
inst✝ : CommMonoid M
p : (ι → M) → Prop
f : ι → M
one : p 1
mul : ∀ (f g : ι → M), p f → p g → p (f * g)
mulSingle : ∀ (i : ι) (m : M), p (Pi.mulSingle i m)
⊢ p f

Tactic:
cases nonempty_fintype ι

Result:
case intro
ι : Type u_1
inst✝² : Finite ι
inst✝¹ : DecidableEq ι
M : Type u_4
inst✝ : CommMonoid M
p : (ι → M) → Prop
f : ι → M
one : p 1
mul : ∀ (f g : ι → M), p f → p g → p (f * g)
mulSingle : ∀ (i : ι) (m : M), p (Pi.mulSingle i m)
val✝ : Fintype ι
⊢ p f

Proof state:
ι : Type u_1
inst✝² : Finite ι
inst✝¹ : DecidableEq ι
M : Type u_4
inst✝ : CommMonoid M
p : (ι → M) → Prop
f : ι → M
one : p 1
mul : ∀ (f g : ι → M), p f → p g → p (f * g)
mulSingle : ∀ (i : ι) (m : M), p (Pi.mulSingle i m)
val✝ : Fintype ι
⊢ ∀ x ∈ Finset.univ, p (Pi.mulSingle x (f x))

Tactic:
simp [mulSingle]

Result:
no goals

Proof state:
case intro
ι : Type u_1
inst✝² : Finite ι
inst✝¹ : DecidableEq ι
M : Type u_4
inst✝ : CommMonoid M
p : (ι → M) → Prop
f : ι → M
one : p 1
mul : ∀ (f g : ι → M), p f → p g → p (f * g)
mulSingle : ∀ (i : ι) (m : M), p (Pi.mulSingle i m)
val✝ : Fintype ι
⊢ p f

Tactic:
rw [← Finset.univ_prod_mulSingle f]

Result:
case intro
ι : Type u_1
inst✝² : Finite ι
inst✝¹ : DecidableEq ι
M : Type u_4
inst✝ : CommMonoid M
p : (ι → M) → Prop
f : ι → M
one : p 1
mul : ∀ (f g : ι → M), p f → p g → p (f * g)
mulSingle : ∀ (i : ι) (m : M), p (Pi.mulSingle i m)
val✝ : Fintype ι
⊢ p (∏ i : ι, Pi.mulSingle i (f i))

Proof state:
case intro
ι : Type u_1
inst✝² : Finite ι
inst✝¹ : DecidableEq ι
M : Type u_4
inst✝ : CommMonoid M
p : (ι → M) → Prop
f : ι → M
one : p 1
mul : ∀ (f g : ι → M), p f → p g → p (f * g)
mulSingle : ∀ (i : ι) (m : M), p (Pi.mulSingle i m)
val✝ : Fintype ι
⊢ p (∏ i : ι, Pi.mulSingle i (f i))

Tactic:
exact Finset.prod_induction _ _ mul one (by simp [mulSingle])

Result:
no goals
-- Mathlib/CategoryTheory/Monoidal/Functor.lean
@[simp] lemma prod'_δ_fst (X Y : C) : (δ (prod' F G) X Y).1 = δ F X Y

Proof state:
C : Type u₁
inst✝⁷ : Category.{v₁, u₁} C
inst✝⁶ : MonoidalCategory C
D : Type u₂
inst✝⁵ : Category.{v₂, u₂} D
inst✝⁴ : MonoidalCategory D
E : Type u₃
inst✝³ : Category.{v₃, u₃} E
inst✝² : MonoidalCategory E
F : C ⥤ D
G : C ⥤ E
inst✝¹ : F.OplaxMonoidal
inst✝ : G.OplaxMonoidal
X Y : C
⊢ F.map (𝟙 ((diag C).obj (X ⊗ Y)).1) ≫ (δ (F.prod G) ((diag C).obj X) ((diag C).obj Y)).1 = δ F X Y

Tactic:
rw [Functor.map_id, Category.id_comp]

Result:
C : Type u₁
inst✝⁷ : Category.{v₁, u₁} C
inst✝⁶ : MonoidalCategory C
D : Type u₂
inst✝⁵ : Category.{v₂, u₂} D
inst✝⁴ : MonoidalCategory D
E : Type u₃
inst✝³ : Category.{v₃, u₃} E
inst✝² : MonoidalCategory E
F : C ⥤ D
G : C ⥤ E
inst✝¹ : F.OplaxMonoidal
inst✝ : G.OplaxMonoidal
X Y : C
⊢ (δ (F.prod G) ((diag C).obj X) ((diag C).obj Y)).1 = δ F X Y

Proof state:
C : Type u₁
inst✝⁷ : Category.{v₁, u₁} C
inst✝⁶ : MonoidalCategory C
D : Type u₂
inst✝⁵ : Category.{v₂, u₂} D
inst✝⁴ : MonoidalCategory D
E : Type u₃
inst✝³ : Category.{v₃, u₃} E
inst✝² : MonoidalCategory E
F : C ⥤ D
G : C ⥤ E
inst✝¹ : F.OplaxMonoidal
inst✝ : G.OplaxMonoidal
X Y : C
⊢ (δ (F.prod G) ((diag C).obj X) ((diag C).obj Y)).1 = δ F X Y

Tactic:
rfl

Result:
no goals

Proof state:
C : Type u₁
inst✝⁷ : Category.{v₁, u₁} C
inst✝⁶ : MonoidalCategory C
D : Type u₂
inst✝⁵ : Category.{v₂, u₂} D
inst✝⁴ : MonoidalCategory D
E : Type u₃
inst✝³ : Category.{v₃, u₃} E
inst✝² : MonoidalCategory E
F : C ⥤ D
G : C ⥤ E
inst✝¹ : F.OplaxMonoidal
inst✝ : G.OplaxMonoidal
X Y : C
⊢ (δ (F.prod' G) X Y).1 = δ F X Y

Tactic:
change F.map (𝟙 _) ≫ _ = _

Result:
C : Type u₁
inst✝⁷ : Category.{v₁, u₁} C
inst✝⁶ : MonoidalCategory C
D : Type u₂
inst✝⁵ : Category.{v₂, u₂} D
inst✝⁴ : MonoidalCategory D
E : Type u₃
inst✝³ : Category.{v₃, u₃} E
inst✝² : MonoidalCategory E
F : C ⥤ D
G : C ⥤ E
inst✝¹ : F.OplaxMonoidal
inst✝ : G.OplaxMonoidal
X Y : C
⊢ F.map (𝟙 ((diag C).obj (X ⊗ Y)).1) ≫ (δ (F.prod G) ((diag C).obj X) ((diag C).obj Y)).1 = δ F X Y
-- Mathlib/LinearAlgebra/FiniteDimensional/Defs.lean
theorem ker_pow_constant {f : End K V} {k : ℕ}
    (h : LinearMap.ker (f ^ k) = LinearMap.ker (f ^ k.succ)) :
    ∀ m, LinearMap.ker (f ^ k) = LinearMap.ker (f ^ (k + m))
  | 0 => by simp
  | m + 1 => by
    apply le_antisymm
    · rw [add_comm, pow_add]
      apply LinearMap.ker_le_ker_comp
    · rw [ker_pow_constant h m, add_comm m 1, ← add_assoc, pow_add, pow_add f k m,
        LinearMap.mul_eq_comp, LinearMap.mul_eq_comp, LinearMap.ker_comp, LinearMap.ker_comp, h,
        Nat.add_one]

Proof state:
case a
K : Type u
V : Type v
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
f : End K V
k : ℕ
h : LinearMap.ker (f ^ k) = LinearMap.ker (f ^ k.succ)
m : ℕ
⊢ LinearMap.ker (f ^ k) ≤ LinearMap.ker (f ^ (m + 1) * f ^ k)

Tactic:
apply LinearMap.ker_le_ker_comp

Result:
no goals

Proof state:
case a
K : Type u
V : Type v
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
f : End K V
k : ℕ
h : LinearMap.ker (f ^ k) = LinearMap.ker (f ^ k.succ)
m : ℕ
⊢ LinearMap.ker (f ^ (k + (m + 1))) ≤ LinearMap.ker (f ^ k)

Tactic:
rw [ker_pow_constant h m, add_comm m 1, ← add_assoc, pow_add, pow_add f k m,
  LinearMap.mul_eq_comp, LinearMap.mul_eq_comp, LinearMap.ker_comp, LinearMap.ker_comp, h,
  Nat.add_one]

Result:
no goals

Proof state:
case a
K : Type u
V : Type v
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
f : End K V
k : ℕ
h : LinearMap.ker (f ^ k) = LinearMap.ker (f ^ k.succ)
m : ℕ
⊢ LinearMap.ker (f ^ k) ≤ LinearMap.ker (f ^ (k + (m + 1)))

Tactic:
rw [add_comm, pow_add]

Result:
case a
K : Type u
V : Type v
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
f : End K V
k : ℕ
h : LinearMap.ker (f ^ k) = LinearMap.ker (f ^ k.succ)
m : ℕ
⊢ LinearMap.ker (f ^ k) ≤ LinearMap.ker (f ^ (m + 1) * f ^ k)

Proof state:
K : Type u
V : Type v
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
f : End K V
k : ℕ
h : LinearMap.ker (f ^ k) = LinearMap.ker (f ^ k.succ)
m : ℕ
⊢ LinearMap.ker (f ^ k) = LinearMap.ker (f ^ (k + (m + 1)))

Tactic:
apply le_antisymm

Result:
case a
K : Type u
V : Type v
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
f : End K V
k : ℕ
h : LinearMap.ker (f ^ k) = LinearMap.ker (f ^ k.succ)
m : ℕ
⊢ LinearMap.ker (f ^ k) ≤ LinearMap.ker (f ^ (k + (m + 1)))

case a
K : Type u
V : Type v
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
f : End K V
k : ℕ
h : LinearMap.ker (f ^ k) = LinearMap.ker (f ^ k.succ)
m : ℕ
⊢ LinearMap.ker (f ^ (k + (m + 1))) ≤ LinearMap.ker (f ^ k)

Proof state:
K : Type u
V : Type v
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
f : End K V
k : ℕ
h : LinearMap.ker (f ^ k) = LinearMap.ker (f ^ k.succ)
⊢ LinearMap.ker (f ^ k) = LinearMap.ker (f ^ (k + 0))

Tactic:
simp

Result:
no goals
-- Mathlib/Algebra/Group/Subgroup/Lattice.lean
theorem closure_induction₂ {p : (x y : G) → x ∈ closure k → y ∈ closure k → Prop}
    (mem : ∀ (x) (y) (hx : x ∈ k) (hy : y ∈ k), p x y (subset_closure hx) (subset_closure hy))
    (one_left : ∀ x hx, p 1 x (one_mem _) hx) (one_right : ∀ x hx, p x 1 hx (one_mem _))
    (mul_left : ∀ x y z hx hy hz, p x z hx hz → p y z hy hz → p (x * y) z (mul_mem hx hy) hz)
    (mul_right : ∀ y z x hy hz hx, p x y hx hy → p x z hx hz → p x (y * z) hx (mul_mem hy hz))
    (inv_left : ∀ x y hx hy, p x y hx hy → p x⁻¹ y (inv_mem hx) hy)
    (inv_right : ∀ x y hx hy, p x y hx hy → p x y⁻¹ hx (inv_mem hy))
    {x y : G} (hx : x ∈ closure k) (hy : y ∈ closure k) : p x y hx hy

Proof state:
G : Type u_1
inst✝ : Group G
k : Set G
p : (x y : G) → x ∈ closure k → y ∈ closure k → Prop
mem : ∀ (x y : G) (hx : x ∈ k) (hy : y ∈ k), p x y ⋯ ⋯
one_left : ∀ (x : G) (hx : x ∈ closure k), p 1 x ⋯ hx
one_right : ∀ (x : G) (hx : x ∈ closure k), p x 1 hx ⋯
mul_left :
  ∀ (x y z : G) (hx : x ∈ closure k) (hy : y ∈ closure k) (hz : z ∈ closure k),
    p x z hx hz → p y z hy hz → p (x * y) z ⋯ hz
mul_right :
  ∀ (y z x : G) (hy : y ∈ closure k) (hz : z ∈ closure k) (hx : x ∈ closure k),
    p x y hx hy → p x z hx hz → p x (y * z) hx ⋯
inv_left : ∀ (x y : G) (hx : x ∈ closure k) (hy : y ∈ closure k), p x y hx hy → p x⁻¹ y ⋯ hy
inv_right : ∀ (x y : G) (hx : x ∈ closure k) (hy : y ∈ closure k), p x y hx hy → p x y⁻¹ hx ⋯
x y : G
hx : x ∈ closure k
hy : y ∈ closure k
⊢ p x y hx hy

Tactic:
induction hy using closure_induction with
| mem z hz => induction hx using closure_induction with
  | mem _ h => exact mem _ _ h hz
  | one => exact one_left _ (subset_closure hz)
  | mul _ _ _ _ h₁ h₂ => exact mul_left _ _ _ _ _ _ h₁ h₂
  | inv _ _ h => exact inv_left _ _ _ _ h
| one => exact one_right x hx
| mul _ _ _ _ h₁ h₂ => exact mul_right _ _ _ _ _ hx h₁ h₂
| inv _ _ h => exact inv_right _ _ _ _ h

Result:
no goals

Proof state:
case mem.inv
G : Type u_1
inst✝ : Group G
k : Set G
p : (x y : G) → x ∈ closure k → y ∈ closure k → Prop
mem : ∀ (x y : G) (hx : x ∈ k) (hy : y ∈ k), p x y ⋯ ⋯
one_left : ∀ (x : G) (hx : x ∈ closure k), p 1 x ⋯ hx
one_right : ∀ (x : G) (hx : x ∈ closure k), p x 1 hx ⋯
mul_left :
  ∀ (x y z : G) (hx : x ∈ closure k) (hy : y ∈ closure k) (hz : z ∈ closure k),
    p x z hx hz → p y z hy hz → p (x * y) z ⋯ hz
mul_right :
  ∀ (y z x : G) (hy : y ∈ closure k) (hz : z ∈ closure k) (hx : x ∈ closure k),
    p x y hx hy → p x z hx hz → p x (y * z) hx ⋯
inv_left : ∀ (x y : G) (hx : x ∈ closure k) (hy : y ∈ closure k), p x y hx hy → p x⁻¹ y ⋯ hy
inv_right : ∀ (x y : G) (hx : x ∈ closure k) (hy : y ∈ closure k), p x y hx hy → p x y⁻¹ hx ⋯
x y z : G
hz : z ∈ k
x✝ : G
hx✝ : x✝ ∈ closure k
h : p x✝ z hx✝ ⋯
⊢ p x✝⁻¹ z ⋯ ⋯

Tactic:
exact inv_left _ _ _ _ h

Result:
no goals
-- Mathlib/Algebra/Polynomial/BigOperators.lean
theorem natDegree_list_prod_le (l : List S[X]) : natDegree l.prod ≤ (l.map natDegree).sum

Proof state:
case nil
S : Type u_1
inst✝ : Semiring S
⊢ [].prod.natDegree ≤ (List.map natDegree []).sum

Tactic:
simp

Result:
no goals

Proof state:
case cons
S : Type u_1
inst✝ : Semiring S
hd : S[X]
tl : List S[X]
IH : tl.prod.natDegree ≤ (List.map natDegree tl).sum
⊢ (hd :: tl).prod.natDegree ≤ (List.map natDegree (hd :: tl)).sum

Tactic:
simpa using natDegree_mul_le.trans (add_le_add_left IH _)

Result:
no goals

Proof state:
S : Type u_1
inst✝ : Semiring S
l : List S[X]
⊢ l.prod.natDegree ≤ (List.map natDegree l).sum

Tactic:
induction' l with hd tl IH

Result:
case nil
S : Type u_1
inst✝ : Semiring S
⊢ [].prod.natDegree ≤ (List.map natDegree []).sum

case cons
S : Type u_1
inst✝ : Semiring S
hd : S[X]
tl : List S[X]
IH : tl.prod.natDegree ≤ (List.map natDegree tl).sum
⊢ (hd :: tl).prod.natDegree ≤ (List.map natDegree (hd :: tl)).sum
-- Mathlib/Algebra/Group/Basic.lean
@[to_additive mul_zsmul'] lemma zpow_mul (a : α) : ∀ m n : ℤ, a ^ (m * n) = (a ^ m) ^ n
  | (m : ℕ), (n : ℕ) => by
    rw [zpow_natCast, zpow_natCast, ← pow_mul, ← zpow_natCast]
    rfl
  | (m : ℕ), .negSucc n => by
    rw [zpow_natCast, zpow_negSucc, ← pow_mul, Int.ofNat_mul_negSucc, zpow_neg, inv_inj,
      ← zpow_natCast]
  | .negSucc m, (n : ℕ) => by
    rw [zpow_natCast, zpow_negSucc, ← inv_pow, ← pow_mul, Int.negSucc_mul_ofNat, zpow_neg, inv_pow,
      inv_inj, ← zpow_natCast]
  | .negSucc m, .negSucc n => by
    rw [zpow_negSucc, zpow_negSucc, Int.negSucc_mul_negSucc, inv_pow, inv_inv, ← pow_mul, ←
      zpow_natCast]
    rfl

Proof state:
α : Type u_1
inst✝ : DivisionMonoid α
a : α
m n : ℕ
⊢ a ^ (↑m.succ * ↑n.succ) = a ^ ↑((m + 1) * (n + 1))

Tactic:
rfl

Result:
no goals

Proof state:
α : Type u_1
inst✝ : DivisionMonoid α
a : α
m n : ℕ
⊢ a ^ (↑m * ↑n) = a ^ ↑(m * n)

Tactic:
rfl

Result:
no goals

Proof state:
α : Type u_1
inst✝ : DivisionMonoid α
a : α
m n : ℕ
⊢ a ^ (Int.negSucc m * ↑n) = (a ^ Int.negSucc m) ^ ↑n

Tactic:
rw [zpow_natCast, zpow_negSucc, ← inv_pow, ← pow_mul, Int.negSucc_mul_ofNat, zpow_neg, inv_pow,
  inv_inj, ← zpow_natCast]

Result:
no goals

Proof state:
α : Type u_1
inst✝ : DivisionMonoid α
a : α
m n : ℕ
⊢ a ^ (↑m * ↑n) = (a ^ ↑m) ^ ↑n

Tactic:
rw [zpow_natCast, zpow_natCast, ← pow_mul, ← zpow_natCast]

Result:
α : Type u_1
inst✝ : DivisionMonoid α
a : α
m n : ℕ
⊢ a ^ (↑m * ↑n) = a ^ ↑(m * n)

Proof state:
α : Type u_1
inst✝ : DivisionMonoid α
a : α
m n : ℕ
⊢ a ^ (Int.negSucc m * Int.negSucc n) = (a ^ Int.negSucc m) ^ Int.negSucc n

Tactic:
rw [zpow_negSucc, zpow_negSucc, Int.negSucc_mul_negSucc, inv_pow, inv_inv, ← pow_mul, ←
  zpow_natCast]

Result:
α : Type u_1
inst✝ : DivisionMonoid α
a : α
m n : ℕ
⊢ a ^ (↑m.succ * ↑n.succ) = a ^ ↑((m + 1) * (n + 1))

Proof state:
α : Type u_1
inst✝ : DivisionMonoid α
a : α
m n : ℕ
⊢ a ^ (↑m * Int.negSucc n) = (a ^ ↑m) ^ Int.negSucc n

Tactic:
rw [zpow_natCast, zpow_negSucc, ← pow_mul, Int.ofNat_mul_negSucc, zpow_neg, inv_inj,
  ← zpow_natCast]

Result:
no goals
-- Mathlib/Data/Complex/Trigonometric.lean
theorem cos_add_sin_I : cos x + sin x * I = exp (x * I)

Proof state:
x : ℂ
⊢ cos x + sin x * I = cexp (x * I)

Tactic:
rw [← cosh_add_sinh, sinh_mul_I, cosh_mul_I]

Result:
no goals
-- Mathlib/CategoryTheory/Iso.lean
theorem hom_eq_inv (α : X ≅ Y) (β : Y ≅ X) : α.hom = β.inv ↔ β.hom = α.inv

Proof state:
C : Type u
inst✝ : Category.{v, u} C
X Y : C
α : X ≅ Y
β : Y ≅ X
⊢ β.hom = α.symm.hom ↔ β.hom = α.inv

Tactic:
rfl

Result:
no goals

Proof state:
C : Type u
inst✝ : Category.{v, u} C
X Y : C
α : X ≅ Y
β : Y ≅ X
⊢ α.hom = β.inv ↔ β.hom = α.inv

Tactic:
erw [inv_eq_inv α.symm β, eq_comm]

Result:
C : Type u
inst✝ : Category.{v, u} C
X Y : C
α : X ≅ Y
β : Y ≅ X
⊢ β.hom = α.symm.hom ↔ β.hom = α.inv
-- Mathlib/NumberTheory/SmoothNumbers.lean
@[simp]
lemma smoothNumbers_zero : smoothNumbers 0 = {1}

Proof state:
⊢ smoothNumbers 0 = {1}

Tactic:
simp only [smoothNumbers_eq_factoredNumbers, Finset.range_zero, factoredNumbers_empty]

Result:
no goals