harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Order/DirectedInverseSystem.lean
theorem lift_injective (h : ∀ i, Function.Injective (ih i)) :
    Function.Injective (DirectLimit.lift f ih compat) :=
  DirectLimit.induction₂ _ fun i x y eq ↦ by simp_rw [lift_def] at eq; rw [h i eq]

Proof state:
ι : Type u_1
inst✝³ : Preorder ι
F : ι → Type u_4
T : ⦃i j : ι⦄ → i ≤ j → Sort u_8
f : (i j : ι) → (h : i ≤ j) → T h
inst✝² : ⦃i j : ι⦄ → (h : i ≤ j) → FunLike (T h) (F i) (F j)
inst✝¹ : DirectedSystem F fun x1 x2 x3 => ⇑(f x1 x2 x3)
inst✝ : IsDirected ι fun x1 x2 => x1 ≤ x2
C : Sort u_9
ih : (i : ι) → F i → C
compat : ∀ (i j : ι) (h : i ≤ j) (x : F i), ih i x = ih j ((f i j h) x)
h : ∀ (i : ι), Function.Injective (ih i)
i : ι
x y : F i
eq : ih i x = ih i y
⊢ ⟦⟨i, x⟩⟧ = ⟦⟨i, y⟩⟧

Tactic:
rw [h i eq]

Result:
no goals

Proof state:
ι : Type u_1
inst✝³ : Preorder ι
F : ι → Type u_4
T : ⦃i j : ι⦄ → i ≤ j → Sort u_8
f : (i j : ι) → (h : i ≤ j) → T h
inst✝² : ⦃i j : ι⦄ → (h : i ≤ j) → FunLike (T h) (F i) (F j)
inst✝¹ : DirectedSystem F fun x1 x2 x3 => ⇑(f x1 x2 x3)
inst✝ : IsDirected ι fun x1 x2 => x1 ≤ x2
C : Sort u_9
ih : (i : ι) → F i → C
compat : ∀ (i j : ι) (h : i ≤ j) (x : F i), ih i x = ih j ((f i j h) x)
h : ∀ (i : ι), Function.Injective (ih i)
i : ι
x y : F i
eq : DirectLimit.lift f ih compat ⟦⟨i, x⟩⟧ = DirectLimit.lift f ih compat ⟦⟨i, y⟩⟧
⊢ ⟦⟨i, x⟩⟧ = ⟦⟨i, y⟩⟧

Tactic:
simp_rw [lift_def] at eq

Result:
ι : Type u_1
inst✝³ : Preorder ι
F : ι → Type u_4
T : ⦃i j : ι⦄ → i ≤ j → Sort u_8
f : (i j : ι) → (h : i ≤ j) → T h
inst✝² : ⦃i j : ι⦄ → (h : i ≤ j) → FunLike (T h) (F i) (F j)
inst✝¹ : DirectedSystem F fun x1 x2 x3 => ⇑(f x1 x2 x3)
inst✝ : IsDirected ι fun x1 x2 => x1 ≤ x2
C : Sort u_9
ih : (i : ι) → F i → C
compat : ∀ (i j : ι) (h : i ≤ j) (x : F i), ih i x = ih j ((f i j h) x)
h : ∀ (i : ι), Function.Injective (ih i)
i : ι
x y : F i
eq : ih i x = ih i y
⊢ ⟦⟨i, x⟩⟧ = ⟦⟨i, y⟩⟧
-- Mathlib/ModelTheory/Equivalence.lean
theorem iff_not_not : φ ⇔[T] φ.not.not := fun M v xs => by
  simp

Proof state:
L : Language
T : L.Theory
α : Type w
n : ℕ
φ : L.BoundedFormula α n
M : T.ModelType
v : α → ↑M
xs : Fin n → ↑M
⊢ (φ ⇔ ∼∼φ).Realize v xs

Tactic:
simp

Result:
no goals
-- Mathlib/LinearAlgebra/Matrix/SchurComplement.lean
theorem det_add_col_mul_row {ι : Type*} [Unique ι]
    {A : Matrix m m α} (hA : IsUnit A.det) (u v : m → α) :
    (A + col ι u * row ι v).det = A.det * (1 + row ι v * A⁻¹ * col ι u).det

Proof state:
m : Type u_2
α : Type u_4
inst✝³ : Fintype m
inst✝² : DecidableEq m
inst✝¹ : CommRing α
ι : Type u_5
inst✝ : Unique ι
A : Matrix m m α
hA : IsUnit A.det
u v : m → α
⊢ (A * 1 + col ι u * row ι v).det = A.det * (1 + row ι v * A⁻¹ * col ι u).det

Tactic:
rwa [← Matrix.mul_nonsing_inv_cancel_left A (col ι u * row ι v),
  ← Matrix.mul_add, det_mul, ← Matrix.mul_assoc, det_one_add_mul_comm,
  ← Matrix.mul_assoc]

Result:
no goals

Proof state:
m : Type u_2
α : Type u_4
inst✝³ : Fintype m
inst✝² : DecidableEq m
inst✝¹ : CommRing α
ι : Type u_5
inst✝ : Unique ι
A : Matrix m m α
hA : IsUnit A.det
u v : m → α
⊢ (A + col ι u * row ι v).det = A.det * (1 + row ι v * A⁻¹ * col ι u).det

Tactic:
nth_rewrite 1 [← Matrix.mul_one A]

Result:
m : Type u_2
α : Type u_4
inst✝³ : Fintype m
inst✝² : DecidableEq m
inst✝¹ : CommRing α
ι : Type u_5
inst✝ : Unique ι
A : Matrix m m α
hA : IsUnit A.det
u v : m → α
⊢ (A * 1 + col ι u * row ι v).det = A.det * (1 + row ι v * A⁻¹ * col ι u).det
-- Mathlib/Algebra/Group/Basic.lean
@[to_additive zsmul_sub]
lemma div_zpow (a b : α) (n : ℤ) : (a / b) ^ n = a ^ n / b ^ n

Proof state:
α : Type u_1
inst✝ : DivisionCommMonoid α
a b : α
n : ℤ
⊢ (a / b) ^ n = a ^ n / b ^ n

Tactic:
simp only [div_eq_mul_inv, mul_zpow, inv_zpow]

Result:
no goals
-- Mathlib/Order/WithBot.lean
lemma forall_gt_iff_eq_top : (∀ a : α, a < y) ↔ y = ⊤

Proof state:
case coe
α : Type u_1
inst✝ : Preorder α
a✝ : α
⊢ ∃ x, ¬x < a✝

Tactic:
simpa using ⟨_, lt_irrefl _⟩

Result:
no goals

Proof state:
α : Type u_1
inst✝ : Preorder α
y : WithTop α
⊢ (∀ (a : α), ↑a < y) ↔ y = ⊤

Tactic:
cases y <;> simp

Result:
case coe
α : Type u_1
inst✝ : Preorder α
a✝ : α
⊢ ∃ x, ¬x < a✝
-- Mathlib/Algebra/Lie/Weights/RootSystem.lean
@[simp]
lemma corootForm_rootSystem_eq_killing :
    (rootSystem H).CorootForm = (killingForm K L).restrict H

Proof state:
K : Type u_1
L : Type u_2
inst✝⁷ : Field K
inst✝⁶ : CharZero K
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra K L
inst✝³ : IsKilling K L
inst✝² : FiniteDimensional K L
H : LieSubalgebra K L
inst✝¹ : H.IsCartanSubalgebra
inst✝ : IsTriangularizable K (↥H) L
⊢ (rootSystem H).CorootForm = (killingForm K L).restrict H.toSubmodule

Tactic:
rw [restrict_killingForm_eq_sum, RootPairing.CorootForm, ← Finset.sum_coe_sort (s := H.root)]

Result:
K : Type u_1
L : Type u_2
inst✝⁷ : Field K
inst✝⁶ : CharZero K
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra K L
inst✝³ : IsKilling K L
inst✝² : FiniteDimensional K L
H : LieSubalgebra K L
inst✝¹ : H.IsCartanSubalgebra
inst✝ : IsTriangularizable K (↥H) L
⊢ ∑ i : { x // x ∈ LieSubalgebra.root }, LinearMap.smulRight ((rootSystem H).root' i) ((rootSystem H).root' i) =
    ∑ i : { x // x ∈ LieSubalgebra.root }, (Weight.toLinear K (↥H) L ↑i).smulRight (Weight.toLinear K (↥H) L ↑i)

Proof state:
K : Type u_1
L : Type u_2
inst✝⁷ : Field K
inst✝⁶ : CharZero K
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra K L
inst✝³ : IsKilling K L
inst✝² : FiniteDimensional K L
H : LieSubalgebra K L
inst✝¹ : H.IsCartanSubalgebra
inst✝ : IsTriangularizable K (↥H) L
⊢ ∑ i : { x // x ∈ LieSubalgebra.root }, LinearMap.smulRight ((rootSystem H).root' i) ((rootSystem H).root' i) =
    ∑ i : { x // x ∈ LieSubalgebra.root }, (Weight.toLinear K (↥H) L ↑i).smulRight (Weight.toLinear K (↥H) L ↑i)

Tactic:
rfl

Result:
no goals
-- Mathlib/NumberTheory/Padics/PadicIntegers.lean
@[simp, norm_cast] lemma valuation_coe (x : ℤ_[p]) : (x : ℚ_[p]).valuation = x.valuation

Proof state:
p : ℕ
hp : Fact (Nat.Prime p)
x : ℤ_[p]
⊢ (↑x).valuation = ↑x.valuation

Tactic:
simp [valuation, valuation_coe_nonneg]

Result:
no goals
-- Mathlib/Algebra/Group/Pointwise/Set/Card.lean
@[to_additive (attr := simp)]
lemma ncard_smul_set (a : G) (s : Set α) : (a • s).ncard = s.ncard

Proof state:
G : Type u_1
α : Type u_3
inst✝¹ : Group G
inst✝ : MulAction G α
a : G
s : Set α
⊢ (a • s).ncard = s.ncard

Tactic:
simp [ncard]

Result:
no goals
-- Mathlib/Order/Hom/Basic.lean
theorem comp_id (f : α →o β) : comp f id = f

Proof state:
α : Type u_2
β : Type u_3
inst✝¹ : Preorder α
inst✝ : Preorder β
f : α →o β
⊢ f.comp id = f

Tactic:
ext

Result:
case h.h
α : Type u_2
β : Type u_3
inst✝¹ : Preorder α
inst✝ : Preorder β
f : α →o β
x✝ : α
⊢ (f.comp id) x✝ = f x✝

Proof state:
case h.h
α : Type u_2
β : Type u_3
inst✝¹ : Preorder α
inst✝ : Preorder β
f : α →o β
x✝ : α
⊢ (f.comp id) x✝ = f x✝

Tactic:
rfl

Result:
no goals
-- Mathlib/MeasureTheory/Integral/Lebesgue.lean
theorem lintegral_of_isEmpty {α} [MeasurableSpace α] [IsEmpty α] (μ : Measure α) (f : α → ℝ≥0∞) :
    ∫⁻ x, f x ∂μ = 0

Proof state:
α : Type u_5
inst✝¹ : MeasurableSpace α
inst✝ : IsEmpty α
μ : Measure α
f : α → ℝ≥0∞
this : Subsingleton (Measure α)
⊢ ∫⁻ (x : α), f x ∂μ = 0

Tactic:
convert lintegral_zero_measure f

Result:
no goals

Proof state:
α : Type u_5
inst✝¹ : MeasurableSpace α
inst✝ : IsEmpty α
μ : Measure α
f : α → ℝ≥0∞
⊢ ∫⁻ (x : α), f x ∂μ = 0

Tactic:
have : Subsingleton (Measure α) := inferInstance

Result:
α : Type u_5
inst✝¹ : MeasurableSpace α
inst✝ : IsEmpty α
μ : Measure α
f : α → ℝ≥0∞
this : Subsingleton (Measure α)
⊢ ∫⁻ (x : α), f x ∂μ = 0
-- Mathlib/AlgebraicGeometry/EllipticCurve/Jacobian.lean
lemma Y_eq_negY_of_Y_eq [NoZeroDivisors R] {P Q : Fin 3 → R} (hQz : Q z ≠ 0)
    (hx : P x * Q z ^ 2 = Q x * P z ^ 2) (hy : P y * Q z ^ 3 = Q y * P z ^ 3)
    (hy' : P y * Q z ^ 3 = W'.negY Q * P z ^ 3) : P y = W'.negY P :=
  mul_left_injective₀ (pow_ne_zero 3 hQz) <| by
    linear_combination (norm := ring1) -Y_sub_Y_add_Y_sub_negY hx + hy + hy'

Proof state:
R : Type r
inst✝¹ : CommRing R
W' : Jacobian R
inst✝ : NoZeroDivisors R
P Q : Fin 3 → R
hQz : Q z ≠ 0
hx : P x * Q z ^ 2 = Q x * P z ^ 2
hy : P y * Q z ^ 3 = Q y * P z ^ 3
hy' : P y * Q z ^ 3 = W'.negY Q * P z ^ 3
⊢ (fun a => a * Q z ^ 3) (P y) = (fun a => a * Q z ^ 3) (W'.negY P)

Tactic:
linear_combination (norm := ring1) -Y_sub_Y_add_Y_sub_negY hx + hy + hy'

Result:
no goals
-- Mathlib/Algebra/Lie/Semisimple/Basic.lean
theorem ad_ker_eq_bot_of_hasTrivialRadical [HasTrivialRadical R L] : (ad R L).ker = ⊥

Proof state:
R : Type u_1
L : Type u_2
inst✝³ : CommRing R
inst✝² : LieRing L
inst✝¹ : LieAlgebra R L
inst✝ : HasTrivialRadical R L
⊢ (ad R L).ker = ⊥

Tactic:
simp

Result:
no goals
-- Mathlib/Algebra/Homology/ShortComplex/RightHomology.lean
@[reassoc]
lemma rightHomologyMap'_comp (φ₁ : S₁ ⟶ S₂) (φ₂ : S₂ ⟶ S₃)
    (h₁ : S₁.RightHomologyData) (h₂ : S₂.RightHomologyData) (h₃ : S₃.RightHomologyData) :
    rightHomologyMap' (φ₁ ≫ φ₂) h₁ h₃ = rightHomologyMap' φ₁ h₁ h₂ ≫
      rightHomologyMap' φ₂ h₂ h₃

Proof state:
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : HasZeroMorphisms C
S₁ S₂ S₃ : ShortComplex C
φ₁ : S₁ ⟶ S₂
φ₂ : S₂ ⟶ S₃
h₁ : S₁.RightHomologyData
h₂ : S₂.RightHomologyData
h₃ : S₃.RightHomologyData
γ₁ : RightHomologyMapData φ₁ h₁ h₂ := rightHomologyMapData φ₁ h₁ h₂
⊢ rightHomologyMap' (φ₁ ≫ φ₂) h₁ h₃ = rightHomologyMap' φ₁ h₁ h₂ ≫ rightHomologyMap' φ₂ h₂ h₃

Tactic:
let γ₂ := rightHomologyMapData φ₂ h₂ h₃

Result:
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : HasZeroMorphisms C
S₁ S₂ S₃ : ShortComplex C
φ₁ : S₁ ⟶ S₂
φ₂ : S₂ ⟶ S₃
h₁ : S₁.RightHomologyData
h₂ : S₂.RightHomologyData
h₃ : S₃.RightHomologyData
γ₁ : RightHomologyMapData φ₁ h₁ h₂ := rightHomologyMapData φ₁ h₁ h₂
γ₂ : RightHomologyMapData φ₂ h₂ h₃ := rightHomologyMapData φ₂ h₂ h₃
⊢ rightHomologyMap' (φ₁ ≫ φ₂) h₁ h₃ = rightHomologyMap' φ₁ h₁ h₂ ≫ rightHomologyMap' φ₂ h₂ h₃

Proof state:
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : HasZeroMorphisms C
S₁ S₂ S₃ : ShortComplex C
φ₁ : S₁ ⟶ S₂
φ₂ : S₂ ⟶ S₃
h₁ : S₁.RightHomologyData
h₂ : S₂.RightHomologyData
h₃ : S₃.RightHomologyData
⊢ rightHomologyMap' (φ₁ ≫ φ₂) h₁ h₃ = rightHomologyMap' φ₁ h₁ h₂ ≫ rightHomologyMap' φ₂ h₂ h₃

Tactic:
let γ₁ := rightHomologyMapData φ₁ h₁ h₂

Result:
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : HasZeroMorphisms C
S₁ S₂ S₃ : ShortComplex C
φ₁ : S₁ ⟶ S₂
φ₂ : S₂ ⟶ S₃
h₁ : S₁.RightHomologyData
h₂ : S₂.RightHomologyData
h₃ : S₃.RightHomologyData
γ₁ : RightHomologyMapData φ₁ h₁ h₂ := rightHomologyMapData φ₁ h₁ h₂
⊢ rightHomologyMap' (φ₁ ≫ φ₂) h₁ h₃ = rightHomologyMap' φ₁ h₁ h₂ ≫ rightHomologyMap' φ₂ h₂ h₃

Proof state:
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : HasZeroMorphisms C
S₁ S₂ S₃ : ShortComplex C
φ₁ : S₁ ⟶ S₂
φ₂ : S₂ ⟶ S₃
h₁ : S₁.RightHomologyData
h₂ : S₂.RightHomologyData
h₃ : S₃.RightHomologyData
γ₁ : RightHomologyMapData φ₁ h₁ h₂ := rightHomologyMapData φ₁ h₁ h₂
γ₂ : RightHomologyMapData φ₂ h₂ h₃ := rightHomologyMapData φ₂ h₂ h₃
⊢ rightHomologyMap' (φ₁ ≫ φ₂) h₁ h₃ = rightHomologyMap' φ₁ h₁ h₂ ≫ rightHomologyMap' φ₂ h₂ h₃

Tactic:
rw [γ₁.rightHomologyMap'_eq, γ₂.rightHomologyMap'_eq, (γ₁.comp γ₂).rightHomologyMap'_eq,
  RightHomologyMapData.comp_φH]

Result:
no goals
-- Mathlib/RingTheory/IsAdjoinRoot.lean
theorem aequiv_self (h : IsAdjoinRoot S f) : h.aequiv h = AlgEquiv.refl

Proof state:
case h
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
f : R[X]
h : IsAdjoinRoot S f
a : S
⊢ (h.aequiv h) a = AlgEquiv.refl a

Tactic:
exact h.lift_self_apply a

Result:
no goals

Proof state:
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
f : R[X]
h : IsAdjoinRoot S f
⊢ h.aequiv h = AlgEquiv.refl

Tactic:
ext a

Result:
case h
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
f : R[X]
h : IsAdjoinRoot S f
a : S
⊢ (h.aequiv h) a = AlgEquiv.refl a
-- Mathlib/Algebra/Group/Units/Hom.lean
theorem liftRight_inv_mul (f : M →* N) (h : ∀ x, IsUnit (f x)) (x) :
    ↑(IsUnit.liftRight f h x)⁻¹ * f x = 1 := Units.liftRight_inv_mul (by intro; rfl) x

Proof state:
M : Type u_3
N : Type u_4
inst✝¹ : Monoid M
inst✝ : Monoid N
f : M →* N
h : ∀ (x : M), IsUnit (f x)
x x✝ : M
⊢ ↑⋯.unit = f x✝

Tactic:
rfl

Result:
no goals

Proof state:
M : Type u_3
N : Type u_4
inst✝¹ : Monoid M
inst✝ : Monoid N
f : M →* N
h : ∀ (x : M), IsUnit (f x)
x : M
⊢ ∀ (x : M), ↑⋯.unit = f x

Tactic:
intro

Result:
M : Type u_3
N : Type u_4
inst✝¹ : Monoid M
inst✝ : Monoid N
f : M →* N
h : ∀ (x : M), IsUnit (f x)
x x✝ : M
⊢ ↑⋯.unit = f x✝
-- Mathlib/Analysis/Convex/SimplicialComplex/Basic.lean
theorem vertices_eq : K.vertices = ⋃ k ∈ K.faces, (k : Set E)

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝² : OrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
K : SimplicialComplex 𝕜 E
⊢ K.vertices = ⋃ k ∈ K.faces, ↑k

Tactic:
ext x

Result:
case h
𝕜 : Type u_1
E : Type u_2
inst✝² : OrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
K : SimplicialComplex 𝕜 E
x : E
⊢ x ∈ K.vertices ↔ x ∈ ⋃ k ∈ K.faces, ↑k

Proof state:
case h
𝕜 : Type u_1
E : Type u_2
inst✝² : OrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
K : SimplicialComplex 𝕜 E
x : E
h : x ∈ ⋃ k ∈ K.faces, ↑k
⊢ x ∈ K.vertices

Tactic:
obtain ⟨s, hs, hx⟩ := mem_iUnion₂.1 h

Result:
case h.intro.intro
𝕜 : Type u_1
E : Type u_2
inst✝² : OrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
K : SimplicialComplex 𝕜 E
x : E
h : x ∈ ⋃ k ∈ K.faces, ↑k
s : Finset E
hs : s ∈ K.faces
hx : x ∈ ↑s
⊢ x ∈ K.vertices

Proof state:
case h.intro.intro
𝕜 : Type u_1
E : Type u_2
inst✝² : OrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
K : SimplicialComplex 𝕜 E
x : E
h : x ∈ ⋃ k ∈ K.faces, ↑k
s : Finset E
hs : s ∈ K.faces
hx : x ∈ ↑s
⊢ x ∈ K.vertices

Tactic:
exact K.down_closed hs (Finset.singleton_subset_iff.2 <| mem_coe.1 hx) (singleton_ne_empty _)

Result:
no goals

Proof state:
case h
𝕜 : Type u_1
E : Type u_2
inst✝² : OrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
K : SimplicialComplex 𝕜 E
x : E
⊢ x ∈ K.vertices ↔ x ∈ ⋃ k ∈ K.faces, ↑k

Tactic:
refine ⟨fun h => mem_biUnion h <| mem_coe.2 <| mem_singleton_self x, fun h => ?_⟩

Result:
case h
𝕜 : Type u_1
E : Type u_2
inst✝² : OrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
K : SimplicialComplex 𝕜 E
x : E
h : x ∈ ⋃ k ∈ K.faces, ↑k
⊢ x ∈ K.vertices
-- Mathlib/Topology/Algebra/InfiniteSum/Constructions.lean
theorem HasSum.star (h : HasSum f a) : HasSum (fun b ↦ star (f b)) (star a)

Proof state:
α : Type u_1
β : Type u_2
inst✝³ : AddCommMonoid α
inst✝² : TopologicalSpace α
inst✝¹ : StarAddMonoid α
inst✝ : ContinuousStar α
f : β → α
a : α
h : HasSum f a
⊢ HasSum (fun b => Star.star (f b)) (Star.star a)

Tactic:
simpa only using h.map (starAddEquiv : α ≃+ α) continuous_star

Result:
no goals
-- Mathlib/Analysis/Calculus/FDeriv/Prod.lean
theorem hasFDerivAtFilter_pi' :
    HasFDerivAtFilter Φ Φ' x L ↔
      ∀ i, HasFDerivAtFilter (fun x => Φ x i) ((proj i).comp Φ') x L

Proof state:
𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
x : E
L : Filter E
ι : Type u_6
inst✝² : Fintype ι
F' : ι → Type u_7
inst✝¹ : (i : ι) → NormedAddCommGroup (F' i)
inst✝ : (i : ι) → NormedSpace 𝕜 (F' i)
Φ : E → (i : ι) → F' i
Φ' : E →L[𝕜] (i : ι) → F' i
⊢ ((fun x' => Φ x' - Φ x - Φ' (x' - x)) =o[L] fun x' => x' - x) ↔
    ∀ (i : ι), (fun x' => Φ x' i - Φ x i - ((proj i).comp Φ') (x' - x)) =o[L] fun x' => x' - x

Tactic:
exact isLittleO_pi

Result:
no goals

Proof state:
𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
x : E
L : Filter E
ι : Type u_6
inst✝² : Fintype ι
F' : ι → Type u_7
inst✝¹ : (i : ι) → NormedAddCommGroup (F' i)
inst✝ : (i : ι) → NormedSpace 𝕜 (F' i)
Φ : E → (i : ι) → F' i
Φ' : E →L[𝕜] (i : ι) → F' i
⊢ HasFDerivAtFilter Φ Φ' x L ↔ ∀ (i : ι), HasFDerivAtFilter (fun x => Φ x i) ((proj i).comp Φ') x L

Tactic:
simp only [hasFDerivAtFilter_iff_isLittleO, ContinuousLinearMap.coe_pi]

Result:
𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
x : E
L : Filter E
ι : Type u_6
inst✝² : Fintype ι
F' : ι → Type u_7
inst✝¹ : (i : ι) → NormedAddCommGroup (F' i)
inst✝ : (i : ι) → NormedSpace 𝕜 (F' i)
Φ : E → (i : ι) → F' i
Φ' : E →L[𝕜] (i : ι) → F' i
⊢ ((fun x' => Φ x' - Φ x - Φ' (x' - x)) =o[L] fun x' => x' - x) ↔
    ∀ (i : ι), (fun x' => Φ x' i - Φ x i - ((proj i).comp Φ') (x' - x)) =o[L] fun x' => x' - x
-- Mathlib/Combinatorics/HalesJewett.lean
theorem apply_none {α ι} (l : Line α ι) (x : α) (i : ι) (h : l.idxFun i = none) : l x i = x

Proof state:
α : Type u_5
ι : Type u_6
l : Line α ι
x : α
i : ι
h : l.idxFun i = none
⊢ ↑l x i = x

Tactic:
simp only [Option.getD_none, h, l.apply_def]

Result:
no goals
-- Mathlib/Algebra/Homology/Additive.lean
theorem singleMapHomologicalComplex_hom_app_ne {i j : ι} (h : i ≠ j) (X : W₁) :
    ((singleMapHomologicalComplex F c j).hom.app X).f i = 0

Proof state:
ι : Type u_1
W₁ : Type u_3
W₂ : Type u_4
inst✝⁷ : Category.{u_6, u_3} W₁
inst✝⁶ : Category.{u_5, u_4} W₂
inst✝⁵ : HasZeroMorphisms W₁
inst✝⁴ : HasZeroMorphisms W₂
inst✝³ : HasZeroObject W₁
inst✝² : HasZeroObject W₂
F : W₁ ⥤ W₂
inst✝¹ : F.PreservesZeroMorphisms
c : ComplexShape ι
inst✝ : DecidableEq ι
i j : ι
h : i ≠ j
X : W₁
⊢ ((singleMapHomologicalComplex F c j).hom.app X).f i = 0

Tactic:
simp [singleMapHomologicalComplex, h]

Result:
no goals
-- Mathlib/NumberTheory/NumberField/Units/Basic.lean
theorem rootsOfUnity_eq_torsion [NumberField K] :
    rootsOfUnity (torsionOrder K) (𝓞 K) = torsion K

Proof state:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
⊢ rootsOfUnity (↑(torsionOrder K)) (𝓞 K) = torsion K

Tactic:
ext ζ

Result:
case h
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
ζ : (𝓞 K)ˣ
⊢ ζ ∈ rootsOfUnity (↑(torsionOrder K)) (𝓞 K) ↔ ζ ∈ torsion K

Proof state:
case h.refine_2
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
ζ : (𝓞 K)ˣ
h : ζ ∈ CommGroup.torsion (𝓞 K)ˣ
⊢ ζ ^ ↑(torsionOrder K) = 1

Tactic:
exact Subtype.ext_iff.mp (@pow_card_eq_one (torsion K) _ _ ⟨ζ, h⟩)

Result:
no goals

Proof state:
case h
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
ζ : (𝓞 K)ˣ
⊢ ζ ∈ rootsOfUnity (↑(torsionOrder K)) (𝓞 K) ↔ ζ ∈ torsion K

Tactic:
rw [torsion, mem_rootsOfUnity]

Result:
case h
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
ζ : (𝓞 K)ˣ
⊢ ζ ^ ↑(torsionOrder K) = 1 ↔ ζ ∈ CommGroup.torsion (𝓞 K)ˣ

Proof state:
case h.refine_1
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
ζ : (𝓞 K)ˣ
h : ζ ^ ↑(torsionOrder K) = 1
⊢ ∃ n, 0 < n ∧ ζ ^ n = 1

Tactic:
exact ⟨↑(torsionOrder K), (torsionOrder K).prop, h⟩

Result:
no goals

Proof state:
case h.refine_1
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
ζ : (𝓞 K)ˣ
h : ζ ^ ↑(torsionOrder K) = 1
⊢ ζ ∈ CommGroup.torsion (𝓞 K)ˣ

Tactic:
rw [CommGroup.mem_torsion, isOfFinOrder_iff_pow_eq_one]

Result:
case h.refine_1
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
ζ : (𝓞 K)ˣ
h : ζ ^ ↑(torsionOrder K) = 1
⊢ ∃ n, 0 < n ∧ ζ ^ n = 1

Proof state:
case h
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
ζ : (𝓞 K)ˣ
⊢ ζ ^ ↑(torsionOrder K) = 1 ↔ ζ ∈ CommGroup.torsion (𝓞 K)ˣ

Tactic:
refine ⟨fun h => ?_, fun h => ?_⟩

Result:
case h.refine_1
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
ζ : (𝓞 K)ˣ
h : ζ ^ ↑(torsionOrder K) = 1
⊢ ζ ∈ CommGroup.torsion (𝓞 K)ˣ

case h.refine_2
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
ζ : (𝓞 K)ˣ
h : ζ ∈ CommGroup.torsion (𝓞 K)ˣ
⊢ ζ ^ ↑(torsionOrder K) = 1
-- Mathlib/Data/Sum/Basic.lean
theorem eq_right_iff_getRight_eq {b : β} : x = inr b ↔ ∃ h, x.getRight h = b

Proof state:
α : Type u
β : Type v
x : α ⊕ β
b : β
⊢ x = inr b ↔ ∃ h, x.getRight h = b

Tactic:
cases x <;> simp

Result:
no goals
-- Mathlib/RingTheory/LaurentSeries.lean
theorem single_zpow (n : ℤ) :
    single (n : ℤ) (1 : F) = single (1 : ℤ) 1 ^ n

Proof state:
case negSucc
F : Type u
inst✝ : Field F
n : ℕ
⊢ (single (Int.negSucc n)) 1 = (single 1) 1 ^ Int.negSucc n

Tactic:
rw [Int.negSucc_coe, Int.ofNat_add, Nat.cast_one, ← inv_one,
  single_inv (n + 1 : ℤ) one_ne_zero, zpow_neg, ← Nat.cast_one, ← Int.ofNat_add,
  Nat.cast_one, inv_inj, zpow_natCast, single_one_eq_pow, inv_one]

Result:
no goals

Proof state:
case ofNat
F : Type u
inst✝ : Field F
n : ℕ
⊢ (single (Int.ofNat n)) 1 = (single 1) 1 ^ Int.ofNat n

Tactic:
apply single_one_eq_pow

Result:
no goals

Proof state:
F : Type u
inst✝ : Field F
n : ℤ
⊢ (single n) 1 = (single 1) 1 ^ n

Tactic:
cases n with
| ofNat n => apply single_one_eq_pow
| negSucc n =>
  rw [Int.negSucc_coe, Int.ofNat_add, Nat.cast_one, ← inv_one,
    single_inv (n + 1 : ℤ) one_ne_zero, zpow_neg, ← Nat.cast_one, ← Int.ofNat_add,
    Nat.cast_one, inv_inj, zpow_natCast, single_one_eq_pow, inv_one]

Result:
no goals
-- Mathlib/RingTheory/Polynomial/Pochhammer.lean
theorem ascPochhammer_succ_comp_X_add_one (n : ℕ) :
    (ascPochhammer S (n + 1)).comp (X + 1) =
      ascPochhammer S (n + 1) + (n + 1) • (ascPochhammer S n).comp (X + 1)

Proof state:
S : Type u
inst✝ : Semiring S
n : ℕ
⊢ (ascPochhammer ℕ (n + 1)).comp (X + 1) = ascPochhammer ℕ (n + 1) + (↑n + 1) * (ascPochhammer ℕ n).comp (X + 1)

Tactic:
nth_rw 2 [ascPochhammer_succ_left]

Result:
S : Type u
inst✝ : Semiring S
n : ℕ
⊢ (ascPochhammer ℕ (n + 1)).comp (X + 1) =
    X * (ascPochhammer ℕ n).comp (X + 1) + (↑n + 1) * (ascPochhammer ℕ n).comp (X + 1)

Proof state:
S : Type u
inst✝ : Semiring S
n : ℕ
this : (ascPochhammer ℕ (n + 1)).comp (X + 1) = ascPochhammer ℕ (n + 1) + (↑n + 1) * (ascPochhammer ℕ n).comp (X + 1)
⊢ (ascPochhammer S (n + 1)).comp (X + 1) = ascPochhammer S (n + 1) + (n + 1) • (ascPochhammer S n).comp (X + 1)

Tactic:
simpa [map_comp] using congr_arg (Polynomial.map (Nat.castRingHom S)) this

Result:
no goals

Proof state:
S : Type u
inst✝ : Semiring S
n : ℕ
⊢ (↑n + X + 1) * (ascPochhammer ℕ n).comp (X + 1) = (X + (↑n + 1)) * (ascPochhammer ℕ n).comp (X + 1)

Tactic:
ring

Result:
no goals

Proof state:
S : Type u
inst✝ : Semiring S
n : ℕ
⊢ (ascPochhammer ℕ (n + 1)).comp (X + 1) =
    X * (ascPochhammer ℕ n).comp (X + 1) + (↑n + 1) * (ascPochhammer ℕ n).comp (X + 1)

Tactic:
rw [← add_mul, ascPochhammer_succ_right ℕ n, mul_comp, mul_comm, add_comp, X_comp, natCast_comp,
  add_comm, ← add_assoc]

Result:
S : Type u
inst✝ : Semiring S
n : ℕ
⊢ (↑n + X + 1) * (ascPochhammer ℕ n).comp (X + 1) = (X + (↑n + 1)) * (ascPochhammer ℕ n).comp (X + 1)

Proof state:
S : Type u
inst✝ : Semiring S
n : ℕ
⊢ (ascPochhammer S (n + 1)).comp (X + 1) = ascPochhammer S (n + 1) + (n + 1) • (ascPochhammer S n).comp (X + 1)

Tactic:
suffices (ascPochhammer ℕ (n + 1)).comp (X + 1) =
    ascPochhammer ℕ (n + 1) + (n + 1) * (ascPochhammer ℕ n).comp (X + 1)
  by simpa [map_comp] using congr_arg (Polynomial.map (Nat.castRingHom S)) this

Result:
S : Type u
inst✝ : Semiring S
n : ℕ
⊢ (ascPochhammer ℕ (n + 1)).comp (X + 1) = ascPochhammer ℕ (n + 1) + (↑n + 1) * (ascPochhammer ℕ n).comp (X + 1)