harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/NumberTheory/LegendreSymbol/Basic.lean
theorem eq_one_of_sq_sub_mul_sq_eq_zero {p : ℕ} [Fact p.Prime] {a : ℤ} (ha : (a : ZMod p) ≠ 0)
    {x y : ZMod p} (hy : y ≠ 0) (hxy : x ^ 2 - a * y ^ 2 = 0) : legendreSym p a = 1

Proof state:
p : ℕ
inst✝ : Fact (Nat.Prime p)
a : ℤ
ha : ↑a ≠ 0
x y : ZMod p
hy : y ≠ 0
hxy : x * y⁻¹ * (x * y⁻¹) = ↑a
⊢ legendreSym p a = 1

Tactic:
exact (eq_one_iff p ha).mpr ⟨x * y⁻¹, hxy.symm⟩

Result:
no goals

Proof state:
p : ℕ
inst✝ : Fact (Nat.Prime p)
a : ℤ
ha : ↑a ≠ 0
x y : ZMod p
hy : y ≠ 0
hxy : (x ^ 2 - ↑a * y ^ 2) * y⁻¹ ^ 2 = 0 * y⁻¹ ^ 2
⊢ legendreSym p a = 1

Tactic:
simp only [zero_mul] at hxy

Result:
p : ℕ
inst✝ : Fact (Nat.Prime p)
a : ℤ
ha : ↑a ≠ 0
x y : ZMod p
hy : y ≠ 0
hxy : (x ^ 2 - ↑a * y ^ 2) * y⁻¹ ^ 2 = 0
⊢ legendreSym p a = 1

Proof state:
p : ℕ
inst✝ : Fact (Nat.Prime p)
a : ℤ
ha : ↑a ≠ 0
x y : ZMod p
hy : y ≠ 0
hxy : (x ^ 2 - ↑a * y ^ 2) * y⁻¹ ^ 2 = 0
⊢ (x ^ 2 - ↑a * y ^ 2) * y⁻¹ ^ 2 = (x * y⁻¹) ^ 2 - ↑a * (y * y⁻¹) ^ 2

Tactic:
ring

Result:
no goals

Proof state:
p : ℕ
inst✝ : Fact (Nat.Prime p)
a : ℤ
ha : ↑a ≠ 0
x y : ZMod p
hy : y ≠ 0
hxy : (x ^ 2 - ↑a * y ^ 2) * y⁻¹ ^ 2 = 0
⊢ legendreSym p a = 1

Tactic:
rw [(by ring : (x ^ 2 - ↑a * y ^ 2) * y⁻¹ ^ 2 = (x * y⁻¹) ^ 2 - a * (y * y⁻¹) ^ 2),
  mul_inv_cancel₀ hy, one_pow, mul_one, sub_eq_zero, pow_two] at hxy

Result:
p : ℕ
inst✝ : Fact (Nat.Prime p)
a : ℤ
ha : ↑a ≠ 0
x y : ZMod p
hy : y ≠ 0
hxy : x * y⁻¹ * (x * y⁻¹) = ↑a
⊢ legendreSym p a = 1
-- Mathlib/AlgebraicTopology/SimplicialObject/Basic.lean
theorem δ_comp_δ {n} {i j : Fin (n + 2)} (H : i ≤ j) :
    X.δ i ≫ X.δ j.succ = X.δ j ≫ X.δ (Fin.castSucc i)

Proof state:
C : Type u
inst✝ : Category.{v, u} C
X : CosimplicialObject C
n : ℕ
i j : Fin (n + 2)
H : i ≤ j
⊢ X.map (SimplexCategory.δ i) ≫ X.map (SimplexCategory.δ j.succ) =
    X.map (SimplexCategory.δ j) ≫ X.map (SimplexCategory.δ i.castSucc)

Tactic:
simp only [← X.map_comp, SimplexCategory.δ_comp_δ H]

Result:
no goals

Proof state:
C : Type u
inst✝ : Category.{v, u} C
X : CosimplicialObject C
n : ℕ
i j : Fin (n + 2)
H : i ≤ j
⊢ X.δ i ≫ X.δ j.succ = X.δ j ≫ X.δ i.castSucc

Tactic:
dsimp [δ]

Result:
C : Type u
inst✝ : Category.{v, u} C
X : CosimplicialObject C
n : ℕ
i j : Fin (n + 2)
H : i ≤ j
⊢ X.map (SimplexCategory.δ i) ≫ X.map (SimplexCategory.δ j.succ) =
    X.map (SimplexCategory.δ j) ≫ X.map (SimplexCategory.δ i.castSucc)
-- Mathlib/Order/CompleteLattice/SetLike.lean
@[simp] lemma mem_iSup : x ∈ ⨆ i : I, f i ↔ ∃ i : I, x ∈ f i

Proof state:
X : Type u_1
L : CompleteSublattice (Set X)
I : Sort u_2
f : I → ↥L
x : X
⊢ x ∈ ⨆ i, f i ↔ ∃ i, x ∈ f i

Tactic:
simp [← mem_subtype]

Result:
no goals
-- Mathlib/NumberTheory/Cyclotomic/CyclotomicCharacter.lean
/-- The relationship between `IsPrimitiveRoot.autToPow` and
`ModularCyclotomicCharacter`. Note that `IsPrimitiveRoot.autToPow`
needs an explicit root of unity, and also an auxiliary "base ring" `R`. -/
lemma IsPrimitiveRoot.autToPow_eq_ModularCyclotomicCharacter (n : ℕ) [NeZero n]
    (R : Type*) [CommRing R] [Algebra R L] {μ : L} (hμ : IsPrimitiveRoot μ n) (g : L ≃ₐ[R] L) :
    hμ.autToPow R g = ModularCyclotomicCharacter L hμ.card_rootsOfUnity g

Proof state:
L : Type u
inst✝⁴ : CommRing L
inst✝³ : IsDomain L
n : ℕ
inst✝² : NeZero n
R : Type u_1
inst✝¹ : CommRing R
inst✝ : Algebra R L
μ : L
hμ : IsPrimitiveRoot μ n
g : L ≃ₐ[R] L
⊢ (autToPow R hμ) g = (ModularCyclotomicCharacter L ⋯) ↑g

Tactic:
ext

Result:
case a
L : Type u
inst✝⁴ : CommRing L
inst✝³ : IsDomain L
n : ℕ
inst✝² : NeZero n
R : Type u_1
inst✝¹ : CommRing R
inst✝ : Algebra R L
μ : L
hμ : IsPrimitiveRoot μ n
g : L ≃ₐ[R] L
⊢ ↑((autToPow R hμ) g) = ↑((ModularCyclotomicCharacter L ⋯) ↑g)

Proof state:
case a.a
L : Type u
inst✝⁴ : CommRing L
inst✝³ : IsDomain L
n : ℕ
inst✝² : NeZero n
R : Type u_1
inst✝¹ : CommRing R
inst✝ : Algebra R L
μ : L
hμ : IsPrimitiveRoot μ n
g : L ≃ₐ[R] L
⊢ μ ^ (↑((autToPow R hμ) g)).val = μ ^ (↑((ModularCyclotomicCharacter L ⋯) ↑g)).val

Tactic:
simpa only [autToPow_spec R hμ g, ModularCyclotomicCharacter, RingEquiv.toMulEquiv_eq_coe,
  MulEquiv.toMonoidHom_eq_coe, ModularCyclotomicCharacter', MonoidHom.coe_comp, MonoidHom.coe_coe,
  Function.comp_apply, Units.coe_mapEquiv, MonoidHom.coe_toHomUnits, MonoidHom.coe_mk,
  OneHom.coe_mk, RingEquiv.coe_toMulEquiv, ZMod.ringEquivCongr_val, AlgEquiv.coe_ringEquiv]
  using ModularCyclotomicCharacter.toFun_spec'' g hμ

Result:
no goals

Proof state:
case a.a
L : Type u
inst✝⁴ : CommRing L
inst✝³ : IsDomain L
n : ℕ
inst✝² : NeZero n
R : Type u_1
inst✝¹ : CommRing R
inst✝ : Algebra R L
μ : L
hμ : IsPrimitiveRoot μ n
g : L ≃ₐ[R] L
⊢ (↑((autToPow R hμ) g)).val = (↑((ModularCyclotomicCharacter L ⋯) ↑g)).val

Tactic:
apply hμ.pow_inj (ZMod.val_lt _) (ZMod.val_lt _)

Result:
case a.a
L : Type u
inst✝⁴ : CommRing L
inst✝³ : IsDomain L
n : ℕ
inst✝² : NeZero n
R : Type u_1
inst✝¹ : CommRing R
inst✝ : Algebra R L
μ : L
hμ : IsPrimitiveRoot μ n
g : L ≃ₐ[R] L
⊢ μ ^ (↑((autToPow R hμ) g)).val = μ ^ (↑((ModularCyclotomicCharacter L ⋯) ↑g)).val

Proof state:
case a
L : Type u
inst✝⁴ : CommRing L
inst✝³ : IsDomain L
n : ℕ
inst✝² : NeZero n
R : Type u_1
inst✝¹ : CommRing R
inst✝ : Algebra R L
μ : L
hμ : IsPrimitiveRoot μ n
g : L ≃ₐ[R] L
⊢ ↑((autToPow R hμ) g) = ↑((ModularCyclotomicCharacter L ⋯) ↑g)

Tactic:
apply ZMod.val_injective

Result:
case a.a
L : Type u
inst✝⁴ : CommRing L
inst✝³ : IsDomain L
n : ℕ
inst✝² : NeZero n
R : Type u_1
inst✝¹ : CommRing R
inst✝ : Algebra R L
μ : L
hμ : IsPrimitiveRoot μ n
g : L ≃ₐ[R] L
⊢ (↑((autToPow R hμ) g)).val = (↑((ModularCyclotomicCharacter L ⋯) ↑g)).val
-- Mathlib/Data/Fintype/Sets.lean
theorem mem_image_univ_iff_mem_range {α β : Type*} [Fintype α] [DecidableEq β] {f : α → β}
    {b : β} : b ∈ univ.image f ↔ b ∈ Set.range f

Proof state:
α : Type u_4
β : Type u_5
inst✝¹ : Fintype α
inst✝ : DecidableEq β
f : α → β
b : β
⊢ b ∈ image f univ ↔ b ∈ Set.range f

Tactic:
simp

Result:
no goals
-- Mathlib/Data/Multiset/Sum.lean
theorem mem_disjSum : x ∈ s.disjSum t ↔ (∃ a, a ∈ s ∧ inl a = x) ∨ ∃ b, b ∈ t ∧ inr b = x

Proof state:
α : Type u_1
β : Type u_2
s : Multiset α
t : Multiset β
x : α ⊕ β
⊢ x ∈ s.disjSum t ↔ (∃ a ∈ s, inl a = x) ∨ ∃ b ∈ t, inr b = x

Tactic:
simp_rw [disjSum, mem_add, mem_map]

Result:
no goals
-- Mathlib/LinearAlgebra/Matrix/NonsingularInverse.lean
theorem inv_subsingleton [Subsingleton m] [Fintype m] [DecidableEq m] (A : Matrix m m α) :
    A⁻¹ = diagonal fun i => Ring.inverse (A i i)

Proof state:
m : Type u
α : Type v
inst✝³ : CommRing α
inst✝² : Subsingleton m
inst✝¹ : Fintype m
inst✝ : DecidableEq m
A : Matrix m m α
⊢ A⁻¹ = diagonal fun i => Ring.inverse (A i i)

Tactic:
rw [inv_def, adjugate_subsingleton, smul_one_eq_diagonal]

Result:
m : Type u
α : Type v
inst✝³ : CommRing α
inst✝² : Subsingleton m
inst✝¹ : Fintype m
inst✝ : DecidableEq m
A : Matrix m m α
⊢ (diagonal fun x => Ring.inverse A.det) = diagonal fun i => Ring.inverse (A i i)

Proof state:
case h.e'_5.h.h.e'_3
m : Type u
α : Type v
inst✝³ : CommRing α
inst✝² : Subsingleton m
inst✝¹ : Fintype m
inst✝ : DecidableEq m
A : Matrix m m α
i : m
⊢ A.det = A i i

Tactic:
exact det_eq_elem_of_subsingleton _ _

Result:
no goals

Proof state:
m : Type u
α : Type v
inst✝³ : CommRing α
inst✝² : Subsingleton m
inst✝¹ : Fintype m
inst✝ : DecidableEq m
A : Matrix m m α
⊢ (diagonal fun x => Ring.inverse A.det) = diagonal fun i => Ring.inverse (A i i)

Tactic:
congr! with i

Result:
case h.e'_5.h.h.e'_3
m : Type u
α : Type v
inst✝³ : CommRing α
inst✝² : Subsingleton m
inst✝¹ : Fintype m
inst✝ : DecidableEq m
A : Matrix m m α
i : m
⊢ A.det = A i i
-- Mathlib/Analysis/Asymptotics/AsymptoticEquivalent.lean
theorem IsEquivalent.tendsto_const {c : β} (hu : u ~[l] const _ c) : Tendsto u l (𝓝 c)

Proof state:
α : Type u_1
β : Type u_2
inst✝ : NormedAddCommGroup β
u : α → β
l : Filter α
c : β
hu : u ~[l] const α c
⊢ Tendsto u l (𝓝 c)

Tactic:
rcases em <| c = 0 with rfl | h

Result:
case inl
α : Type u_1
β : Type u_2
inst✝ : NormedAddCommGroup β
u : α → β
l : Filter α
hu : u ~[l] const α 0
⊢ Tendsto u l (𝓝 0)

case inr
α : Type u_1
β : Type u_2
inst✝ : NormedAddCommGroup β
u : α → β
l : Filter α
c : β
hu : u ~[l] const α c
h : ¬c = 0
⊢ Tendsto u l (𝓝 c)

Proof state:
case inr
α : Type u_1
β : Type u_2
inst✝ : NormedAddCommGroup β
u : α → β
l : Filter α
c : β
hu : u ~[l] const α c
h : ¬c = 0
⊢ Tendsto u l (𝓝 c)

Tactic:
exact (isEquivalent_const_iff_tendsto h).mp hu

Result:
no goals

Proof state:
case inl
α : Type u_1
β : Type u_2
inst✝ : NormedAddCommGroup β
u : α → β
l : Filter α
hu : u ~[l] const α 0
⊢ Tendsto u l (𝓝 0)

Tactic:
exact (tendsto_congr' <| isEquivalent_zero_iff_eventually_zero.mp hu).mpr tendsto_const_nhds

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Bool.lean
theorem or_self_right : ∀ (a b : Bool), ((a || b) || b) = (a || b)

Proof state:
⊢ ∀ (a b : Bool), (a || b || b) = (a || b)

Tactic:
decide

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem zero_udiv {x : BitVec w} : (0#w) / x = 0#w

Proof state:
w : Nat
x : BitVec w
⊢ 0#w / x = 0#w

Tactic:
simp [bv_toNat]

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/AdjMatrix.lean
theorem adjMatrix_mul_apply [NonAssocSemiring α] (M : Matrix V V α) (v w : V) :
    (G.adjMatrix α * M) v w = ∑ u ∈ G.neighborFinset v, M u w

Proof state:
V : Type u_1
α : Type u_2
G : SimpleGraph V
inst✝² : DecidableRel G.Adj
inst✝¹ : Fintype V
inst✝ : NonAssocSemiring α
M : Matrix V V α
v w : V
⊢ (adjMatrix α G * M) v w = ∑ u ∈ G.neighborFinset v, M u w

Tactic:
simp [mul_apply, neighborFinset_eq_filter, sum_filter]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Lemmas.lean
theorem mem_alter_self [EquivBEq α] [LawfulHashable α] {k : α} {f : Option β → Option β} :
    k ∈ Const.alter m k f ↔ (f (Const.get? m k)).isSome

Proof state:
α : Type u
x✝¹ : BEq α
x✝ : Hashable α
β : Type v
m : DHashMap α fun x => β
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
k : α
f : Option β → Option β
⊢ k ∈ alter m k f ↔ (f (get? m k)).isSome = true

Tactic:
rw [mem_iff_contains, contains_alter_self]

Result:
no goals
-- Mathlib/AlgebraicTopology/SimplicialSet/StrictSegal.lean
/-- If we take the path along the spine of the `j`th face of a `spineToSimplex`,
the common arrows will agree with those of the original path `f`. In particular,
an arrow `i` with `i + 1 < j` can be identified with the same arrow in `f`. -/
lemma spine_δ_arrow_lt (f : Path X (n + 1)) {i : Fin n} {j : Fin (n + 2)}
    (h : i.succ.castSucc < j) :
    (X.spine n (X.δ j (spineToSimplex f))).arrow i = f.arrow i.castSucc

Proof state:
X : SSet
inst✝ : X.StrictSegal
n : ℕ
f : X.Path (n + 1)
i : Fin n
j : Fin (n + 2)
h : i.succ.castSucc < j
⊢ (X.spine n (SimplicialObject.δ X j (spineToSimplex f))).arrow i = f.arrow i.castSucc

Tactic:
simp only [SimplicialObject.δ, spine_arrow]

Result:
X : SSet
inst✝ : X.StrictSegal
n : ℕ
f : X.Path (n + 1)
i : Fin n
j : Fin (n + 2)
h : i.succ.castSucc < j
⊢ X.map (mkOfSucc i).op (X.map (SimplexCategory.δ j).op (spineToSimplex f)) = f.arrow i.castSucc

Proof state:
X : SSet
inst✝ : X.StrictSegal
n : ℕ
f : X.Path (n + 1)
i : Fin n
j : Fin (n + 2)
h : i.succ.castSucc < j
⊢ X.map (mkOfSucc i ≫ SimplexCategory.δ j).op (spineToSimplex f) = f.arrow i.castSucc

Tactic:
rw [mkOfSucc_δ_lt h, spineToSimplex_arrow]

Result:
no goals

Proof state:
X : SSet
inst✝ : X.StrictSegal
n : ℕ
f : X.Path (n + 1)
i : Fin n
j : Fin (n + 2)
h : i.succ.castSucc < j
⊢ X.map (mkOfSucc i).op (X.map (SimplexCategory.δ j).op (spineToSimplex f)) = f.arrow i.castSucc

Tactic:
rw [← FunctorToTypes.map_comp_apply, ← op_comp]

Result:
X : SSet
inst✝ : X.StrictSegal
n : ℕ
f : X.Path (n + 1)
i : Fin n
j : Fin (n + 2)
h : i.succ.castSucc < j
⊢ X.map (mkOfSucc i ≫ SimplexCategory.δ j).op (spineToSimplex f) = f.arrow i.castSucc
-- Mathlib/Algebra/Module/LocalizedModule/Basic.lean
theorem liftOn_mk {α : Type*} {f : M × S → α} (wd : ∀ (p p' : M × S), p ≈ p' → f p = f p')
    (m : M) (s : S) : liftOn (mk m s) f wd = f ⟨m, s⟩

Proof state:
R : Type u
inst✝² : CommSemiring R
S : Submonoid R
M : Type v
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
α : Type u_2
f : M × ↥S → α
wd : ∀ (p p' : M × ↥S), p ≈ p' → f p = f p'
m : M
s : ↥S
⊢ (mk m s).liftOn f wd = f (m, s)

Tactic:
convert Quotient.liftOn_mk f wd ⟨m, s⟩

Result:
no goals
-- Mathlib/AlgebraicGeometry/EllipticCurve/Jacobian.lean
lemma addY_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 ^ 2 ≠ Q x * P z ^ 2) :
    W.addY P Q / addZ P Q ^ 3 = W.toAffine.addY (P x / P z ^ 2) (Q x / Q z ^ 2) (P y / P z ^ 3)
      (W.toAffine.slope (P x / P z ^ 2) (Q x / Q z ^ 2) (P y / P z ^ 3) (Q y / Q z ^ 3))

Proof state:
F : Type u
inst✝ : Field F
W : Jacobian 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 ^ 2 ≠ Q x * P z ^ 2
⊢ W.addY P Q / addZ P Q ^ 3 =
    (toAffine W).addY (P x / P z ^ 2) (Q x / Q z ^ 2) (P y / P z ^ 3)
      ((toAffine W).slope (P x / P z ^ 2) (Q x / Q z ^ 2) (P y / P z ^ 3) (Q y / Q z ^ 3))

Tactic:
erw [addY, negY_of_Z_ne_zero <| addZ_ne_zero_of_X_ne hx, addX_of_Z_ne_zero hP hQ hPz hQz hx,
  negAddY_of_Z_ne_zero hP hQ hPz hQz hx, Affine.addY]

Result:
no goals
-- Mathlib/Data/Finset/Union.lean
lemma biUnion_mono (h : ∀ a ∈ s, t₁ a ⊆ t₂ a) : s.biUnion t₁ ⊆ s.biUnion t₂

Proof state:
α : Type u_1
β : Type u_2
s : Finset α
t₁ t₂ : α → Finset β
inst✝ : DecidableEq β
h : ∀ a ∈ s, t₁ a ⊆ t₂ a
this : ∀ (b : β), ∀ a ∈ s, b ∈ t₁ a → ∃ a ∈ s, b ∈ t₂ a
⊢ s.biUnion t₁ ⊆ s.biUnion t₂

Tactic:
simpa only [subset_iff, mem_biUnion, exists_imp, and_imp, exists_prop]

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
s : Finset α
t₁ t₂ : α → Finset β
inst✝ : DecidableEq β
h : ∀ a ∈ s, t₁ a ⊆ t₂ a
⊢ s.biUnion t₁ ⊆ s.biUnion t₂

Tactic:
have : ∀ b a, a ∈ s → b ∈ t₁ a → ∃ a : α, a ∈ s ∧ b ∈ t₂ a := fun b a ha hb ↦
  ⟨a, ha, Finset.mem_of_subset (h a ha) hb⟩

Result:
α : Type u_1
β : Type u_2
s : Finset α
t₁ t₂ : α → Finset β
inst✝ : DecidableEq β
h : ∀ a ∈ s, t₁ a ⊆ t₂ a
this : ∀ (b : β), ∀ a ∈ s, b ∈ t₁ a → ∃ a ∈ s, b ∈ t₂ a
⊢ s.biUnion t₁ ⊆ s.biUnion t₂
-- Mathlib/Topology/Algebra/Order/LiminfLimsup.lean
/-- `limsup (c - xᵢ) = c - liminf xᵢ`. -/
lemma limsup_const_sub (F : Filter ι) [AddCommSemigroup R] [Sub R] [ContinuousSub R] [OrderedSub R]
    [AddLeftMono R] (f : ι → R) (c : R)
    (cobdd : F.IsCoboundedUnder (· ≥ ·) f) (bdd_below : F.IsBoundedUnder (· ≥ ·) f) :
    Filter.limsup (fun i ↦ c - f i) F = c - Filter.liminf f F

Proof state:
case inl.intro.refine_1
ι : Type u_1
R : Type u_4
inst✝⁷ : ConditionallyCompleteLinearOrder R
inst✝⁶ : TopologicalSpace R
inst✝⁵ : OrderTopology R
inst✝⁴ : AddCommSemigroup R
inst✝³ : Sub R
inst✝² : ContinuousSub R
inst✝¹ : OrderedSub R
inst✝ : AddLeftMono R
f : ι → R
c : R
bdd_below : IsBoundedUnder (fun x1 x2 => x1 ≥ x2) ⊥ f
x : R
hx : ∀ (a : R), x ≥ a
y : R
⊢ y ∈ Set.univ → x - x ≤ y

Tactic:
simp only [Set.mem_univ, true_implies]

Result:
case inl.intro.refine_1
ι : Type u_1
R : Type u_4
inst✝⁷ : ConditionallyCompleteLinearOrder R
inst✝⁶ : TopologicalSpace R
inst✝⁵ : OrderTopology R
inst✝⁴ : AddCommSemigroup R
inst✝³ : Sub R
inst✝² : ContinuousSub R
inst✝¹ : OrderedSub R
inst✝ : AddLeftMono R
f : ι → R
c : R
bdd_below : IsBoundedUnder (fun x1 x2 => x1 ≥ x2) ⊥ f
x : R
hx : ∀ (a : R), x ≥ a
y : R
⊢ x - x ≤ y

Proof state:
ι : Type u_1
R : Type u_4
inst✝⁷ : ConditionallyCompleteLinearOrder R
inst✝⁶ : TopologicalSpace R
inst✝⁵ : OrderTopology R
F : Filter ι
inst✝⁴ : AddCommSemigroup R
inst✝³ : Sub R
inst✝² : ContinuousSub R
inst✝¹ : OrderedSub R
inst✝ : AddLeftMono R
f : ι → R
c : R
cobdd : IsCoboundedUnder (fun x1 x2 => x1 ≥ x2) F f
bdd_below : IsBoundedUnder (fun x1 x2 => x1 ≥ x2) F f
⊢ limsup (fun i => c - f i) F = c - liminf f F

Tactic:
rcases F.eq_or_neBot with rfl | _

Result:
case inl
ι : Type u_1
R : Type u_4
inst✝⁷ : ConditionallyCompleteLinearOrder R
inst✝⁶ : TopologicalSpace R
inst✝⁵ : OrderTopology R
inst✝⁴ : AddCommSemigroup R
inst✝³ : Sub R
inst✝² : ContinuousSub R
inst✝¹ : OrderedSub R
inst✝ : AddLeftMono R
f : ι → R
c : R
cobdd : IsCoboundedUnder (fun x1 x2 => x1 ≥ x2) ⊥ f
bdd_below : IsBoundedUnder (fun x1 x2 => x1 ≥ x2) ⊥ f
⊢ limsup (fun i => c - f i) ⊥ = c - liminf f ⊥

case inr
ι : Type u_1
R : Type u_4
inst✝⁷ : ConditionallyCompleteLinearOrder R
inst✝⁶ : TopologicalSpace R
inst✝⁵ : OrderTopology R
F : Filter ι
inst✝⁴ : AddCommSemigroup R
inst✝³ : Sub R
inst✝² : ContinuousSub R
inst✝¹ : OrderedSub R
inst✝ : AddLeftMono R
f : ι → R
c : R
cobdd : IsCoboundedUnder (fun x1 x2 => x1 ≥ x2) F f
bdd_below : IsBoundedUnder (fun x1 x2 => x1 ≥ x2) F f
h✝ : F.NeBot
⊢ limsup (fun i => c - f i) F = c - liminf f F
-- Mathlib/GroupTheory/Coset/Basic.lean
@[to_additive]
lemma orbit_mk_eq_smul (x : α) : MulAction.orbitRel.Quotient.orbit (x : α ⧸ s) = x • s

Proof state:
case h
α : Type u_1
inst✝ : Group α
s : Subgroup α
x x✝ : α
⊢ Quotient.mk'' x✝ = ↑x ↔ x✝ ∈ x • ↑s

Tactic:
simpa [mem_smul_set_iff_inv_smul_mem, ← leftRel_apply, Quotient.eq''] using Setoid.comm' _

Result:
no goals

Proof state:
case h
α : Type u_1
inst✝ : Group α
s : Subgroup α
x x✝ : α
⊢ x✝ ∈ orbitRel.Quotient.orbit ↑x ↔ x✝ ∈ x • ↑s

Tactic:
rw [orbitRel.Quotient.mem_orbit]

Result:
case h
α : Type u_1
inst✝ : Group α
s : Subgroup α
x x✝ : α
⊢ Quotient.mk'' x✝ = ↑x ↔ x✝ ∈ x • ↑s

Proof state:
α : Type u_1
inst✝ : Group α
s : Subgroup α
x : α
⊢ orbitRel.Quotient.orbit ↑x = x • ↑s

Tactic:
ext

Result:
case h
α : Type u_1
inst✝ : Group α
s : Subgroup α
x x✝ : α
⊢ x✝ ∈ orbitRel.Quotient.orbit ↑x ↔ x✝ ∈ x • ↑s
-- Mathlib/Analysis/Calculus/Deriv/Slope.lean
theorem hasDerivAtFilter_iff_tendsto_slope {x : 𝕜} {L : Filter 𝕜} :
    HasDerivAtFilter f f' x L ↔ Tendsto (slope f x) (L ⊓ 𝓟 {x}ᶜ) (𝓝 f') :=
  calc HasDerivAtFilter f f' x L
    ↔ Tendsto (fun y ↦ slope f x y - (y - x)⁻¹ • (y - x) • f') L (𝓝 0)

Proof state:
𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : 𝕜 → F
f' : F
x : 𝕜
L : Filter 𝕜
y : 𝕜
hy : y ∈ {x}ᶜ
⊢ slope f x y - (y - x)⁻¹ • (y - x) • f' = slope f x y - f'

Tactic:
rw [inv_smul_smul₀ (sub_ne_zero.2 hy) f']

Result:
no goals

Proof state:
𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : 𝕜 → F
f' : F
x : 𝕜
L : Filter 𝕜
⊢ ∀ a ∉ {x}ᶜ, slope f x a - (a - x)⁻¹ • (a - x) • f' = 0

Tactic:
simp

Result:
no goals

Proof state:
𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : 𝕜 → F
f' : F
x : 𝕜
L : Filter 𝕜
⊢ Tendsto (fun y => slope f x y - f') (L ⊓ 𝓟 {x}ᶜ) (𝓝 0) ↔ Tendsto ((fun x => x - f') ∘ slope f x) (L ⊓ 𝓟 {x}ᶜ) (𝓝 0)

Tactic:
rfl

Result:
no goals

Proof state:
𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : 𝕜 → F
f' : F
x : 𝕜
L : Filter 𝕜
⊢ HasDerivAtFilter f f' x L ↔ Tendsto (fun y => slope f x y - (y - x)⁻¹ • (y - x) • f') L (𝓝 0)

Tactic:
simp only [hasDerivAtFilter_iff_tendsto, ← norm_inv, ← norm_smul,
  ← tendsto_zero_iff_norm_tendsto_zero, slope_def_module, smul_sub]

Result:
no goals

Proof state:
𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : 𝕜 → F
f' : F
x : 𝕜
L : Filter 𝕜
⊢ Tendsto (fun y => slope f x y - f') (L ⊓ 𝓟 {x}ᶜ) (𝓝 0) ↔ Tendsto (slope f x) (L ⊓ 𝓟 {x}ᶜ) (𝓝 f')

Tactic:
rw [← nhds_translation_sub f', tendsto_comap_iff]

Result:
𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : 𝕜 → F
f' : F
x : 𝕜
L : Filter 𝕜
⊢ Tendsto (fun y => slope f x y - f') (L ⊓ 𝓟 {x}ᶜ) (𝓝 0) ↔ Tendsto ((fun x => x - f') ∘ slope f x) (L ⊓ 𝓟 {x}ᶜ) (𝓝 0)

Proof state:
𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : 𝕜 → F
f' : F
x : 𝕜
L : Filter 𝕜
⊢ (fun y => slope f x y - (y - x)⁻¹ • (y - x) • f') =ᶠ[L ⊓ 𝓟 {x}ᶜ] fun y => slope f x y - f'

Tactic:
refine (EqOn.eventuallyEq fun y hy ↦ ?_).filter_mono inf_le_right

Result:
𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : 𝕜 → F
f' : F
x : 𝕜
L : Filter 𝕜
y : 𝕜
hy : y ∈ {x}ᶜ
⊢ slope f x y - (y - x)⁻¹ • (y - x) • f' = slope f x y - f'
-- Mathlib/CategoryTheory/Sites/Grothendieck.lean
lemma mem_sInf (s : Set (GrothendieckTopology C)) {X : C} (S : Sieve X) :
    S ∈ sInf s X ↔ ∀ t ∈ s, S ∈ t X

Proof state:
C : Type u
inst✝ : Category.{v, u} C
s : Set (GrothendieckTopology C)
X : C
S : Sieve X
⊢ S ∈ sInf (sieves '' s) X ↔ ∀ t ∈ s, S ∈ t X

Tactic:
simp

Result:
no goals

Proof state:
C : Type u
inst✝ : Category.{v, u} C
s : Set (GrothendieckTopology C)
X : C
S : Sieve X
⊢ S ∈ (sInf s) X ↔ ∀ t ∈ s, S ∈ t X

Tactic:
show S ∈ sInf (sieves '' s) X ↔ _

Result:
C : Type u
inst✝ : Category.{v, u} C
s : Set (GrothendieckTopology C)
X : C
S : Sieve X
⊢ S ∈ sInf (sieves '' s) X ↔ ∀ t ∈ s, S ∈ t X
-- Mathlib/Computability/PostTuringMachine.lean
theorem Machine.map_step {S : Set Λ} (f₂₁ : Function.RightInverse f₁ f₂)
    (g₂₁ : ∀ q ∈ S, g₂ (g₁ q) = q) :
    ∀ c : Cfg Γ Λ,
      c.q ∈ S → (step M c).map (Cfg.map f₁ g₁) = step (M.map f₁ f₂ g₁ g₂) (Cfg.map f₁ g₁ c)
  | ⟨q, T⟩, h => by
    unfold step Machine.map Cfg.map
    simp only [Turing.Tape.map_fst, g₂₁ q h, f₂₁ _]
    rcases M q T.1 with (_ | ⟨q', d | a⟩); · rfl
    · simp only [step, Cfg.map, Option.map_some', Tape.map_move f₁]
      rfl
    · simp only [step, Cfg.map, Option.map_some', Tape.map_write]
      rfl

Proof state:
case none
Γ : Type u_1
inst✝³ : Inhabited Γ
Γ' : Type u_2
inst✝² : Inhabited Γ'
Λ : Type u_3
inst✝¹ : Inhabited Λ
Λ' : Type u_4
inst✝ : Inhabited Λ'
M : Machine Γ Λ
f₁ : PointedMap Γ Γ'
f₂ : PointedMap Γ' Γ
g₁ : Λ → Λ'
g₂ : Λ' → Λ
S : Set Λ
f₂₁ : Function.RightInverse f₁.f f₂.f
g₂₁ : ∀ q ∈ S, g₂ (g₁ q) = q
q : Λ
T : Tape Γ
h : { q := q, Tape := T }.q ∈ S
⊢ Option.map (fun x => { q := g₁ x.q, Tape := Tape.map f₁ x.Tape })
      (Option.map
        (fun x =>
          { q := x.1,
            Tape :=
              match x.2 with
              | Stmt.move d => Tape.move d T
              | Stmt.write a => Tape.write a T })
        none) =
    Option.map
      (fun x =>
        { q := x.1,
          Tape :=
            match x.2 with
            | Stmt.move d => Tape.move d (Tape.map f₁ T)
            | Stmt.write a => Tape.write a (Tape.map f₁ T) })
      (Option.map (Prod.map g₁ (Stmt.map f₁)) none)

Tactic:
rfl

Result:
no goals

Proof state:
case some.mk.move
Γ : Type u_1
inst✝³ : Inhabited Γ
Γ' : Type u_2
inst✝² : Inhabited Γ'
Λ : Type u_3
inst✝¹ : Inhabited Λ
Λ' : Type u_4
inst✝ : Inhabited Λ'
M : Machine Γ Λ
f₁ : PointedMap Γ Γ'
f₂ : PointedMap Γ' Γ
g₁ : Λ → Λ'
g₂ : Λ' → Λ
S : Set Λ
f₂₁ : Function.RightInverse f₁.f f₂.f
g₂₁ : ∀ q ∈ S, g₂ (g₁ q) = q
q : Λ
T : Tape Γ
h : { q := q, Tape := T }.q ∈ S
q' : Λ
d : Dir
⊢ some { q := g₁ q', Tape := Tape.move d (Tape.map f₁ T) } =
    some
      { q := (Prod.map g₁ (Stmt.map f₁) (q', Stmt.move d)).1,
        Tape :=
          match (Prod.map g₁ (Stmt.map f₁) (q', Stmt.move d)).2 with
          | Stmt.move d => Tape.move d (Tape.map f₁ T)
          | Stmt.write a => Tape.write a (Tape.map f₁ T) }

Tactic:
rfl

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Monadic.lean
theorem forIn_yield_eq_foldl
    (l : Array α) (f : α → β → β) (init : β) :
    forIn (m := Id) l init (fun a b => .yield (f a b)) =
      l.foldl (fun b a => f a b) init

Proof state:
case mk
α : Type u_1
β : Type u_2
f : α → β → β
init : β
toList✝ : List α
⊢ (forIn { toList := toList✝ } init fun a b => ForInStep.yield (f a b)) =
    foldl (fun b a => f a b) init { toList := toList✝ }

Tactic:
simp [List.foldl_map]

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
l : Array α
f : α → β → β
init : β
⊢ (forIn l init fun a b => ForInStep.yield (f a b)) = foldl (fun b a => f a b) init l

Tactic:
cases l

Result:
case mk
α : Type u_1
β : Type u_2
f : α → β → β
init : β
toList✝ : List α
⊢ (forIn { toList := toList✝ } init fun a b => ForInStep.yield (f a b)) =
    foldl (fun b a => f a b) init { toList := toList✝ }