harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Data/SetLike/Basic.lean
theorem lt_iff_le_and_exists : p < q ↔ p ≤ q ∧ ∃ x ∈ q, x ∉ p

Proof state:
A : Type u_1
B : Type u_2
i : SetLike A B
p q : A
⊢ p < q ↔ p ≤ q ∧ ∃ x ∈ q, x ∉ p

Tactic:
rw [lt_iff_le_not_le, not_le_iff_exists]

Result:
no goals
-- Mathlib/LinearAlgebra/LinearIndependent/Lemmas.lean
theorem linearIndependent_fin_snoc {n} {v : Fin n → V} :
    LinearIndependent K (Fin.snoc v x : Fin (n + 1) → V) ↔
      LinearIndependent K v ∧ x ∉ Submodule.span K (range v)

Proof state:
K : Type u_3
V : Type u
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
x : V
n : ℕ
v : Fin n → V
⊢ LinearIndependent K (Fin.snoc v x) ↔ LinearIndependent K v ∧ x ∉ span K (range v)

Tactic:
rw [Fin.snoc_eq_cons_rotate, ← Function.comp_def, linearIndependent_equiv,
  linearIndependent_fin_cons]

Result:
no goals
-- Mathlib/Analysis/Convex/Exposed.lean
theorem isExposed_empty : IsExposed 𝕜 A ∅ := fun ⟨_, hx⟩ => by
  exfalso
  exact hx

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : TopologicalSpace 𝕜
inst✝³ : OrderedRing 𝕜
inst✝² : AddCommMonoid E
inst✝¹ : TopologicalSpace E
inst✝ : Module 𝕜 E
A : Set E
x✝ : ∅.Nonempty
w✝ : E
hx : w✝ ∈ ∅
⊢ ∃ l, ∅ = {x | x ∈ A ∧ ∀ y ∈ A, l y ≤ l x}

Tactic:
exfalso

Result:
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : TopologicalSpace 𝕜
inst✝³ : OrderedRing 𝕜
inst✝² : AddCommMonoid E
inst✝¹ : TopologicalSpace E
inst✝ : Module 𝕜 E
A : Set E
x✝ : ∅.Nonempty
w✝ : E
hx : w✝ ∈ ∅
⊢ False

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : TopologicalSpace 𝕜
inst✝³ : OrderedRing 𝕜
inst✝² : AddCommMonoid E
inst✝¹ : TopologicalSpace E
inst✝ : Module 𝕜 E
A : Set E
x✝ : ∅.Nonempty
w✝ : E
hx : w✝ ∈ ∅
⊢ False

Tactic:
exact hx

Result:
no goals
-- Mathlib/Algebra/Polynomial/Smeval.lean
theorem smeval_monomial (n : ℕ) :
    (monomial n r).smeval x = r • x ^ n

Proof state:
R : Type u_1
inst✝³ : Semiring R
r : R
S : Type u_2
inst✝² : AddCommMonoid S
inst✝¹ : Pow S ℕ
inst✝ : MulActionWithZero R S
x : S
n : ℕ
⊢ ((monomial n) r).smeval x = r • x ^ n

Tactic:
simp only [smeval_eq_sum, smul_pow, zero_smul, sum_monomial_index]

Result:
no goals
-- Mathlib/Topology/Instances/AddCircle.lean
theorem equivIccQuot_comp_mk_eq_toIocMod :
    equivIccQuot p a ∘ Quotient.mk'' = fun x =>
      Quot.mk _ ⟨toIocMod hp.out a x, Ioc_subset_Icc_self <| toIocMod_mem_Ioc _ _ x⟩

Proof state:
case h
𝕜 : Type u_1
inst✝¹ : LinearOrderedAddCommGroup 𝕜
p a : 𝕜
hp : Fact (0 < p)
inst✝ : Archimedean 𝕜
x : 𝕜
⊢ Quot.mk (EndpointIdent p a) ⟨toIcoMod ⋯ a x, ⋯⟩ = Quot.mk (EndpointIdent p a) ⟨toIocMod ⋯ a x, ⋯⟩

Tactic:
by_cases h : a ≡ x [PMOD p]

Result:
case pos
𝕜 : Type u_1
inst✝¹ : LinearOrderedAddCommGroup 𝕜
p a : 𝕜
hp : Fact (0 < p)
inst✝ : Archimedean 𝕜
x : 𝕜
h : a ≡ x [PMOD p]
⊢ Quot.mk (EndpointIdent p a) ⟨toIcoMod ⋯ a x, ⋯⟩ = Quot.mk (EndpointIdent p a) ⟨toIocMod ⋯ a x, ⋯⟩

case neg
𝕜 : Type u_1
inst✝¹ : LinearOrderedAddCommGroup 𝕜
p a : 𝕜
hp : Fact (0 < p)
inst✝ : Archimedean 𝕜
x : 𝕜
h : ¬a ≡ x [PMOD p]
⊢ Quot.mk (EndpointIdent p a) ⟨toIcoMod ⋯ a x, ⋯⟩ = Quot.mk (EndpointIdent p a) ⟨toIocMod ⋯ a x, ⋯⟩

Proof state:
𝕜 : Type u_1
inst✝¹ : LinearOrderedAddCommGroup 𝕜
p a : 𝕜
hp : Fact (0 < p)
inst✝ : Archimedean 𝕜
⊢ ⇑(equivIccQuot p a) ∘ Quotient.mk'' = fun x => Quot.mk (EndpointIdent p a) ⟨toIocMod ⋯ a x, ⋯⟩

Tactic:
rw [equivIccQuot_comp_mk_eq_toIcoMod]

Result:
𝕜 : Type u_1
inst✝¹ : LinearOrderedAddCommGroup 𝕜
p a : 𝕜
hp : Fact (0 < p)
inst✝ : Archimedean 𝕜
⊢ (fun x => Quot.mk (EndpointIdent p a) ⟨toIcoMod ⋯ a x, ⋯⟩) = fun x => Quot.mk (EndpointIdent p a) ⟨toIocMod ⋯ a x, ⋯⟩

Proof state:
case pos
𝕜 : Type u_1
inst✝¹ : LinearOrderedAddCommGroup 𝕜
p a : 𝕜
hp : Fact (0 < p)
inst✝ : Archimedean 𝕜
x : 𝕜
h : a ≡ x [PMOD p]
⊢ Quot.mk (EndpointIdent p a) ⟨a, ⋯⟩ = Quot.mk (EndpointIdent p a) ⟨a + p, ⋯⟩

Tactic:
exact Quot.sound EndpointIdent.mk

Result:
no goals

Proof state:
case neg
𝕜 : Type u_1
inst✝¹ : LinearOrderedAddCommGroup 𝕜
p a : 𝕜
hp : Fact (0 < p)
inst✝ : Archimedean 𝕜
x : 𝕜
h : ¬a ≡ x [PMOD p]
⊢ Quot.mk (EndpointIdent p a) ⟨toIcoMod ⋯ a x, ⋯⟩ = Quot.mk (EndpointIdent p a) ⟨toIocMod ⋯ a x, ⋯⟩

Tactic:
simp_rw [(not_modEq_iff_toIcoMod_eq_toIocMod hp.out).1 h]

Result:
no goals

Proof state:
case pos
𝕜 : Type u_1
inst✝¹ : LinearOrderedAddCommGroup 𝕜
p a : 𝕜
hp : Fact (0 < p)
inst✝ : Archimedean 𝕜
x : 𝕜
h : a ≡ x [PMOD p]
⊢ Quot.mk (EndpointIdent p a) ⟨toIcoMod ⋯ a x, ⋯⟩ = Quot.mk (EndpointIdent p a) ⟨toIocMod ⋯ a x, ⋯⟩

Tactic:
simp_rw [(modEq_iff_toIcoMod_eq_left hp.out).1 h, (modEq_iff_toIocMod_eq_right hp.out).1 h]

Result:
case pos
𝕜 : Type u_1
inst✝¹ : LinearOrderedAddCommGroup 𝕜
p a : 𝕜
hp : Fact (0 < p)
inst✝ : Archimedean 𝕜
x : 𝕜
h : a ≡ x [PMOD p]
⊢ Quot.mk (EndpointIdent p a) ⟨a, ⋯⟩ = Quot.mk (EndpointIdent p a) ⟨a + p, ⋯⟩

Proof state:
𝕜 : Type u_1
inst✝¹ : LinearOrderedAddCommGroup 𝕜
p a : 𝕜
hp : Fact (0 < p)
inst✝ : Archimedean 𝕜
⊢ (fun x => Quot.mk (EndpointIdent p a) ⟨toIcoMod ⋯ a x, ⋯⟩) = fun x => Quot.mk (EndpointIdent p a) ⟨toIocMod ⋯ a x, ⋯⟩

Tactic:
funext x

Result:
case h
𝕜 : Type u_1
inst✝¹ : LinearOrderedAddCommGroup 𝕜
p a : 𝕜
hp : Fact (0 < p)
inst✝ : Archimedean 𝕜
x : 𝕜
⊢ Quot.mk (EndpointIdent p a) ⟨toIcoMod ⋯ a x, ⋯⟩ = Quot.mk (EndpointIdent p a) ⟨toIocMod ⋯ a x, ⋯⟩
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem getElem_xor {x y : BitVec w} {i : Nat} (h : i < w) : (x ^^^ y)[i] = (x[i] ^^ y[i])

Proof state:
w : Nat
x y : BitVec w
i : Nat
h : i < w
⊢ (x ^^^ y)[i] = (x[i] ^^ y[i])

Tactic:
simp [getElem_eq_testBit_toNat]

Result:
no goals
-- Mathlib/Analysis/NormedSpace/Multilinear/Curry.lean
theorem ContinuousMultilinearMap.curry0_norm (f : G[×0]→L[𝕜] G') : ‖f.curry0‖ = ‖f‖

Proof state:
𝕜 : Type u
G : Type wG
G' : Type wG'
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
inst✝¹ : NormedAddCommGroup G'
inst✝ : NormedSpace 𝕜 G'
f : ContinuousMultilinearMap 𝕜 (fun i => G) G'
⊢ ‖f.curry0‖ = ‖f‖

Tactic:
simp

Result:
no goals
-- Mathlib/Algebra/Homology/ShortComplex/SnakeLemma.lean
/-- The upper part of the first column of the snake diagram is exact. -/
lemma exact_C₁_up : (ShortComplex.mk S.v₀₁.τ₁ S.v₁₂.τ₁
    (by rw [← comp_τ₁, S.w₀₂, zero_τ₁])).Exact :=
  exact_of_f_is_kernel _ S.h₀τ₁

Proof state:
C : Type u_1
inst✝¹ : Category.{?u.29860, u_1} C
inst✝ : Abelian C
S : SnakeInput C
⊢ S.v₀₁.τ₁ ≫ S.v₁₂.τ₁ = 0

Tactic:
rw [← comp_τ₁, S.w₀₂, zero_τ₁]

Result:
no goals
-- Mathlib/Algebra/Order/Group/Pointwise/Interval.lean
theorem preimage_const_mul_Icc_of_neg (a b : α) {c : α} (h : c < 0) :
    (c * ·) ⁻¹' Icc a b = Icc (b / c) (a / c)

Proof state:
α : Type u_1
inst✝ : LinearOrderedField α
a b c : α
h : c < 0
⊢ (fun x => c * x) ⁻¹' Icc a b = Icc (b / c) (a / c)

Tactic:
simpa only [mul_comm] using preimage_mul_const_Icc_of_neg a b h

Result:
no goals
-- Mathlib/Data/Nat/Factorization/Basic.lean
@[simp]
lemma factorizationLCMLeft_zero_right : factorizationLCMLeft a 0 = 1

Proof state:
a : ℕ
⊢ a.factorizationLCMLeft 0 = 1

Tactic:
simp [factorizationLCMLeft]

Result:
no goals
-- Mathlib/Algebra/MvPolynomial/Eval.lean
theorem aevalTower_id :
    aevalTower (AlgHom.id S S) = (aeval : (σ → S) → MvPolynomial σ S →ₐ[S] S)

Proof state:
case h.hf
σ : Type u_1
S : Type u_2
inst✝ : CommSemiring S
x✝ : σ → S
i✝ : σ
⊢ (aevalTower (AlgHom.id S S) x✝) (X i✝) = (aeval x✝) (X i✝)

Tactic:
simp only [aevalTower_X, aeval_X]

Result:
no goals

Proof state:
σ : Type u_1
S : Type u_2
inst✝ : CommSemiring S
⊢ aevalTower (AlgHom.id S S) = aeval

Tactic:
ext

Result:
case h.hf
σ : Type u_1
S : Type u_2
inst✝ : CommSemiring S
x✝ : σ → S
i✝ : σ
⊢ (aevalTower (AlgHom.id S S) x✝) (X i✝) = (aeval x✝) (X i✝)
-- Mathlib/RingTheory/Polynomial/Cyclotomic/Basic.lean
theorem int_cyclotomic_rw {n : ℕ} (h : n ≠ 0) :
    cyclotomic n ℤ = (int_coeff_of_cyclotomic' (Complex.isPrimitiveRoot_exp n h)).choose

Proof state:
n : ℕ
h : n ≠ 0
⊢ cyclotomic n ℤ = ⋯.choose

Tactic:
simp only [cyclotomic, h, dif_neg, not_false_iff]

Result:
n : ℕ
h : n ≠ 0
⊢ map (Int.castRingHom ℤ) ⋯.choose = ⋯.choose

Proof state:
case a
n : ℕ
h : n ≠ 0
i : ℕ
⊢ (map (Int.castRingHom ℤ) ⋯.choose).coeff i = ⋯.choose.coeff i

Tactic:
simp only [coeff_map, Int.cast_id, eq_intCast]

Result:
no goals

Proof state:
n : ℕ
h : n ≠ 0
⊢ map (Int.castRingHom ℤ) ⋯.choose = ⋯.choose

Tactic:
ext i

Result:
case a
n : ℕ
h : n ≠ 0
i : ℕ
⊢ (map (Int.castRingHom ℤ) ⋯.choose).coeff i = ⋯.choose.coeff i
-- Mathlib/Order/Interval/Set/UnorderedInterval.lean
lemma uIcc_injective_right (a : α) : Injective fun b => uIcc b a := fun b c h => by
  rw [Set.ext_iff] at h
  exact eq_of_mem_uIcc_of_mem_uIcc ((h _).1 left_mem_uIcc) ((h _).2 left_mem_uIcc)

Proof state:
α : Type u_1
inst✝ : DistribLattice α
a b c : α
h : (fun b => [[b, a]]) b = (fun b => [[b, a]]) c
⊢ b = c

Tactic:
rw [Set.ext_iff] at h

Result:
α : Type u_1
inst✝ : DistribLattice α
a b c : α
h : ∀ (x : α), x ∈ (fun b => [[b, a]]) b ↔ x ∈ (fun b => [[b, a]]) c
⊢ b = c

Proof state:
α : Type u_1
inst✝ : DistribLattice α
a b c : α
h : ∀ (x : α), x ∈ (fun b => [[b, a]]) b ↔ x ∈ (fun b => [[b, a]]) c
⊢ b = c

Tactic:
exact eq_of_mem_uIcc_of_mem_uIcc ((h _).1 left_mem_uIcc) ((h _).2 left_mem_uIcc)

Result:
no goals
-- Mathlib/Algebra/Polynomial/Basic.lean
theorem coeff_update (p : R[X]) (n : ℕ) (a : R) :
    (p.update n a).coeff = Function.update p.coeff n a

Proof state:
case h.ofFinsupp
R : Type u
inst✝ : Semiring R
n : ℕ
a : R
x✝ : ℕ
toFinsupp✝ : R[ℕ]
⊢ ({ toFinsupp := toFinsupp✝ }.update n a).coeff x✝ = Function.update { toFinsupp := toFinsupp✝ }.coeff n a x✝

Tactic:
simp only [coeff, update, Function.update_apply, coe_update]

Result:
no goals

Proof state:
R : Type u
inst✝ : Semiring R
p : R[X]
n : ℕ
a : R
⊢ (p.update n a).coeff = Function.update p.coeff n a

Tactic:
ext

Result:
case h
R : Type u
inst✝ : Semiring R
p : R[X]
n : ℕ
a : R
x✝ : ℕ
⊢ (p.update n a).coeff x✝ = Function.update p.coeff n a x✝

Proof state:
case h
R : Type u
inst✝ : Semiring R
p : R[X]
n : ℕ
a : R
x✝ : ℕ
⊢ (p.update n a).coeff x✝ = Function.update p.coeff n a x✝

Tactic:
cases p

Result:
case h.ofFinsupp
R : Type u
inst✝ : Semiring R
n : ℕ
a : R
x✝ : ℕ
toFinsupp✝ : R[ℕ]
⊢ ({ toFinsupp := toFinsupp✝ }.update n a).coeff x✝ = Function.update { toFinsupp := toFinsupp✝ }.coeff n a x✝
-- Mathlib/Order/SymmDiff.lean
theorem bihimp_bihimp_bihimp_comm : a ⇔ b ⇔ (c ⇔ d) = a ⇔ c ⇔ (b ⇔ d)

Proof state:
α : Type u_2
inst✝ : BooleanAlgebra α
a b c d : α
⊢ a ⇔ b ⇔ (c ⇔ d) = a ⇔ c ⇔ (b ⇔ d)

Tactic:
simp_rw [bihimp_assoc, bihimp_left_comm]

Result:
no goals
-- Mathlib/Probability/Kernel/Composition/IntegralCompProd.lean
theorem setIntegral_compProd_univ_left (f : β × γ → E) {t : Set γ} (ht : MeasurableSet t)
    (hf : IntegrableOn f (univ ×ˢ t) ((κ ⊗ₖ η) a)) :
    ∫ z in univ ×ˢ t, f z ∂(κ ⊗ₖ η) a = ∫ x, ∫ y in t, f (x, y) ∂η (a, x) ∂κ a

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
E : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝³ : NormedAddCommGroup E
a : α
κ : Kernel α β
inst✝² : IsSFiniteKernel κ
η : Kernel (α × β) γ
inst✝¹ : IsSFiniteKernel η
inst✝ : NormedSpace ℝ E
f : β × γ → E
t : Set γ
ht : MeasurableSet t
hf : IntegrableOn f (univ ×ˢ t) ((κ ⊗ₖ η) a)
⊢ ∫ (z : β × γ) in univ ×ˢ t, f z ∂(κ ⊗ₖ η) a = ∫ (x : β), ∫ (y : γ) in t, f (x, y) ∂η (a, x) ∂κ a

Tactic:
simp_rw [setIntegral_compProd MeasurableSet.univ ht hf, Measure.restrict_univ]

Result:
no goals
-- Mathlib/Order/SupClosed.lean
@[simp] lemma supClosure_singleton : supClosure {a} = {a}

Proof state:
α : Type u_3
inst✝ : SemilatticeSup α
a : α
⊢ supClosure {a} = {a}

Tactic:
simp

Result:
no goals
-- Mathlib/Topology/MetricSpace/HausdorffDistance.lean
theorem exists_dist_lt_of_hausdorffDist_lt' {r : ℝ} (h : y ∈ t) (H : hausdorffDist s t < r)
    (fin : hausdorffEdist s t ≠ ⊤) : ∃ x ∈ s, dist x y < r

Proof state:
α : Type u
inst✝ : PseudoMetricSpace α
s t : Set α
y : α
r : ℝ
h : y ∈ t
H : hausdorffDist t s < r
fin : hausdorffEdist s t ≠ ⊤
⊢ ∃ x ∈ s, dist x y < r

Tactic:
rw [hausdorffEdist_comm] at fin

Result:
α : Type u
inst✝ : PseudoMetricSpace α
s t : Set α
y : α
r : ℝ
h : y ∈ t
H : hausdorffDist t s < r
fin : hausdorffEdist t s ≠ ⊤
⊢ ∃ x ∈ s, dist x y < r

Proof state:
α : Type u
inst✝ : PseudoMetricSpace α
s t : Set α
y : α
r : ℝ
h : y ∈ t
H : hausdorffDist t s < r
fin : hausdorffEdist t s ≠ ⊤
⊢ ∃ x ∈ s, dist x y < r

Tactic:
simpa [dist_comm] using exists_dist_lt_of_hausdorffDist_lt h H fin

Result:
no goals

Proof state:
α : Type u
inst✝ : PseudoMetricSpace α
s t : Set α
y : α
r : ℝ
h : y ∈ t
H : hausdorffDist s t < r
fin : hausdorffEdist s t ≠ ⊤
⊢ ∃ x ∈ s, dist x y < r

Tactic:
rw [hausdorffDist_comm] at H

Result:
α : Type u
inst✝ : PseudoMetricSpace α
s t : Set α
y : α
r : ℝ
h : y ∈ t
H : hausdorffDist t s < r
fin : hausdorffEdist s t ≠ ⊤
⊢ ∃ x ∈ s, dist x y < r
-- Mathlib/Algebra/Lie/Submodule.lean
theorem map_id : N.map LieModuleHom.id = N

Proof state:
case h
R : Type u
L : Type v
M : Type w
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : LieRingModule L M
N : LieSubmodule R L M
m✝ : M
⊢ m✝ ∈ map LieModuleHom.id N ↔ m✝ ∈ N

Tactic:
simp

Result:
no goals

Proof state:
R : Type u
L : Type v
M : Type w
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : LieRingModule L M
N : LieSubmodule R L M
⊢ map LieModuleHom.id N = N

Tactic:
ext

Result:
case h
R : Type u
L : Type v
M : Type w
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : LieRingModule L M
N : LieSubmodule R L M
m✝ : M
⊢ m✝ ∈ map LieModuleHom.id N ↔ m✝ ∈ N
-- Mathlib/.lake/packages/lean4/src/lean/Init/SimpLemmas.lean
theorem Bool.and_true (b : Bool) : (b && true) = b

Proof state:
b : Bool
⊢ (b && true) = b

Tactic:
cases b <;> rfl

Result:
no goals
-- Mathlib/Data/Set/Finite/Basic.lean
theorem toFinset_empty (h : (∅ : Set α).Finite) : h.toFinset = ∅

Proof state:
α : Type u
h : ∅.Finite
⊢ h.toFinset = ∅

Tactic:
simp

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Erase.lean
theorem le_size_eraseP (l : Array α) : l.size - 1 ≤ (l.eraseP p).size

Proof state:
case mk
α : Type u_1
p : α → Bool
l : List α
⊢ { toList := l }.size - 1 ≤ ({ toList := l }.eraseP p).size

Tactic:
simpa using List.le_length_eraseP l

Result:
no goals

Proof state:
α : Type u_1
p : α → Bool
l : Array α
⊢ l.size - 1 ≤ (l.eraseP p).size

Tactic:
rcases l with ⟨l⟩

Result:
case mk
α : Type u_1
p : α → Bool
l : List α
⊢ { toList := l }.size - 1 ≤ ({ toList := l }.eraseP p).size
-- Mathlib/Topology/UniformSpace/UniformConvergence.lean
theorem TendstoUniformly.tendstoLocallyUniformly (h : TendstoUniformly F f p) :
    TendstoLocallyUniformly F f p := fun u hu _ => ⟨univ, univ_mem, by simpa using h u hu⟩

Proof state:
α : Type u
β : Type v
ι : Type x
inst✝¹ : UniformSpace β
F : ι → α → β
f : α → β
p : Filter ι
inst✝ : TopologicalSpace α
h : TendstoUniformly F f p
u : Set (β × β)
hu : u ∈ 𝓤 β
x✝ : α
⊢ ∀ᶠ (n : ι) in p, ∀ y ∈ univ, (f y, F n y) ∈ u

Tactic:
simpa using h u hu

Result:
no goals
-- Mathlib/Data/Multiset/ZeroCons.lean
@[simp] lemma le_singleton : s ≤ {a} ↔ s = 0 ∨ s = {a} :=
  Quot.induction_on s fun l ↦ by simp only [cons_zero, ← coe_singleton, quot_mk_to_coe'', coe_le,
    coe_eq_zero, coe_eq_coe, perm_singleton, subperm_singleton_iff]

Proof state:
α : Type u_1
s : Multiset α
a : α
l : List α
⊢ Quot.mk (⇑(isSetoid α)) l ≤ {a} ↔ Quot.mk (⇑(isSetoid α)) l = 0 ∨ Quot.mk (⇑(isSetoid α)) l = {a}

Tactic:
simp only [cons_zero, ← coe_singleton, quot_mk_to_coe'', coe_le,
coe_eq_zero, coe_eq_coe, perm_singleton, subperm_singleton_iff]

Result:
no goals
-- Mathlib/CategoryTheory/Limits/Shapes/Images.lean
theorem image.factor_map :
    factorThruImage f.hom ≫ image.map sq = sq.left ≫ factorThruImage g.hom

Proof state:
C : Type u
inst✝³ : Category.{v, u} C
f g : Arrow C
inst✝² : HasImage f.hom
inst✝¹ : HasImage g.hom
sq : f ⟶ g
inst✝ : HasImageMap sq
⊢ factorThruImage f.hom ≫ map sq = sq.left ≫ factorThruImage g.hom

Tactic:
simp

Result:
no goals
-- Mathlib/FieldTheory/Perfect.lean
theorem iterateFrobeniusEquiv_symm_add_apply (x : R) : (iterateFrobeniusEquiv R p (m + n)).symm x =
    (iterateFrobeniusEquiv R p m).symm ((iterateFrobeniusEquiv R p n).symm x) :=
  (iterateFrobeniusEquiv R p (m + n)).injective <| by rw [RingEquiv.apply_symm_apply, add_comm,
    iterateFrobeniusEquiv_add_apply, RingEquiv.apply_symm_apply, RingEquiv.apply_symm_apply]

Proof state:
R : Type u_1
p m n : ℕ
inst✝² : CommSemiring R
inst✝¹ : ExpChar R p
inst✝ : PerfectRing R p
x : R
⊢ (iterateFrobeniusEquiv R p (m + n)) ((iterateFrobeniusEquiv R p (m + n)).symm x) =
    (iterateFrobeniusEquiv R p (m + n)) ((iterateFrobeniusEquiv R p m).symm ((iterateFrobeniusEquiv R p n).symm x))

Tactic:
rw [RingEquiv.apply_symm_apply, add_comm,
iterateFrobeniusEquiv_add_apply, RingEquiv.apply_symm_apply, RingEquiv.apply_symm_apply]

Result:
no goals
-- Mathlib/FieldTheory/IsAlgClosed/Basic.lean
theorem equivOfEquiv_symm_algebraMap (hSR : S ≃+* R) (r : R) :
    (equivOfEquiv L M hSR).symm (algebraMap R M r) = algebraMap S L (hSR.symm r) :=
  (equivOfEquiv L M hSR).injective (by simp)

Proof state:
R : Type u
S : Type u_3
L : Type v
M : Type w
inst✝⁹ : CommRing R
inst✝⁸ : CommRing S
inst✝⁷ : Field L
inst✝⁶ : Field M
inst✝⁵ : Algebra R M
inst✝⁴ : NoZeroSMulDivisors R M
inst✝³ : IsAlgClosure R M
inst✝² : Algebra S L
inst✝¹ : NoZeroSMulDivisors S L
inst✝ : IsAlgClosure S L
hSR : S ≃+* R
r : R
⊢ (equivOfEquiv L M hSR) ((equivOfEquiv L M hSR).symm ((algebraMap R M) r)) =
    (equivOfEquiv L M hSR) ((algebraMap S L) (hSR.symm r))

Tactic:
simp

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Find.lean
theorem Sublist.findSome?_eq_none {l₁ l₂ : List α} (h : l₁ <+ l₂) :
    l₂.findSome? f = none → l₁.findSome? f = none

Proof state:
α : Type u_1
α✝ : Type u_2
f : α → Option α✝
l₁ l₂ : List α
h : l₁ <+ l₂
⊢ findSome? f l₂ = none → findSome? f l₁ = none

Tactic:
simp only [List.findSome?_eq_none_iff, Bool.not_eq_true]

Result:
α : Type u_1
α✝ : Type u_2
f : α → Option α✝
l₁ l₂ : List α
h : l₁ <+ l₂
⊢ (∀ (x : α), x ∈ l₂ → f x = none) → ∀ (x : α), x ∈ l₁ → f x = none

Proof state:
α : Type u_1
α✝ : Type u_2
f : α → Option α✝
l₁ l₂ : List α
h : l₁ <+ l₂
⊢ (∀ (x : α), x ∈ l₂ → f x = none) → ∀ (x : α), x ∈ l₁ → f x = none

Tactic:
exact fun w x m => w x (Sublist.mem m h)

Result:
no goals
-- Mathlib/RingTheory/Ideal/Maps.lean
theorem LinearMap.annihilator_le_of_injective (f : M →ₗ[R] M') (hf : Function.Injective f) :
    Module.annihilator R M' ≤ Module.annihilator R M := fun x h ↦ by
  rw [Module.mem_annihilator] at h ⊢; exact fun m ↦ hf (by rw [map_smul, h, f.map_zero])

Proof state:
R : Type u_1
M : Type u_2
M' : Type u_3
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid M'
inst✝ : Module R M'
f : M →ₗ[R] M'
hf : Function.Injective ⇑f
x : R
h : ∀ (m : M'), x • m = 0
m : M
⊢ f (x • m) = f 0

Tactic:
rw [map_smul, h, f.map_zero]

Result:
no goals

Proof state:
R : Type u_1
M : Type u_2
M' : Type u_3
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid M'
inst✝ : Module R M'
f : M →ₗ[R] M'
hf : Function.Injective ⇑f
x : R
h : ∀ (m : M'), x • m = 0
⊢ ∀ (m : M), x • m = 0

Tactic:
exact fun m ↦ hf (by rw [map_smul, h, f.map_zero])

Result:
no goals

Proof state:
R : Type u_1
M : Type u_2
M' : Type u_3
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid M'
inst✝ : Module R M'
f : M →ₗ[R] M'
hf : Function.Injective ⇑f
x : R
h : x ∈ Module.annihilator R M'
⊢ x ∈ Module.annihilator R M

Tactic:
rw [Module.mem_annihilator] at h ⊢

Result:
R : Type u_1
M : Type u_2
M' : Type u_3
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid M'
inst✝ : Module R M'
f : M →ₗ[R] M'
hf : Function.Injective ⇑f
x : R
h : ∀ (m : M'), x • m = 0
⊢ ∀ (m : M), x • m = 0
-- Mathlib/LinearAlgebra/LinearIndependent/Defs.lean
theorem not_linearIndependent_iffₛ :
    ¬LinearIndependent R v ↔ ∃ s : Finset ι,
      ∃ f g : ι → R, ∑ i ∈ s, f i • v i = ∑ i ∈ s, g i • v i ∧ ∃ i ∈ s, f i ≠ g i

Proof state:
ι : Type u'
R : Type u_2
M : Type u_4
v : ι → M
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
⊢ ¬LinearIndependent R v ↔ ∃ s f g, ∑ i ∈ s, f i • v i = ∑ i ∈ s, g i • v i ∧ ∃ i ∈ s, f i ≠ g i

Tactic:
rw [linearIndependent_iff'ₛ]

Result:
ι : Type u'
R : Type u_2
M : Type u_4
v : ι → M
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
⊢ (¬∀ (s : Finset ι) (f g : ι → R), ∑ i ∈ s, f i • v i = ∑ i ∈ s, g i • v i → ∀ i ∈ s, f i = g i) ↔
    ∃ s f g, ∑ i ∈ s, f i • v i = ∑ i ∈ s, g i • v i ∧ ∃ i ∈ s, f i ≠ g i

Proof state:
ι : Type u'
R : Type u_2
M : Type u_4
v : ι → M
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
⊢ (¬∀ (s : Finset ι) (f g : ι → R), ∑ i ∈ s, f i • v i = ∑ i ∈ s, g i • v i → ∀ i ∈ s, f i = g i) ↔
    ∃ s f g, ∑ i ∈ s, f i • v i = ∑ i ∈ s, g i • v i ∧ ∃ i ∈ s, f i ≠ g i

Tactic:
simp only [exists_prop, not_forall]

Result:
no goals
-- Mathlib/SetTheory/Game/PGame.lean
theorem relabel_moveLeft {x : PGame} {xl' xr'} (el : xl' ≃ x.LeftMoves) (er : xr' ≃ x.RightMoves)
    (i : x.LeftMoves) : moveLeft (relabel el er) (el.symm i) = x.moveLeft i

Proof state:
x : PGame
xl' xr' : Type u_1
el : xl' ≃ x.LeftMoves
er : xr' ≃ x.RightMoves
i : x.LeftMoves
⊢ (relabel el er).moveLeft (el.symm i) = x.moveLeft i

Tactic:
simp

Result:
no goals
-- Mathlib/Data/Matroid/Circuit.lean
@[simp] lemma fundCircuit_restrict_univ (M : Matroid α) :
    (M ↾ univ).fundCircuit e I = M.fundCircuit e I

Proof state:
α : Type u_1
I : Set α
e : α
M : Matroid α
aux : ∀ (A B : Set α), M.closure A ⊆ B ∪ univ \ M.E ↔ M.closure A ⊆ B
⊢ (M ↾ univ).fundCircuit e I = M.fundCircuit e I

Tactic:
simp [fundCircuit, aux]

Result:
no goals

Proof state:
α : Type u_1
I : Set α
e : α
M : Matroid α
A B : Set α
⊢ M.closure A ⊆ B ∪ univ \ M.E ↔ M.closure A ⊆ B

Tactic:
refine ⟨fun h ↦ ?_, fun h ↦ h.trans subset_union_left⟩

Result:
α : Type u_1
I : Set α
e : α
M : Matroid α
A B : Set α
h : M.closure A ⊆ B ∪ univ \ M.E
⊢ M.closure A ⊆ B

Proof state:
α : Type u_1
I : Set α
e : α
M : Matroid α
A B : Set α
h : M.closure A ⊆ B ∪ univ \ M.E
⊢ M.closure A ⊆ B

Tactic:
refine (subset_inter h (M.closure_subset_ground A)).trans ?_

Result:
α : Type u_1
I : Set α
e : α
M : Matroid α
A B : Set α
h : M.closure A ⊆ B ∪ univ \ M.E
⊢ (B ∪ univ \ M.E) ∩ M.E ⊆ B

Proof state:
α : Type u_1
I : Set α
e : α
M : Matroid α
A B : Set α
h : M.closure A ⊆ B ∪ univ \ M.E
⊢ (B ∪ univ \ M.E) ∩ M.E ⊆ B

Tactic:
simp [union_inter_distrib_right]

Result:
no goals

Proof state:
α : Type u_1
I : Set α
e : α
M : Matroid α
⊢ (M ↾ univ).fundCircuit e I = M.fundCircuit e I

Tactic:
have aux (A B) : M.closure A ⊆ B ∪ univ \ M.E ↔ M.closure A ⊆ B := by
  refine ⟨fun h ↦ ?_, fun h ↦ h.trans subset_union_left⟩
  refine (subset_inter h (M.closure_subset_ground A)).trans ?_
  simp [union_inter_distrib_right]

Result:
α : Type u_1
I : Set α
e : α
M : Matroid α
aux : ∀ (A B : Set α), M.closure A ⊆ B ∪ univ \ M.E ↔ M.closure A ⊆ B
⊢ (M ↾ univ).fundCircuit e I = M.fundCircuit e I
-- Mathlib/Data/Fin/Tuple/Take.lean
theorem get_take_ofFn_eq_take_comp_cast {α : Type*} {m : ℕ} (v : Fin n → α) (h : m ≤ n) :
    ((List.ofFn v).take m).get = take m h v ∘ Fin.cast (by simp [h])

Proof state:
n : ℕ
α✝ : Fin n → Sort u_1
α : Type u_2
m : ℕ
v : Fin n → α
h : m ≤ n
⊢ (List.take m (List.ofFn v)).length = m

Tactic:
simp [h]

Result:
no goals

Proof state:
case h
n : ℕ
α : Type u_2
m : ℕ
v : Fin n → α
h : m ≤ n
i : Fin (List.take m (List.ofFn v)).length
⊢ (List.take m (List.ofFn v)).get i = (take m h v ∘ Fin.cast ⋯) i

Tactic:
simp [castLE]

Result:
no goals

Proof state:
n : ℕ
α : Type u_2
m : ℕ
v : Fin n → α
h : m ≤ n
⊢ (List.take m (List.ofFn v)).get = take m h v ∘ Fin.cast ⋯

Tactic:
ext i

Result:
case h
n : ℕ
α : Type u_2
m : ℕ
v : Fin n → α
h : m ≤ n
i : Fin (List.take m (List.ofFn v)).length
⊢ (List.take m (List.ofFn v)).get i = (take m h v ∘ Fin.cast ⋯) i
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Sum/Lemmas.lean
theorem isLeft_swap (x : α ⊕ β) : x.swap.isLeft = x.isRight

Proof state:
α : Type u_1
β : Type u_2
x : α ⊕ β
⊢ x.swap.isLeft = x.isRight

Tactic:
cases x <;> rfl

Result:
no goals