harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/CategoryTheory/Localization/CalculusOfFractions.lean
lemma Localization.exists_rightFraction {X Y : C} (f : L.obj X ⟶ L.obj Y) :
    ∃ (φ : W.RightFraction X Y), f = φ.map L (Localization.inverts L W)

Proof state:
case intro
C : Type u_1
D : Type u_2
inst✝³ : Category.{u_4, u_1} C
inst✝² : Category.{u_3, u_2} D
L : C ⥤ D
W : MorphismProperty C
inst✝¹ : L.IsLocalization W
inst✝ : W.HasRightCalculusOfFractions
X Y : C
f : L.obj X ⟶ L.obj Y
φ : W.op.LeftFraction (Opposite.op Y) (Opposite.op X)
eq : f.op = φ.map L.op ⋯
⊢ f.op = (φ.unop.map L ⋯).op

Tactic:
rw [eq, MorphismProperty.RightFraction.op_map]

Result:
case intro
C : Type u_1
D : Type u_2
inst✝³ : Category.{u_4, u_1} C
inst✝² : Category.{u_3, u_2} D
L : C ⥤ D
W : MorphismProperty C
inst✝¹ : L.IsLocalization W
inst✝ : W.HasRightCalculusOfFractions
X Y : C
f : L.obj X ⟶ L.obj Y
φ : W.op.LeftFraction (Opposite.op Y) (Opposite.op X)
eq : f.op = φ.map L.op ⋯
⊢ φ.map L.op ⋯ = φ.unop.op.map L.op ⋯

Proof state:
case intro
C : Type u_1
D : Type u_2
inst✝³ : Category.{u_4, u_1} C
inst✝² : Category.{u_3, u_2} D
L : C ⥤ D
W : MorphismProperty C
inst✝¹ : L.IsLocalization W
inst✝ : W.HasRightCalculusOfFractions
X Y : C
f : L.obj X ⟶ L.obj Y
φ : W.op.LeftFraction (Opposite.op Y) (Opposite.op X)
eq : f.op = φ.map L.op ⋯
⊢ φ.map L.op ⋯ = φ.unop.op.map L.op ⋯

Tactic:
rfl

Result:
no goals

Proof state:
case intro
C : Type u_1
D : Type u_2
inst✝³ : Category.{u_4, u_1} C
inst✝² : Category.{u_3, u_2} D
L : C ⥤ D
W : MorphismProperty C
inst✝¹ : L.IsLocalization W
inst✝ : W.HasRightCalculusOfFractions
X Y : C
f : L.obj X ⟶ L.obj Y
φ : W.op.LeftFraction (Opposite.op Y) (Opposite.op X)
eq : f.op = φ.map L.op ⋯
⊢ ∃ φ, f = φ.map L ⋯

Tactic:
refine ⟨φ.unop, Quiver.Hom.op_inj ?_⟩

Result:
case intro
C : Type u_1
D : Type u_2
inst✝³ : Category.{u_4, u_1} C
inst✝² : Category.{u_3, u_2} D
L : C ⥤ D
W : MorphismProperty C
inst✝¹ : L.IsLocalization W
inst✝ : W.HasRightCalculusOfFractions
X Y : C
f : L.obj X ⟶ L.obj Y
φ : W.op.LeftFraction (Opposite.op Y) (Opposite.op X)
eq : f.op = φ.map L.op ⋯
⊢ f.op = (φ.unop.map L ⋯).op

Proof state:
C : Type u_1
D : Type u_2
inst✝³ : Category.{u_4, u_1} C
inst✝² : Category.{u_3, u_2} D
L : C ⥤ D
W : MorphismProperty C
inst✝¹ : L.IsLocalization W
inst✝ : W.HasRightCalculusOfFractions
X Y : C
f : L.obj X ⟶ L.obj Y
⊢ ∃ φ, f = φ.map L ⋯

Tactic:
obtain ⟨φ, eq⟩ := Localization.exists_leftFraction L.op W.op f.op

Result:
case intro
C : Type u_1
D : Type u_2
inst✝³ : Category.{u_4, u_1} C
inst✝² : Category.{u_3, u_2} D
L : C ⥤ D
W : MorphismProperty C
inst✝¹ : L.IsLocalization W
inst✝ : W.HasRightCalculusOfFractions
X Y : C
f : L.obj X ⟶ L.obj Y
φ : W.op.LeftFraction (Opposite.op Y) (Opposite.op X)
eq : f.op = φ.map L.op ⋯
⊢ ∃ φ, f = φ.map L ⋯
-- Mathlib/RingTheory/MvPolynomial/Homogeneous.lean
lemma pow (hφ : φ.IsHomogeneous m) (n : ℕ) : (φ ^ n).IsHomogeneous (m * n)

Proof state:
σ : Type u_1
R : Type u_3
inst✝ : CommSemiring R
φ : MvPolynomial σ R
m : ℕ
hφ : φ.IsHomogeneous m
n : ℕ
⊢ m * n = ∑ _i ∈ Finset.range n, m

Tactic:
simp [mul_comm]

Result:
no goals

Proof state:
σ : Type u_1
R : Type u_3
inst✝ : CommSemiring R
φ : MvPolynomial σ R
m : ℕ
hφ : φ.IsHomogeneous m
n : ℕ
⊢ (φ ^ n).IsHomogeneous (m * n)

Tactic:
rw [show φ ^ n = ∏ _i ∈ Finset.range n, φ by simp]

Result:
σ : Type u_1
R : Type u_3
inst✝ : CommSemiring R
φ : MvPolynomial σ R
m : ℕ
hφ : φ.IsHomogeneous m
n : ℕ
⊢ (∏ _i ∈ Finset.range n, φ).IsHomogeneous (m * n)

Proof state:
σ : Type u_1
R : Type u_3
inst✝ : CommSemiring R
φ : MvPolynomial σ R
m : ℕ
hφ : φ.IsHomogeneous m
n : ℕ
⊢ (∏ _i ∈ Finset.range n, φ).IsHomogeneous (m * n)

Tactic:
rw [show m * n = ∑ _i ∈ Finset.range n, m by simp [mul_comm]]

Result:
σ : Type u_1
R : Type u_3
inst✝ : CommSemiring R
φ : MvPolynomial σ R
m : ℕ
hφ : φ.IsHomogeneous m
n : ℕ
⊢ (∏ _i ∈ Finset.range n, φ).IsHomogeneous (∑ _i ∈ Finset.range n, m)

Proof state:
σ : Type u_1
R : Type u_3
inst✝ : CommSemiring R
φ : MvPolynomial σ R
m : ℕ
hφ : φ.IsHomogeneous m
n : ℕ
⊢ φ ^ n = ∏ _i ∈ Finset.range n, φ

Tactic:
simp

Result:
no goals

Proof state:
σ : Type u_1
R : Type u_3
inst✝ : CommSemiring R
φ : MvPolynomial σ R
m : ℕ
hφ : φ.IsHomogeneous m
n : ℕ
⊢ (∏ _i ∈ Finset.range n, φ).IsHomogeneous (∑ _i ∈ Finset.range n, m)

Tactic:
apply IsHomogeneous.prod _ _ _ (fun _ _ ↦ hφ)

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/System/Platform.lean
theorem le_numBits : 32 ≤ numBits

Proof state:
⊢ 32 ≤ numBits

Tactic:
cases numBits_eq <;> next h => simp [h]

Result:
no goals

Proof state:
h : numBits = 64
⊢ 32 ≤ numBits

Tactic:
simp [h]

Result:
no goals
-- Mathlib/NumberTheory/LucasLehmer.lean
theorem coe_natCast (n : ℕ) : ((n : ℤ) : X q) = (n : X q)

Proof state:
q : ℕ+
n : ℕ
⊢ ↑↑n = ↑n

Tactic:
ext <;> simp

Result:
no goals
-- Mathlib/Data/Fin/Tuple/Finset.lean
lemma filter_piFinset_eq_map_insertNthEquiv (P : (∀ i, α (p.succAbove i)) → Prop)
    [DecidablePred P] :
    {r ∈ piFinset S | P (p.removeNth r)} =
      (S p ×ˢ {r ∈ piFinset (p.removeNth  S) | P r}).map (p.insertNthEquiv α).toEmbedding

Proof state:
n : ℕ
α : Fin (n + 1) → Type u_1
p : Fin (n + 1)
S : (i : Fin (n + 1)) → Finset (α i)
P : ((i : Fin n) → α (p.succAbove i)) → Prop
inst✝ : DecidablePred P
⊢ filter (fun r => P (p.removeNth r)) (piFinset S) =
    map (insertNthEquiv α p).toEmbedding (S p ×ˢ filter (fun r => P r) (piFinset (p.removeNth S)))

Tactic:
simp [← map_insertNthEquiv_filter_piFinset, map_map]

Result:
no goals
-- Mathlib/GroupTheory/Nilpotent.lean
theorem nilpotent_iff_finite_ascending_central_series :
    IsNilpotent G ↔ ∃ n : ℕ, ∃ H : ℕ → Subgroup G, IsAscendingCentralSeries H ∧ H n = ⊤

Proof state:
case mp
G : Type u_1
inst✝ : Group G
⊢ IsNilpotent G → ∃ n H, IsAscendingCentralSeries H ∧ H n = ⊤

Tactic:
rintro ⟨n, nH⟩

Result:
case mp.mk.intro
G : Type u_1
inst✝ : Group G
n : ℕ
nH : upperCentralSeries G n = ⊤
⊢ ∃ n H, IsAscendingCentralSeries H ∧ H n = ⊤

Proof state:
case h
G : Type u_1
inst✝ : Group G
n : ℕ
H : ℕ → Subgroup G
hH : IsAscendingCentralSeries H
hn : H n = ⊤
⊢ upperCentralSeries G n = ⊤

Tactic:
rw [eq_top_iff, ← hn]

Result:
case h
G : Type u_1
inst✝ : Group G
n : ℕ
H : ℕ → Subgroup G
hH : IsAscendingCentralSeries H
hn : H n = ⊤
⊢ H n ≤ upperCentralSeries G n

Proof state:
case h
G : Type u_1
inst✝ : Group G
n : ℕ
H : ℕ → Subgroup G
hH : IsAscendingCentralSeries H
hn : H n = ⊤
⊢ H n ≤ upperCentralSeries G n

Tactic:
exact ascending_central_series_le_upper H hH n

Result:
no goals

Proof state:
G : Type u_1
inst✝ : Group G
⊢ IsNilpotent G ↔ ∃ n H, IsAscendingCentralSeries H ∧ H n = ⊤

Tactic:
constructor

Result:
case mp
G : Type u_1
inst✝ : Group G
⊢ IsNilpotent G → ∃ n H, IsAscendingCentralSeries H ∧ H n = ⊤

case mpr
G : Type u_1
inst✝ : Group G
⊢ (∃ n H, IsAscendingCentralSeries H ∧ H n = ⊤) → IsNilpotent G

Proof state:
case mpr
G : Type u_1
inst✝ : Group G
⊢ (∃ n H, IsAscendingCentralSeries H ∧ H n = ⊤) → IsNilpotent G

Tactic:
rintro ⟨n, H, hH, hn⟩

Result:
case mpr.intro.intro.intro
G : Type u_1
inst✝ : Group G
n : ℕ
H : ℕ → Subgroup G
hH : IsAscendingCentralSeries H
hn : H n = ⊤
⊢ IsNilpotent G

Proof state:
case mp.mk.intro
G : Type u_1
inst✝ : Group G
n : ℕ
nH : upperCentralSeries G n = ⊤
⊢ ∃ n H, IsAscendingCentralSeries H ∧ H n = ⊤

Tactic:
exact ⟨_, _, upperCentralSeries_isAscendingCentralSeries G, nH⟩

Result:
no goals

Proof state:
case mpr.intro.intro.intro
G : Type u_1
inst✝ : Group G
n : ℕ
H : ℕ → Subgroup G
hH : IsAscendingCentralSeries H
hn : H n = ⊤
⊢ IsNilpotent G

Tactic:
use n

Result:
case h
G : Type u_1
inst✝ : Group G
n : ℕ
H : ℕ → Subgroup G
hH : IsAscendingCentralSeries H
hn : H n = ⊤
⊢ upperCentralSeries G n = ⊤
-- Mathlib/Analysis/InnerProductSpace/LinearMap.lean
theorem ext_inner_map (S T : V →ₗ[ℂ] V) : (∀ x : V, ⟪S x, x⟫_ℂ = ⟪T x, x⟫_ℂ) ↔ S = T

Proof state:
V : Type u_4
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℂ V
S T : V →ₗ[ℂ] V
⊢ (∀ (x : V), ⟪S x, x⟫_ℂ = ⟪T x, x⟫_ℂ) ↔ S = T

Tactic:
rw [← sub_eq_zero, ← inner_map_self_eq_zero]

Result:
V : Type u_4
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℂ V
S T : V →ₗ[ℂ] V
⊢ (∀ (x : V), ⟪S x, x⟫_ℂ = ⟪T x, x⟫_ℂ) ↔ ∀ (x : V), ⟪(S - T) x, x⟫_ℂ = 0

Proof state:
V : Type u_4
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℂ V
S T : V →ₗ[ℂ] V
⊢ (∀ (x : V), ⟪S x, x⟫_ℂ = ⟪T x, x⟫_ℂ) ↔ ∀ (x : V), ⟪(S - T) x, x⟫_ℂ = 0

Tactic:
refine forall_congr' fun x => ?_

Result:
V : Type u_4
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℂ V
S T : V →ₗ[ℂ] V
x : V
⊢ ⟪S x, x⟫_ℂ = ⟪T x, x⟫_ℂ ↔ ⟪(S - T) x, x⟫_ℂ = 0

Proof state:
V : Type u_4
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℂ V
S T : V →ₗ[ℂ] V
x : V
⊢ ⟪S x, x⟫_ℂ = ⟪T x, x⟫_ℂ ↔ ⟪(S - T) x, x⟫_ℂ = 0

Tactic:
rw [LinearMap.sub_apply, inner_sub_left, sub_eq_zero]

Result:
no goals
-- Mathlib/Order/Heyting/Basic.lean
theorem himp_himp (a b c : α) : a ⇨ b ⇨ c = a ⊓ b ⇨ c :=
  eq_of_forall_le_iff fun d => by simp_rw [le_himp_iff, inf_assoc]

Proof state:
α : Type u_2
inst✝ : GeneralizedHeytingAlgebra α
a b c d : α
⊢ d ≤ a ⇨ b ⇨ c ↔ d ≤ a ⊓ b ⇨ c

Tactic:
simp_rw [le_himp_iff, inf_assoc]

Result:
no goals
-- Mathlib/Analysis/SpecificLimits/Basic.lean
theorem Tendsto.den {α K : Type*} [LinearOrderedField K] [TopologicalSpace K] [OrderTopology K]
    [ContinuousInv K] {f g : α → K} {l : Filter α} (hf : Tendsto f l atTop) {a : K} (ha : 0 < a)
    (hlim : Tendsto (fun x => f x / g x) l (𝓝 a)) :
    Tendsto g l atTop

Proof state:
α : Type u_4
K : Type u_5
inst✝³ : LinearOrderedField K
inst✝² : TopologicalSpace K
inst✝¹ : OrderTopology K
inst✝ : ContinuousInv K
f g : α → K
l : Filter α
hf : Tendsto f l atTop
a : K
ha : 0 < a
hlim : Tendsto (fun x => f x / g x) l (𝓝 a)
⊢ Tendsto g l atTop

Tactic:
have hlim' : Tendsto (fun x => g x / f x) l (𝓝 a⁻¹) := by
  simp_rw [← inv_div (f _)]
  exact Filter.Tendsto.inv (f := fun x => f x / g x) hlim

Result:
α : Type u_4
K : Type u_5
inst✝³ : LinearOrderedField K
inst✝² : TopologicalSpace K
inst✝¹ : OrderTopology K
inst✝ : ContinuousInv K
f g : α → K
l : Filter α
hf : Tendsto f l atTop
a : K
ha : 0 < a
hlim : Tendsto (fun x => f x / g x) l (𝓝 a)
hlim' : Tendsto (fun x => g x / f x) l (𝓝 a⁻¹)
⊢ Tendsto g l atTop

Proof state:
α : Type u_4
K : Type u_5
inst✝³ : LinearOrderedField K
inst✝² : TopologicalSpace K
inst✝¹ : OrderTopology K
inst✝ : ContinuousInv K
f g : α → K
l : Filter α
hf : Tendsto f l atTop
a : K
ha : 0 < a
hlim : Tendsto (fun x => f x / g x) l (𝓝 a)
hlim' : Tendsto (fun x => g x / f x) l (𝓝 a⁻¹)
⊢ Tendsto g l atTop

Tactic:
apply Tendsto.congr' (EventuallyEq.div_mul_cancel_atTop hf)
  (Tendsto.mul_atTop (inv_pos_of_pos ha) hlim' hf)

Result:
no goals

Proof state:
α : Type u_4
K : Type u_5
inst✝³ : LinearOrderedField K
inst✝² : TopologicalSpace K
inst✝¹ : OrderTopology K
inst✝ : ContinuousInv K
f g : α → K
l : Filter α
hf : Tendsto f l atTop
a : K
ha : 0 < a
hlim : Tendsto (fun x => f x / g x) l (𝓝 a)
⊢ Tendsto (fun x => (f x / g x)⁻¹) l (𝓝 a⁻¹)

Tactic:
exact Filter.Tendsto.inv (f := fun x => f x / g x) hlim

Result:
no goals

Proof state:
α : Type u_4
K : Type u_5
inst✝³ : LinearOrderedField K
inst✝² : TopologicalSpace K
inst✝¹ : OrderTopology K
inst✝ : ContinuousInv K
f g : α → K
l : Filter α
hf : Tendsto f l atTop
a : K
ha : 0 < a
hlim : Tendsto (fun x => f x / g x) l (𝓝 a)
⊢ Tendsto (fun x => g x / f x) l (𝓝 a⁻¹)

Tactic:
simp_rw [← inv_div (f _)]

Result:
α : Type u_4
K : Type u_5
inst✝³ : LinearOrderedField K
inst✝² : TopologicalSpace K
inst✝¹ : OrderTopology K
inst✝ : ContinuousInv K
f g : α → K
l : Filter α
hf : Tendsto f l atTop
a : K
ha : 0 < a
hlim : Tendsto (fun x => f x / g x) l (𝓝 a)
⊢ Tendsto (fun x => (f x / g x)⁻¹) l (𝓝 a⁻¹)
-- Mathlib/Algebra/Ring/Parity.lean
lemma Even.neg_one_zpow (h : Even n) : (-1 : α) ^ n = 1

Proof state:
α : Type u_2
inst✝¹ : DivisionMonoid α
inst✝ : HasDistribNeg α
n : ℤ
h : Even n
⊢ (-1) ^ n = 1

Tactic:
rw [h.neg_zpow, one_zpow]

Result:
no goals
-- Mathlib/CategoryTheory/GuitartExact/Basic.lean
lemma guitartExact_iff_initial :
    w.GuitartExact ↔ ∀ (X₂ : C₂), (w.structuredArrowDownwards X₂).Initial :=
  ⟨fun _ _ => ⟨fun _ => inferInstance⟩, by
    rw [guitartExact_iff_isConnected_downwards]
    intros
    infer_instance⟩

Proof state:
C₁ : Type u₁
C₂ : Type u₂
C₃ : Type u₃
C₄ : Type u₄
inst✝³ : Category.{v₁, u₁} C₁
inst✝² : Category.{v₂, u₂} C₂
inst✝¹ : Category.{v₃, u₃} C₃
inst✝ : Category.{v₄, u₄} C₄
T : C₁ ⥤ C₂
L : C₁ ⥤ C₃
R : C₂ ⥤ C₄
B : C₃ ⥤ C₄
w : TwoSquare T L R B
⊢ (∀ (X₂ : C₂), (w.structuredArrowDownwards X₂).Initial) → w.GuitartExact

Tactic:
rw [guitartExact_iff_isConnected_downwards]

Result:
C₁ : Type u₁
C₂ : Type u₂
C₃ : Type u₃
C₄ : Type u₄
inst✝³ : Category.{v₁, u₁} C₁
inst✝² : Category.{v₂, u₂} C₂
inst✝¹ : Category.{v₃, u₃} C₃
inst✝ : Category.{v₄, u₄} C₄
T : C₁ ⥤ C₂
L : C₁ ⥤ C₃
R : C₂ ⥤ C₄
B : C₃ ⥤ C₄
w : TwoSquare T L R B
⊢ (∀ (X₂ : C₂), (w.structuredArrowDownwards X₂).Initial) →
    ∀ {X₂ : C₂} {X₃ : C₃} (g : R.obj X₂ ⟶ B.obj X₃), IsConnected (w.CostructuredArrowDownwards g)

Proof state:
C₁ : Type u₁
C₂ : Type u₂
C₃ : Type u₃
C₄ : Type u₄
inst✝³ : Category.{v₁, u₁} C₁
inst✝² : Category.{v₂, u₂} C₂
inst✝¹ : Category.{v₃, u₃} C₃
inst✝ : Category.{v₄, u₄} C₄
T : C₁ ⥤ C₂
L : C₁ ⥤ C₃
R : C₂ ⥤ C₄
B : C₃ ⥤ C₄
w : TwoSquare T L R B
⊢ (∀ (X₂ : C₂), (w.structuredArrowDownwards X₂).Initial) →
    ∀ {X₂ : C₂} {X₃ : C₃} (g : R.obj X₂ ⟶ B.obj X₃), IsConnected (w.CostructuredArrowDownwards g)

Tactic:
intros

Result:
C₁ : Type u₁
C₂ : Type u₂
C₃ : Type u₃
C₄ : Type u₄
inst✝³ : Category.{v₁, u₁} C₁
inst✝² : Category.{v₂, u₂} C₂
inst✝¹ : Category.{v₃, u₃} C₃
inst✝ : Category.{v₄, u₄} C₄
T : C₁ ⥤ C₂
L : C₁ ⥤ C₃
R : C₂ ⥤ C₄
B : C₃ ⥤ C₄
w : TwoSquare T L R B
a✝ : ∀ (X₂ : C₂), (w.structuredArrowDownwards X₂).Initial
X₂✝ : C₂
X₃✝ : C₃
g✝ : R.obj X₂✝ ⟶ B.obj X₃✝
⊢ IsConnected (w.CostructuredArrowDownwards g✝)

Proof state:
C₁ : Type u₁
C₂ : Type u₂
C₃ : Type u₃
C₄ : Type u₄
inst✝³ : Category.{v₁, u₁} C₁
inst✝² : Category.{v₂, u₂} C₂
inst✝¹ : Category.{v₃, u₃} C₃
inst✝ : Category.{v₄, u₄} C₄
T : C₁ ⥤ C₂
L : C₁ ⥤ C₃
R : C₂ ⥤ C₄
B : C₃ ⥤ C₄
w : TwoSquare T L R B
a✝ : ∀ (X₂ : C₂), (w.structuredArrowDownwards X₂).Initial
X₂✝ : C₂
X₃✝ : C₃
g✝ : R.obj X₂✝ ⟶ B.obj X₃✝
⊢ IsConnected (w.CostructuredArrowDownwards g✝)

Tactic:
infer_instance

Result:
no goals
-- Mathlib/Data/Seq/Seq.lean
theorem head_dropn (s : Seq α) (n) : head (drop s n) = get? s n

Proof state:
case zero
α : Type u
s : Seq α
⊢ (s.drop 0).head = s.get? 0

Tactic:
rfl

Result:
no goals

Proof state:
case succ
α : Type u
n : ℕ
IH : ∀ (s : Seq α), (s.drop n).head = s.get? n
s : Seq α
⊢ (s.tail.drop n).head = s.tail.get? n

Tactic:
apply IH

Result:
no goals

Proof state:
α : Type u
s : Seq α
n : ℕ
⊢ (s.drop n).head = s.get? n

Tactic:
induction' n with n IH generalizing s

Result:
case zero
α : Type u
s : Seq α
⊢ (s.drop 0).head = s.get? 0

case succ
α : Type u
n : ℕ
IH : ∀ (s : Seq α), (s.drop n).head = s.get? n
s : Seq α
⊢ (s.drop (n + 1)).head = s.get? (n + 1)

Proof state:
case succ
α : Type u
n : ℕ
IH : ∀ (s : Seq α), (s.drop n).head = s.get? n
s : Seq α
⊢ (s.drop (n + 1)).head = s.get? (n + 1)

Tactic:
rw [← get?_tail, ← dropn_tail]

Result:
case succ
α : Type u
n : ℕ
IH : ∀ (s : Seq α), (s.drop n).head = s.get? n
s : Seq α
⊢ (s.tail.drop n).head = s.tail.get? n
-- Mathlib/Geometry/Manifold/MFDeriv/Basic.lean
theorem MDifferentiable.mfderivWithin (h : MDifferentiableAt I I' f x)
    (hxs : UniqueMDiffWithinAt I s x) : mfderivWithin I I' f s x = mfderiv I I' 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'
x : M
s : Set M
h : MDifferentiableAt I I' f x
hxs : UniqueMDiffWithinAt I s x
⊢ _root_.mfderivWithin I I' f s x = mfderiv I I' f x

Tactic:
apply HasMFDerivWithinAt.mfderivWithin _ hxs

Result:
𝕜 : 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'
x : M
s : Set M
h : MDifferentiableAt I I' f x
hxs : UniqueMDiffWithinAt I s x
⊢ HasMFDerivWithinAt I I' f s x (mfderiv I I' 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'
x : M
s : Set M
h : MDifferentiableAt I I' f x
hxs : UniqueMDiffWithinAt I s x
⊢ HasMFDerivWithinAt I I' f s x (mfderiv I I' f x)

Tactic:
exact h.hasMFDerivAt.hasMFDerivWithinAt

Result:
no goals
-- Mathlib/Analysis/RCLike/Basic.lean
theorem inv_re (z : K) : re z⁻¹ = re z / normSq z

Proof state:
K : Type u_1
inst✝ : RCLike K
z : K
⊢ re z⁻¹ = re z / normSq z

Tactic:
rw [inv_def, normSq_eq_def', mul_comm, re_ofReal_mul, conj_re, div_eq_inv_mul]

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Walk.lean
theorem getLast_darts_snd {G : SimpleGraph V} {a b : V} (p : G.Walk a b) (hp : p.darts ≠ []) :
    (p.darts.getLast hp).snd = b

Proof state:
V : Type u
G : SimpleGraph V
a b : V
p : G.Walk a b
hp : p.darts ≠ []
⊢ (List.map (fun x => x.toProd.2) p.darts).getLast ?h = b

Tactic:
simp_rw [p.map_snd_darts, List.getLast_tail, p.getLast_support]

Result:
no goals

Proof state:
V : Type u
G : SimpleGraph V
a b : V
p : G.Walk a b
hp : p.darts ≠ []
⊢ (p.darts.getLast hp).toProd.2 = b

Tactic:
rw [← List.getLast_map (f := fun x : G.Dart ↦ x.snd)]

Result:
V : Type u
G : SimpleGraph V
a b : V
p : G.Walk a b
hp : p.darts ≠ []
⊢ (List.map (fun x => x.toProd.2) p.darts).getLast ?h = b

case h
V : Type u
G : SimpleGraph V
a b : V
p : G.Walk a b
hp : p.darts ≠ []
⊢ List.map (fun x => x.toProd.2) p.darts ≠ []

Proof state:
case h
V : Type u
G : SimpleGraph V
a b : V
p : G.Walk a b
hp : p.darts ≠ []
⊢ List.map (fun x => x.toProd.2) p.darts ≠ []

Tactic:
simpa

Result:
no goals
-- Mathlib/Data/Real/Archimedean.lean
theorem isGLB_sInf (h₁ : s.Nonempty) (h₂ : BddBelow s) : IsGLB s (sInf s)

Proof state:
s : Set ℝ
h₁ : s.Nonempty
h₂ : BddBelow s
⊢ IsLUB (-s) (sSup (-s))

Tactic:
exact Real.isLUB_sSup h₁.neg h₂.neg

Result:
no goals

Proof state:
s : Set ℝ
h₁ : s.Nonempty
h₂ : BddBelow s
⊢ IsGLB s (sInf s)

Tactic:
rw [sInf_def, ← isLUB_neg', neg_neg]

Result:
s : Set ℝ
h₁ : s.Nonempty
h₂ : BddBelow s
⊢ IsLUB (-s) (sSup (-s))
-- Mathlib/Topology/UniformSpace/Equicontinuity.lean
theorem equicontinuousWithinAt_iInf_dom {t : κ → TopologicalSpace X'} {F : ι → X' → α}
    {S : Set X'} {x₀ : X'} {k : κ} (hk : EquicontinuousWithinAt (tX := t k) F S x₀) :
    EquicontinuousWithinAt (tX := ⨅ k, t k) F S x₀

Proof state:
ι : Type u_1
κ : Type u_2
X' : Type u_4
α : Type u_6
uα : UniformSpace α
t : κ → TopologicalSpace X'
F : ι → X' → α
S : Set X'
x₀ : X'
k : κ
hk : ContinuousWithinAt (⇑ofFun ∘ swap F) S x₀
⊢ ContinuousWithinAt (⇑ofFun ∘ swap F) S x₀

Tactic:
unfold ContinuousWithinAt nhdsWithin at hk ⊢

Result:
ι : Type u_1
κ : Type u_2
X' : Type u_4
α : Type u_6
uα : UniformSpace α
t : κ → TopologicalSpace X'
F : ι → X' → α
S : Set X'
x₀ : X'
k : κ
hk : Tendsto (⇑ofFun ∘ swap F) (𝓝 x₀ ⊓ 𝓟 S) (𝓝 ((⇑ofFun ∘ swap F) x₀))
⊢ Tendsto (⇑ofFun ∘ swap F) (𝓝 x₀ ⊓ 𝓟 S) (𝓝 ((⇑ofFun ∘ swap F) x₀))

Proof state:
ι : Type u_1
κ : Type u_2
X' : Type u_4
α : Type u_6
uα : UniformSpace α
t : κ → TopologicalSpace X'
F : ι → X' → α
S : Set X'
x₀ : X'
k : κ
hk : Tendsto (⇑ofFun ∘ swap F) (𝓝 x₀ ⊓ 𝓟 S) (𝓝 ((⇑ofFun ∘ swap F) x₀))
⊢ Tendsto (⇑ofFun ∘ swap F) (𝓝 x₀ ⊓ 𝓟 S) (𝓝 ((⇑ofFun ∘ swap F) x₀))

Tactic:
rw [nhds_iInf]

Result:
ι : Type u_1
κ : Type u_2
X' : Type u_4
α : Type u_6
uα : UniformSpace α
t : κ → TopologicalSpace X'
F : ι → X' → α
S : Set X'
x₀ : X'
k : κ
hk : Tendsto (⇑ofFun ∘ swap F) (𝓝 x₀ ⊓ 𝓟 S) (𝓝 ((⇑ofFun ∘ swap F) x₀))
⊢ Tendsto (⇑ofFun ∘ swap F) ((⨅ i, 𝓝 x₀) ⊓ 𝓟 S) (𝓝 ((⇑ofFun ∘ swap F) x₀))

Proof state:
ι : Type u_1
κ : Type u_2
X' : Type u_4
α : Type u_6
uα : UniformSpace α
t : κ → TopologicalSpace X'
F : ι → X' → α
S : Set X'
x₀ : X'
k : κ
hk : Tendsto (⇑ofFun ∘ swap F) (𝓝 x₀ ⊓ 𝓟 S) (𝓝 ((⇑ofFun ∘ swap F) x₀))
⊢ Tendsto (⇑ofFun ∘ swap F) ((⨅ i, 𝓝 x₀) ⊓ 𝓟 S) (𝓝 ((⇑ofFun ∘ swap F) x₀))

Tactic:
exact hk.mono_left <| inf_le_inf_right _ <| iInf_le _ k

Result:
no goals

Proof state:
ι : Type u_1
κ : Type u_2
X' : Type u_4
α : Type u_6
uα : UniformSpace α
t : κ → TopologicalSpace X'
F : ι → X' → α
S : Set X'
x₀ : X'
k : κ
hk : EquicontinuousWithinAt F S x₀
⊢ EquicontinuousWithinAt F S x₀

Tactic:
simp only [equicontinuousWithinAt_iff_continuousWithinAt (tX := _)] at hk ⊢

Result:
ι : Type u_1
κ : Type u_2
X' : Type u_4
α : Type u_6
uα : UniformSpace α
t : κ → TopologicalSpace X'
F : ι → X' → α
S : Set X'
x₀ : X'
k : κ
hk : ContinuousWithinAt (⇑ofFun ∘ swap F) S x₀
⊢ ContinuousWithinAt (⇑ofFun ∘ swap F) S x₀
-- Mathlib/Probability/Independence/Kernel.lean
lemma iIndepSets_congr (h : κ =ᵐ[μ] η) : iIndepSets π κ μ ↔ iIndepSets π η μ

Proof state:
case h
α : Type u_1
Ω : Type u_2
ι : Type u_3
_mα : MeasurableSpace α
_mΩ : MeasurableSpace Ω
κ η : Kernel α Ω
μ : Measure α
π : ι → Set (Set Ω)
h : ⇑κ =ᶠ[ae μ] ⇑η
a✝² : Finset ι
a✝¹ : ι → Set Ω
a✝ : ∀ i ∈ a✝², a✝¹ i ∈ π i
h' : ∀ᵐ (a : α) ∂μ, (η a) (⋂ i ∈ a✝², a✝¹ i) = ∏ i ∈ a✝², (η a) (a✝¹ i)
a : α
ha : κ a = η a
h'a : (η a) (⋂ i ∈ a✝², a✝¹ i) = ∏ i ∈ a✝², (η a) (a✝¹ i)
⊢ (κ a) (⋂ i ∈ a✝², a✝¹ i) = ∏ i ∈ a✝², (κ a) (a✝¹ i)

Tactic:
simpa [ha] using h'a

Result:
no goals

Proof state:
α : Type u_1
Ω : Type u_2
ι : Type u_3
_mα : MeasurableSpace α
_mΩ : MeasurableSpace Ω
κ η : Kernel α Ω
μ : Measure α
π : ι → Set (Set Ω)
h : ⇑κ =ᶠ[ae μ] ⇑η
⊢ iIndepSets π κ μ ↔ iIndepSets π η μ

Tactic:
peel 3

Result:
case h.h.h
α : Type u_1
Ω : Type u_2
ι : Type u_3
_mα : MeasurableSpace α
_mΩ : MeasurableSpace Ω
κ η : Kernel α Ω
μ : Measure α
π : ι → Set (Set Ω)
h : ⇑κ =ᶠ[ae μ] ⇑η
a✝² : Finset ι
a✝¹ : ι → Set Ω
a✝ : ∀ i ∈ a✝², a✝¹ i ∈ π i
⊢ (∀ᵐ (a : α) ∂μ, (κ a) (⋂ i ∈ a✝², a✝¹ i) = ∏ i ∈ a✝², (κ a) (a✝¹ i)) ↔
    ∀ᵐ (a : α) ∂μ, (η a) (⋂ i ∈ a✝², a✝¹ i) = ∏ i ∈ a✝², (η a) (a✝¹ i)

Proof state:
case h.h.h.refine_2
α : Type u_1
Ω : Type u_2
ι : Type u_3
_mα : MeasurableSpace α
_mΩ : MeasurableSpace Ω
κ η : Kernel α Ω
μ : Measure α
π : ι → Set (Set Ω)
h : ⇑κ =ᶠ[ae μ] ⇑η
a✝² : Finset ι
a✝¹ : ι → Set Ω
a✝ : ∀ i ∈ a✝², a✝¹ i ∈ π i
h' : ∀ᵐ (a : α) ∂μ, (η a) (⋂ i ∈ a✝², a✝¹ i) = ∏ i ∈ a✝², (η a) (a✝¹ i)
⊢ ∀ᵐ (a : α) ∂μ, (κ a) (⋂ i ∈ a✝², a✝¹ i) = ∏ i ∈ a✝², (κ a) (a✝¹ i)

Tactic:
filter_upwards [h, h'] with a ha h'a

Result:
case h
α : Type u_1
Ω : Type u_2
ι : Type u_3
_mα : MeasurableSpace α
_mΩ : MeasurableSpace Ω
κ η : Kernel α Ω
μ : Measure α
π : ι → Set (Set Ω)
h : ⇑κ =ᶠ[ae μ] ⇑η
a✝² : Finset ι
a✝¹ : ι → Set Ω
a✝ : ∀ i ∈ a✝², a✝¹ i ∈ π i
h' : ∀ᵐ (a : α) ∂μ, (η a) (⋂ i ∈ a✝², a✝¹ i) = ∏ i ∈ a✝², (η a) (a✝¹ i)
a : α
ha : κ a = η a
h'a : (η a) (⋂ i ∈ a✝², a✝¹ i) = ∏ i ∈ a✝², (η a) (a✝¹ i)
⊢ (κ a) (⋂ i ∈ a✝², a✝¹ i) = ∏ i ∈ a✝², (κ a) (a✝¹ i)
-- Mathlib/MeasureTheory/Decomposition/Lebesgue.lean
lemma rnDeriv_ne_top (μ ν : Measure α) [SigmaFinite μ] : ∀ᵐ x ∂ν, μ.rnDeriv ν x ≠ ∞

Proof state:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst✝ : SigmaFinite μ
⊢ ∀ᵐ (x : α) ∂ν, μ.rnDeriv ν x ≠ ⊤

Tactic:
filter_upwards [Measure.rnDeriv_lt_top μ ν] with x hx using hx.ne

Result:
no goals