harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Algebra/Homology/HomotopyCategory/HomComplexShift.lean
lemma leftShift_v (a n' : ℤ) (hn' : n + a = n') (p q : ℤ) (hpq : p + n' = q)
    (p' : ℤ) (hp' : p' + n = q) :
    (γ.leftShift a n' hn').v p q hpq = (a * n' + ((a * (a - 1))/2)).negOnePow •
      (K.shiftFunctorObjXIso a p p'
        (by rw [← add_left_inj n, hp', add_assoc, add_comm a, hn', hpq])).hom ≫ γ.v p' q hp'

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
K L : CochainComplex C ℤ
n : ℤ
γ : Cochain K L n
a n' : ℤ
hn' : n + a = n'
p q : ℤ
hpq : p + n' = q
p' : ℤ
hp' : p' + n = q
⊢ p' = p + a

Tactic:
omega

Result:
no goals

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
K L : CochainComplex C ℤ
n : ℤ
γ : Cochain K L n
a n' : ℤ
hn' : n + a = n'
p q : ℤ
hpq : p + n' = q
hp' : p + a + n = q
⊢ (γ.leftShift a n' hn').v p q hpq =
    (a * n' + a * (a - 1) / 2).negOnePow • (K.shiftFunctorObjXIso a p (p + a) ⋯).hom ≫ γ.v (p + a) q hp'

Tactic:
dsimp only [leftShift]

Result:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
K L : CochainComplex C ℤ
n : ℤ
γ : Cochain K L n
a n' : ℤ
hn' : n + a = n'
p q : ℤ
hpq : p + n' = q
hp' : p + a + n = q
⊢ (mk fun p q hpq =>
          (a * n' + a * (a - 1) / 2).negOnePow • (K.shiftFunctorObjXIso a p (p + a) ⋯).hom ≫ γ.v (p + a) q ⋯).v
      p q hpq =
    (a * n' + a * (a - 1) / 2).negOnePow • (K.shiftFunctorObjXIso a p (p + a) ⋯).hom ≫ γ.v (p + a) q hp'

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
K L : CochainComplex C ℤ
n : ℤ
γ : Cochain K L n
a n' : ℤ
hn' : n + a = n'
p q : ℤ
hpq : p + n' = q
hp' : p + a + n = q
⊢ (mk fun p q hpq =>
          (a * n' + a * (a - 1) / 2).negOnePow • (K.shiftFunctorObjXIso a p (p + a) ⋯).hom ≫ γ.v (p + a) q ⋯).v
      p q hpq =
    (a * n' + a * (a - 1) / 2).negOnePow • (K.shiftFunctorObjXIso a p (p + a) ⋯).hom ≫ γ.v (p + a) q hp'

Tactic:
simp only [mk_v]

Result:
no goals

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
K L : CochainComplex C ℤ
n : ℤ
γ : Cochain K L n
a n' : ℤ
hn' : n + a = n'
p q : ℤ
hpq : p + n' = q
p' : ℤ
hp' : p' + n = q
⊢ (γ.leftShift a n' hn').v p q hpq =
    (a * n' + a * (a - 1) / 2).negOnePow • (K.shiftFunctorObjXIso a p p' ⋯).hom ≫ γ.v p' q hp'

Tactic:
obtain rfl : p' = p + a := by omega

Result:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
K L : CochainComplex C ℤ
n : ℤ
γ : Cochain K L n
a n' : ℤ
hn' : n + a = n'
p q : ℤ
hpq : p + n' = q
hp' : p + a + n = q
⊢ (γ.leftShift a n' hn').v p q hpq =
    (a * n' + a * (a - 1) / 2).negOnePow • (K.shiftFunctorObjXIso a p (p + a) ⋯).hom ≫ γ.v (p + a) q hp'

Proof state:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
R : Type u_1
inst✝¹ : Ring R
inst✝ : Linear R C
K L M : CochainComplex C ℤ
n : ℤ
γ γ₁ γ₂ : Cochain K L n
a n' : ℤ
hn' : n + a = n'
p q : ℤ
hpq : p + n' = q
p' : ℤ
hp' : p' + n = q
⊢ p' = p + a

Tactic:
rw [← add_left_inj n, hp', add_assoc, add_comm a, hn', hpq]

Result:
no goals
-- Mathlib/AlgebraicGeometry/EllipticCurve/Projective.lean
lemma negDblY_of_Z_ne_zero {P Q : Fin 3 → F} (hP : W.Equation P) (hQ : W.Equation Q)
    (hPz : P z ≠ 0) (hQz : Q z ≠ 0) (hx : P x * Q z = Q x * P z) (hy : P y * Q z ≠ W.negY Q * P z) :
    W.negDblY P / W.dblZ P = W.toAffine.negAddY (P x / P z) (Q x / Q z) (P y / P z)
      (W.toAffine.slope (P x / P z) (Q x / Q z) (P y / P z) (Q y / Q z))

Proof state:
F : Type u
inst✝ : Field F
W : Projective F
P Q : Fin 3 → F
hP : W.Equation P
hQ : W.Equation Q
hPz : P z ≠ 0
hQz : Q z ≠ 0
hx : P x * Q z = Q x * P z
hy : P y * Q z ≠ W.negY Q * P z
⊢ W.negDblY P / W.dblZ P =
    (toAffine W).negAddY (P x / P z) (Q x / Q z) (P y / P z)
      ((toAffine W).slope (P x / P z) (Q x / Q z) (P y / P z) (Q y / Q z))

Tactic:
rw [negDblY_eq hP hPz, dblZ, toAffine_slope_of_eq hP hQ hPz hQz hx hy, ← (X_eq_iff hPz hQz).mp hx,
  toAffine_negAddY_of_eq hPz <| sub_ne_zero.mpr <| Y_ne_negY_of_Y_ne' hP hQ hPz hQz hx hy]

Result:
no goals
-- Mathlib/Order/Interval/Multiset.lean
theorem Ico_add_Ico_eq_Ico {a b c : α} (hab : a ≤ b) (hbc : b ≤ c) :
    Ico a b + Ico b c = Ico a c

Proof state:
α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : LocallyFiniteOrder α
a b c : α
hab : a ≤ b
hbc : b ≤ c
⊢ Ico a b + Ico b c = Ico a c

Tactic:
rw [add_eq_union_iff_disjoint.2 (Ico_disjoint_Ico le_rfl), Ico, Ico, Ico, ← Finset.union_val,
  Finset.Ico_union_Ico_eq_Ico hab hbc]

Result:
no goals
-- Mathlib/SetTheory/Cardinal/Arithmetic.lean
theorem mk_list_eq_mk (α : Type u) [Infinite α] : #(List α) = #α :=
  have H1 : ℵ₀ ≤ #α := aleph0_le_mk α
  Eq.symm <|
    le_antisymm ((le_def _ _).2 ⟨⟨fun a => [a], fun _ => by simp⟩⟩) <|
      calc
        #(List α) = sum fun n : ℕ => #α ^ (n : Cardinal.{u}) := mk_list_eq_sum_pow α
        _ ≤ sum fun _ : ℕ => #α := sum_le_sum _ _ fun n => pow_le H1 <| nat_lt_aleph0 n
        _ = #α

Proof state:
α : Type u
inst✝ : Infinite α
H1 : ℵ₀ ≤ #α
x✝ : α
⊢ ∀ ⦃a₂ : α⦄, (fun a => [a]) x✝ = (fun a => [a]) a₂ → x✝ = a₂

Tactic:
simp

Result:
no goals

Proof state:
α : Type u
inst✝ : Infinite α
H1 : ℵ₀ ≤ #α
⊢ (sum fun x => #α) = #α

Tactic:
simp [H1]

Result:
no goals
-- Mathlib/Data/Finset/Basic.lean
theorem erase_cons {s : Finset α} {a : α} (h : a ∉ s) : (s.cons a h).erase a = s

Proof state:
α : Type u_1
inst✝ : DecidableEq α
s : Finset α
a : α
h : a ∉ s
⊢ (cons a s h).erase a = s

Tactic:
rw [cons_eq_insert, erase_insert_eq_erase, erase_eq_of_not_mem h]

Result:
no goals
-- Mathlib/.lake/packages/batteries/Batteries/Data/RBMap/WF.lean
theorem All_and {t : RBNode α} : t.All (fun a => p a ∧ q a) ↔ t.All p ∧ t.All q

Proof state:
α : Type u_1
p q : α → Prop
t : RBNode α
⊢ All (fun a => p a ∧ q a) t ↔ All p t ∧ All q t

Tactic:
induction t <;> simp [*, and_assoc, and_left_comm]

Result:
no goals
-- Mathlib/Data/Set/Lattice.lean
theorem preimage_iUnion₂ {f : α → β} {s : ∀ i, κ i → Set β} :
    (f ⁻¹' ⋃ (i) (j), s i j) = ⋃ (i) (j), f ⁻¹' s i j

Proof state:
α : Type u_1
β : Type u_2
ι : Sort u_5
κ : ι → Sort u_8
f : α → β
s : (i : ι) → κ i → Set β
⊢ f ⁻¹' ⋃ i, ⋃ j, s i j = ⋃ i, ⋃ j, f ⁻¹' s i j

Tactic:
simp_rw [preimage_iUnion]

Result:
no goals
-- Mathlib/Analysis/Calculus/IteratedDeriv/Lemmas.lean
/-- The iterated derivative commutes with shifting the function by a constant on the right. -/
lemma iteratedDeriv_comp_add_const (n : ℕ) (f : 𝕜 → F) (s : 𝕜) :
    iteratedDeriv n (fun z ↦ f (z + s)) = fun t ↦ iteratedDeriv n f (t + s)

Proof state:
case zero
𝕜 : Type u_1
F : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : 𝕜 → F
s : 𝕜
⊢ (iteratedDeriv 0 fun z => f (z + s)) = fun t => iteratedDeriv 0 f (t + s)

Tactic:
simp only [iteratedDeriv_zero]

Result:
no goals

Proof state:
case succ
𝕜 : Type u_1
F : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : 𝕜 → F
s : 𝕜
n : ℕ
IH : (iteratedDeriv n fun z => f (z + s)) = fun t => iteratedDeriv n f (t + s)
⊢ (iteratedDeriv (n + 1) fun z => f (z + s)) = fun t => iteratedDeriv (n + 1) f (t + s)

Tactic:
simpa only [iteratedDeriv_succ, IH] using funext <| deriv_comp_add_const _ s

Result:
no goals

Proof state:
𝕜 : Type u_1
F : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
n : ℕ
f : 𝕜 → F
s : 𝕜
⊢ (iteratedDeriv n fun z => f (z + s)) = fun t => iteratedDeriv n f (t + s)

Tactic:
induction n with
| zero => simp only [iteratedDeriv_zero]
| succ n IH =>
  simpa only [iteratedDeriv_succ, IH] using funext <| deriv_comp_add_const _ s

Result:
no goals
-- Mathlib/Data/Finset/Lattice/Lemmas.lean
theorem insert_inter_of_not_mem {s₁ s₂ : Finset α} {a : α} (h : a ∉ s₂) :
    insert a s₁ ∩ s₂ = s₁ ∩ s₂ :=
  ext fun x => by
    have : ¬(x = a ∧ x ∈ s₂)

Proof state:
α : Type u_1
inst✝ : DecidableEq α
s₁ s₂ : Finset α
a : α
h : a ∉ s₂
x : α
⊢ x ∈ insert a s₁ ∩ s₂ ↔ x ∈ s₁ ∩ s₂

Tactic:
have : ¬(x = a ∧ x ∈ s₂) := by rintro ⟨rfl, H⟩; exact h H

Result:
α : Type u_1
inst✝ : DecidableEq α
s₁ s₂ : Finset α
a : α
h : a ∉ s₂
x : α
this : ¬(x = a ∧ x ∈ s₂)
⊢ x ∈ insert a s₁ ∩ s₂ ↔ x ∈ s₁ ∩ s₂

Proof state:
case intro
α : Type u_1
inst✝ : DecidableEq α
s₁ s₂ : Finset α
x : α
H : x ∈ s₂
h : x ∉ s₂
⊢ False

Tactic:
exact h H

Result:
no goals

Proof state:
α : Type u_1
inst✝ : DecidableEq α
s₁ s₂ : Finset α
a : α
h : a ∉ s₂
x : α
⊢ ¬(x = a ∧ x ∈ s₂)

Tactic:
rintro ⟨rfl, H⟩

Result:
case intro
α : Type u_1
inst✝ : DecidableEq α
s₁ s₂ : Finset α
x : α
H : x ∈ s₂
h : x ∉ s₂
⊢ False

Proof state:
α : Type u_1
inst✝ : DecidableEq α
s₁ s₂ : Finset α
a : α
h : a ∉ s₂
x : α
this : ¬(x = a ∧ x ∈ s₂)
⊢ x ∈ insert a s₁ ∩ s₂ ↔ x ∈ s₁ ∩ s₂

Tactic:
simp only [mem_inter, mem_insert, or_and_right, this, false_or]

Result:
no goals
-- Mathlib/Topology/Separation/Basic.lean
theorem IsCompact.closure_eq_biUnion_closure_singleton {K : Set X} (hK : IsCompact K) :
    closure K = ⋃ x ∈ K, closure {x}

Proof state:
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : R1Space X
K : Set X
hK : IsCompact K
⊢ closure K = ⋃ x ∈ K, closure {x}

Tactic:
simp only [hK.closure_eq_biUnion_inseparable, ← specializes_iff_inseparable,
  specializes_iff_mem_closure, setOf_mem_eq]

Result:
no goals
-- Mathlib/Topology/Compactness/DeltaGeneratedSpace.lean
/-- The delta-generated topology on `X` does in fact turn `X` into a delta-generated space. -/
lemma deltaGeneratedSpace_deltaGenerated {X : Type*} {t : TopologicalSpace X} :
    @DeltaGeneratedSpace X (@deltaGenerated X t)

Proof state:
X : Type u_3
t : TopologicalSpace X
⊢ DeltaGeneratedSpace X

Tactic:
let _ := @deltaGenerated X t

Result:
X : Type u_3
t : TopologicalSpace X
x✝ : TopologicalSpace X := deltaGenerated X
⊢ DeltaGeneratedSpace X

Proof state:
case le_deltaGenerated
X : Type u_3
t : TopologicalSpace X
x✝ : TopologicalSpace X := deltaGenerated X
⊢ deltaGenerated X ≤ deltaGenerated X

Tactic:
rw [@deltaGenerated_deltaGenerated_eq X t]

Result:
no goals

Proof state:
X : Type u_3
t : TopologicalSpace X
x✝ : TopologicalSpace X := deltaGenerated X
⊢ DeltaGeneratedSpace X

Tactic:
constructor

Result:
case le_deltaGenerated
X : Type u_3
t : TopologicalSpace X
x✝ : TopologicalSpace X := deltaGenerated X
⊢ deltaGenerated X ≤ deltaGenerated X
-- Mathlib/Geometry/Manifold/MFDeriv/Basic.lean
theorem mfderiv_congr {f' : M → M'} (h : f = f') :
    @Eq (E →L[𝕜] E') (mfderiv I I' f 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
f' : M → M'
h : f = f'
⊢ mfderiv I I' f x = mfderiv I I' f' x

Tactic:
subst h

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
⊢ mfderiv I I' f 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
⊢ mfderiv I I' f x = mfderiv I I' f x

Tactic:
rfl

Result:
no goals
-- Mathlib/Analysis/LocallyConvex/AbsConvex.lean
theorem absConvexHull_eq_iInter :
    absConvexHull 𝕜 s = ⋂ (t : Set E) (_ : s ⊆ t) (_ : AbsConvex 𝕜 t), t

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝³ : SeminormedRing 𝕜
inst✝² : SMul 𝕜 E
inst✝¹ : SMul ℝ E
inst✝ : AddCommMonoid E
s : Set E
⊢ (absConvexHull 𝕜) s = ⋂ t, ⋂ (_ : s ⊆ t), ⋂ (_ : AbsConvex 𝕜 t), t

Tactic:
simp [absConvexHull, iInter_subtype, iInter_and]

Result:
no goals
-- Mathlib/Data/Matroid/Circuit.lean
lemma IsCircuit.minimal_not_indep (hC : M.IsCircuit C) : Minimal (¬ M.Indep ·) C

Proof state:
α : Type u_1
M : Matroid α
C : Set α
hC : M.IsCircuit C
⊢ ∀ ⦃t : Set α⦄, t ⊂ C → M.Indep t

Tactic:
exact fun ⦃t⦄ a ↦ ssubset_indep hC a

Result:
no goals

Proof state:
α : Type u_1
M : Matroid α
C : Set α
hC : M.IsCircuit C
⊢ Minimal (fun x => ¬M.Indep x) C

Tactic:
simp_rw [minimal_iff_forall_ssubset, and_iff_right hC.not_indep, not_not]

Result:
α : Type u_1
M : Matroid α
C : Set α
hC : M.IsCircuit C
⊢ ∀ ⦃t : Set α⦄, t ⊂ C → M.Indep t
-- Mathlib/LinearAlgebra/Orientation.lean
theorem orientation_eq_or_eq_neg (e : Basis ι R M) (x : Orientation R M ι) :
    x = e.orientation ∨ x = -e.orientation

Proof state:
R : Type u_1
inst✝⁴ : LinearOrderedCommRing R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
ι : Type u_3
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
e : Basis ι R M
x : Orientation R M ι
⊢ x = e.orientation ∨ x = -e.orientation

Tactic:
induction x using Module.Ray.ind with | h x hx =>
rw [← x.map_basis_ne_zero_iff e] at hx
rwa [Basis.orientation, ray_eq_iff, neg_rayOfNeZero, ray_eq_iff, x.eq_smul_basis_det e,
  sameRay_neg_smul_left_iff_of_ne e.det_ne_zero hx, sameRay_smul_left_iff_of_ne e.det_ne_zero hx,
  lt_or_lt_iff_ne, ne_comm]

Result:
no goals

Proof state:
case h
R : Type u_1
inst✝⁴ : LinearOrderedCommRing R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
ι : Type u_3
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
e : Basis ι R M
x : M [⋀^ι]→ₗ[R] R
hx : x ≠ 0
⊢ rayOfNeZero R x hx = e.orientation ∨ rayOfNeZero R x hx = -e.orientation

Tactic:
rw [← x.map_basis_ne_zero_iff e] at hx

Result:
case h
R : Type u_1
inst✝⁴ : LinearOrderedCommRing R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
ι : Type u_3
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
e : Basis ι R M
x : M [⋀^ι]→ₗ[R] R
hx✝ : x ≠ 0
hx : x ⇑e ≠ 0
⊢ rayOfNeZero R x hx✝ = e.orientation ∨ rayOfNeZero R x hx✝ = -e.orientation

Proof state:
case h
R : Type u_1
inst✝⁴ : LinearOrderedCommRing R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
ι : Type u_3
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
e : Basis ι R M
x : M [⋀^ι]→ₗ[R] R
hx✝ : x ≠ 0
hx : x ⇑e ≠ 0
⊢ rayOfNeZero R x hx✝ = e.orientation ∨ rayOfNeZero R x hx✝ = -e.orientation

Tactic:
rwa [Basis.orientation, ray_eq_iff, neg_rayOfNeZero, ray_eq_iff, x.eq_smul_basis_det e,
  sameRay_neg_smul_left_iff_of_ne e.det_ne_zero hx, sameRay_smul_left_iff_of_ne e.det_ne_zero hx,
  lt_or_lt_iff_ne, ne_comm]

Result:
no goals
-- Mathlib/CategoryTheory/Limits/Shapes/Pullback/Mono.lean
theorem epi_inr_of_is_pushout_of_epi {t : PushoutCocone f g} (ht : IsColimit t) [Epi f] :
    Epi t.inr :=
  ⟨fun {W} h k i => IsColimit.hom_ext ht (by simp [← cancel_epi f, t.condition_assoc, i]) i⟩

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
t : PushoutCocone f g
ht : IsColimit t
inst✝ : Epi f
W : C
h k : t.pt ⟶ W
i : t.inr ≫ h = t.inr ≫ k
⊢ t.inl ≫ h = t.inl ≫ k

Tactic:
simp [← cancel_epi f, t.condition_assoc, i]

Result:
no goals
-- Mathlib/Analysis/Asymptotics/Defs.lean
theorem isBigO_snd_prod' {f' : α → E' × F'} : (fun x => (f' x).2) =O[l] f'

Proof state:
α : Type u_1
E' : Type u_6
F' : Type u_7
inst✝¹ : SeminormedAddCommGroup E'
inst✝ : SeminormedAddCommGroup F'
l : Filter α
f' : α → E' × F'
⊢ (fun x => (f' x).2) =O[l] f'

Tactic:
simpa [IsBigO_def, IsBigOWith_def] using isBigO_snd_prod (E' := E') (F' := F')

Result:
no goals
-- Mathlib/Geometry/Euclidean/Angle/Oriented/Rotation.lean
theorem rotation_map (θ : Real.Angle) (f : V ≃ₗᵢ[ℝ] V') (x : V') :
    (Orientation.map (Fin 2) f.toLinearEquiv o).rotation θ x = f (o.rotation θ (f.symm x))

Proof state:
V : Type u_1
V' : Type u_2
inst✝⁵ : NormedAddCommGroup V
inst✝⁴ : NormedAddCommGroup V'
inst✝³ : InnerProductSpace ℝ V
inst✝² : InnerProductSpace ℝ V'
inst✝¹ : Fact (finrank ℝ V = 2)
inst✝ : Fact (finrank ℝ V' = 2)
o : Orientation ℝ V (Fin 2)
θ : Real.Angle
f : V ≃ₗᵢ[ℝ] V'
x : V'
⊢ (((map (Fin 2) f.toLinearEquiv) o).rotation θ) x = f ((o.rotation θ) (f.symm x))

Tactic:
simp [rotation_apply, o.rightAngleRotation_map]

Result:
no goals
-- Mathlib/Analysis/Analytic/Inverse.lean
theorem leftInv_eq_rightInv (p : FormalMultilinearSeries 𝕜 E F) (i : E ≃L[𝕜] F) (x : E)
    (h : p 1 = (continuousMultilinearCurryFin1 𝕜 E F).symm i) :
    leftInv p i x = rightInv p i x :=
  calc
    leftInv p i x = (leftInv p i x).comp (id 𝕜 F (p 0 0))

Proof state:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
i : E ≃L[𝕜] F
x : E
h : p 1 = (continuousMultilinearCurryFin1 𝕜 E F).symm ↑i
⊢ (id 𝕜 E x).comp (p.rightInv i x) = p.rightInv i x

Tactic:
simp [id_comp' _ _ 0]

Result:
no goals

Proof state:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
i : E ≃L[𝕜] F
x : E
h : p 1 = (continuousMultilinearCurryFin1 𝕜 E F).symm ↑i
⊢ (p.leftInv i x).comp (id 𝕜 F ((p 0) 0)) = (p.leftInv i x).comp (p.comp (p.rightInv i x))

Tactic:
rw [comp_rightInv p i _ h]

Result:
no goals

Proof state:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
i : E ≃L[𝕜] F
x : E
h : p 1 = (continuousMultilinearCurryFin1 𝕜 E F).symm ↑i
⊢ ((p.leftInv i x).comp p).comp (p.rightInv i x) = (id 𝕜 E x).comp (p.rightInv i x)

Tactic:
rw [leftInv_comp p i _ h]

Result:
no goals

Proof state:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
i : E ≃L[𝕜] F
x : E
h : p 1 = (continuousMultilinearCurryFin1 𝕜 E F).symm ↑i
⊢ (p.leftInv i x).comp (p.comp (p.rightInv i x)) = ((p.leftInv i x).comp p).comp (p.rightInv i x)

Tactic:
rw [comp_assoc]

Result:
no goals

Proof state:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
i : E ≃L[𝕜] F
x : E
h : p 1 = (continuousMultilinearCurryFin1 𝕜 E F).symm ↑i
⊢ p.leftInv i x = (p.leftInv i x).comp (id 𝕜 F ((p 0) 0))

Tactic:
simp

Result:
no goals
-- Mathlib/SetTheory/Ordinal/Veblen.lean
theorem veblenWith_le_veblenWith_iff :
    veblenWith f o₁ a ≤ veblenWith f o₂ b ↔
      o₁ = o₂ ∧ a ≤ b ∨ o₁ < o₂ ∧ a ≤ veblenWith f o₂ b ∨ o₂ < o₁ ∧ veblenWith f o₁ a ≤ b

Proof state:
f : Ordinal.{u} → Ordinal.{u}
o₁ o₂ a b : Ordinal.{u}
hf : IsNormal f
⊢ veblenWith f o₁ a ≤ veblenWith f o₂ b ↔
    o₁ = o₂ ∧ a ≤ b ∨ o₁ < o₂ ∧ a ≤ veblenWith f o₂ b ∨ o₂ < o₁ ∧ veblenWith f o₁ a ≤ b

Tactic:
rw [← not_lt, ← cmp_eq_gt_iff, cmp_veblenWith hf]

Result:
f : Ordinal.{u} → Ordinal.{u}
o₁ o₂ a b : Ordinal.{u}
hf : IsNormal f
⊢ ¬(match cmp o₁ o₂ with
        | Ordering.eq => cmp a b
        | Ordering.lt => cmp a (veblenWith f o₂ b)
        | Ordering.gt => cmp (veblenWith f o₁ a) b) =
        Ordering.gt ↔
    o₁ = o₂ ∧ a ≤ b ∨ o₁ < o₂ ∧ a ≤ veblenWith f o₂ b ∨ o₂ < o₁ ∧ veblenWith f o₁ a ≤ b

Proof state:
f : Ordinal.{u} → Ordinal.{u}
o₁ o₂ a b : Ordinal.{u}
hf : IsNormal f
⊢ ¬(match cmp o₁ o₂ with
        | Ordering.eq => cmp a b
        | Ordering.lt => cmp a (veblenWith f o₂ b)
        | Ordering.gt => cmp (veblenWith f o₁ a) b) =
        Ordering.gt ↔
    o₁ = o₂ ∧ a ≤ b ∨ o₁ < o₂ ∧ a ≤ veblenWith f o₂ b ∨ o₂ < o₁ ∧ veblenWith f o₁ a ≤ b

Tactic:
aesop (add simp [not_lt_of_le, lt_asymm])

Result:
no goals
-- Mathlib/Algebra/Polynomial/Div.lean
theorem degree_modByMonic_le (p : R[X]) {q : R[X]} (hq : Monic q) : degree (p %ₘ q) ≤ degree q

Proof state:
R : Type u
inst✝ : Ring R
p q : R[X]
hq : q.Monic
a✝ : Nontrivial R
⊢ (p %ₘ q).degree ≤ q.degree

Tactic:
exact (degree_modByMonic_lt _ hq).le

Result:
no goals

Proof state:
R : Type u
inst✝ : Ring R
p q : R[X]
hq : q.Monic
⊢ (p %ₘ q).degree ≤ q.degree

Tactic:
nontriviality R

Result:
R : Type u
inst✝ : Ring R
p q : R[X]
hq : q.Monic
a✝ : Nontrivial R
⊢ (p %ₘ q).degree ≤ q.degree
-- Mathlib/MeasureTheory/Function/EssSup.lean
theorem essSup_eq_sInf {m : MeasurableSpace α} (μ : Measure α) (f : α → β) :
    essSup f μ = sInf { a | μ { x | a < f x } = 0 }

Proof state:
α : Type u_1
β : Type u_2
inst✝ : ConditionallyCompleteLinearOrder β
m : MeasurableSpace α
μ : Measure α
f : α → β
⊢ sInf {a | ∀ᶠ (n : β) in map f (ae μ), n ≤ a} = sInf {a | μ {x | a < f x} = 0}

Tactic:
simp only [eventually_map, ae_iff, not_le]

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
inst✝ : ConditionallyCompleteLinearOrder β
m : MeasurableSpace α
μ : Measure α
f : α → β
⊢ essSup f μ = sInf {a | μ {x | a < f x} = 0}

Tactic:
dsimp [essSup, limsup, limsSup]

Result:
α : Type u_1
β : Type u_2
inst✝ : ConditionallyCompleteLinearOrder β
m : MeasurableSpace α
μ : Measure α
f : α → β
⊢ sInf {a | ∀ᶠ (n : β) in map f (ae μ), n ≤ a} = sInf {a | μ {x | a < f x} = 0}
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Nat/Bitwise/Lemmas.lean
theorem testBit_two_pow_add_eq (x i : Nat) : testBit (2^i + x) i = !(testBit x i)

Proof state:
x i : Nat
⊢ decide (1 - x / 2 ^ i % 2 = 1) = !decide (x / 2 ^ i % 2 = 1)

Tactic:
cases mod_two_eq_zero_or_one (x / 2 ^ i) with
| _ p => simp [p]

Result:
no goals

Proof state:
x i : Nat
⊢ (2 ^ i + x).testBit i = !x.testBit i

Tactic:
simp [testBit_to_div_mod, add_div_left, Nat.two_pow_pos, succ_mod_two]

Result:
x i : Nat
⊢ decide (1 - x / 2 ^ i % 2 = 1) = !decide (x / 2 ^ i % 2 = 1)

Proof state:
case inr
x i : Nat
p : x / 2 ^ i % 2 = 1
⊢ decide (1 - x / 2 ^ i % 2 = 1) = !decide (x / 2 ^ i % 2 = 1)

Tactic:
simp [p]

Result:
no goals
-- Mathlib/Analysis/Calculus/Deriv/Comp.lean
theorem HasDerivAtFilter.scomp_of_eq (hg : HasDerivAtFilter g₁ g₁' y L')
    (hh : HasDerivAtFilter h h' x L) (hy : y = h x) (hL : Tendsto h L L') :
    HasDerivAtFilter (g₁ ∘ h) (h' • g₁') x L

Proof state:
𝕜 : Type u
inst✝⁶ : NontriviallyNormedField 𝕜
F : Type v
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
x : 𝕜
L : Filter 𝕜
𝕜' : Type u_1
inst✝³ : NontriviallyNormedField 𝕜'
inst✝² : NormedAlgebra 𝕜 𝕜'
inst✝¹ : NormedSpace 𝕜' F
inst✝ : IsScalarTower 𝕜 𝕜' F
h : 𝕜 → 𝕜'
h' : 𝕜'
g₁ : 𝕜' → F
g₁' : F
L' : Filter 𝕜'
y : 𝕜'
hg : HasDerivAtFilter g₁ g₁' (h x) L'
hh : HasDerivAtFilter h h' x L
hy : y = h x
hL : Tendsto h L L'
⊢ HasDerivAtFilter (g₁ ∘ h) (h' • g₁') x L

Tactic:
exact hg.scomp x hh hL

Result:
no goals

Proof state:
𝕜 : Type u
inst✝⁶ : NontriviallyNormedField 𝕜
F : Type v
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
x : 𝕜
L : Filter 𝕜
𝕜' : Type u_1
inst✝³ : NontriviallyNormedField 𝕜'
inst✝² : NormedAlgebra 𝕜 𝕜'
inst✝¹ : NormedSpace 𝕜' F
inst✝ : IsScalarTower 𝕜 𝕜' F
h : 𝕜 → 𝕜'
h' : 𝕜'
g₁ : 𝕜' → F
g₁' : F
L' : Filter 𝕜'
y : 𝕜'
hg : HasDerivAtFilter g₁ g₁' y L'
hh : HasDerivAtFilter h h' x L
hy : y = h x
hL : Tendsto h L L'
⊢ HasDerivAtFilter (g₁ ∘ h) (h' • g₁') x L

Tactic:
rw [hy] at hg

Result:
𝕜 : Type u
inst✝⁶ : NontriviallyNormedField 𝕜
F : Type v
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
x : 𝕜
L : Filter 𝕜
𝕜' : Type u_1
inst✝³ : NontriviallyNormedField 𝕜'
inst✝² : NormedAlgebra 𝕜 𝕜'
inst✝¹ : NormedSpace 𝕜' F
inst✝ : IsScalarTower 𝕜 𝕜' F
h : 𝕜 → 𝕜'
h' : 𝕜'
g₁ : 𝕜' → F
g₁' : F
L' : Filter 𝕜'
y : 𝕜'
hg : HasDerivAtFilter g₁ g₁' (h x) L'
hh : HasDerivAtFilter h h' x L
hy : y = h x
hL : Tendsto h L L'
⊢ HasDerivAtFilter (g₁ ∘ h) (h' • g₁') x L