harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/RingTheory/PowerBasis.lean
theorem constr_pow_mul (pb : PowerBasis A S) {y : S'} (hy : aeval y (minpoly A pb.gen) = 0)
    (x x' : S) : pb.basis.constr A (fun i => y ^ (i : ℕ)) (x * x') =
      pb.basis.constr A (fun i => y ^ (i : ℕ)) x * pb.basis.constr A (fun i => y ^ (i : ℕ)) x'

Proof state:
S : Type u_2
inst✝⁴ : Ring S
A : Type u_4
inst✝³ : CommRing A
inst✝² : Algebra A S
S' : Type u_7
inst✝¹ : Ring S'
inst✝ : Algebra A S'
pb : PowerBasis A S
y : S'
hy : (aeval y) (minpoly A pb.gen) = 0
x x' : S
⊢ ((pb.basis.constr A) fun i => y ^ ↑i) (x * x') =
    ((pb.basis.constr A) fun i => y ^ ↑i) x * ((pb.basis.constr A) fun i => y ^ ↑i) x'

Tactic:
obtain ⟨f, rfl⟩ := pb.exists_eq_aeval' x

Result:
case intro
S : Type u_2
inst✝⁴ : Ring S
A : Type u_4
inst✝³ : CommRing A
inst✝² : Algebra A S
S' : Type u_7
inst✝¹ : Ring S'
inst✝ : Algebra A S'
pb : PowerBasis A S
y : S'
hy : (aeval y) (minpoly A pb.gen) = 0
x' : S
f : A[X]
⊢ ((pb.basis.constr A) fun i => y ^ ↑i) ((aeval pb.gen) f * x') =
    ((pb.basis.constr A) fun i => y ^ ↑i) ((aeval pb.gen) f) * ((pb.basis.constr A) fun i => y ^ ↑i) x'

Proof state:
case intro
S : Type u_2
inst✝⁴ : Ring S
A : Type u_4
inst✝³ : CommRing A
inst✝² : Algebra A S
S' : Type u_7
inst✝¹ : Ring S'
inst✝ : Algebra A S'
pb : PowerBasis A S
y : S'
hy : (aeval y) (minpoly A pb.gen) = 0
x' : S
f : A[X]
⊢ ((pb.basis.constr A) fun i => y ^ ↑i) ((aeval pb.gen) f * x') =
    ((pb.basis.constr A) fun i => y ^ ↑i) ((aeval pb.gen) f) * ((pb.basis.constr A) fun i => y ^ ↑i) x'

Tactic:
obtain ⟨g, rfl⟩ := pb.exists_eq_aeval' x'

Result:
case intro.intro
S : Type u_2
inst✝⁴ : Ring S
A : Type u_4
inst✝³ : CommRing A
inst✝² : Algebra A S
S' : Type u_7
inst✝¹ : Ring S'
inst✝ : Algebra A S'
pb : PowerBasis A S
y : S'
hy : (aeval y) (minpoly A pb.gen) = 0
f g : A[X]
⊢ ((pb.basis.constr A) fun i => y ^ ↑i) ((aeval pb.gen) f * (aeval pb.gen) g) =
    ((pb.basis.constr A) fun i => y ^ ↑i) ((aeval pb.gen) f) * ((pb.basis.constr A) fun i => y ^ ↑i) ((aeval pb.gen) g)

Proof state:
case intro.intro
S : Type u_2
inst✝⁴ : Ring S
A : Type u_4
inst✝³ : CommRing A
inst✝² : Algebra A S
S' : Type u_7
inst✝¹ : Ring S'
inst✝ : Algebra A S'
pb : PowerBasis A S
y : S'
hy : (aeval y) (minpoly A pb.gen) = 0
f g : A[X]
⊢ ((pb.basis.constr A) fun i => y ^ ↑i) ((aeval pb.gen) f * (aeval pb.gen) g) =
    ((pb.basis.constr A) fun i => y ^ ↑i) ((aeval pb.gen) f) * ((pb.basis.constr A) fun i => y ^ ↑i) ((aeval pb.gen) g)

Tactic:
simp only [← aeval_mul, pb.constr_pow_aeval hy]

Result:
no goals
-- Mathlib/Algebra/Group/End.lean
theorem sigmaCongrRightHom_injective {α : Type*} {β : α → Type*} :
    Function.Injective (sigmaCongrRightHom β)

Proof state:
α : Type u_6
β : α → Type u_7
x y : (a : α) → Perm (β a)
h : (sigmaCongrRightHom β) x = (sigmaCongrRightHom β) y
⊢ x = y

Tactic:
ext a b

Result:
case h.H
α : Type u_6
β : α → Type u_7
x y : (a : α) → Perm (β a)
h : (sigmaCongrRightHom β) x = (sigmaCongrRightHom β) y
a : α
b : β a
⊢ (x a) b = (y a) b

Proof state:
case h.H
α : Type u_6
β : α → Type u_7
x y : (a : α) → Perm (β a)
h : (sigmaCongrRightHom β) x = (sigmaCongrRightHom β) y
a : α
b : β a
⊢ (x a) b = (y a) b

Tactic:
simpa using Equiv.congr_fun h ⟨a, b⟩

Result:
no goals

Proof state:
α : Type u_6
β : α → Type u_7
⊢ Function.Injective ⇑(sigmaCongrRightHom β)

Tactic:
intro x y h

Result:
α : Type u_6
β : α → Type u_7
x y : (a : α) → Perm (β a)
h : (sigmaCongrRightHom β) x = (sigmaCongrRightHom β) y
⊢ x = y
-- Mathlib/LinearAlgebra/Determinant.lean
theorem Basis.det_ne_zero [Nontrivial R] : e.det ≠ 0 := fun h => by simpa [h] using e.det_self

Proof state:
R : Type u_1
inst✝⁵ : CommRing R
M : Type u_2
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
ι : Type u_4
inst✝² : DecidableEq ι
inst✝¹ : Fintype ι
e : Basis ι R M
inst✝ : Nontrivial R
h : e.det = 0
⊢ False

Tactic:
simpa [h] using e.det_self

Result:
no goals
-- Mathlib/Algebra/Group/ForwardDiff.lean
@[simp] lemma fwdDiff_iter_add (f g : M → G) (n : ℕ) :
    Δ_[h]^[n] (f + g) = Δ_[h]^[n] f + Δ_[h]^[n] g

Proof state:
M : Type u_1
G : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : AddCommGroup G
h : M
f g : M → G
n : ℕ
⊢ Δ_[h]^[n] (f + g) = Δ_[h]^[n] f + Δ_[h]^[n] g

Tactic:
simpa only [coe_fwdDiffₗ_pow] using map_add (fwdDiffₗ M G h ^ n) f g

Result:
no goals
-- Mathlib/Data/Complex/Exponential.lean
theorem isCauSeq_norm_exp (z : ℂ) :
    IsCauSeq abs fun n => ∑ m ∈ range n, ‖z ^ m / m.factorial‖ :=
  let ⟨n, hn⟩ := exists_nat_gt ‖z‖
  have hn0 : (0 : ℝ) < n := lt_of_le_of_lt (norm_nonneg _) hn
  IsCauSeq.series_ratio_test n (‖z‖ / n) (div_nonneg (norm_nonneg _) (le_of_lt hn0))
    (by rwa [div_lt_iff₀ hn0, one_mul]) fun m hm => by
      rw [abs_norm, abs_norm, Nat.factorial_succ, pow_succ', mul_comm m.succ, Nat.cast_mul,
        ← div_div, mul_div_assoc, mul_div_right_comm, Complex.norm_mul, Complex.norm_div,
        norm_natCast]
      gcongr
      exact le_trans hm (Nat.le_succ _)

Proof state:
z : ℂ
n : ℕ
hn : ‖z‖ < ↑n
hn0 : 0 < ↑n
⊢ ‖z‖ / ↑n < 1

Tactic:
rwa [div_lt_iff₀ hn0, one_mul]

Result:
no goals

Proof state:
case h.h.h
z : ℂ
n : ℕ
hn : ‖z‖ < ↑n
hn0 : 0 < ↑n
m : ℕ
hm : n ≤ m
⊢ n ≤ m.succ

Tactic:
exact le_trans hm (Nat.le_succ _)

Result:
no goals

Proof state:
z : ℂ
n : ℕ
hn : ‖z‖ < ↑n
hn0 : 0 < ↑n
m : ℕ
hm : n ≤ m
⊢ |‖z ^ m.succ / ↑m.succ.factorial‖| ≤ ‖z‖ / ↑n * |‖z ^ m / ↑m.factorial‖|

Tactic:
rw [abs_norm, abs_norm, Nat.factorial_succ, pow_succ', mul_comm m.succ, Nat.cast_mul,
  ← div_div, mul_div_assoc, mul_div_right_comm, Complex.norm_mul, Complex.norm_div,
  norm_natCast]

Result:
z : ℂ
n : ℕ
hn : ‖z‖ < ↑n
hn0 : 0 < ↑n
m : ℕ
hm : n ≤ m
⊢ ‖z‖ / ↑m.succ * ‖z ^ m / ↑m.factorial‖ ≤ ‖z‖ / ↑n * ‖z ^ m / ↑m.factorial‖

Proof state:
z : ℂ
n : ℕ
hn : ‖z‖ < ↑n
hn0 : 0 < ↑n
m : ℕ
hm : n ≤ m
⊢ ‖z‖ / ↑m.succ * ‖z ^ m / ↑m.factorial‖ ≤ ‖z‖ / ↑n * ‖z ^ m / ↑m.factorial‖

Tactic:
gcongr

Result:
case h.h.h
z : ℂ
n : ℕ
hn : ‖z‖ < ↑n
hn0 : 0 < ↑n
m : ℕ
hm : n ≤ m
⊢ n ≤ m.succ
-- Mathlib/Data/Finsupp/Weight.lean
theorem le_degree {R : Type*} [OrderedAddCommMonoid R] [CanonicallyOrderedAdd R]
    (s : σ) (f : σ →₀ R) :
    f s ≤ degree f

Proof state:
case pos
σ : Type u_1
R : Type u_5
inst✝¹ : OrderedAddCommMonoid R
inst✝ : CanonicallyOrderedAdd R
s : σ
f : σ →₀ R
h : s ∈ f.support
⊢ f s ≤ f.degree

Tactic:
exact CanonicallyOrderedAddCommMonoid.single_le_sum h

Result:
no goals

Proof state:
σ : Type u_1
R : Type u_5
inst✝¹ : OrderedAddCommMonoid R
inst✝ : CanonicallyOrderedAdd R
s : σ
f : σ →₀ R
⊢ f s ≤ f.degree

Tactic:
by_cases h : s ∈ f.support

Result:
case pos
σ : Type u_1
R : Type u_5
inst✝¹ : OrderedAddCommMonoid R
inst✝ : CanonicallyOrderedAdd R
s : σ
f : σ →₀ R
h : s ∈ f.support
⊢ f s ≤ f.degree

case neg
σ : Type u_1
R : Type u_5
inst✝¹ : OrderedAddCommMonoid R
inst✝ : CanonicallyOrderedAdd R
s : σ
f : σ →₀ R
h : s ∉ f.support
⊢ f s ≤ f.degree

Proof state:
case neg
σ : Type u_1
R : Type u_5
inst✝¹ : OrderedAddCommMonoid R
inst✝ : CanonicallyOrderedAdd R
s : σ
f : σ →₀ R
h : s ∉ f.support
⊢ f s ≤ f.degree

Tactic:
simp only [not_mem_support_iff] at h

Result:
case neg
σ : Type u_1
R : Type u_5
inst✝¹ : OrderedAddCommMonoid R
inst✝ : CanonicallyOrderedAdd R
s : σ
f : σ →₀ R
h : f s = 0
⊢ f s ≤ f.degree

Proof state:
case neg
σ : Type u_1
R : Type u_5
inst✝¹ : OrderedAddCommMonoid R
inst✝ : CanonicallyOrderedAdd R
s : σ
f : σ →₀ R
h : f s = 0
⊢ f s ≤ f.degree

Tactic:
simp only [h, zero_le]

Result:
no goals
-- Mathlib/Data/Multiset/Powerset.lean
theorem revzip_powersetAux_perm {l₁ l₂ : List α} (p : l₁ ~ l₂) :
    revzip (powersetAux l₁) ~ revzip (powersetAux l₂)

Proof state:
α : Type u_1
l₁ l₂ : List α
p : l₁ ~ l₂
this : DecidableEq α
⊢ List.map (fun x => (x, ↑l₂ - x)) (powersetAux l₁) ~ List.map (fun x => (x, ↑l₂ - x)) (powersetAux l₂)

Tactic:
exact (powersetAux_perm p).map _

Result:
no goals

Proof state:
α : Type u_1
l₁ l₂ : List α
p : l₁ ~ l₂
this : DecidableEq α
⊢ (powersetAux l₁).revzip ~ (powersetAux l₂).revzip

Tactic:
simp only [fun l : List α => revzip_powersetAux_lemma l revzip_powersetAux, coe_eq_coe.2 p]

Result:
α : Type u_1
l₁ l₂ : List α
p : l₁ ~ l₂
this : DecidableEq α
⊢ List.map (fun x => (x, ↑l₂ - x)) (powersetAux l₁) ~ List.map (fun x => (x, ↑l₂ - x)) (powersetAux l₂)

Proof state:
α : Type u_1
l₁ l₂ : List α
p : l₁ ~ l₂
⊢ (powersetAux l₁).revzip ~ (powersetAux l₂).revzip

Tactic:
haveI := Classical.decEq α

Result:
α : Type u_1
l₁ l₂ : List α
p : l₁ ~ l₂
this : DecidableEq α
⊢ (powersetAux l₁).revzip ~ (powersetAux l₂).revzip
-- Mathlib/MeasureTheory/Measure/DiracProba.lean
/-- In a T0 topological space equipped with a sigma algebra which contains all open sets,
the assignment `x ↦ diracProba x` is injective. -/
lemma injective_diracProba_of_T0 [T0Space X] :
    Function.Injective (fun (x : X) ↦ diracProba x)

Proof state:
X : Type u_1
inst✝³ : MeasurableSpace X
inst✝² : TopologicalSpace X
inst✝¹ : OpensMeasurableSpace X
inst✝ : T0Space X
x y : X
δx_eq_δy : (fun x => diracProba x) x = (fun x => diracProba x) y
⊢ x = y

Tactic:
by_contra x_ne_y

Result:
X : Type u_1
inst✝³ : MeasurableSpace X
inst✝² : TopologicalSpace X
inst✝¹ : OpensMeasurableSpace X
inst✝ : T0Space X
x y : X
δx_eq_δy : (fun x => diracProba x) x = (fun x => diracProba x) y
x_ne_y : ¬x = y
⊢ False

Proof state:
X : Type u_1
inst✝³ : MeasurableSpace X
inst✝² : TopologicalSpace X
inst✝¹ : OpensMeasurableSpace X
inst✝ : T0Space X
x y : X
δx_eq_δy : (fun x => diracProba x) x = (fun x => diracProba x) y
x_ne_y : ¬x = y
⊢ False

Tactic:
exact dirac_ne_dirac x_ne_y <| congr_arg Subtype.val δx_eq_δy

Result:
no goals

Proof state:
X : Type u_1
inst✝³ : MeasurableSpace X
inst✝² : TopologicalSpace X
inst✝¹ : OpensMeasurableSpace X
inst✝ : T0Space X
⊢ Function.Injective fun x => diracProba x

Tactic:
intro x y δx_eq_δy

Result:
X : Type u_1
inst✝³ : MeasurableSpace X
inst✝² : TopologicalSpace X
inst✝¹ : OpensMeasurableSpace X
inst✝ : T0Space X
x y : X
δx_eq_δy : (fun x => diracProba x) x = (fun x => diracProba x) y
⊢ x = y
-- Mathlib/Tactic/CategoryTheory/Bicategory/Normalize.lean
theorem evalWhiskerRight_nil (α : f ≅ g) (h : b ⟶ c) :
    α.hom ▷ h = α.hom ▷ h

Proof state:
B : Type u
inst✝ : Bicategory B
a b c : B
f g : a ⟶ b
α : f ≅ g
h : b ⟶ c
⊢ α.hom ▷ h = α.hom ▷ h

Tactic:
simp

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem toNat_shiftConcat_eq_of_lt {x : BitVec w} {b : Bool} {k : Nat}
    (hk : k < w) (hx : x.toNat < 2 ^ k) :
    (x.shiftConcat b).toNat = x.toNat * 2 + b.toNat

Proof state:
w : Nat
x : BitVec w
b : Bool
k : Nat
hk : k < w
hx : x.toNat < 2 ^ k
this : 2 ^ k < 2 ^ w
⊢ (x.toNat * 2 + b.toNat) % 2 ^ w = x.toNat * 2 + b.toNat

Tactic:
have : 2 ^ k * 2 ≤ 2 ^ w := (Nat.pow_lt_pow_iff_pow_mul_le_pow (by omega)).mp this

Result:
w : Nat
x : BitVec w
b : Bool
k : Nat
hk : k < w
hx : x.toNat < 2 ^ k
this✝ : 2 ^ k < 2 ^ w
this : 2 ^ k * 2 ≤ 2 ^ w
⊢ (x.toNat * 2 + b.toNat) % 2 ^ w = x.toNat * 2 + b.toNat

Proof state:
w : Nat
x : BitVec w
b : Bool
k : Nat
hk : k < w
hx : x.toNat < 2 ^ k
this✝ : 2 ^ k < 2 ^ w
this : 2 ^ k * 2 ≤ 2 ^ w
⊢ x.toNat * 2 + b.toNat < 2 ^ w

Tactic:
cases b <;> simp [bv_toNat] <;> omega

Result:
no goals

Proof state:
w : Nat
x : BitVec w
b : Bool
k : Nat
hk : k < w
hx : x.toNat < 2 ^ k
⊢ 1 < 2

Tactic:
omega

Result:
no goals

Proof state:
w : Nat
x : BitVec w
b : Bool
k : Nat
hk : k < w
hx : x.toNat < 2 ^ k
⊢ (x.toNat * 2 + b.toNat) % 2 ^ w = x.toNat * 2 + b.toNat

Tactic:
have : 2 ^ k < 2 ^ w := Nat.pow_lt_pow_of_lt (by omega) (by omega)

Result:
w : Nat
x : BitVec w
b : Bool
k : Nat
hk : k < w
hx : x.toNat < 2 ^ k
this : 2 ^ k < 2 ^ w
⊢ (x.toNat * 2 + b.toNat) % 2 ^ w = x.toNat * 2 + b.toNat

Proof state:
w : Nat
x : BitVec w
b : Bool
k : Nat
hk : k < w
hx : x.toNat < 2 ^ k
this✝ : 2 ^ k < 2 ^ w
this : 2 ^ k * 2 ≤ 2 ^ w
⊢ (x.toNat * 2 + b.toNat) % 2 ^ w = x.toNat * 2 + b.toNat

Tactic:
rw [Nat.mod_eq_of_lt (by cases b <;> simp [bv_toNat] <;> omega)]

Result:
no goals

Proof state:
w : Nat
x : BitVec w
b : Bool
k : Nat
hk : k < w
hx : x.toNat < 2 ^ k
⊢ (x.shiftConcat b).toNat = x.toNat * 2 + b.toNat

Tactic:
simp only [toNat_shiftConcat, Nat.shiftLeft_eq, Nat.pow_one]

Result:
w : Nat
x : BitVec w
b : Bool
k : Nat
hk : k < w
hx : x.toNat < 2 ^ k
⊢ (x.toNat * 2 + b.toNat) % 2 ^ w = x.toNat * 2 + b.toNat

Proof state:
w : Nat
x : BitVec w
b : Bool
k : Nat
hk : k < w
hx : x.toNat < 2 ^ k
this : 2 ^ k < 2 ^ w
⊢ 1 < 2

Tactic:
omega

Result:
no goals

Proof state:
w : Nat
x : BitVec w
b : Bool
k : Nat
hk : k < w
hx : x.toNat < 2 ^ k
⊢ k < w

Tactic:
omega

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Nat/Dvd.lean
theorem mul_div_assoc (m : Nat) (H : k ∣ n) : m * n / k = m * (n / k)

Proof state:
k n m : Nat
H : k ∣ n
⊢ m * n / k = m * (n / k)

Tactic:
match Nat.eq_zero_or_pos k with
| .inl h0 => rw [h0, Nat.div_zero, Nat.div_zero, Nat.mul_zero]
| .inr hpos =>
  have h1 : m * n / k = m * (n / k * k) / k := by rw [Nat.div_mul_cancel H]
  rw [h1, ← Nat.mul_assoc, Nat.mul_div_cancel _ hpos]

Result:
no goals

Proof state:
k n m : Nat
H : k ∣ n
hpos : k > 0
⊢ m * n / k = m * (n / k * k) / k

Tactic:
rw [Nat.div_mul_cancel H]

Result:
no goals

Proof state:
k n m : Nat
H : k ∣ n
hpos : k > 0
h1 : m * n / k = m * (n / k * k) / k
⊢ m * n / k = m * (n / k)

Tactic:
rw [h1, ← Nat.mul_assoc, Nat.mul_div_cancel _ hpos]

Result:
no goals

Proof state:
k n m : Nat
H : k ∣ n
h0 : k = 0
⊢ m * n / k = m * (n / k)

Tactic:
rw [h0, Nat.div_zero, Nat.div_zero, Nat.mul_zero]

Result:
no goals

Proof state:
k n m : Nat
H : k ∣ n
hpos : k > 0
⊢ m * n / k = m * (n / k)

Tactic:
have h1 : m * n / k = m * (n / k * k) / k := by rw [Nat.div_mul_cancel H]

Result:
k n m : Nat
H : k ∣ n
hpos : k > 0
h1 : m * n / k = m * (n / k * k) / k
⊢ m * n / k = m * (n / k)
-- Mathlib/Data/Finset/Empty.lean
theorem eq_empty_iff_forall_not_mem {s : Finset α} : s = ∅ ↔ ∀ x, x ∉ s :=
  -- Porting note: used `id`
  ⟨by rintro rfl x; apply not_mem_empty, fun h => eq_empty_of_forall_not_mem h⟩

Proof state:
α : Type u_1
s : Finset α
⊢ s = ∅ → ∀ (x : α), x ∉ s

Tactic:
rintro rfl x

Result:
α : Type u_1
x : α
⊢ x ∉ ∅

Proof state:
α : Type u_1
x : α
⊢ x ∉ ∅

Tactic:
apply not_mem_empty

Result:
no goals
-- Mathlib/Analysis/Convex/EGauge.lean
/-- If `c • x ∈ s` and `c ≠ 0`, then `egauge 𝕜 s x` is at most `(‖c‖₊⁻¹ : ℝ≥0)`.

See also `egauge_le_of_smul_mem`. -/
lemma egauge_le_of_smul_mem_of_ne (h : c • x ∈ s) (hc : c ≠ 0) : egauge 𝕜 s x ≤ (‖c‖₊⁻¹ : ℝ≥0)

Proof state:
𝕜 : Type u_1
inst✝² : NormedDivisionRing 𝕜
E : Type u_2
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
c : 𝕜
s : Set E
x : E
h : c • x ∈ s
hc : c ≠ 0
⊢ egauge 𝕜 s x ≤ ↑‖c⁻¹‖₊

Tactic:
exact egauge_le_of_mem_smul <| (mem_inv_smul_set_iff₀ hc _ _).2 h

Result:
no goals

Proof state:
𝕜 : Type u_1
inst✝² : NormedDivisionRing 𝕜
E : Type u_2
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
c : 𝕜
s : Set E
x : E
h : c • x ∈ s
hc : c ≠ 0
⊢ egauge 𝕜 s x ≤ ↑‖c‖₊⁻¹

Tactic:
rw [← nnnorm_inv]

Result:
𝕜 : Type u_1
inst✝² : NormedDivisionRing 𝕜
E : Type u_2
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
c : 𝕜
s : Set E
x : E
h : c • x ∈ s
hc : c ≠ 0
⊢ egauge 𝕜 s x ≤ ↑‖c⁻¹‖₊
-- Mathlib/Analysis/SpecialFunctions/Pow/Continuity.lean
theorem rpow_eq_nhds_of_neg {p : ℝ × ℝ} (hp_fst : p.fst < 0) :
    (fun x : ℝ × ℝ => x.1 ^ x.2) =ᶠ[𝓝 p] fun x => exp (log x.1 * x.2) * cos (x.2 * π)

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

Tactic:
rw [rpow_def_of_neg hx]

Result:
no goals

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

Tactic:
dsimp only

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

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

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

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

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

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

Result:
no goals
-- Mathlib/Algebra/ContinuedFractions/Translations.lean
theorem first_den_eq {gp : Pair K} (zeroth_s_eq : g.s.get? 0 = some gp) :
    g.dens 1 = gp.b

Proof state:
K : Type u_1
g : GenContFract K
inst✝ : DivisionRing K
gp : Pair K
zeroth_s_eq : g.s.get? 0 = some gp
⊢ g.dens 1 = gp.b

Tactic:
simp [den_eq_conts_b, first_cont_eq zeroth_s_eq]

Result:
no goals
-- Mathlib/Topology/LocallyFinite.lean
theorem Equiv.locallyFinite_comp_iff (e : ι' ≃ ι) : LocallyFinite (f ∘ e) ↔ LocallyFinite f :=
  ⟨fun h => by simpa only [comp_def, e.apply_symm_apply] using h.comp_injective e.symm.injective,
    fun h => h.comp_injective e.injective⟩

Proof state:
ι : Type u_1
ι' : Type u_2
X : Type u_4
inst✝ : TopologicalSpace X
f : ι → Set X
e : ι' ≃ ι
h : LocallyFinite (f ∘ ⇑e)
⊢ LocallyFinite f

Tactic:
simpa only [comp_def, e.apply_symm_apply] using h.comp_injective e.symm.injective

Result:
no goals
-- Mathlib/Algebra/Lie/Weights/Basic.lean
lemma injOn_genWeightSpace [NoZeroSMulDivisors R M] :
    InjOn (fun (χ : L → R) ↦ genWeightSpace M χ) {χ | genWeightSpace M χ ≠ ⊥}

Proof state:
R : Type u_2
L : Type u_3
M : Type u_4
inst✝⁸ : CommRing R
inst✝⁷ : LieRing L
inst✝⁶ : LieAlgebra R L
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : LieRingModule L M
inst✝² : LieModule R L M
inst✝¹ : LieRing.IsNilpotent L
inst✝ : NoZeroSMulDivisors R M
χ₁ : L → R
a✝ : χ₁ ∈ {χ | genWeightSpace M χ ≠ ⊥}
χ₂ : L → R
hχ₂ : χ₂ ∈ {χ | genWeightSpace M χ ≠ ⊥}
hχ₁₂ : genWeightSpace M χ₁ = genWeightSpace M χ₂
⊢ χ₁ = χ₂

Tactic:
contrapose! hχ₂

Result:
R : Type u_2
L : Type u_3
M : Type u_4
inst✝⁸ : CommRing R
inst✝⁷ : LieRing L
inst✝⁶ : LieAlgebra R L
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : LieRingModule L M
inst✝² : LieModule R L M
inst✝¹ : LieRing.IsNilpotent L
inst✝ : NoZeroSMulDivisors R M
χ₁ : L → R
a✝ : χ₁ ∈ {χ | genWeightSpace M χ ≠ ⊥}
χ₂ : L → R
hχ₁₂ : genWeightSpace M χ₁ = genWeightSpace M χ₂
hχ₂ : χ₁ ≠ χ₂
⊢ χ₂ ∉ {χ | genWeightSpace M χ ≠ ⊥}

Proof state:
R : Type u_2
L : Type u_3
M : Type u_4
inst✝⁸ : CommRing R
inst✝⁷ : LieRing L
inst✝⁶ : LieAlgebra R L
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : LieRingModule L M
inst✝² : LieModule R L M
inst✝¹ : LieRing.IsNilpotent L
inst✝ : NoZeroSMulDivisors R M
χ₁ : L → R
a✝ : χ₁ ∈ {χ | genWeightSpace M χ ≠ ⊥}
χ₂ : L → R
hχ₁₂ : genWeightSpace M χ₁ = genWeightSpace M χ₂
hχ₂ : χ₁ ≠ χ₂
⊢ χ₂ ∉ {χ | genWeightSpace M χ ≠ ⊥}

Tactic:
simpa [hχ₁₂] using disjoint_genWeightSpace R L M hχ₂

Result:
no goals

Proof state:
R : Type u_2
L : Type u_3
M : Type u_4
inst✝⁸ : CommRing R
inst✝⁷ : LieRing L
inst✝⁶ : LieAlgebra R L
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : LieRingModule L M
inst✝² : LieModule R L M
inst✝¹ : LieRing.IsNilpotent L
inst✝ : NoZeroSMulDivisors R M
⊢ InjOn (fun χ => genWeightSpace M χ) {χ | genWeightSpace M χ ≠ ⊥}

Tactic:
rintro χ₁ _ χ₂ hχ₂ (hχ₁₂ : genWeightSpace M χ₁ = genWeightSpace M χ₂)

Result:
R : Type u_2
L : Type u_3
M : Type u_4
inst✝⁸ : CommRing R
inst✝⁷ : LieRing L
inst✝⁶ : LieAlgebra R L
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : LieRingModule L M
inst✝² : LieModule R L M
inst✝¹ : LieRing.IsNilpotent L
inst✝ : NoZeroSMulDivisors R M
χ₁ : L → R
a✝ : χ₁ ∈ {χ | genWeightSpace M χ ≠ ⊥}
χ₂ : L → R
hχ₂ : χ₂ ∈ {χ | genWeightSpace M χ ≠ ⊥}
hχ₁₂ : genWeightSpace M χ₁ = genWeightSpace M χ₂
⊢ χ₁ = χ₂
-- Mathlib/Data/Vector/Basic.lean
theorem ne_cons_iff (a : α) (v : Vector α n.succ) (v' : Vector α n) :
    v ≠ a ::ᵥ v' ↔ v.head ≠ a ∨ v.tail ≠ v'

Proof state:
α : Type u_1
n : ℕ
a : α
v : Vector α n.succ
v' : Vector α n
⊢ v ≠ a ::ᵥ v' ↔ v.head ≠ a ∨ v.tail ≠ v'

Tactic:
rw [Ne, eq_cons_iff a v v', not_and_or]

Result:
no goals
-- Mathlib/Data/Matrix/Block.lean
theorem blockDiagonal'_add [AddZeroClass α] (M N : ∀ i, Matrix (m' i) (n' i) α) :
    blockDiagonal' (M + N) = blockDiagonal' M + blockDiagonal' N

Proof state:
case a
o : Type u_4
m' : o → Type u_7
n' : o → Type u_8
α : Type u_12
inst✝¹ : DecidableEq o
inst✝ : AddZeroClass α
M N : (i : o) → Matrix (m' i) (n' i) α
i✝ : (i : o) × m' i
j✝ : (i : o) × n' i
⊢ (if h : i✝.fst = j✝.fst then M i✝.fst i✝.snd (cast ⋯ j✝.snd) + N i✝.fst i✝.snd (cast ⋯ j✝.snd) else 0) =
    (if h : i✝.fst = j✝.fst then M i✝.fst i✝.snd (cast ⋯ j✝.snd) else 0) +
      if h : i✝.fst = j✝.fst then N i✝.fst i✝.snd (cast ⋯ j✝.snd) else 0

Tactic:
split_ifs <;> simp

Result:
no goals

Proof state:
o : Type u_4
m' : o → Type u_7
n' : o → Type u_8
α : Type u_12
inst✝¹ : DecidableEq o
inst✝ : AddZeroClass α
M N : (i : o) → Matrix (m' i) (n' i) α
⊢ blockDiagonal' (M + N) = blockDiagonal' M + blockDiagonal' N

Tactic:
ext

Result:
case a
o : Type u_4
m' : o → Type u_7
n' : o → Type u_8
α : Type u_12
inst✝¹ : DecidableEq o
inst✝ : AddZeroClass α
M N : (i : o) → Matrix (m' i) (n' i) α
i✝ : (i : o) × m' i
j✝ : (i : o) × n' i
⊢ blockDiagonal' (M + N) i✝ j✝ = (blockDiagonal' M + blockDiagonal' N) i✝ j✝

Proof state:
case a
o : Type u_4
m' : o → Type u_7
n' : o → Type u_8
α : Type u_12
inst✝¹ : DecidableEq o
inst✝ : AddZeroClass α
M N : (i : o) → Matrix (m' i) (n' i) α
i✝ : (i : o) × m' i
j✝ : (i : o) × n' i
⊢ blockDiagonal' (M + N) i✝ j✝ = (blockDiagonal' M + blockDiagonal' N) i✝ j✝

Tactic:
simp only [blockDiagonal'_apply, Pi.add_apply, add_apply]

Result:
case a
o : Type u_4
m' : o → Type u_7
n' : o → Type u_8
α : Type u_12
inst✝¹ : DecidableEq o
inst✝ : AddZeroClass α
M N : (i : o) → Matrix (m' i) (n' i) α
i✝ : (i : o) × m' i
j✝ : (i : o) × n' i
⊢ (if h : i✝.fst = j✝.fst then M i✝.fst i✝.snd (cast ⋯ j✝.snd) + N i✝.fst i✝.snd (cast ⋯ j✝.snd) else 0) =
    (if h : i✝.fst = j✝.fst then M i✝.fst i✝.snd (cast ⋯ j✝.snd) else 0) +
      if h : i✝.fst = j✝.fst then N i✝.fst i✝.snd (cast ⋯ j✝.snd) else 0
-- Mathlib/Analysis/InnerProductSpace/Basic.lean
theorem norm_sub_eq_sqrt_iff_real_inner_eq_zero {x y : F} :
    ‖x - y‖ = √(‖x‖ * ‖x‖ + ‖y‖ * ‖y‖) ↔ ⟪x, y⟫_ℝ = 0

Proof state:
F : Type u_3
inst✝¹ : SeminormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
x y : F
⊢ ‖x - y‖ = √(‖x‖ * ‖x‖ + ‖y‖ * ‖y‖) ↔ ⟪x, y⟫_ℝ = 0

Tactic:
rw [← norm_sub_sq_eq_norm_sq_add_norm_sq_iff_real_inner_eq_zero, eq_comm, sqrt_eq_iff_mul_self_eq,
  eq_comm] <;> positivity

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Trigonometric/Angle.lean
theorem cos_zero : cos (0 : Angle) = 1

Proof state:
⊢ cos 0 = 1

Tactic:
rw [← coe_zero, cos_coe, Real.cos_zero]

Result:
no goals