harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/RingTheory/Multiplicity.lean
theorem FiniteMultiplicity.multiplicity_pow {p a : α} (hp : Prime p)
    (ha : FiniteMultiplicity p a) {k : ℕ} : multiplicity p (a ^ k) = k * multiplicity p a

Proof state:
α : Type u_1
inst✝ : CancelCommMonoidWithZero α
p a : α
hp : Prime p
ha : FiniteMultiplicity p a
k : ℕ
⊢ multiplicity p (a ^ k) = k * multiplicity p a

Tactic:
exact_mod_cast (ha.pow hp).emultiplicity_eq_multiplicity ▸
  ha.emultiplicity_eq_multiplicity ▸ emultiplicity_pow hp

Result:
no goals
-- Mathlib/Algebra/Polynomial/Degree/Definitions.lean
theorem degree_le_iff_coeff_zero (f : R[X]) (n : WithBot ℕ) :
    degree f ≤ n ↔ ∀ m : ℕ, n < m → coeff f m = 0

Proof state:
R : Type u
inst✝ : Semiring R
f : R[X]
n : WithBot ℕ
⊢ f.degree ≤ n ↔ ∀ (m : ℕ), n < ↑m → f.coeff m = 0

Tactic:
simp only [degree, Finset.max, Finset.sup_le_iff, mem_support_iff, Ne, ← not_le,
  not_imp_comm, Nat.cast_withBot]

Result:
no goals
-- Mathlib/Order/SupClosed.lean
@[simp] lemma infClosed_univ : InfClosed (univ : Set α)

Proof state:
α : Type u_3
inst✝ : SemilatticeInf α
⊢ InfClosed univ

Tactic:
simp [InfClosed]

Result:
no goals
-- Mathlib/FieldTheory/IsPerfectClosure.lean
theorem lift_lift : lift g (lift i j p) p = lift (g.comp i) j p

Proof state:
K : Type u_1
L : Type u_2
M : Type u_3
N : Type u_4
inst✝¹¹ : CommRing K
inst✝¹⁰ : CommRing L
inst✝⁹ : CommRing M
inst✝⁸ : CommRing N
i : K →+* L
j : K →+* M
g : L →+* N
p : ℕ
inst✝⁷ : ExpChar M p
inst✝⁶ : ExpChar K p
inst✝⁵ : PerfectRing M p
inst✝⁴ : IsPRadical i p
inst✝³ : ExpChar L p
inst✝² : ExpChar N p
inst✝¹ : IsPRadical g p
inst✝ : IsPRadical (g.comp i) p
⊢ lift g (lift i j p) p = lift (g.comp i) j p

Tactic:
refine IsPRadical.injective_comp_of_perfect _ (g.comp i) p ?_

Result:
K : Type u_1
L : Type u_2
M : Type u_3
N : Type u_4
inst✝¹¹ : CommRing K
inst✝¹⁰ : CommRing L
inst✝⁹ : CommRing M
inst✝⁸ : CommRing N
i : K →+* L
j : K →+* M
g : L →+* N
p : ℕ
inst✝⁷ : ExpChar M p
inst✝⁶ : ExpChar K p
inst✝⁵ : PerfectRing M p
inst✝⁴ : IsPRadical i p
inst✝³ : ExpChar L p
inst✝² : ExpChar N p
inst✝¹ : IsPRadical g p
inst✝ : IsPRadical (g.comp i) p
⊢ (fun f => f.comp (g.comp i)) (lift g (lift i j p) p) = (fun f => f.comp (g.comp i)) (lift (g.comp i) j p)

Proof state:
K : Type u_1
L : Type u_2
M : Type u_3
N : Type u_4
inst✝¹¹ : CommRing K
inst✝¹⁰ : CommRing L
inst✝⁹ : CommRing M
inst✝⁸ : CommRing N
i : K →+* L
j : K →+* M
g : L →+* N
p : ℕ
inst✝⁷ : ExpChar M p
inst✝⁶ : ExpChar K p
inst✝⁵ : PerfectRing M p
inst✝⁴ : IsPRadical i p
inst✝³ : ExpChar L p
inst✝² : ExpChar N p
inst✝¹ : IsPRadical g p
inst✝ : IsPRadical (g.comp i) p
⊢ (fun f => f.comp (g.comp i)) (lift g (lift i j p) p) = (fun f => f.comp (g.comp i)) (lift (g.comp i) j p)

Tactic:
simp_rw [← RingHom.comp_assoc _ _ (lift g _ p), lift_comp]

Result:
no goals
-- Mathlib/Analysis/Normed/Group/SemiNormedGrp.lean
lemma inv_hom_apply {M N : SemiNormedGrp} (e : M ≅ N) (r : M) : e.inv (e.hom r) = r

Proof state:
M N : SemiNormedGrp
e : M ≅ N
r : M.carrier
⊢ (ConcreteCategory.hom e.inv) ((ConcreteCategory.hom e.hom) r) = r

Tactic:
simp

Result:
no goals
-- Mathlib/Computability/Primrec.lean
theorem nat_le : PrimrecRel ((· ≤ ·) : ℕ → ℕ → Prop) :=
  (nat_casesOn nat_sub (const true) (const false).to₂).of_eq fun p => by
    dsimp [swap]
    rcases e : p.1 - p.2 with - | n
    · simp [Nat.sub_eq_zero_iff_le.1 e]
    · simp [not_le.2 (Nat.lt_of_sub_eq_succ e)]

Proof state:
case zero
p : ℕ × ℕ
e : p.1 - p.2 = 0
⊢ Nat.rec true (fun n n_ih => false) 0 = decide (p.1 ≤ p.2)

Tactic:
simp [Nat.sub_eq_zero_iff_le.1 e]

Result:
no goals

Proof state:
p : ℕ × ℕ
⊢ (Nat.casesOn ((fun x1 x2 => x1 - x2) p.1 p.2) true fun b => false) =
    (fun a b => decide ((fun x1 x2 => x1 ≤ x2) a b)) p.1 p.2

Tactic:
dsimp [swap]

Result:
p : ℕ × ℕ
⊢ Nat.rec true (fun n n_ih => false) (p.1 - p.2) = decide (p.1 ≤ p.2)

Proof state:
p : ℕ × ℕ
⊢ Nat.rec true (fun n n_ih => false) (p.1 - p.2) = decide (p.1 ≤ p.2)

Tactic:
rcases e : p.1 - p.2 with - | n

Result:
case zero
p : ℕ × ℕ
e : p.1 - p.2 = 0
⊢ Nat.rec true (fun n n_ih => false) 0 = decide (p.1 ≤ p.2)

case succ
p : ℕ × ℕ
n : ℕ
e : p.1 - p.2 = n + 1
⊢ Nat.rec true (fun n n_ih => false) (n + 1) = decide (p.1 ≤ p.2)

Proof state:
case succ
p : ℕ × ℕ
n : ℕ
e : p.1 - p.2 = n + 1
⊢ Nat.rec true (fun n n_ih => false) (n + 1) = decide (p.1 ≤ p.2)

Tactic:
simp [not_le.2 (Nat.lt_of_sub_eq_succ e)]

Result:
no goals
-- Mathlib/LinearAlgebra/SesquilinearForm.lean
theorem isOrtho_zero_left (B : M₁ →ₛₗ[I₁] M₂ →ₛₗ[I₂] M) (x) : IsOrtho B (0 : M₁) x

Proof state:
R : Type u_1
R₁ : Type u_2
R₂ : Type u_3
M : Type u_5
M₁ : Type u_6
M₂ : Type u_7
inst✝⁸ : CommSemiring R
inst✝⁷ : CommSemiring R₁
inst✝⁶ : AddCommMonoid M₁
inst✝⁵ : Module R₁ M₁
inst✝⁴ : CommSemiring R₂
inst✝³ : AddCommMonoid M₂
inst✝² : Module R₂ M₂
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
I₁ : R₁ →+* R
I₂ : R₂ →+* R
B : M₁ →ₛₗ[I₁] M₂ →ₛₗ[I₂] M
x : M₂
⊢ (B 0) x = 0

Tactic:
rw [map_zero B, zero_apply]

Result:
no goals

Proof state:
R : Type u_1
R₁ : Type u_2
R₂ : Type u_3
M : Type u_5
M₁ : Type u_6
M₂ : Type u_7
inst✝⁸ : CommSemiring R
inst✝⁷ : CommSemiring R₁
inst✝⁶ : AddCommMonoid M₁
inst✝⁵ : Module R₁ M₁
inst✝⁴ : CommSemiring R₂
inst✝³ : AddCommMonoid M₂
inst✝² : Module R₂ M₂
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
I₁ : R₁ →+* R
I₂ : R₂ →+* R
B : M₁ →ₛₗ[I₁] M₂ →ₛₗ[I₂] M
x : M₂
⊢ B.IsOrtho 0 x

Tactic:
dsimp only [IsOrtho]

Result:
R : Type u_1
R₁ : Type u_2
R₂ : Type u_3
M : Type u_5
M₁ : Type u_6
M₂ : Type u_7
inst✝⁸ : CommSemiring R
inst✝⁷ : CommSemiring R₁
inst✝⁶ : AddCommMonoid M₁
inst✝⁵ : Module R₁ M₁
inst✝⁴ : CommSemiring R₂
inst✝³ : AddCommMonoid M₂
inst✝² : Module R₂ M₂
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
I₁ : R₁ →+* R
I₂ : R₂ →+* R
B : M₁ →ₛₗ[I₁] M₂ →ₛₗ[I₂] M
x : M₂
⊢ (B 0) x = 0
-- Mathlib/Data/Matroid/Constructions.lean
theorem ground_indep_iff_eq_freeOn : M.Indep M.E ↔ M = freeOn M.E

Proof state:
α : Type u_1
M : Matroid α
⊢ M.Indep M.E ↔ M = freeOn M.E

Tactic:
simp [eq_freeOn_iff]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Integrals.lean
theorem integral_sin_sq : ∫ x in a..b, sin x ^ 2 = (sin a * cos a - sin b * cos b + b - a) / 2

Proof state:
a b : ℝ
⊢ ∫ (x : ℝ) in a..b, sin x ^ 2 = (sin a * cos a - sin b * cos b + b - a) / 2

Tactic:
field_simp [integral_sin_pow, add_sub_assoc]

Result:
no goals
-- Mathlib/Algebra/Group/Basic.lean
@[to_additive (attr := simp)]
lemma mul_left_iterate (a : M) : ∀ n : ℕ, (a * ·)^[n] = (a ^ n * ·)
  | 0 =>  by ext; simp
  | n + 1 => by ext; simp [pow_succ, mul_left_iterate]

Proof state:
case h
M : Type u_4
inst✝ : Monoid M
a x✝ : M
⊢ (fun x => a * x)^[0] x✝ = a ^ 0 * x✝

Tactic:
simp

Result:
no goals

Proof state:
M : Type u_4
inst✝ : Monoid M
a : M
n : ℕ
⊢ (fun x => a * x)^[n + 1] = fun x => a ^ (n + 1) * x

Tactic:
ext

Result:
case h
M : Type u_4
inst✝ : Monoid M
a : M
n : ℕ
x✝ : M
⊢ (fun x => a * x)^[n + 1] x✝ = a ^ (n + 1) * x✝

Proof state:
M : Type u_4
inst✝ : Monoid M
a : M
⊢ (fun x => a * x)^[0] = fun x => a ^ 0 * x

Tactic:
ext

Result:
case h
M : Type u_4
inst✝ : Monoid M
a x✝ : M
⊢ (fun x => a * x)^[0] x✝ = a ^ 0 * x✝

Proof state:
case h
M : Type u_4
inst✝ : Monoid M
a : M
n : ℕ
x✝ : M
⊢ (fun x => a * x)^[n + 1] x✝ = a ^ (n + 1) * x✝

Tactic:
simp [pow_succ, mul_left_iterate]

Result:
no goals
-- Mathlib/Data/Set/Card.lean
theorem Infinite.exists_subset_ncard_eq {s : Set α} (hs : s.Infinite) (k : ℕ) :
    ∃ t, t ⊆ s ∧ t.Finite ∧ t.ncard = k

Proof state:
α : Type u_1
s : Set α
hs : s.Infinite
k : ℕ
⊢ ∃ t ⊆ s, t.Finite ∧ t.ncard = k

Tactic:
have := hs.to_subtype

Result:
α : Type u_1
s : Set α
hs : s.Infinite
k : ℕ
this : Infinite ↑s
⊢ ∃ t ⊆ s, t.Finite ∧ t.ncard = k

Proof state:
α : Type u_1
s : Set α
hs : s.Infinite
this : Infinite ↑s
t' : Finset ↑s
⊢ Subtype.val '' ↑t' ⊆ s

Tactic:
simp

Result:
no goals

Proof state:
case intro.intro
α : Type u_1
s : Set α
hs : s.Infinite
this : Infinite ↑s
t' : Finset ↑s
⊢ ∃ t ⊆ s, t.Finite ∧ t.ncard = t'.card

Tactic:
refine ⟨Subtype.val '' (t' : Set s), by simp, Finite.image _ (by simp), ?_⟩

Result:
case intro.intro
α : Type u_1
s : Set α
hs : s.Infinite
this : Infinite ↑s
t' : Finset ↑s
⊢ (Subtype.val '' ↑t').ncard = t'.card

Proof state:
α : Type u_1
s : Set α
hs : s.Infinite
k : ℕ
this : Infinite ↑s
⊢ ∃ t ⊆ s, t.Finite ∧ t.ncard = k

Tactic:
obtain ⟨t', -, rfl⟩ := @Infinite.exists_subset_card_eq s univ infinite_univ k

Result:
case intro.intro
α : Type u_1
s : Set α
hs : s.Infinite
this : Infinite ↑s
t' : Finset ↑s
⊢ ∃ t ⊆ s, t.Finite ∧ t.ncard = t'.card

Proof state:
case intro.intro
α : Type u_1
s : Set α
hs : s.Infinite
this : Infinite ↑s
t' : Finset ↑s
⊢ (↑t').ncard = t'.card

Tactic:
simp

Result:
no goals

Proof state:
case intro.intro
α : Type u_1
s : Set α
hs : s.Infinite
this : Infinite ↑s
t' : Finset ↑s
⊢ (Subtype.val '' ↑t').ncard = t'.card

Tactic:
rw [ncard_image_of_injective _ Subtype.coe_injective]

Result:
case intro.intro
α : Type u_1
s : Set α
hs : s.Infinite
this : Infinite ↑s
t' : Finset ↑s
⊢ (↑t').ncard = t'.card

Proof state:
α : Type u_1
s : Set α
hs : s.Infinite
this : Infinite ↑s
t' : Finset ↑s
⊢ (↑t').Finite

Tactic:
simp

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Option/Lemmas.lean
theorem map_pmap {p : α → Prop} (g : β → γ) (f : ∀ a, p a → β) (o H) :
    Option.map g (pmap f o H) = pmap (fun a h => g (f a h)) o H

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
p : α → Prop
g : β → γ
f : (a : α) → p a → β
o : Option α
H : ∀ (a : α), a ∈ o → p a
⊢ Option.map g (pmap f o H) = pmap (fun a h => g (f a h)) o H

Tactic:
cases o <;> simp

Result:
no goals
-- Mathlib/LinearAlgebra/Matrix/BilinearForm.lean
theorem mem_selfAdjointMatricesSubmodule' :
    A ∈ selfAdjointMatricesSubmodule J ↔ J.IsSelfAdjoint A

Proof state:
R₂ : Type u_3
inst✝² : CommRing R₂
n : Type u_5
inst✝¹ : Fintype n
J A : Matrix n n R₂
inst✝ : DecidableEq n
⊢ A ∈ selfAdjointMatricesSubmodule J ↔ J.IsSelfAdjoint A

Tactic:
simp only [mem_selfAdjointMatricesSubmodule]

Result:
no goals
-- Mathlib/Algebra/Order/Ring/Abs.lean
lemma abs_pow_eq_one (a : α) (h : n ≠ 0) : |a ^ n| = 1 ↔ |a| = 1

Proof state:
α : Type u_1
inst✝ : LinearOrderedRing α
n : ℕ
a : α
h : n ≠ 0
⊢ |a ^ n| = 1 ↔ |a| = 1

Tactic:
convert pow_left_inj₀ (abs_nonneg a) zero_le_one h

Result:
case h.e'_1.h.e'_2
α : Type u_1
inst✝ : LinearOrderedRing α
n : ℕ
a : α
h : n ≠ 0
⊢ |a ^ n| = |a| ^ n

case h.e'_1.h.e'_3
α : Type u_1
inst✝ : LinearOrderedRing α
n : ℕ
a : α
h : n ≠ 0
⊢ 1 = 1 ^ n

Proof state:
case h.e'_1.h.e'_2
α : Type u_1
inst✝ : LinearOrderedRing α
n : ℕ
a : α
h : n ≠ 0
⊢ |a ^ n| = |a| ^ n

case h.e'_1.h.e'_3
α : Type u_1
inst✝ : LinearOrderedRing α
n : ℕ
a : α
h : n ≠ 0
⊢ 1 = 1 ^ n

Tactic:
exacts [(pow_abs _ _).symm, (one_pow _).symm]

Result:
no goals
-- Mathlib/Algebra/Star/Module.lean
theorem algebraMap_star_comm (r : R) : algebraMap R A (star r) = star (algebraMap R A r)

Proof state:
R : Type u_1
A : Type u_2
inst✝⁵ : CommSemiring R
inst✝⁴ : StarRing R
inst✝³ : Semiring A
inst✝² : StarMul A
inst✝¹ : Algebra R A
inst✝ : StarModule R A
r : R
⊢ (algebraMap R A) (star r) = star ((algebraMap R A) r)

Tactic:
simp only [Algebra.algebraMap_eq_smul_one, star_smul, star_one]

Result:
no goals
-- Mathlib/LinearAlgebra/RootSystem/RootPositive.lean
@[simp] lemma algebraMap_posForm {x y : span S (range P.root)} :
    algebraMap S R (B.posForm x y) = B.form x y

Proof state:
ι : Type u_1
R : Type u_2
S : Type u_3
M : Type u_4
N : Type u_5
inst✝¹⁰ : LinearOrderedCommRing S
inst✝⁹ : CommRing R
inst✝⁸ : Algebra S R
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R N
P : RootPairing ι R M N
inst✝³ : P.IsValuedIn S
B : RootPositiveForm S P
inst✝² : FaithfulSMul S R
inst✝¹ : Module S M
inst✝ : IsScalarTower S R M
x y : ↥(span S (range ⇑P.root))
⊢ (algebraMap S R) ((B.posForm x) y) = (B.form ↑x) ↑y

Tactic:
change Algebra.linearMap S R _ = _

Result:
ι : Type u_1
R : Type u_2
S : Type u_3
M : Type u_4
N : Type u_5
inst✝¹⁰ : LinearOrderedCommRing S
inst✝⁹ : CommRing R
inst✝⁸ : Algebra S R
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R N
P : RootPairing ι R M N
inst✝³ : P.IsValuedIn S
B : RootPositiveForm S P
inst✝² : FaithfulSMul S R
inst✝¹ : Module S M
inst✝ : IsScalarTower S R M
x y : ↥(span S (range ⇑P.root))
⊢ (Algebra.linearMap S R) ((B.posForm x) y) = (B.form ↑x) ↑y

Proof state:
ι : Type u_1
R : Type u_2
S : Type u_3
M : Type u_4
N : Type u_5
inst✝¹⁰ : LinearOrderedCommRing S
inst✝⁹ : CommRing R
inst✝⁸ : Algebra S R
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R N
P : RootPairing ι R M N
inst✝³ : P.IsValuedIn S
B : RootPositiveForm S P
inst✝² : FaithfulSMul S R
inst✝¹ : Module S M
inst✝ : IsScalarTower S R M
x y : ↥(span S (range ⇑P.root))
⊢ (Algebra.linearMap S R) ((B.posForm x) y) = (B.form ↑x) ↑y

Tactic:
simp [posForm]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Tactic/BVDecide/Bitblast/BVExpr/Basic.lean
theorem eval_xor : eval .xor = ((· ^^^ ·) : BitVec w → BitVec w → BitVec w)

Proof state:
w : Nat
⊢ xor.eval = fun x1 x2 => x1 ^^^ x2

Tactic:
rfl

Result:
no goals
-- Mathlib/Analysis/InnerProductSpace/LinearMap.lean
theorem inner_map_polarization (T : V →ₗ[ℂ] V) (x y : V) :
    ⟪T y, x⟫_ℂ =
      (⟪T (x + y), x + y⟫_ℂ - ⟪T (x - y), x - y⟫_ℂ +
            Complex.I * ⟪T (x + Complex.I • y), x + Complex.I • y⟫_ℂ -
          Complex.I * ⟪T (x - Complex.I • y), x - Complex.I • y⟫_ℂ) /
        4

Proof state:
V : Type u_4
inst✝¹ : SeminormedAddCommGroup V
inst✝ : InnerProductSpace ℂ V
T : V →ₗ[ℂ] V
x y : V
⊢ ⟪T y, x⟫_ℂ =
    (⟪T x, x⟫_ℂ + ⟪T y, x⟫_ℂ + (⟪T x, y⟫_ℂ + ⟪T y, y⟫_ℂ) - (⟪T x, x⟫_ℂ - (⟪T y, x⟫_ℂ + (⟪T x, y⟫_ℂ - ⟪T y, y⟫_ℂ))) +
          (Complex.I * ⟪T x, x⟫_ℂ + ⟪T y, x⟫_ℂ + (-⟪T x, y⟫_ℂ + Complex.I * ⟪T y, y⟫_ℂ)) -
        (Complex.I * ⟪T x, x⟫_ℂ - (⟪T y, x⟫_ℂ + (-⟪T x, y⟫_ℂ - Complex.I * ⟪T y, y⟫_ℂ)))) /
      4

Tactic:
ring

Result:
no goals

Proof state:
V : Type u_4
inst✝¹ : SeminormedAddCommGroup V
inst✝ : InnerProductSpace ℂ V
T : V →ₗ[ℂ] V
x y : V
⊢ ⟪T y, x⟫_ℂ =
    (⟪T (x + y), x + y⟫_ℂ - ⟪T (x - y), x - y⟫_ℂ + Complex.I * ⟪T (x + Complex.I • y), x + Complex.I • y⟫_ℂ -
        Complex.I * ⟪T (x - Complex.I • y), x - Complex.I • y⟫_ℂ) /
      4

Tactic:
simp only [map_add, map_sub, inner_add_left, inner_add_right, LinearMap.map_smul, inner_smul_left,
  inner_smul_right, Complex.conj_I, ← pow_two, Complex.I_sq, inner_sub_left, inner_sub_right,
  mul_add, ← mul_assoc, mul_neg, neg_neg, sub_neg_eq_add, one_mul, neg_one_mul, mul_sub, sub_sub]

Result:
V : Type u_4
inst✝¹ : SeminormedAddCommGroup V
inst✝ : InnerProductSpace ℂ V
T : V →ₗ[ℂ] V
x y : V
⊢ ⟪T y, x⟫_ℂ =
    (⟪T x, x⟫_ℂ + ⟪T y, x⟫_ℂ + (⟪T x, y⟫_ℂ + ⟪T y, y⟫_ℂ) - (⟪T x, x⟫_ℂ - (⟪T y, x⟫_ℂ + (⟪T x, y⟫_ℂ - ⟪T y, y⟫_ℂ))) +
          (Complex.I * ⟪T x, x⟫_ℂ + ⟪T y, x⟫_ℂ + (-⟪T x, y⟫_ℂ + Complex.I * ⟪T y, y⟫_ℂ)) -
        (Complex.I * ⟪T x, x⟫_ℂ - (⟪T y, x⟫_ℂ + (-⟪T x, y⟫_ℂ - Complex.I * ⟪T y, y⟫_ℂ)))) /
      4
-- Mathlib/Algebra/Order/CauSeq/Basic.lean
theorem not_limZero_of_not_congr_zero {f : CauSeq _ abv} (hf : ¬f ≈ 0) : ¬LimZero f

Proof state:
α : Type u_1
β : Type u_2
inst✝² : LinearOrderedField α
inst✝¹ : Ring β
abv : β → α
inst✝ : IsAbsoluteValue abv
f : CauSeq β abv
hf : ¬f ≈ 0
h : f.LimZero
⊢ False

Tactic:
have : LimZero (f - 0) := by simp [h]

Result:
α : Type u_1
β : Type u_2
inst✝² : LinearOrderedField α
inst✝¹ : Ring β
abv : β → α
inst✝ : IsAbsoluteValue abv
f : CauSeq β abv
hf : ¬f ≈ 0
h : f.LimZero
this : (f - 0).LimZero
⊢ False

Proof state:
α : Type u_1
β : Type u_2
inst✝² : LinearOrderedField α
inst✝¹ : Ring β
abv : β → α
inst✝ : IsAbsoluteValue abv
f : CauSeq β abv
hf : ¬f ≈ 0
h : f.LimZero
this : (f - 0).LimZero
⊢ False

Tactic:
exact hf this

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
inst✝² : LinearOrderedField α
inst✝¹ : Ring β
abv : β → α
inst✝ : IsAbsoluteValue abv
f : CauSeq β abv
hf : ¬f ≈ 0
⊢ ¬f.LimZero

Tactic:
intro h

Result:
α : Type u_1
β : Type u_2
inst✝² : LinearOrderedField α
inst✝¹ : Ring β
abv : β → α
inst✝ : IsAbsoluteValue abv
f : CauSeq β abv
hf : ¬f ≈ 0
h : f.LimZero
⊢ False

Proof state:
α : Type u_1
β : Type u_2
inst✝² : LinearOrderedField α
inst✝¹ : Ring β
abv : β → α
inst✝ : IsAbsoluteValue abv
f : CauSeq β abv
hf : ¬f ≈ 0
h : f.LimZero
⊢ (f - 0).LimZero

Tactic:
simp [h]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Pow/Continuity.lean
theorem rpow_eq_nhds_of_pos {p : ℝ × ℝ} (hp_fst : 0 < p.fst) :
    (fun x : ℝ × ℝ => x.1 ^ x.2) =ᶠ[𝓝 p] fun x => exp (log x.1 * x.2)

Proof state:
p : ℝ × ℝ
hp_fst : 0 < p.1
⊢ (fun x => x.1 ^ x.2) =ᶠ[𝓝 p] fun x => rexp (log x.1 * x.2)

Tactic:
suffices ∀ᶠ x : ℝ × ℝ in 𝓝 p, 0 < x.1 from
  this.mono fun x hx ↦ by
    dsimp only
    rw [rpow_def_of_pos hx]

Result:
p : ℝ × ℝ
hp_fst : 0 < p.1
⊢ ∀ᶠ (x : ℝ × ℝ) in 𝓝 p, 0 < x.1

Proof state:
p : ℝ × ℝ
hp_fst : 0 < p.1
this : ∀ᶠ (x : ℝ × ℝ) in 𝓝 p, 0 < x.1
x : ℝ × ℝ
hx : 0 < x.1
⊢ x.1 ^ x.2 = rexp (log x.1 * x.2)

Tactic:
rw [rpow_def_of_pos hx]

Result:
no goals

Proof state:
p : ℝ × ℝ
hp_fst : 0 < p.1
⊢ ∀ᶠ (x : ℝ × ℝ) in 𝓝 p, 0 < x.1

Tactic:
exact IsOpen.eventually_mem (isOpen_lt continuous_const continuous_fst) hp_fst

Result:
no goals

Proof state:
p : ℝ × ℝ
hp_fst : 0 < p.1
this : ∀ᶠ (x : ℝ × ℝ) in 𝓝 p, 0 < x.1
x : ℝ × ℝ
hx : 0 < x.1
⊢ (fun x => x.1 ^ x.2) x = (fun x => rexp (log x.1 * x.2)) x

Tactic:
dsimp only

Result:
p : ℝ × ℝ
hp_fst : 0 < p.1
this : ∀ᶠ (x : ℝ × ℝ) in 𝓝 p, 0 < x.1
x : ℝ × ℝ
hx : 0 < x.1
⊢ x.1 ^ x.2 = rexp (log x.1 * x.2)
-- Mathlib/Topology/Algebra/Monoid.lean
theorem exists_nhds_one_split4 {u : Set M} (hu : u ∈ 𝓝 (1 : M)) :
    ∃ V ∈ 𝓝 (1 : M), ∀ {v w s t}, v ∈ V → w ∈ V → s ∈ V → t ∈ V → v * w * s * t ∈ u

Proof state:
case intro.intro.intro.intro
M : Type u_3
inst✝² : TopologicalSpace M
inst✝¹ : Monoid M
inst✝ : ContinuousMul M
u : Set M
hu : u ∈ 𝓝 1
W : Set M
W1 : W ∈ 𝓝 1
h : ∀ v ∈ W, ∀ w ∈ W, v * w ∈ u
V : Set M
V1 : V ∈ 𝓝 1
h' : ∀ v ∈ V, ∀ w ∈ V, v * w ∈ W
⊢ ∃ V ∈ 𝓝 1, ∀ {v w s t : M}, v ∈ V → w ∈ V → s ∈ V → t ∈ V → v * w * s * t ∈ u

Tactic:
use V, V1

Result:
case right
M : Type u_3
inst✝² : TopologicalSpace M
inst✝¹ : Monoid M
inst✝ : ContinuousMul M
u : Set M
hu : u ∈ 𝓝 1
W : Set M
W1 : W ∈ 𝓝 1
h : ∀ v ∈ W, ∀ w ∈ W, v * w ∈ u
V : Set M
V1 : V ∈ 𝓝 1
h' : ∀ v ∈ V, ∀ w ∈ V, v * w ∈ W
⊢ ∀ {v w s t : M}, v ∈ V → w ∈ V → s ∈ V → t ∈ V → v * w * s * t ∈ u

Proof state:
case intro.intro
M : Type u_3
inst✝² : TopologicalSpace M
inst✝¹ : Monoid M
inst✝ : ContinuousMul M
u : Set M
hu : u ∈ 𝓝 1
W : Set M
W1 : W ∈ 𝓝 1
h : ∀ v ∈ W, ∀ w ∈ W, v * w ∈ u
⊢ ∃ V ∈ 𝓝 1, ∀ {v w s t : M}, v ∈ V → w ∈ V → s ∈ V → t ∈ V → v * w * s * t ∈ u

Tactic:
rcases exists_nhds_one_split W1 with ⟨V, V1, h'⟩

Result:
case intro.intro.intro.intro
M : Type u_3
inst✝² : TopologicalSpace M
inst✝¹ : Monoid M
inst✝ : ContinuousMul M
u : Set M
hu : u ∈ 𝓝 1
W : Set M
W1 : W ∈ 𝓝 1
h : ∀ v ∈ W, ∀ w ∈ W, v * w ∈ u
V : Set M
V1 : V ∈ 𝓝 1
h' : ∀ v ∈ V, ∀ w ∈ V, v * w ∈ W
⊢ ∃ V ∈ 𝓝 1, ∀ {v w s t : M}, v ∈ V → w ∈ V → s ∈ V → t ∈ V → v * w * s * t ∈ u

Proof state:
case right
M : Type u_3
inst✝² : TopologicalSpace M
inst✝¹ : Monoid M
inst✝ : ContinuousMul M
u : Set M
hu : u ∈ 𝓝 1
W : Set M
W1 : W ∈ 𝓝 1
h : ∀ v ∈ W, ∀ w ∈ W, v * w ∈ u
V : Set M
V1 : V ∈ 𝓝 1
h' : ∀ v ∈ V, ∀ w ∈ V, v * w ∈ W
v w s t : M
v_in : v ∈ V
w_in : w ∈ V
s_in : s ∈ V
t_in : t ∈ V
⊢ v * w * s * t ∈ u

Tactic:
simpa only [mul_assoc] using h _ (h' v v_in w w_in) _ (h' s s_in t t_in)

Result:
no goals

Proof state:
case right
M : Type u_3
inst✝² : TopologicalSpace M
inst✝¹ : Monoid M
inst✝ : ContinuousMul M
u : Set M
hu : u ∈ 𝓝 1
W : Set M
W1 : W ∈ 𝓝 1
h : ∀ v ∈ W, ∀ w ∈ W, v * w ∈ u
V : Set M
V1 : V ∈ 𝓝 1
h' : ∀ v ∈ V, ∀ w ∈ V, v * w ∈ W
⊢ ∀ {v w s t : M}, v ∈ V → w ∈ V → s ∈ V → t ∈ V → v * w * s * t ∈ u

Tactic:
intro v w s t v_in w_in s_in t_in

Result:
case right
M : Type u_3
inst✝² : TopologicalSpace M
inst✝¹ : Monoid M
inst✝ : ContinuousMul M
u : Set M
hu : u ∈ 𝓝 1
W : Set M
W1 : W ∈ 𝓝 1
h : ∀ v ∈ W, ∀ w ∈ W, v * w ∈ u
V : Set M
V1 : V ∈ 𝓝 1
h' : ∀ v ∈ V, ∀ w ∈ V, v * w ∈ W
v w s t : M
v_in : v ∈ V
w_in : w ∈ V
s_in : s ∈ V
t_in : t ∈ V
⊢ v * w * s * t ∈ u

Proof state:
M : Type u_3
inst✝² : TopologicalSpace M
inst✝¹ : Monoid M
inst✝ : ContinuousMul M
u : Set M
hu : u ∈ 𝓝 1
⊢ ∃ V ∈ 𝓝 1, ∀ {v w s t : M}, v ∈ V → w ∈ V → s ∈ V → t ∈ V → v * w * s * t ∈ u

Tactic:
rcases exists_nhds_one_split hu with ⟨W, W1, h⟩

Result:
case intro.intro
M : Type u_3
inst✝² : TopologicalSpace M
inst✝¹ : Monoid M
inst✝ : ContinuousMul M
u : Set M
hu : u ∈ 𝓝 1
W : Set M
W1 : W ∈ 𝓝 1
h : ∀ v ∈ W, ∀ w ∈ W, v * w ∈ u
⊢ ∃ V ∈ 𝓝 1, ∀ {v w s t : M}, v ∈ V → w ∈ V → s ∈ V → t ∈ V → v * w * s * t ∈ u
-- Mathlib/CategoryTheory/Limits/Shapes/WideEqualizers.lean
theorem Trident.app_zero (s : Trident f) (j : J) : s.π.app zero ≫ f j = s.π.app one

Proof state:
J : Type w
C : Type u
inst✝ : Category.{v, u} C
X Y : C
f : J → (X ⟶ Y)
s : Trident f
j : J
⊢ s.π.app zero ≫ f j = s.π.app one

Tactic:
rw [← s.w (line j), parallelFamily_map_left]

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Operations.lean
lemma edge_self_eq_bot : edge s s = ⊥

Proof state:
V : Type u_1
s : V
⊢ edge s s = ⊥

Tactic:
ext

Result:
case Adj.h.h.a
V : Type u_1
s x✝¹ x✝ : V
⊢ (edge s s).Adj x✝¹ x✝ ↔ ⊥.Adj x✝¹ x✝

Proof state:
case Adj.h.h.a
V : Type u_1
s x✝¹ x✝ : V
⊢ (edge s s).Adj x✝¹ x✝ ↔ ⊥.Adj x✝¹ x✝

Tactic:
rw [edge_adj]

Result:
case Adj.h.h.a
V : Type u_1
s x✝¹ x✝ : V
⊢ (x✝¹ = s ∧ x✝ = s ∨ x✝¹ = s ∧ x✝ = s) ∧ x✝¹ ≠ x✝ ↔ ⊥.Adj x✝¹ x✝

Proof state:
case Adj.h.h.a
V : Type u_1
s x✝¹ x✝ : V
⊢ (x✝¹ = s ∧ x✝ = s ∨ x✝¹ = s ∧ x✝ = s) ∧ x✝¹ ≠ x✝ ↔ ⊥.Adj x✝¹ x✝

Tactic:
aesop

Result:
no goals
-- Mathlib/RingTheory/HahnSeries/Basic.lean
theorem order_eq_orderTop_of_ne {x : HahnSeries Γ R} (hx : x ≠ 0) : order x = orderTop x

Proof state:
Γ : Type u_1
R : Type u_3
inst✝² : PartialOrder Γ
inst✝¹ : Zero R
inst✝ : Zero Γ
x : HahnSeries Γ R
hx : x ≠ 0
⊢ ↑x.order = x.orderTop

Tactic:
rw [order_of_ne hx, orderTop_of_ne hx]

Result:
no goals
-- Mathlib/CategoryTheory/Abelian/RightDerived.lean
@[reassoc]
lemma InjectiveResolution.isoRightDerivedObj_inv_naturality
    {X Y : C} (f : X ⟶ Y) (I : InjectiveResolution X) (J : InjectiveResolution Y)
    (φ : I.cocomplex ⟶ J.cocomplex) (comm : I.ι.f 0 ≫ φ.f 0 = f ≫ J.ι.f 0)
    (F : C ⥤ D) [F.Additive] (n : ℕ) :
    (I.isoRightDerivedObj F n).inv ≫ (F.rightDerived n).map f =
        (F.mapHomologicalComplex _ ⋙ HomologicalComplex.homologyFunctor _ _ n).map φ ≫
          (J.isoRightDerivedObj F n).inv

Proof state:
C : Type u
inst✝⁵ : Category.{v, u} C
D : Type u_1
inst✝⁴ : Category.{u_2, u_1} D
inst✝³ : Abelian C
inst✝² : HasInjectiveResolutions C
inst✝¹ : Abelian D
X Y : C
f : X ⟶ Y
I : InjectiveResolution X
J : InjectiveResolution Y
φ : I.cocomplex ⟶ J.cocomplex
comm : I.ι.f 0 ≫ φ.f 0 = f ≫ J.ι.f 0
F : C ⥤ D
inst✝ : F.Additive
n : ℕ
⊢ (I.isoRightDerivedObj F n).inv ≫ (F.rightDerived n).map f =
    (F.mapHomologicalComplex (ComplexShape.up ℕ) ⋙ HomologicalComplex.homologyFunctor D (ComplexShape.up ℕ) n).map φ ≫
      (J.isoRightDerivedObj F n).inv

Tactic:
rw [← cancel_mono (J.isoRightDerivedObj F n).hom, assoc, assoc,
  InjectiveResolution.isoRightDerivedObj_hom_naturality f I J φ comm F n,
  Iso.inv_hom_id_assoc, Iso.inv_hom_id, comp_id]

Result:
no goals
-- Mathlib/Geometry/Manifold/ContMDiff/Defs.lean
theorem contMDiffAt_iff_target_of_mem_source
    [IsManifold I' n M'] {x : M} {y : M'} (hy : f x ∈ (chartAt H' y).source) :
    ContMDiffAt I I' n f x ↔
      ContinuousAt f x ∧ ContMDiffAt I 𝓘(𝕜, E') n (extChartAt I' y ∘ f) x

Proof state:
𝕜 : Type u_1
inst✝¹¹ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedSpace 𝕜 E
H : Type u_3
inst✝⁸ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝⁷ : TopologicalSpace M
inst✝⁶ : ChartedSpace H M
E' : Type u_5
inst✝⁵ : NormedAddCommGroup E'
inst✝⁴ : NormedSpace 𝕜 E'
H' : Type u_6
inst✝³ : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst✝² : TopologicalSpace M'
inst✝¹ : ChartedSpace H' M'
f : M → M'
n : WithTop ℕ∞
inst✝ : IsManifold I' n M'
x : M
y : M'
hy : f x ∈ (chartAt H' y).source
⊢ ContMDiffAt I I' n f x ↔ ContinuousAt f x ∧ ContMDiffAt I 𝓘(𝕜, E') n (↑(extChartAt I' y) ∘ f) x

Tactic:
rw [ContMDiffAt, contMDiffWithinAt_iff_target_of_mem_source hy, continuousWithinAt_univ,
  ContMDiffAt]

Result:
no goals