harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Data/List/Basic.lean
theorem get_eq_getElem? (l : List α) (i : Fin l.length) :
    l.get i = l[i]?.get (by simp [getElem?_eq_getElem])

Proof state:
ι : Type u_1
α : Type u
β : Type v
γ : Type w
l₁ l₂ l : List α
i : Fin l.length
⊢ l[i]?.isSome = true

Tactic:
simp [getElem?_eq_getElem]

Result:
no goals

Proof state:
α : Type u
l : List α
i : Fin l.length
⊢ l.get i = l[i]?.get ⋯

Tactic:
simp

Result:
no goals
-- Mathlib/Data/Matroid/Closure.lean
lemma indep_iff_forall_closure_diff_ne :
    M.Indep I ↔ ∀ ⦃e⦄, e ∈ I → M.closure (I \ {e}) ≠ M.closure I

Proof state:
case refine_1
α : Type u_2
M : Matroid α
I : Set α
h : ∀ ⦃e : α⦄, e ∈ I → M.closure (I \ {e}) ≠ M.closure I
e : α
heI : e ∈ I
heE : e ∉ M.E
⊢ M.closure (I \ {e}) = M.closure I

Tactic:
rw [← closure_inter_ground, inter_comm, inter_diff_distrib_left,
  inter_singleton_eq_empty.mpr heE, diff_empty, inter_comm, closure_inter_ground]

Result:
no goals

Proof state:
α : Type u_2
M : Matroid α
I : Set α
h : ∀ ⦃e : α⦄, e ∈ I → M.closure (I \ {e}) ≠ M.closure I
e : α
heI : e ∈ I
hin : e ∈ M.closure (I \ {e})
⊢ I = insert e (I \ {e})

Tactic:
simp [heI]

Result:
no goals

Proof state:
case refine_2
α : Type u_2
M : Matroid α
I : Set α
h : ∀ ⦃e : α⦄, e ∈ I → M.closure (I \ {e}) ≠ M.closure I
e : α
heI : e ∈ I
hin : e ∈ M.closure (I \ {e})
⊢ M.closure (I \ {e}) = M.closure I

Tactic:
nth_rw 2 [show I = insert e (I \ {e}) by simp [heI]]

Result:
case refine_2
α : Type u_2
M : Matroid α
I : Set α
h : ∀ ⦃e : α⦄, e ∈ I → M.closure (I \ {e}) ≠ M.closure I
e : α
heI : e ∈ I
hin : e ∈ M.closure (I \ {e})
⊢ M.closure (I \ {e}) = M.closure (insert e (I \ {e}))

Proof state:
α : Type u_2
M : Matroid α
I : Set α
⊢ (I ⊆ M.E ∧ ∀ e ∈ I, e ∉ M.closure (I \ {e})) ↔ ∀ ⦃e : α⦄, e ∈ I → M.closure (I \ {e}) ≠ M.closure I

Tactic:
refine ⟨fun ⟨hIE, h⟩ e heI h_eq ↦ h e heI (h_eq.symm.subset (M.mem_closure_of_mem heI)),
  fun h ↦ ⟨fun e heI ↦ by_contra fun heE ↦ h heI ?_,fun e heI hin ↦ h heI ?_⟩⟩

Result:
case refine_1
α : Type u_2
M : Matroid α
I : Set α
h : ∀ ⦃e : α⦄, e ∈ I → M.closure (I \ {e}) ≠ M.closure I
e : α
heI : e ∈ I
heE : e ∉ M.E
⊢ M.closure (I \ {e}) = M.closure I

case refine_2
α : Type u_2
M : Matroid α
I : Set α
h : ∀ ⦃e : α⦄, e ∈ I → M.closure (I \ {e}) ≠ M.closure I
e : α
heI : e ∈ I
hin : e ∈ M.closure (I \ {e})
⊢ M.closure (I \ {e}) = M.closure I

Proof state:
case refine_2
α : Type u_2
M : Matroid α
I : Set α
h : ∀ ⦃e : α⦄, e ∈ I → M.closure (I \ {e}) ≠ M.closure I
e : α
heI : e ∈ I
hin : e ∈ M.closure (I \ {e})
⊢ M.closure (I \ {e}) = M.closure (insert e (I \ {e}))

Tactic:
rw [← closure_insert_closure_eq_closure_insert, insert_eq_of_mem hin, closure_closure]

Result:
no goals

Proof state:
α : Type u_2
M : Matroid α
I : Set α
⊢ M.Indep I ↔ ∀ ⦃e : α⦄, e ∈ I → M.closure (I \ {e}) ≠ M.closure I

Tactic:
rw [indep_iff_forall_not_mem_closure_diff']

Result:
α : Type u_2
M : Matroid α
I : Set α
⊢ (I ⊆ M.E ∧ ∀ e ∈ I, e ∉ M.closure (I \ {e})) ↔ ∀ ⦃e : α⦄, e ∈ I → M.closure (I \ {e}) ≠ M.closure I
-- Mathlib/Data/Seq/WSeq.lean
theorem cons_congr {s t : WSeq α} (a : α) (h : s ~ʷ t) : cons a s ~ʷ cons a t

Proof state:
α : Type u
s t : WSeq α
a : α
h : s ~ʷ t
⊢ LiftRel (fun x1 x2 => x1 = x2) (cons a s) (cons a t)

Tactic:
simpa using h

Result:
no goals

Proof state:
α : Type u
s t : WSeq α
a : α
h : s ~ʷ t
⊢ cons a s ~ʷ cons a t

Tactic:
unfold Equiv

Result:
α : Type u
s t : WSeq α
a : α
h : s ~ʷ t
⊢ LiftRel (fun x1 x2 => x1 = x2) (cons a s) (cons a t)
-- Mathlib/.lake/packages/lean4/src/lean/Init/GetElem.lean
theorem getElem_congr [GetElem coll idx elem valid] {c d : coll} (h : c = d)
    {i j : idx} (h' : i = j) (w : valid c i) : c[i] = d[j]'(h' ▸ h ▸ w)

Proof state:
case refl
coll : Type u_1
idx : Type u_2
elem : Type u_3
valid : coll → idx → Prop
inst✝ : GetElem coll idx elem valid
c : coll
i j : idx
h' : i = j
w : valid c i
⊢ getElem c i w = getElem c j ⋯

Tactic:
cases h'

Result:
case refl.refl
coll : Type u_1
idx : Type u_2
elem : Type u_3
valid : coll → idx → Prop
inst✝ : GetElem coll idx elem valid
c : coll
i : idx
w : valid c i
⊢ getElem c i w = getElem c i ⋯

Proof state:
coll : Type u_1
idx : Type u_2
elem : Type u_3
valid : coll → idx → Prop
inst✝ : GetElem coll idx elem valid
c d : coll
h : c = d
i j : idx
h' : i = j
w : valid c i
⊢ getElem c i w = getElem d j ⋯

Tactic:
cases h

Result:
case refl
coll : Type u_1
idx : Type u_2
elem : Type u_3
valid : coll → idx → Prop
inst✝ : GetElem coll idx elem valid
c : coll
i j : idx
h' : i = j
w : valid c i
⊢ getElem c i w = getElem c j ⋯

Proof state:
case refl.refl
coll : Type u_1
idx : Type u_2
elem : Type u_3
valid : coll → idx → Prop
inst✝ : GetElem coll idx elem valid
c : coll
i : idx
w : valid c i
⊢ getElem c i w = getElem c i ⋯

Tactic:
rfl

Result:
no goals
-- Mathlib/Topology/Order/DenselyOrdered.lean
theorem frontier_Icc [NoMinOrder α] [NoMaxOrder α] {a b : α} (h : a ≤ b) :
    frontier (Icc a b) = {a, b}

Proof state:
α : Type u_1
inst✝⁵ : TopologicalSpace α
inst✝⁴ : LinearOrder α
inst✝³ : OrderTopology α
inst✝² : DenselyOrdered α
inst✝¹ : NoMinOrder α
inst✝ : NoMaxOrder α
a b : α
h : a ≤ b
⊢ frontier (Icc a b) = {a, b}

Tactic:
simp [frontier, h, Icc_diff_Ioo_same]

Result:
no goals
-- Mathlib/NumberTheory/NumberField/Embeddings.lean
lemma not_isUnramified_iff :
    ¬ IsUnramified k w ↔ IsComplex w ∧ IsReal (w.comap (algebraMap k K))

Proof state:
k : Type u_1
inst✝² : Field k
K : Type u_2
inst✝¹ : Field K
inst✝ : Algebra k K
w : InfinitePlace K
⊢ ¬IsUnramified k w ↔ w.IsComplex ∧ (w.comap (algebraMap k K)).IsReal

Tactic:
rw [IsUnramified, mult, mult, ← not_isReal_iff_isComplex]

Result:
k : Type u_1
inst✝² : Field k
K : Type u_2
inst✝¹ : Field K
inst✝ : Algebra k K
w : InfinitePlace K
⊢ (¬(if (w.comap (algebraMap k K)).IsReal then 1 else 2) = if w.IsReal then 1 else 2) ↔
    ¬w.IsReal ∧ (w.comap (algebraMap k K)).IsReal

Proof state:
k : Type u_1
inst✝² : Field k
K : Type u_2
inst✝¹ : Field K
inst✝ : Algebra k K
w : InfinitePlace K
⊢ (¬(if (w.comap (algebraMap k K)).IsReal then 1 else 2) = if w.IsReal then 1 else 2) ↔
    ¬w.IsReal ∧ (w.comap (algebraMap k K)).IsReal

Tactic:
split_ifs with h₁ h₂ h₂ <;>
  simp only [not_true_eq_false, false_iff, and_self, forall_true_left, IsEmpty.forall_iff,
    not_and, OfNat.one_ne_ofNat, not_false_eq_true, true_iff, OfNat.ofNat_ne_one, h₁, h₂]

Result:
case pos
k : Type u_1
inst✝² : Field k
K : Type u_2
inst✝¹ : Field K
inst✝ : Algebra k K
w : InfinitePlace K
h₁ : ¬(w.comap (algebraMap k K)).IsReal
h₂ : w.IsReal
⊢ False

Proof state:
case pos
k : Type u_1
inst✝² : Field k
K : Type u_2
inst✝¹ : Field K
inst✝ : Algebra k K
w : InfinitePlace K
h₁ : ¬(w.comap (algebraMap k K)).IsReal
h₂ : w.IsReal
⊢ False

Tactic:
exact h₁ (h₂.comap _)

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Erase.lean
theorem mem_eraseIdx_iff_getElem {x : α} {l : Vector α n} {k} {h} : x ∈ eraseIdx l k h ↔ ∃ i w, i ≠ k ∧ l[i]'w = x

Proof state:
α : Type u_1
n : Nat
x : α
l : Vector α n
k : Nat
h : k < n
⊢ x ∈ l.eraseIdx k h ↔ ∃ i w, i ≠ k ∧ l[i] = x

Tactic:
rcases l with ⟨l, rfl⟩

Result:
case mk
α : Type u_1
x : α
k : Nat
l : Array α
h : k < l.size
⊢ x ∈ { toArray := l, size_toArray := ⋯ }.eraseIdx k h ↔ ∃ i w, i ≠ k ∧ { toArray := l, size_toArray := ⋯ }[i] = x

Proof state:
case mk
α : Type u_1
x : α
k : Nat
l : Array α
h : k < l.size
⊢ x ∈ { toArray := l, size_toArray := ⋯ }.eraseIdx k h ↔ ∃ i w, i ≠ k ∧ { toArray := l, size_toArray := ⋯ }[i] = x

Tactic:
simp [Array.mem_eraseIdx_iff_getElem, *]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem getElem_swap_left (a : Array α) {i j : Nat} {hi hj} :
    (a.swap i j hi hj)[i]'(by simpa using hi) = a[j]

Proof state:
α : Type u_1
a : Array α
i j : Nat
hi : i < a.size
hj : j < a.size
⊢ (a.swap i j hi hj)[i] = a[j]

Tactic:
simp +contextual [swap_def, getElem_set]

Result:
no goals

Proof state:
α : Type ?u.518686
a : Array α
i j : Nat
hi : i < a.size
hj : j < a.size
⊢ i < (a.swap i j hi hj).size

Tactic:
simpa using hi

Result:
no goals
-- Mathlib/LinearAlgebra/AffineSpace/AffineSubspace/Defs.lean
@[simp] lemma mk'_top (p : P) : mk' p (⊤ : Submodule k V) = ⊤

Proof state:
k : Type u_1
V : Type u_2
P : Type u_3
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
S : AffineSpace V P
p : P
⊢ mk' p ⊤ = ⊤

Tactic:
ext x

Result:
case h
k : Type u_1
V : Type u_2
P : Type u_3
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
S : AffineSpace V P
p x : P
⊢ x ∈ mk' p ⊤ ↔ x ∈ ⊤

Proof state:
case h
k : Type u_1
V : Type u_2
P : Type u_3
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
S : AffineSpace V P
p x : P
⊢ x ∈ mk' p ⊤ ↔ x ∈ ⊤

Tactic:
simp [mem_mk'_iff_vsub_mem]

Result:
no goals
-- Mathlib/RingTheory/Localization/Integral.lean
theorem integerNormalization_eq_zero_iff {p : K[X]} :
    integerNormalization (nonZeroDivisors A) p = 0 ↔ p = 0

Proof state:
case intro.mk
A : Type u_3
K : Type u_4
inst✝⁴ : CommRing A
inst✝³ : IsDomain A
inst✝² : Field K
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
p : K[X]
b : A
nonzero : b ∈ nonZeroDivisors A
hb : ∀ (i : ℕ), (algebraMap A K) ((integerNormalization (nonZeroDivisors A) p).coeff i) = ↑⟨b, nonzero⟩ • p.coeff i
⊢ (∀ (n : ℕ), p.coeff n = coeff 0 n) ↔ ∀ (n : ℕ), (integerNormalization (nonZeroDivisors A) p).coeff n = coeff 0 n

Tactic:
constructor <;> intro h i

Result:
case intro.mk.mp
A : Type u_3
K : Type u_4
inst✝⁴ : CommRing A
inst✝³ : IsDomain A
inst✝² : Field K
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
p : K[X]
b : A
nonzero : b ∈ nonZeroDivisors A
hb : ∀ (i : ℕ), (algebraMap A K) ((integerNormalization (nonZeroDivisors A) p).coeff i) = ↑⟨b, nonzero⟩ • p.coeff i
h : ∀ (n : ℕ), p.coeff n = coeff 0 n
i : ℕ
⊢ (integerNormalization (nonZeroDivisors A) p).coeff i = coeff 0 i

case intro.mk.mpr
A : Type u_3
K : Type u_4
inst✝⁴ : CommRing A
inst✝³ : IsDomain A
inst✝² : Field K
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
p : K[X]
b : A
nonzero : b ∈ nonZeroDivisors A
hb : ∀ (i : ℕ), (algebraMap A K) ((integerNormalization (nonZeroDivisors A) p).coeff i) = ↑⟨b, nonzero⟩ • p.coeff i
h : ∀ (n : ℕ), (integerNormalization (nonZeroDivisors A) p).coeff n = coeff 0 n
i : ℕ
⊢ p.coeff i = coeff 0 i
-- Mathlib/Analysis/InnerProductSpace/Subspace.lean
theorem Orthonormal.orthogonalFamily {v : ι → E} (hv : Orthonormal 𝕜 v) :
    OrthogonalFamily 𝕜 (fun _i : ι => 𝕜) fun i => LinearIsometry.toSpanSingleton 𝕜 E (hv.1 i) :=
  fun i j hij a b => by simp [inner_smul_left, inner_smul_right, hv.2 hij]

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
ι : Type u_4
v : ι → E
hv : Orthonormal 𝕜 v
i j : ι
hij : i ≠ j
a : (fun _i => 𝕜) i
b : (fun _i => 𝕜) j
⊢ inner (((fun i => LinearIsometry.toSpanSingleton 𝕜 E ⋯) i) a)
      (((fun i => LinearIsometry.toSpanSingleton 𝕜 E ⋯) j) b) =
    0

Tactic:
simp [inner_smul_left, inner_smul_right, hv.2 hij]

Result:
no goals
-- Mathlib/CategoryTheory/Limits/Constructions/ZeroObjects.lean
theorem inr_zeroCoprodIso_hom (X : C) : coprod.inr ≫ (zeroCoprodIso X).hom = 𝟙 X

Proof state:
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
X : C
⊢ coprod.inr ≫ (zeroCoprodIso X).hom = 𝟙 X

Tactic:
dsimp [zeroCoprodIso, binaryCofanZeroLeft]

Result:
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
X : C
⊢ coprod.inr ≫
      (colimit.isoColimitCocone { cocone := BinaryCofan.mk 0 (𝟙 X), isColimit := binaryCofanZeroLeftIsColimit X }).hom =
    𝟙 X

Proof state:
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
X : C
⊢ coprod.inr ≫
      (colimit.isoColimitCocone { cocone := BinaryCofan.mk 0 (𝟙 X), isColimit := binaryCofanZeroLeftIsColimit X }).hom =
    𝟙 X

Tactic:
simp

Result:
no goals
-- Mathlib/Data/TypeVec.lean
theorem eq_of_drop_last_eq {α β : TypeVec (n + 1)} {f g : α ⟹ β} (h₀ : dropFun f = dropFun g)
    (h₁ : lastFun f = lastFun g) : f = g

Proof state:
n : ℕ
α : TypeVec.{u_1} (n + 1)
β : TypeVec.{u_2} (n + 1)
f g : α ⟹ β
h₀ : dropFun f = dropFun g
h₁ : lastFun f = lastFun g
x : Fin2 (n + 1)
⊢ f x = g x

Tactic:
cases x

Result:
case fz
n : ℕ
α : TypeVec.{u_1} (n + 1)
β : TypeVec.{u_2} (n + 1)
f g : α ⟹ β
h₀ : dropFun f = dropFun g
h₁ : lastFun f = lastFun g
⊢ f Fin2.fz = g Fin2.fz

case fs
n : ℕ
α : TypeVec.{u_1} (n + 1)
β : TypeVec.{u_2} (n + 1)
f g : α ⟹ β
h₀ : dropFun f = dropFun g
h₁ : lastFun f = lastFun g
a✝ : Fin2 n
⊢ f a✝.fs = g a✝.fs

Proof state:
case fs
n : ℕ
α : TypeVec.{u_1} (n + 1)
β : TypeVec.{u_2} (n + 1)
f g : α ⟹ β
h₀ : dropFun f = dropFun g
h₁ : lastFun f = lastFun g
a✝ : Fin2 n
⊢ f a✝.fs = g a✝.fs

Tactic:
apply congr_fun h₀

Result:
no goals

Proof state:
n : ℕ
α : TypeVec.{u_1} (n + 1)
β : TypeVec.{u_2} (n + 1)
f g : α ⟹ β
h₀ : dropFun f = dropFun g
h₁ : lastFun f = lastFun g
⊢ f = g

Tactic:
refine funext (fun x => ?_)

Result:
n : ℕ
α : TypeVec.{u_1} (n + 1)
β : TypeVec.{u_2} (n + 1)
f g : α ⟹ β
h₀ : dropFun f = dropFun g
h₁ : lastFun f = lastFun g
x : Fin2 (n + 1)
⊢ f x = g x

Proof state:
case fz
n : ℕ
α : TypeVec.{u_1} (n + 1)
β : TypeVec.{u_2} (n + 1)
f g : α ⟹ β
h₀ : dropFun f = dropFun g
h₁ : lastFun f = lastFun g
⊢ f Fin2.fz = g Fin2.fz

Tactic:
apply h₁

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Pow/Deriv.lean
theorem hasStrictFDerivAt_rpow_of_pos (p : ℝ × ℝ) (hp : 0 < p.1) :
    HasStrictFDerivAt (fun x : ℝ × ℝ => x.1 ^ x.2)
      ((p.2 * p.1 ^ (p.2 - 1)) • ContinuousLinearMap.fst ℝ ℝ ℝ +
        (p.1 ^ p.2 * log p.1) • ContinuousLinearMap.snd ℝ ℝ ℝ) p

Proof state:
p : ℝ × ℝ
hp : 0 < p.1
this : (fun x => x.1 ^ x.2) =ᶠ[𝓝 p] fun x => rexp (log x.1 * x.2)
⊢ HasStrictFDerivAt (fun x => x.1 ^ x.2)
    ((p.2 * p.1 ^ (p.2 - 1)) • ContinuousLinearMap.fst ℝ ℝ ℝ + (p.1 ^ p.2 * log p.1) • ContinuousLinearMap.snd ℝ ℝ ℝ) p

Tactic:
refine HasStrictFDerivAt.congr_of_eventuallyEq ?_ this.symm

Result:
p : ℝ × ℝ
hp : 0 < p.1
this : (fun x => x.1 ^ x.2) =ᶠ[𝓝 p] fun x => rexp (log x.1 * x.2)
⊢ HasStrictFDerivAt (fun x => rexp (log x.1 * x.2))
    ((p.2 * p.1 ^ (p.2 - 1)) • ContinuousLinearMap.fst ℝ ℝ ℝ + (p.1 ^ p.2 * log p.1) • ContinuousLinearMap.snd ℝ ℝ ℝ) p

Proof state:
p : ℝ × ℝ
hp : 0 < p.1
this : (fun x => x.1 ^ x.2) =ᶠ[𝓝 p] fun x => rexp (log x.1 * x.2)
⊢ HasStrictFDerivAt (fun x => rexp (log x.1 * x.2))
    ((p.2 * p.1 ^ (p.2 - 1)) • ContinuousLinearMap.fst ℝ ℝ ℝ + (p.1 ^ p.2 * log p.1) • ContinuousLinearMap.snd ℝ ℝ ℝ) p

Tactic:
convert ((hasStrictFDerivAt_fst.log hp.ne').mul hasStrictFDerivAt_snd).exp using 1

Result:
case h.e'_12
p : ℝ × ℝ
hp : 0 < p.1
this : (fun x => x.1 ^ x.2) =ᶠ[𝓝 p] fun x => rexp (log x.1 * x.2)
⊢ (p.2 * p.1 ^ (p.2 - 1)) • ContinuousLinearMap.fst ℝ ℝ ℝ + (p.1 ^ p.2 * log p.1) • ContinuousLinearMap.snd ℝ ℝ ℝ =
    rexp (log p.1 * p.2) • (log p.1 • ContinuousLinearMap.snd ℝ ℝ ℝ + p.2 • p.1⁻¹ • ContinuousLinearMap.fst ℝ ℝ ℝ)

Proof state:
case h.e'_12
p : ℝ × ℝ
hp : 0 < p.1
this : (fun x => x.1 ^ x.2) =ᶠ[𝓝 p] fun x => rexp (log x.1 * x.2)
⊢ (p.2 * p.1 ^ (p.2 - 1)) • ContinuousLinearMap.fst ℝ ℝ ℝ + (p.1 ^ p.2 * log p.1) • ContinuousLinearMap.snd ℝ ℝ ℝ =
    rexp (log p.1 * p.2) • (log p.1 • ContinuousLinearMap.snd ℝ ℝ ℝ + p.2 • p.1⁻¹ • ContinuousLinearMap.fst ℝ ℝ ℝ)

Tactic:
rw [rpow_sub_one hp.ne', ← rpow_def_of_pos hp, smul_add, smul_smul, mul_div_left_comm,
  div_eq_mul_inv, smul_smul, smul_smul, mul_assoc, add_comm]

Result:
no goals

Proof state:
p : ℝ × ℝ
hp : 0 < p.1
⊢ HasStrictFDerivAt (fun x => x.1 ^ x.2)
    ((p.2 * p.1 ^ (p.2 - 1)) • ContinuousLinearMap.fst ℝ ℝ ℝ + (p.1 ^ p.2 * log p.1) • ContinuousLinearMap.snd ℝ ℝ ℝ) p

Tactic:
have : (fun x : ℝ × ℝ => x.1 ^ x.2) =ᶠ[𝓝 p] fun x => exp (log x.1 * x.2) :=
  (continuousAt_fst.eventually (lt_mem_nhds hp)).mono fun p hp => rpow_def_of_pos hp _

Result:
p : ℝ × ℝ
hp : 0 < p.1
this : (fun x => x.1 ^ x.2) =ᶠ[𝓝 p] fun x => rexp (log x.1 * x.2)
⊢ HasStrictFDerivAt (fun x => x.1 ^ x.2)
    ((p.2 * p.1 ^ (p.2 - 1)) • ContinuousLinearMap.fst ℝ ℝ ℝ + (p.1 ^ p.2 * log p.1) • ContinuousLinearMap.snd ℝ ℝ ℝ) p
-- Mathlib/LinearAlgebra/Alternating/Basic.lean
theorem compLinearMap_injective (f : M₂ →ₗ[R] M) (hf : Function.Surjective f) :
    Function.Injective fun g : M [⋀^ι]→ₗ[R] N => g.compLinearMap f := fun g₁ g₂ h =>
  ext fun x => by
    simpa [Function.surjInv_eq hf] using AlternatingMap.ext_iff.mp h (Function.surjInv hf ∘ x)

Proof state:
R : Type u_1
inst✝⁶ : Semiring R
M : Type u_2
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
N : Type u_3
inst✝³ : AddCommMonoid N
inst✝² : Module R N
ι : Type u_7
M₂ : Type u_10
inst✝¹ : AddCommMonoid M₂
inst✝ : Module R M₂
f : M₂ →ₗ[R] M
hf : Function.Surjective ⇑f
g₁ g₂ : M [⋀^ι]→ₗ[R] N
h : (fun g => g.compLinearMap f) g₁ = (fun g => g.compLinearMap f) g₂
x : ι → M
⊢ g₁ x = g₂ x

Tactic:
simpa [Function.surjInv_eq hf] using AlternatingMap.ext_iff.mp h (Function.surjInv hf ∘ x)

Result:
no goals
-- Mathlib/LinearAlgebra/Dual.lean
theorem mem_of_mem_span {H : Set ι} {x : M} (hmem : x ∈ Submodule.span R (e '' H)) :
    ∀ i : ι, ε i x ≠ 0 → i ∈ H

Proof state:
case intro.intro
R : Type u_1
M : Type u_2
ι : Type u_3
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
e : ι → M
ε : ι → Dual R M
h : DualBases e ε
H : Set ι
i : ι
l : ι →₀ R
supp_l : l ∈ Finsupp.supported R R H
hmem : (Finsupp.linearCombination R e) l ∈ span R (e '' H)
hi : (ε i) ((Finsupp.linearCombination R e) l) ≠ 0
⊢ i ∈ H

Tactic:
apply not_imp_comm.mp ((Finsupp.mem_supported' _ _).mp supp_l i)

Result:
case intro.intro
R : Type u_1
M : Type u_2
ι : Type u_3
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
e : ι → M
ε : ι → Dual R M
h : DualBases e ε
H : Set ι
i : ι
l : ι →₀ R
supp_l : l ∈ Finsupp.supported R R H
hmem : (Finsupp.linearCombination R e) l ∈ span R (e '' H)
hi : (ε i) ((Finsupp.linearCombination R e) l) ≠ 0
⊢ ¬l i = 0

Proof state:
R : Type u_1
M : Type u_2
ι : Type u_3
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
e : ι → M
ε : ι → Dual R M
h : DualBases e ε
H : Set ι
x : M
hmem : x ∈ span R (e '' H)
i : ι
hi : (ε i) x ≠ 0
⊢ i ∈ H

Tactic:
rcases (Finsupp.mem_span_image_iff_linearCombination _).mp hmem with ⟨l, supp_l, rfl⟩

Result:
case intro.intro
R : Type u_1
M : Type u_2
ι : Type u_3
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
e : ι → M
ε : ι → Dual R M
h : DualBases e ε
H : Set ι
i : ι
l : ι →₀ R
supp_l : l ∈ Finsupp.supported R R H
hmem : (Finsupp.linearCombination R e) l ∈ span R (e '' H)
hi : (ε i) ((Finsupp.linearCombination R e) l) ≠ 0
⊢ i ∈ H

Proof state:
case intro.intro
R : Type u_1
M : Type u_2
ι : Type u_3
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
e : ι → M
ε : ι → Dual R M
h : DualBases e ε
H : Set ι
i : ι
l : ι →₀ R
supp_l : l ∈ Finsupp.supported R R H
hmem : (Finsupp.linearCombination R e) l ∈ span R (e '' H)
hi : (ε i) ((Finsupp.linearCombination R e) l) ≠ 0
⊢ ¬l i = 0

Tactic:
rwa [← lc_def, h.dual_lc] at hi

Result:
no goals

Proof state:
R : Type u_1
M : Type u_2
ι : Type u_3
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
e : ι → M
ε : ι → Dual R M
h : DualBases e ε
H : Set ι
x : M
hmem : x ∈ span R (e '' H)
⊢ ∀ (i : ι), (ε i) x ≠ 0 → i ∈ H

Tactic:
intro i hi

Result:
R : Type u_1
M : Type u_2
ι : Type u_3
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
e : ι → M
ε : ι → Dual R M
h : DualBases e ε
H : Set ι
x : M
hmem : x ∈ span R (e '' H)
i : ι
hi : (ε i) x ≠ 0
⊢ i ∈ H
-- Mathlib/NumberTheory/PellMatiyasevic.lean
theorem asq_pos : 0 < a * a :=
  le_trans (le_of_lt a1)
    (by have := @Nat.mul_le_mul_left 1 a a (le_of_lt a1); rwa [mul_one] at this)

Proof state:
a : ℕ
a1 : 1 < a
⊢ a ≤ a * a

Tactic:
have := @Nat.mul_le_mul_left 1 a a (le_of_lt a1)

Result:
a : ℕ
a1 : 1 < a
this : a * 1 ≤ a * a
⊢ a ≤ a * a

Proof state:
a : ℕ
a1 : 1 < a
this : a * 1 ≤ a * a
⊢ a ≤ a * a

Tactic:
rwa [mul_one] at this

Result:
no goals
-- Mathlib/FieldTheory/Galois/Basic.lean
theorem isGalois_iff_isGalois_bot : IsGalois (⊥ : IntermediateField F E) E ↔ IsGalois F E

Proof state:
case mp
F : Type u_1
E : Type u_3
inst✝² : Field F
inst✝¹ : Field E
inst✝ : Algebra F E
h : IsGalois (↥⊥) E
⊢ IsGalois F E

Tactic:
exact IsGalois.tower_top_of_isGalois (⊥ : IntermediateField F E) F E

Result:
no goals

Proof state:
F : Type u_1
E : Type u_3
inst✝² : Field F
inst✝¹ : Field E
inst✝ : Algebra F E
⊢ IsGalois (↥⊥) E ↔ IsGalois F E

Tactic:
constructor

Result:
case mp
F : Type u_1
E : Type u_3
inst✝² : Field F
inst✝¹ : Field E
inst✝ : Algebra F E
⊢ IsGalois (↥⊥) E → IsGalois F E

case mpr
F : Type u_1
E : Type u_3
inst✝² : Field F
inst✝¹ : Field E
inst✝ : Algebra F E
⊢ IsGalois F E → IsGalois (↥⊥) E

Proof state:
case mpr
F : Type u_1
E : Type u_3
inst✝² : Field F
inst✝¹ : Field E
inst✝ : Algebra F E
⊢ IsGalois F E → IsGalois (↥⊥) E

Tactic:
intro h

Result:
case mpr
F : Type u_1
E : Type u_3
inst✝² : Field F
inst✝¹ : Field E
inst✝ : Algebra F E
h : IsGalois F E
⊢ IsGalois (↥⊥) E

Proof state:
case mpr
F : Type u_1
E : Type u_3
inst✝² : Field F
inst✝¹ : Field E
inst✝ : Algebra F E
h : IsGalois F E
⊢ IsGalois (↥⊥) E

Tactic:
infer_instance

Result:
no goals

Proof state:
case mp
F : Type u_1
E : Type u_3
inst✝² : Field F
inst✝¹ : Field E
inst✝ : Algebra F E
⊢ IsGalois (↥⊥) E → IsGalois F E

Tactic:
intro h

Result:
case mp
F : Type u_1
E : Type u_3
inst✝² : Field F
inst✝¹ : Field E
inst✝ : Algebra F E
h : IsGalois (↥⊥) E
⊢ IsGalois F E
-- Mathlib/RingTheory/Ideal/Operations.lean
theorem mem_smul_top_iff (N : Submodule R M) (x : N) :
    x ∈ I • (⊤ : Submodule R N) ↔ (x : M) ∈ I • N

Proof state:
R : Type u
M : Type v
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
I : Ideal R
N : Submodule R M
x : ↥N
this : map N.subtype (I • ⊤) = I • N
⊢ x ∈ I • ⊤ ↔ N.subtype x ∈ map N.subtype (I • ⊤)

Tactic:
exact (Function.Injective.mem_set_image N.injective_subtype).symm

Result:
no goals

Proof state:
R : Type u
M : Type v
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
I : Ideal R
N : Submodule R M
x : ↥N
⊢ x ∈ I • ⊤ ↔ ↑x ∈ I • N

Tactic:
change _ ↔ N.subtype x ∈ I • N

Result:
R : Type u
M : Type v
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
I : Ideal R
N : Submodule R M
x : ↥N
⊢ x ∈ I • ⊤ ↔ N.subtype x ∈ I • N

Proof state:
R : Type u
M : Type v
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
I : Ideal R
N : Submodule R M
x : ↥N
⊢ map N.subtype (I • ⊤) = I • N

Tactic:
rw [Submodule.map_smul'', Submodule.map_top, Submodule.range_subtype]

Result:
no goals

Proof state:
R : Type u
M : Type v
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
I : Ideal R
N : Submodule R M
x : ↥N
⊢ x ∈ I • ⊤ ↔ N.subtype x ∈ I • N

Tactic:
have : Submodule.map N.subtype (I • ⊤) = I • N := by
  rw [Submodule.map_smul'', Submodule.map_top, Submodule.range_subtype]

Result:
R : Type u
M : Type v
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
I : Ideal R
N : Submodule R M
x : ↥N
this : map N.subtype (I • ⊤) = I • N
⊢ x ∈ I • ⊤ ↔ N.subtype x ∈ I • N

Proof state:
R : Type u
M : Type v
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
I : Ideal R
N : Submodule R M
x : ↥N
this : map N.subtype (I • ⊤) = I • N
⊢ x ∈ I • ⊤ ↔ N.subtype x ∈ I • N

Tactic:
rw [← this]

Result:
R : Type u
M : Type v
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
I : Ideal R
N : Submodule R M
x : ↥N
this : map N.subtype (I • ⊤) = I • N
⊢ x ∈ I • ⊤ ↔ N.subtype x ∈ map N.subtype (I • ⊤)
-- Mathlib/Algebra/Algebra/Subalgebra/Basic.lean
theorem equivOfEq_rfl (S : Subalgebra R A) : equivOfEq S S rfl = AlgEquiv.refl

Proof state:
R : Type u
A : Type v
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
S : Subalgebra R A
⊢ S.equivOfEq S ⋯ = AlgEquiv.refl

Tactic:
ext

Result:
case h.a
R : Type u
A : Type v
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
S : Subalgebra R A
a✝ : ↥S
⊢ ↑((S.equivOfEq S ⋯) a✝) = ↑(AlgEquiv.refl a✝)

Proof state:
case h.a
R : Type u
A : Type v
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
S : Subalgebra R A
a✝ : ↥S
⊢ ↑((S.equivOfEq S ⋯) a✝) = ↑(AlgEquiv.refl a✝)

Tactic:
rfl

Result:
no goals