harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Analysis/Normed/Operator/Compact.lean
theorem IsCompactOperator.image_subset_compact_of_isVonNBounded {f : M₁ →ₛₗ[σ₁₂] M₂}
    (hf : IsCompactOperator f) {S : Set M₁} (hS : IsVonNBounded 𝕜₁ S) :
    ∃ K : Set M₂, IsCompact K ∧ f '' S ⊆ K :=
  let ⟨K, hK, hKf⟩ := hf
  let ⟨r, hr, hrS⟩ := (hS hKf).exists_pos
  let ⟨c, hc⟩ := NormedField.exists_lt_norm 𝕜₁ r
  let this := ne_zero_of_norm_ne_zero (hr.trans hc).ne.symm
  ⟨σ₁₂ c • K, hK.image <| continuous_id.const_smul (σ₁₂ c), by
    rw [image_subset_iff, preimage_smul_setₛₗ _ _ _ f this.isUnit]; exact hrS c hc.le⟩

Proof state:
𝕜₁ : Type u_1
𝕜₂ : Type u_2
inst✝⁸ : NontriviallyNormedField 𝕜₁
inst✝⁷ : SeminormedRing 𝕜₂
σ₁₂ : 𝕜₁ →+* 𝕜₂
M₁ : Type u_3
M₂ : Type u_4
inst✝⁶ : TopologicalSpace M₁
inst✝⁵ : AddCommMonoid M₁
inst✝⁴ : TopologicalSpace M₂
inst✝³ : AddCommMonoid M₂
inst✝² : Module 𝕜₁ M₁
inst✝¹ : Module 𝕜₂ M₂
inst✝ : ContinuousConstSMul 𝕜₂ M₂
f : M₁ →ₛₗ[σ₁₂] M₂
hf : IsCompactOperator ⇑f
S : Set M₁
hS : IsVonNBounded 𝕜₁ S
K : Set M₂
hK : IsCompact K
hKf : ⇑f ⁻¹' K ∈ 𝓝 0
r : ℝ
hr : r > 0
hrS : ∀ (c : 𝕜₁), r ≤ ‖c‖ → S ⊆ c • ⇑f ⁻¹' K
c : 𝕜₁
hc : r < ‖c‖
this : c ≠ 0 := ne_zero_of_norm_ne_zero (Ne.symm (LT.lt.ne (LT.lt.trans hr hc)))
⊢ S ⊆ c • ⇑f ⁻¹' K

Tactic:
exact hrS c hc.le

Result:
no goals

Proof state:
𝕜₁ : Type u_1
𝕜₂ : Type u_2
inst✝⁸ : NontriviallyNormedField 𝕜₁
inst✝⁷ : SeminormedRing 𝕜₂
σ₁₂ : 𝕜₁ →+* 𝕜₂
M₁ : Type u_3
M₂ : Type u_4
inst✝⁶ : TopologicalSpace M₁
inst✝⁵ : AddCommMonoid M₁
inst✝⁴ : TopologicalSpace M₂
inst✝³ : AddCommMonoid M₂
inst✝² : Module 𝕜₁ M₁
inst✝¹ : Module 𝕜₂ M₂
inst✝ : ContinuousConstSMul 𝕜₂ M₂
f : M₁ →ₛₗ[σ₁₂] M₂
hf : IsCompactOperator ⇑f
S : Set M₁
hS : IsVonNBounded 𝕜₁ S
K : Set M₂
hK : IsCompact K
hKf : ⇑f ⁻¹' K ∈ 𝓝 0
r : ℝ
hr : r > 0
hrS : ∀ (c : 𝕜₁), r ≤ ‖c‖ → S ⊆ c • ⇑f ⁻¹' K
c : 𝕜₁
hc : r < ‖c‖
this : c ≠ 0 := ne_zero_of_norm_ne_zero (Ne.symm (LT.lt.ne (LT.lt.trans hr hc)))
⊢ ⇑f '' S ⊆ σ₁₂ c • K

Tactic:
rw [image_subset_iff, preimage_smul_setₛₗ _ _ _ f this.isUnit]

Result:
𝕜₁ : Type u_1
𝕜₂ : Type u_2
inst✝⁸ : NontriviallyNormedField 𝕜₁
inst✝⁷ : SeminormedRing 𝕜₂
σ₁₂ : 𝕜₁ →+* 𝕜₂
M₁ : Type u_3
M₂ : Type u_4
inst✝⁶ : TopologicalSpace M₁
inst✝⁵ : AddCommMonoid M₁
inst✝⁴ : TopologicalSpace M₂
inst✝³ : AddCommMonoid M₂
inst✝² : Module 𝕜₁ M₁
inst✝¹ : Module 𝕜₂ M₂
inst✝ : ContinuousConstSMul 𝕜₂ M₂
f : M₁ →ₛₗ[σ₁₂] M₂
hf : IsCompactOperator ⇑f
S : Set M₁
hS : IsVonNBounded 𝕜₁ S
K : Set M₂
hK : IsCompact K
hKf : ⇑f ⁻¹' K ∈ 𝓝 0
r : ℝ
hr : r > 0
hrS : ∀ (c : 𝕜₁), r ≤ ‖c‖ → S ⊆ c • ⇑f ⁻¹' K
c : 𝕜₁
hc : r < ‖c‖
this : c ≠ 0 := ne_zero_of_norm_ne_zero (Ne.symm (LT.lt.ne (LT.lt.trans hr hc)))
⊢ S ⊆ c • ⇑f ⁻¹' K
-- Mathlib/Algebra/IsPrimePow.lean
theorem isPrimePow_nat_iff (n : ℕ) : IsPrimePow n ↔ ∃ p k : ℕ, Nat.Prime p ∧ 0 < k ∧ p ^ k = n

Proof state:
n : ℕ
⊢ IsPrimePow n ↔ ∃ p k, Nat.Prime p ∧ 0 < k ∧ p ^ k = n

Tactic:
simp only [isPrimePow_def, Nat.prime_iff]

Result:
no goals
-- Mathlib/Algebra/Order/Star/Basic.lean
theorem star_mul_self_pos [Nontrivial R] {x : R} (hx : IsRegular x) : 0 < star x * x

Proof state:
R : Type u
inst✝⁴ : NonUnitalSemiring R
inst✝³ : PartialOrder R
inst✝² : StarRing R
inst✝¹ : StarOrderedRing R
inst✝ : Nontrivial R
x : R
hx : IsRegular x
⊢ 0 ≠ x

Tactic:
exact hx.ne_zero.symm

Result:
no goals

Proof state:
R : Type u
inst✝⁴ : NonUnitalSemiring R
inst✝³ : PartialOrder R
inst✝² : StarRing R
inst✝¹ : StarOrderedRing R
inst✝ : Nontrivial R
x : R
hx : IsRegular x
⊢ 0 < star x * x

Tactic:
rw [(star_mul_self_nonneg _).lt_iff_ne, ← mul_zero (star x), hx.star.left.ne_iff]

Result:
R : Type u
inst✝⁴ : NonUnitalSemiring R
inst✝³ : PartialOrder R
inst✝² : StarRing R
inst✝¹ : StarOrderedRing R
inst✝ : Nontrivial R
x : R
hx : IsRegular x
⊢ 0 ≠ x
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/ToArray.lean
theorem findM?_toArray [Monad m] [LawfulMonad m] (f : α → m Bool) (l : List α) :
    l.toArray.findM? f = l.findM? f

Proof state:
case cons
m : Type → Type
α : Type
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : α → m Bool
a : α
l : List α
ih :
  (do
      let r ←
        forIn l ⟨none, PUnit.unit⟩ fun a r => do
            let __do_lift ← f a
            if __do_lift = true then pure (ForInStep.done ⟨some (some a), PUnit.unit⟩)
              else pure (ForInStep.yield ⟨none, PUnit.unit⟩)
      match r.fst with
        | none => pure none
        | some a => pure a) =
    findM? f l
⊢ (do
      let x ← f a
      let x ←
        if x = true then pure (ForInStep.done ⟨some (some a), PUnit.unit⟩)
          else pure (ForInStep.yield ⟨none, PUnit.unit⟩)
      let r ←
        match x with
          | ForInStep.done b => pure b
          | ForInStep.yield b =>
            forIn l b fun a r => do
              let __do_lift ← f a
              if __do_lift = true then pure (ForInStep.done ⟨some (some a), PUnit.unit⟩)
                else pure (ForInStep.yield ⟨none, PUnit.unit⟩)
      match r.fst with
        | none => pure none
        | some a => pure a) =
    do
    let __do_lift ← f a
    match __do_lift with
      | true => pure (some a)
      | false => findM? f l

Tactic:
congr

Result:
case cons.e_a
m : Type → Type
α : Type
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : α → m Bool
a : α
l : List α
ih :
  (do
      let r ←
        forIn l ⟨none, PUnit.unit⟩ fun a r => do
            let __do_lift ← f a
            if __do_lift = true then pure (ForInStep.done ⟨some (some a), PUnit.unit⟩)
              else pure (ForInStep.yield ⟨none, PUnit.unit⟩)
      match r.fst with
        | none => pure none
        | some a => pure a) =
    findM? f l
⊢ (fun x => do
      let x ←
        if x = true then pure (ForInStep.done ⟨some (some a), PUnit.unit⟩)
          else pure (ForInStep.yield ⟨none, PUnit.unit⟩)
      let r ←
        match x with
          | ForInStep.done b => pure b
          | ForInStep.yield b =>
            forIn l b fun a r => do
              let __do_lift ← f a
              if __do_lift = true then pure (ForInStep.done ⟨some (some a), PUnit.unit⟩)
                else pure (ForInStep.yield ⟨none, PUnit.unit⟩)
      match r.fst with
        | none => pure none
        | some a => pure a) =
    fun __do_lift =>
    match __do_lift with
    | true => pure (some a)
    | false => findM? f l

Proof state:
case nil
m : Type → Type
α : Type
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : α → m Bool
⊢ (do
      let r ←
        forIn [] ⟨none, PUnit.unit⟩ fun a r => do
            let __do_lift ← f a
            if __do_lift = true then pure (ForInStep.done ⟨some (some a), PUnit.unit⟩)
              else pure (ForInStep.yield ⟨none, PUnit.unit⟩)
      match r.fst with
        | none => pure none
        | some a => pure a) =
    findM? f []

Tactic:
simp

Result:
no goals
-- Mathlib/LinearAlgebra/RootSystem/Reduced.lean
lemma coxeterWeight_ne_four_of_linearIndependent [NeZero (2 : R)] [NoZeroSMulDivisors ℤ M]
    (hl : LinearIndependent R ![P.root i, P.root j]) :
    P.coxeterWeight i j ≠ 4

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 : ι
inst✝² : Finite ι
inst✝¹ : NeZero 2
inst✝ : NoZeroSMulDivisors ℤ M
hl : LinearIndependent R ![P.root i, P.root j]
⊢ P.coxeterWeight i j ≠ 4

Tactic:
intro contra

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 : ι
inst✝² : Finite ι
inst✝¹ : NeZero 2
inst✝ : NoZeroSMulDivisors ℤ M
hl : LinearIndependent R ![P.root i, P.root j]
contra : P.coxeterWeight i j = 4
⊢ False

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 : ι
inst✝² : Finite ι
inst✝¹ : NeZero 2
inst✝ : NoZeroSMulDivisors ℤ M
hl : LinearIndependent R ![P.root i, P.root j]
contra : P.coxeterWeight i j = 4
⊢ False

Tactic:
have := P.infinite_of_linInd_coxeterWeight_four hl contra

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 : ι
inst✝² : Finite ι
inst✝¹ : NeZero 2
inst✝ : NoZeroSMulDivisors ℤ M
hl : LinearIndependent R ![P.root i, P.root j]
contra : P.coxeterWeight i j = 4
this : Infinite ι
⊢ False

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 : ι
inst✝² : Finite ι
inst✝¹ : NeZero 2
inst✝ : NoZeroSMulDivisors ℤ M
hl : LinearIndependent R ![P.root i, P.root j]
contra : P.coxeterWeight i j = 4
this : Infinite ι
⊢ False

Tactic:
exact not_finite ι

Result:
no goals
-- Mathlib/LinearAlgebra/LinearDisjoint.lean
theorem linearDisjoint_op :
    M.LinearDisjoint N ↔ (equivOpposite.symm (MulOpposite.op N)).LinearDisjoint
      (equivOpposite.symm (MulOpposite.op M))

Proof state:
R : Type u
S : Type v
inst✝² : CommSemiring R
inst✝¹ : Semiring S
inst✝ : Algebra R S
M N : Submodule R S
⊢ M.LinearDisjoint N ↔ (equivOpposite.symm (MulOpposite.op N)).LinearDisjoint (equivOpposite.symm (MulOpposite.op M))

Tactic:
simp only [linearDisjoint_iff, mulMap_op, LinearMap.coe_comp,
  LinearEquiv.coe_coe, EquivLike.comp_injective, EquivLike.injective_comp]

Result:
no goals
-- Mathlib/Algebra/Group/Ext.lean
theorem CommMonoid.toMonoid_injective {M : Type u} :
    Function.Injective (@CommMonoid.toMonoid M)

Proof state:
M : Type u
⊢ Injective (@toMonoid M)

Tactic:
rintro ⟨⟩ ⟨⟩ h

Result:
case mk.mk
M : Type u
toMonoid✝¹ : Monoid M
mul_comm✝¹ : ∀ (a b : M), a * b = b * a
toMonoid✝ : Monoid M
mul_comm✝ : ∀ (a b : M), a * b = b * a
h : toMonoid = toMonoid
⊢ mk mul_comm✝¹ = mk mul_comm✝

Proof state:
case mk.mk
M : Type u
toMonoid✝¹ : Monoid M
mul_comm✝¹ : ∀ (a b : M), a * b = b * a
toMonoid✝ : Monoid M
mul_comm✝ : ∀ (a b : M), a * b = b * a
h : toMonoid = toMonoid
⊢ mk mul_comm✝¹ = mk mul_comm✝

Tactic:
congr

Result:
no goals
-- Mathlib/Order/Rel/GaloisConnection.lean
theorem leftDual_rightDual_le_of_le {I I' : Set β} (h : I' ∈ R.rightFixedPoints) (h₁ : I ≤ I') :
    R.leftDual (R.rightDual I) ≤ I'

Proof state:
case a
α : Type u_1
β : Type u_2
R : Rel α β
I I' : Set β
h : I' ∈ R.rightFixedPoints
h₁ : I ≤ I'
⊢ R.rightDual I' ≤ R.rightDual I

Tactic:
apply R.gc_leftDual_rightDual.monotone_u

Result:
case a.a
α : Type u_1
β : Type u_2
R : Rel α β
I I' : Set β
h : I' ∈ R.rightFixedPoints
h₁ : I ≤ I'
⊢ I' ≤ I

Proof state:
case a.a
α : Type u_1
β : Type u_2
R : Rel α β
I I' : Set β
h : I' ∈ R.rightFixedPoints
h₁ : I ≤ I'
⊢ I' ≤ I

Tactic:
exact h₁

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
R : Rel α β
I I' : Set β
h : I' ∈ R.rightFixedPoints
h₁ : I ≤ I'
⊢ R.leftDual (R.rightDual I) ≤ R.leftDual (R.rightDual I')

Tactic:
apply R.gc_leftDual_rightDual.monotone_l

Result:
case a
α : Type u_1
β : Type u_2
R : Rel α β
I I' : Set β
h : I' ∈ R.rightFixedPoints
h₁ : I ≤ I'
⊢ R.rightDual I' ≤ R.rightDual I

Proof state:
α : Type u_1
β : Type u_2
R : Rel α β
I I' : Set β
h : I' ∈ R.rightFixedPoints
h₁ : I ≤ I'
⊢ R.leftDual (R.rightDual I) ≤ I'

Tactic:
rw [← h]

Result:
α : Type u_1
β : Type u_2
R : Rel α β
I I' : Set β
h : I' ∈ R.rightFixedPoints
h₁ : I ≤ I'
⊢ R.leftDual (R.rightDual I) ≤ R.leftDual (R.rightDual I')
-- Mathlib/.lake/packages/batteries/Batteries/Data/HashMap/WF.lean
theorem expand_size [Hashable α] {buckets : Buckets α β} :
    (expand sz buckets).buckets.size = buckets.size

Proof state:
case e_a
α : Type u_1
β : Type u_2
sz : Nat
inst✝ : Hashable α
buckets : Buckets α β
i : Nat
source : Array (AssocList α β)
target : Buckets α β
hs : ∀ (j : Nat), j < i → source.toList[j]?.getD AssocList.nil = AssocList.nil
H : i < source.size
l₁ l₂ : List (AssocList α β)
h₁ : source.toList = l₁ ++ source.toList[i] :: l₂
left✝ : l₁.length = i
eq : source.toList.set i AssocList.nil = l₁ ++ AssocList.nil :: l₂
⊢ (List.map (fun x => x.toList.length) l₂).sum +
      (List.map (fun x => x.toList.length)
          (List.foldl (fun d x => reinsertAux d x.fst x.snd) target source[i].toList).val.toList).sum =
    source.toList[i].toList.length +
      ((List.map (fun x => x.toList.length) l₂).sum + (List.map (fun x => x.toList.length) target.val.toList).sum)

Tactic:
(conv => rhs; rw [Nat.add_left_comm])

Result:
case e_a
α : Type u_1
β : Type u_2
sz : Nat
inst✝ : Hashable α
buckets : Buckets α β
i : Nat
source : Array (AssocList α β)
target : Buckets α β
hs : ∀ (j : Nat), j < i → source.toList[j]?.getD AssocList.nil = AssocList.nil
H : i < source.size
l₁ l₂ : List (AssocList α β)
h₁ : source.toList = l₁ ++ source.toList[i] :: l₂
left✝ : l₁.length = i
eq : source.toList.set i AssocList.nil = l₁ ++ AssocList.nil :: l₂
⊢ (List.map (fun x => x.toList.length) l₂).sum +
      (List.map (fun x => x.toList.length)
          (List.foldl (fun d x => reinsertAux d x.fst x.snd) target source[i].toList).val.toList).sum =
    (List.map (fun x => x.toList.length) l₂).sum +
      (source.toList[i].toList.length + (List.map (fun x => x.toList.length) target.val.toList).sum)

Proof state:
α : Type u_1
β : Type u_2
sz : Nat
inst✝ : Hashable α
buckets : Buckets α β
i : Nat
source : Array (AssocList α β)
target : Buckets α β
hs : ∀ (j : Nat), j < i → source.toList[j]?.getD AssocList.nil = AssocList.nil
H : ¬i < source.size
j : Nat
h₁ : j < (List.map (fun x => AssocList.nil) source.toList).length
h₂ : j < source.toList.length
⊢ (List.map (fun x => AssocList.nil) source.toList)[j] = source.toList[j]

Tactic:
simp only [List.getElem_map, Array.length_toList]

Result:
α : Type u_1
β : Type u_2
sz : Nat
inst✝ : Hashable α
buckets : Buckets α β
i : Nat
source : Array (AssocList α β)
target : Buckets α β
hs : ∀ (j : Nat), j < i → source.toList[j]?.getD AssocList.nil = AssocList.nil
H : ¬i < source.size
j : Nat
h₁ : j < (List.map (fun x => AssocList.nil) source.toList).length
h₂ : j < source.toList.length
⊢ AssocList.nil = source.toList[j]
-- Mathlib/Data/Set/Pointwise/SMul.lean
theorem image_op_smul : (op '' s) • t = t * s

Proof state:
α : Type u_2
inst✝ : Mul α
s t : Set α
⊢ op '' s • t = t * s

Tactic:
rw [← image2_smul, ← image2_mul, image2_image_left, image2_swap]

Result:
α : Type u_2
inst✝ : Mul α
s t : Set α
⊢ image2 (fun a b => SMul.smul (op b) a) t s = image2 (fun x1 x2 => x1 * x2) t s

Proof state:
α : Type u_2
inst✝ : Mul α
s t : Set α
⊢ image2 (fun a b => SMul.smul (op b) a) t s = image2 (fun x1 x2 => x1 * x2) t s

Tactic:
rfl

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Trigonometric/EulerSineProd.lean
theorem integral_cos_mul_cos_pow_aux (hn : 2 ≤ n) (hz : z ≠ 0) :
    (∫ x in (0 : ℝ)..π / 2, Complex.cos (2 * z * x) * (cos x : ℂ) ^ n) =
      n / (2 * z) *
        ∫ x in (0 : ℝ)..π / 2, Complex.sin (2 * z * x) * sin x * (cos x : ℂ) ^ (n - 1)

Proof state:
case h.e'_3
z : ℂ
n : ℕ
hn : 2 ≤ n
hz : z ≠ 0
der1 : ∀ x ∈ uIcc 0 (π / 2), HasDerivAt (fun y => ↑(cos y) ^ n) (-↑n * ↑(sin x) * ↑(cos x) ^ (n - 1)) x
⊢ ↑n / (2 * z) * ∫ (x : ℝ) in 0 ..π / 2, Complex.sin (2 * z * ↑x) * ↑(sin x) * ↑(cos x) ^ (n - 1) =
    ↑(cos (π / 2)) ^ n * (Complex.sin (2 * z * ↑(π / 2)) / (2 * z)) -
        ↑(cos 0) ^ n * (Complex.sin (2 * z * ↑0) / (2 * z)) -
      ∫ (x : ℝ) in 0 ..π / 2, -↑n * ↑(sin x) * ↑(cos x) ^ (n - 1) * (Complex.sin (2 * z * ↑x) / (2 * z))

Tactic:
rw [Complex.ofReal_zero, mul_zero, Complex.sin_zero, zero_div, mul_zero, sub_zero,
  cos_pi_div_two, Complex.ofReal_zero, zero_pow (by positivity : n ≠ 0), zero_mul, zero_sub,
  ← integral_neg, ← integral_const_mul]

Result:
case h.e'_3
z : ℂ
n : ℕ
hn : 2 ≤ n
hz : z ≠ 0
der1 : ∀ x ∈ uIcc 0 (π / 2), HasDerivAt (fun y => ↑(cos y) ^ n) (-↑n * ↑(sin x) * ↑(cos x) ^ (n - 1)) x
⊢ ∫ (x : ℝ) in 0 ..π / 2, ↑n / (2 * z) * (Complex.sin (2 * z * ↑x) * ↑(sin x) * ↑(cos x) ^ (n - 1)) =
    ∫ (x : ℝ) in 0 ..π / 2, -(-↑n * ↑(sin x) * ↑(cos x) ^ (n - 1) * (Complex.sin (2 * z * ↑x) / (2 * z)))

Proof state:
case convert_1.hu
z : ℂ
n : ℕ
hn : 2 ≤ n
hz : z ≠ 0
der1 : ∀ x ∈ uIcc 0 (π / 2), HasDerivAt (fun y => ↑(cos y) ^ n) (-↑n * ↑(sin x) * ↑(cos x) ^ (n - 1)) x
⊢ Continuous fun x => -↑n * ↑(sin x) * ↑(cos x) ^ (n - 1)

Tactic:
exact
  (continuous_const.mul (Complex.continuous_ofReal.comp continuous_sin)).mul
    ((Complex.continuous_ofReal.comp continuous_cos).pow (n - 1))

Result:
no goals

Proof state:
case h.e'_3
z : ℂ
n : ℕ
hn : 2 ≤ n
hz : z ≠ 0
der1 : ∀ x ∈ uIcc 0 (π / 2), HasDerivAt (fun y => ↑(cos y) ^ n) (-↑n * ↑(sin x) * ↑(cos x) ^ (n - 1)) x
x : ℝ
x✝ : x ∈ uIcc 0 (π / 2)
⊢ ↑n * (Complex.sin (2 * z * ↑x) * Complex.sin ↑x * Complex.cos ↑x ^ (n - 1)) =
    ↑n * Complex.sin ↑x * Complex.cos ↑x ^ (n - 1) * Complex.sin (2 * z * ↑x)

Tactic:
ring

Result:
no goals

Proof state:
z : ℂ
n : ℕ
hn : 2 ≤ n
hz : z ≠ 0
x : ℝ
a✝ : x ∈ uIcc 0 (π / 2)
⊢ HasDerivAt (fun y => ↑(cos y)) (-↑(sin x)) x

Tactic:
simpa using (hasDerivAt_cos x).ofReal_comp

Result:
no goals

Proof state:
case h.e'_2.h.e'_4.h
z : ℂ
n : ℕ
hn : 2 ≤ n
hz : z ≠ 0
der1 : ∀ x ∈ uIcc 0 (π / 2), HasDerivAt (fun y => ↑(cos y) ^ n) (-↑n * ↑(sin x) * ↑(cos x) ^ (n - 1)) x
x : ℝ
⊢ Complex.cos (2 * z * ↑x) * ↑(cos x) ^ n = ↑(cos x) ^ n * Complex.cos (2 * z * ↑x)

Tactic:
rw [mul_comm]

Result:
no goals
-- Mathlib/Data/PFunctor/Univariate/Basic.lean
theorem iget_map [DecidableEq P.A] [Inhabited α] [Inhabited β] (x : P α)
    (f : α → β) (i : P.Idx) (h : i.1 = x.1) : (P.map f x).iget i = f (x.iget i)

Proof state:
case mk
P : PFunctor.{u}
α : Type v₁
β : Type v₂
inst✝² : DecidableEq P.A
inst✝¹ : Inhabited α
inst✝ : Inhabited β
f : α → β
i : P.Idx
fst✝ : P.A
snd✝ : P.B fst✝ → α
h : i.fst = ⟨fst✝, snd✝⟩.fst
⊢ (P.map f ⟨fst✝, snd✝⟩).snd (cast ⋯ i.snd) = f (⟨fst✝, snd✝⟩.snd (cast ⋯ i.snd))

Tactic:
rfl

Result:
no goals

Proof state:
P : PFunctor.{u}
α : Type v₁
β : Type v₂
inst✝² : DecidableEq P.A
inst✝¹ : Inhabited α
inst✝ : Inhabited β
x : ↑P α
f : α → β
i : P.Idx
h : i.fst = x.fst
⊢ (P.map f x).snd (cast ⋯ i.snd) = f (x.snd (cast ⋯ i.snd))

Tactic:
cases x

Result:
case mk
P : PFunctor.{u}
α : Type v₁
β : Type v₂
inst✝² : DecidableEq P.A
inst✝¹ : Inhabited α
inst✝ : Inhabited β
f : α → β
i : P.Idx
fst✝ : P.A
snd✝ : P.B fst✝ → α
h : i.fst = ⟨fst✝, snd✝⟩.fst
⊢ (P.map f ⟨fst✝, snd✝⟩).snd (cast ⋯ i.snd) = f (⟨fst✝, snd✝⟩.snd (cast ⋯ i.snd))

Proof state:
P : PFunctor.{u}
α : Type v₁
β : Type v₂
inst✝² : DecidableEq P.A
inst✝¹ : Inhabited α
inst✝ : Inhabited β
x : ↑P α
f : α → β
i : P.Idx
h : i.fst = x.fst
⊢ (P.map f x).iget i = f (x.iget i)

Tactic:
simp only [Obj.iget, fst_map, *, dif_pos, eq_self_iff_true]

Result:
P : PFunctor.{u}
α : Type v₁
β : Type v₂
inst✝² : DecidableEq P.A
inst✝¹ : Inhabited α
inst✝ : Inhabited β
x : ↑P α
f : α → β
i : P.Idx
h : i.fst = x.fst
⊢ (P.map f x).snd (cast ⋯ i.snd) = f (x.snd (cast ⋯ i.snd))
-- Mathlib/Algebra/Algebra/Quasispectrum.lean
lemma IsQuasiregular.isUnit_one_add {R : Type*} [Semiring R] {x : R} (hx : IsQuasiregular x) :
    IsUnit (1 + x)

Proof state:
case intro.intro.refine_2
R : Type u_1
inst✝ : Semiring R
x : R
hx : IsQuasiregular x
y : R
hy₁ : y + x + x * y = 0
hy₂ : x + y + y * x = 0
⊢ (1 + y) * (1 + x) = 1

Tactic:
convert congr(1 + $(hy₂)) using 1 <;> [noncomm_ring; simp]

Result:
no goals

Proof state:
case intro.intro
R : Type u_1
inst✝ : Semiring R
x : R
hx : IsQuasiregular x
y : R
hy₁ : y + x + x * y = 0
hy₂ : x + y + y * x = 0
⊢ IsUnit (1 + x)

Tactic:
refine ⟨⟨1 + x, 1 + y, ?_, ?_⟩, rfl⟩

Result:
case intro.intro.refine_1
R : Type u_1
inst✝ : Semiring R
x : R
hx : IsQuasiregular x
y : R
hy₁ : y + x + x * y = 0
hy₂ : x + y + y * x = 0
⊢ (1 + x) * (1 + y) = 1

case intro.intro.refine_2
R : Type u_1
inst✝ : Semiring R
x : R
hx : IsQuasiregular x
y : R
hy₁ : y + x + x * y = 0
hy₂ : x + y + y * x = 0
⊢ (1 + y) * (1 + x) = 1

Proof state:
R : Type u_1
inst✝ : Semiring R
x : R
hx : IsQuasiregular x
⊢ IsUnit (1 + x)

Tactic:
obtain ⟨y, hy₁, hy₂⟩ := isQuasiregular_iff.mp hx

Result:
case intro.intro
R : Type u_1
inst✝ : Semiring R
x : R
hx : IsQuasiregular x
y : R
hy₁ : y + x + x * y = 0
hy₂ : x + y + y * x = 0
⊢ IsUnit (1 + x)

Proof state:
case intro.intro.refine_1
R : Type u_1
inst✝ : Semiring R
x : R
hx : IsQuasiregular x
y : R
hy₁ : y + x + x * y = 0
hy₂ : x + y + y * x = 0
⊢ (1 + x) * (1 + y) = 1

Tactic:
convert congr(1 + $(hy₁)) using 1 <;> [noncomm_ring; simp]

Result:
no goals
-- Mathlib/Order/Chain.lean
theorem IsChain.superChain_succChain (hs₁ : IsChain r s) (hs₂ : ¬IsMaxChain r s) :
    SuperChain r s (SuccChain r s)

Proof state:
α : Type u_1
r : α → α → Prop
s : Set α
hs₁ : IsChain r s
hs₂ : IsChain r s → ∃ x, IsChain r x ∧ s ⊆ x ∧ ¬s = x
⊢ SuperChain r s (SuccChain r s)

Tactic:
obtain ⟨t, ht, hst⟩ := hs₂ hs₁

Result:
case intro.intro
α : Type u_1
r : α → α → Prop
s : Set α
hs₁ : IsChain r s
hs₂ : IsChain r s → ∃ x, IsChain r x ∧ s ⊆ x ∧ ¬s = x
t : Set α
ht : IsChain r t
hst : s ⊆ t ∧ ¬s = t
⊢ SuperChain r s (SuccChain r s)

Proof state:
case intro.intro
α : Type u_1
r : α → α → Prop
s : Set α
hs₁ : IsChain r s
hs₂ : IsChain r s → ∃ x, IsChain r x ∧ s ⊆ x ∧ ¬s = x
t : Set α
ht : IsChain r t
hst : s ⊆ t ∧ ¬s = t
⊢ SuperChain r s (SuccChain r s)

Tactic:
exact succChain_spec ⟨t, hs₁, ht, ssubset_iff_subset_ne.2 hst⟩

Result:
no goals

Proof state:
α : Type u_1
r : α → α → Prop
s : Set α
hs₁ : IsChain r s
hs₂ : ¬IsMaxChain r s
⊢ SuperChain r s (SuccChain r s)

Tactic:
simp only [IsMaxChain, _root_.not_and, not_forall, exists_prop, exists_and_left] at hs₂

Result:
α : Type u_1
r : α → α → Prop
s : Set α
hs₁ : IsChain r s
hs₂ : IsChain r s → ∃ x, IsChain r x ∧ s ⊆ x ∧ ¬s = x
⊢ SuperChain r s (SuccChain r s)
-- Mathlib/AlgebraicTopology/SimplicialSet/Path.lean
/-- Two paths of the same nonzero length are equal if all of their arrows are equal. -/
@[ext]
lemma Path.ext' {n : ℕ} {f g : Path X (n + 1)}
    (h : ∀ i : Fin (n + 1), f.arrow i = g.arrow i) :
    f = g

Proof state:
case vertex.h.inl.intro
X : SSet
n : ℕ
f g : X.Path (n + 1)
h : ∀ (i : Fin (n + 1)), f.arrow i = g.arrow i
j : Fin (n + 1 + 1)
k : Fin (n + 1)
hk : j = k.castSucc
⊢ f.vertex j = g.vertex j

Tactic:
rw [hk, ← f.arrow_src k, ← g.arrow_src k, h]

Result:
no goals

Proof state:
X : SSet
n : ℕ
f g : X.Path (n + 1)
h : ∀ (i : Fin (n + 1)), f.arrow i = g.arrow i
⊢ f = g

Tactic:
ext j

Result:
case vertex.h
X : SSet
n : ℕ
f g : X.Path (n + 1)
h : ∀ (i : Fin (n + 1)), f.arrow i = g.arrow i
j : Fin (n + 1 + 1)
⊢ f.vertex j = g.vertex j

case arrow.h
X : SSet
n : ℕ
f g : X.Path (n + 1)
h : ∀ (i : Fin (n + 1)), f.arrow i = g.arrow i
j : Fin (n + 1)
⊢ f.arrow j = g.arrow j

Proof state:
case vertex.h
X : SSet
n : ℕ
f g : X.Path (n + 1)
h : ∀ (i : Fin (n + 1)), f.arrow i = g.arrow i
j : Fin (n + 1 + 1)
⊢ f.vertex j = g.vertex j

Tactic:
rcases Fin.eq_castSucc_or_eq_last j with ⟨k, hk⟩ | hl

Result:
case vertex.h.inl.intro
X : SSet
n : ℕ
f g : X.Path (n + 1)
h : ∀ (i : Fin (n + 1)), f.arrow i = g.arrow i
j : Fin (n + 1 + 1)
k : Fin (n + 1)
hk : j = k.castSucc
⊢ f.vertex j = g.vertex j

case vertex.h.inr
X : SSet
n : ℕ
f g : X.Path (n + 1)
h : ∀ (i : Fin (n + 1)), f.arrow i = g.arrow i
j : Fin (n + 1 + 1)
hl : j = Fin.last (n + 1)
⊢ f.vertex j = g.vertex j

Proof state:
case arrow.h
X : SSet
n : ℕ
f g : X.Path (n + 1)
h : ∀ (i : Fin (n + 1)), f.arrow i = g.arrow i
j : Fin (n + 1)
⊢ f.arrow j = g.arrow j

Tactic:
exact h j

Result:
no goals

Proof state:
case vertex.h.inr
X : SSet
n : ℕ
f g : X.Path (n + 1)
h : ∀ (i : Fin (n + 1)), f.arrow i = g.arrow i
j : Fin (n + 1 + 1)
hl : j = Fin.last (n + 1)
⊢ f.vertex (Fin.last n).succ = g.vertex (Fin.last n).succ

Tactic:
rw [← f.arrow_tgt (Fin.last n), ← g.arrow_tgt (Fin.last n), h]

Result:
no goals

Proof state:
case vertex.h.inr
X : SSet
n : ℕ
f g : X.Path (n + 1)
h : ∀ (i : Fin (n + 1)), f.arrow i = g.arrow i
j : Fin (n + 1 + 1)
hl : j = Fin.last (n + 1)
⊢ f.vertex j = g.vertex j

Tactic:
simp only [hl, ← Fin.succ_last]

Result:
case vertex.h.inr
X : SSet
n : ℕ
f g : X.Path (n + 1)
h : ∀ (i : Fin (n + 1)), f.arrow i = g.arrow i
j : Fin (n + 1 + 1)
hl : j = Fin.last (n + 1)
⊢ f.vertex (Fin.last n).succ = g.vertex (Fin.last n).succ