harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/LinearAlgebra/Finsupp/Defs.lean
theorem lapply_comp_lsingle_of_ne (a a' : α) (h : a ≠ a') :
    lapply a ∘ₗ lsingle a' = (0 : M →ₗ[R] M)

Proof state:
α : Type u_1
M : Type u_2
R : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
a a' : α
h : a ≠ a'
⊢ lapply a ∘ₗ lsingle a' = 0

Tactic:
ext

Result:
case h
α : Type u_1
M : Type u_2
R : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
a a' : α
h : a ≠ a'
x✝ : M
⊢ (lapply a ∘ₗ lsingle a') x✝ = 0 x✝

Proof state:
case h
α : Type u_1
M : Type u_2
R : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
a a' : α
h : a ≠ a'
x✝ : M
⊢ (lapply a ∘ₗ lsingle a') x✝ = 0 x✝

Tactic:
simp [h.symm]

Result:
no goals
-- Mathlib/.lake/packages/batteries/Batteries/Data/String/Lemmas.lean
theorem revFind_of_valid (p s) :
    revFind s p = (s.1.reverse.dropWhile (!p ·)).tail?.map (⟨utf8Len ·⟩)

Proof state:
p : Char → Bool
s : String
⊢ s.revFind p = Option.map (fun x => { byteIdx := utf8Len x }) (List.dropWhile (fun x => !p x) s.data.reverse).tail?

Tactic:
simpa using revFindAux_of_valid p s.1.reverse []

Result:
no goals
-- Mathlib/Probability/IdentDistrib.lean
theorem evariance_eq {f : α → ℝ} {g : β → ℝ} (h : IdentDistrib f g μ ν) :
    evariance f μ = evariance g ν

Proof state:
case h.e'_3
α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
μ : Measure α
ν : Measure β
f : α → ℝ
g : β → ℝ
h : IdentDistrib f g μ ν
⊢ eVar[g; ν] = ∫⁻ (x : β), ↑‖g x - ∫ (x : β), g x ∂ν‖₊ ^ 2 ∂ν

Tactic:
rfl

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
μ : Measure α
ν : Measure β
f : α → ℝ
g : β → ℝ
h : IdentDistrib f g μ ν
⊢ eVar[f; μ] = eVar[g; ν]

Tactic:
convert (h.sub_const (∫ x, f x ∂μ)).nnnorm.coe_nnreal_ennreal.sq.lintegral_eq

Result:
case h.e'_3
α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
μ : Measure α
ν : Measure β
f : α → ℝ
g : β → ℝ
h : IdentDistrib f g μ ν
⊢ eVar[g; ν] = ∫⁻ (x : β), ↑‖g x - ∫ (x : α), f x ∂μ‖₊ ^ 2 ∂ν

Proof state:
case h.e'_3
α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
μ : Measure α
ν : Measure β
f : α → ℝ
g : β → ℝ
h : IdentDistrib f g μ ν
⊢ eVar[g; ν] = ∫⁻ (x : β), ↑‖g x - ∫ (x : α), f x ∂μ‖₊ ^ 2 ∂ν

Tactic:
rw [h.integral_eq]

Result:
case h.e'_3
α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
μ : Measure α
ν : Measure β
f : α → ℝ
g : β → ℝ
h : IdentDistrib f g μ ν
⊢ eVar[g; ν] = ∫⁻ (x : β), ↑‖g x - ∫ (x : β), g x ∂ν‖₊ ^ 2 ∂ν
-- Mathlib/MeasureTheory/MeasurableSpace/Defs.lean
theorem MeasurableSet.ite' {s t : Set α} {p : Prop} (hs : p → MeasurableSet s)
    (ht : ¬p → MeasurableSet t) : MeasurableSet (ite p s t)

Proof state:
case pos
α : Type u_1
m : MeasurableSpace α
s t : Set α
p : Prop
hs : p → MeasurableSet s
ht : ¬p → MeasurableSet t
h : p
⊢ MeasurableSet s

case neg
α : Type u_1
m : MeasurableSpace α
s t : Set α
p : Prop
hs : p → MeasurableSet s
ht : ¬p → MeasurableSet t
h : ¬p
⊢ MeasurableSet t

Tactic:
exacts [hs h, ht h]

Result:
no goals

Proof state:
α : Type u_1
m : MeasurableSpace α
s t : Set α
p : Prop
hs : p → MeasurableSet s
ht : ¬p → MeasurableSet t
⊢ MeasurableSet (if p then s else t)

Tactic:
split_ifs with h

Result:
case pos
α : Type u_1
m : MeasurableSpace α
s t : Set α
p : Prop
hs : p → MeasurableSet s
ht : ¬p → MeasurableSet t
h : p
⊢ MeasurableSet s

case neg
α : Type u_1
m : MeasurableSpace α
s t : Set α
p : Prop
hs : p → MeasurableSet s
ht : ¬p → MeasurableSet t
h : ¬p
⊢ MeasurableSet t
-- Mathlib/Algebra/Algebra/Operations.lean
lemma mul_mem_smul_iff {S} [CommRing S] [Algebra R S] {x : S} {p : Submodule R S} {y : S}
    (hx : x ∈ nonZeroDivisors S) :
    x * y ∈ x • p ↔ y ∈ p :=
  show Exists _ ↔ _ by simp [mul_cancel_left_mem_nonZeroDivisors hx]

Proof state:
R : Type u
inst✝² : CommSemiring R
S : Type u_1
inst✝¹ : CommRing S
inst✝ : Algebra R S
x : S
p : Submodule R S
y : S
hx : x ∈ nonZeroDivisors S
⊢ (∃ a ∈ ↑p, (DistribMulAction.toLinearMap R S x) a = x * y) ↔ y ∈ p

Tactic:
simp [mul_cancel_left_mem_nonZeroDivisors hx]

Result:
no goals
-- Mathlib/Analysis/Normed/Group/Basic.lean
theorem edist_eq_enorm_div (a b : E) : edist a b = ‖a / b‖ₑ

Proof state:
E : Type u_5
inst✝ : SeminormedGroup E
a b : E
⊢ edist a b = ‖a / b‖ₑ

Tactic:
rw [edist_dist, dist_eq_norm_div, ofReal_norm_eq_enorm']

Result:
no goals
-- Mathlib/FieldTheory/Separable.lean
theorem Separable.of_pow' {f : R[X]} :
    ∀ {n : ℕ} (_h : (f ^ n).Separable), IsUnit f ∨ f.Separable ∧ n = 1 ∨ n = 0
  | 0 => fun _h => Or.inr <| Or.inr rfl
  | 1 => fun h => Or.inr <| Or.inl ⟨pow_one f ▸ h, rfl⟩
  | n + 2 => fun h => by
    rw [pow_succ, pow_succ] at h
    exact Or.inl (isCoprime_self.1 h.isCoprime.of_mul_left_right)

Proof state:
R : Type u
inst✝ : CommSemiring R
f : R[X]
n : ℕ
h : (f ^ n * f * f).Separable
⊢ IsUnit f ∨ f.Separable ∧ n + 2 = 1 ∨ n + 2 = 0

Tactic:
exact Or.inl (isCoprime_self.1 h.isCoprime.of_mul_left_right)

Result:
no goals

Proof state:
R : Type u
inst✝ : CommSemiring R
f : R[X]
n : ℕ
h : (f ^ (n + 2)).Separable
⊢ IsUnit f ∨ f.Separable ∧ n + 2 = 1 ∨ n + 2 = 0

Tactic:
rw [pow_succ, pow_succ] at h

Result:
R : Type u
inst✝ : CommSemiring R
f : R[X]
n : ℕ
h : (f ^ n * f * f).Separable
⊢ IsUnit f ∨ f.Separable ∧ n + 2 = 1 ∨ n + 2 = 0
-- Mathlib/Tactic/CancelDenoms/Core.lean
theorem cancel_factors_le {α} [LinearOrderedField α] {a b ad bd a' b' gcd : α}
    (ha : ad * a = a') (hb : bd * b = b') (had : 0 < ad) (hbd : 0 < bd) (hgcd : 0 < gcd) :
    (a ≤ b) = (1 / gcd * (bd * a') ≤ 1 / gcd * (ad * b'))

Proof state:
α : Type u_1
inst✝ : LinearOrderedField α
a b ad bd a' b' gcd : α
ha : ad * a = a'
hb : bd * b = b'
had : 0 < ad
hbd : 0 < bd
hgcd : 0 < gcd
⊢ 0 < 1 / gcd

Tactic:
exact one_div_pos.2 hgcd

Result:
no goals

Proof state:
α : Type u_1
inst✝ : LinearOrderedField α
a b ad bd a' b' gcd : α
ha : ad * a = a'
hb : bd * b = b'
had : 0 < ad
hbd : 0 < bd
hgcd : 0 < gcd
⊢ (a ≤ b) = (1 / gcd * (bd * a') ≤ 1 / gcd * (ad * b'))

Tactic:
rw [mul_le_mul_left, ← ha, ← hb, ← mul_assoc, ← mul_assoc, mul_comm bd, mul_le_mul_left]

Result:
α : Type u_1
inst✝ : LinearOrderedField α
a b ad bd a' b' gcd : α
ha : ad * a = a'
hb : bd * b = b'
had : 0 < ad
hbd : 0 < bd
hgcd : 0 < gcd
⊢ 0 < ad * bd

α : Type u_1
inst✝ : LinearOrderedField α
a b ad bd a' b' gcd : α
ha : ad * a = a'
hb : bd * b = b'
had : 0 < ad
hbd : 0 < bd
hgcd : 0 < gcd
⊢ 0 < 1 / gcd

Proof state:
α : Type u_1
inst✝ : LinearOrderedField α
a b ad bd a' b' gcd : α
ha : ad * a = a'
hb : bd * b = b'
had : 0 < ad
hbd : 0 < bd
hgcd : 0 < gcd
⊢ 0 < ad * bd

Tactic:
exact mul_pos had hbd

Result:
no goals
-- Mathlib/Topology/IsLocalHomeomorph.lean
theorem isLocalHomeomorph_iff_isOpenEmbedding_restrict {f : X → Y} :
    IsLocalHomeomorph f ↔ ∀ x : X, ∃ U ∈ 𝓝 x, IsOpenEmbedding (U.restrict f)

Proof state:
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
⊢ IsLocalHomeomorph f ↔ ∀ (x : X), ∃ U ∈ 𝓝 x, IsOpenEmbedding (U.restrict f)

Tactic:
simp_rw [isLocalHomeomorph_iff_isLocalHomeomorphOn_univ,
  isLocalHomeomorphOn_iff_isOpenEmbedding_restrict, imp_iff_right (Set.mem_univ _)]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Sat/AIG/CachedGatesLemmas.lean
theorem xor_as_aig : ∀ (a b : Bool), (!(a && b) && !(!a && !b)) = (a ^^ b)

Proof state:
⊢ ∀ (a b : Bool), (!(a && b) && !(!a && !b)) = (a ^^ b)

Tactic:
decide

Result:
no goals
-- Mathlib/LinearAlgebra/AffineSpace/Combination.lean
theorem affineCombinationSingleWeights_apply_of_ne [DecidableEq ι] {i j : ι} (h : j ≠ i) :
    affineCombinationSingleWeights k i j = 0

Proof state:
k : Type u_1
inst✝¹ : Ring k
ι : Type u_4
inst✝ : DecidableEq ι
i j : ι
h : j ≠ i
⊢ affineCombinationSingleWeights k i j = 0

Tactic:
simp [affineCombinationSingleWeights, h]

Result:
no goals
-- Mathlib/Analysis/InnerProductSpace/Orthogonal.lean
theorem inf_orthogonal_eq_bot : K ⊓ Kᗮ = ⊥

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
K : Submodule 𝕜 E
⊢ K ⊓ Kᗮ = ⊥

Tactic:
rw [eq_bot_iff]

Result:
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
K : Submodule 𝕜 E
⊢ K ⊓ Kᗮ ≤ ⊥

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
K : Submodule 𝕜 E
x : E
⊢ x ∈ K ⊓ Kᗮ → x ∈ ⊥

Tactic:
rw [mem_inf]

Result:
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
K : Submodule 𝕜 E
x : E
⊢ x ∈ K ∧ x ∈ Kᗮ → x ∈ ⊥

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
K : Submodule 𝕜 E
x : E
⊢ x ∈ K ∧ x ∈ Kᗮ → x ∈ ⊥

Tactic:
exact fun ⟨hx, ho⟩ => inner_self_eq_zero.1 (ho x hx)

Result:
no goals

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
K : Submodule 𝕜 E
⊢ K ⊓ Kᗮ ≤ ⊥

Tactic:
intro x

Result:
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
K : Submodule 𝕜 E
x : E
⊢ x ∈ K ⊓ Kᗮ → x ∈ ⊥
-- Mathlib/Combinatorics/SimpleGraph/Subgraph.lean
theorem degree_le (G' : Subgraph G) (v : V) [Fintype (G'.neighborSet v)]
    [Fintype (G.neighborSet v)] : G'.degree v ≤ G.degree v

Proof state:
V : Type u
G : SimpleGraph V
G' : G.Subgraph
v : V
inst✝¹ : Fintype ↑(G'.neighborSet v)
inst✝ : Fintype ↑(G.neighborSet v)
⊢ G'.degree v ≤ G.degree v

Tactic:
rw [← card_neighborSet_eq_degree]

Result:
V : Type u
G : SimpleGraph V
G' : G.Subgraph
v : V
inst✝¹ : Fintype ↑(G'.neighborSet v)
inst✝ : Fintype ↑(G.neighborSet v)
⊢ G'.degree v ≤ Fintype.card ↑(G.neighborSet v)

Proof state:
V : Type u
G : SimpleGraph V
G' : G.Subgraph
v : V
inst✝¹ : Fintype ↑(G'.neighborSet v)
inst✝ : Fintype ↑(G.neighborSet v)
⊢ G'.degree v ≤ Fintype.card ↑(G.neighborSet v)

Tactic:
exact Set.card_le_card (G'.neighborSet_subset v)

Result:
no goals
-- Mathlib/Algebra/MvPolynomial/Basic.lean
@[simp]
lemma coeff_single_X [DecidableEq σ] (s s' : σ) (n : ℕ) :
    (X s).coeff (R := R) (Finsupp.single s' n) = if n = 1 ∧ s = s' then 1 else 0

Proof state:
R : Type u
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : DecidableEq σ
s s' : σ
n : ℕ
⊢ coeff (Finsupp.single s' n) (X s) = if n = 1 ∧ s = s' then 1 else 0

Tactic:
simpa [eq_comm, and_comm] using coeff_single_X_pow s s' 1 n

Result:
no goals
-- Mathlib/Data/Finset/Filter.lean
lemma filter_inj : s.filter p = t.filter p ↔ ∀ ⦃a⦄, p a → (a ∈ s ↔ a ∈ t)

Proof state:
α : Type u_1
p : α → Prop
inst✝ : DecidablePred p
s t : Finset α
⊢ filter p s = filter p t ↔ ∀ ⦃a : α⦄, p a → (a ∈ s ↔ a ∈ t)

Tactic:
simp [Finset.ext_iff]

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Operations.lean
@[simp]
lemma sup_edge_self : G ⊔ edge s s = G

Proof state:
V : Type u_1
G : SimpleGraph V
s : V
⊢ G ⊔ edge s s = G

Tactic:
rw [edge_self_eq_bot, sup_of_le_left bot_le]

Result:
no goals
-- Mathlib/Analysis/InnerProductSpace/Basic.lean
theorem norm_add_sq_eq_norm_sq_add_norm_sq_of_inner_eq_zero (x y : E) (h : ⟪x, y⟫ = 0) :
    ‖x + y‖ * ‖x + y‖ = ‖x‖ * ‖x‖ + ‖y‖ * ‖y‖

Proof state:
case h
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
x y : E
h : ⟪x, y⟫_𝕜 = 0
⊢ re ⟪x, y⟫_𝕜 = 0

Tactic:
simp only [h, zero_re']

Result:
no goals

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
x y : E
h : ⟪x, y⟫_𝕜 = 0
⊢ ‖x + y‖ * ‖x + y‖ = ‖x‖ * ‖x‖ + ‖y‖ * ‖y‖

Tactic:
rw [@norm_add_mul_self 𝕜, add_right_cancel_iff, add_right_eq_self, mul_eq_zero]

Result:
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
x y : E
h : ⟪x, y⟫_𝕜 = 0
⊢ 2 = 0 ∨ re ⟪x, y⟫_𝕜 = 0

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
x y : E
h : ⟪x, y⟫_𝕜 = 0
⊢ 2 = 0 ∨ re ⟪x, y⟫_𝕜 = 0

Tactic:
apply Or.inr

Result:
case h
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
x y : E
h : ⟪x, y⟫_𝕜 = 0
⊢ re ⟪x, y⟫_𝕜 = 0
-- Mathlib/Algebra/Star/Subalgebra.lean
lemma StarSubalgebra.toNonUnitalStarSubalgebra_toStarSubalgebra (S : StarSubalgebra R A) :
    S.toNonUnitalStarSubalgebra.toStarSubalgebra S.one_mem' = S

Proof state:
R : Type u_1
A : Type u_2
inst✝⁵ : CommSemiring R
inst✝⁴ : StarRing R
inst✝³ : Semiring A
inst✝² : StarRing A
inst✝¹ : Algebra R A
inst✝ : StarModule R A
S : StarSubalgebra R A
⊢ S.toNonUnitalStarSubalgebra.toStarSubalgebra ⋯ = S

Tactic:
cases S

Result:
case mk
R : Type u_1
A : Type u_2
inst✝⁵ : CommSemiring R
inst✝⁴ : StarRing R
inst✝³ : Semiring A
inst✝² : StarRing A
inst✝¹ : Algebra R A
inst✝ : StarModule R A
toSubalgebra✝ : Subalgebra R A
star_mem'✝ : ∀ {a : A}, a ∈ toSubalgebra✝.carrier → star a ∈ toSubalgebra✝.carrier
⊢ { toSubalgebra := toSubalgebra✝, star_mem' := star_mem'✝ }.toNonUnitalStarSubalgebra.toStarSubalgebra ⋯ =
    { toSubalgebra := toSubalgebra✝, star_mem' := star_mem'✝ }

Proof state:
case mk
R : Type u_1
A : Type u_2
inst✝⁵ : CommSemiring R
inst✝⁴ : StarRing R
inst✝³ : Semiring A
inst✝² : StarRing A
inst✝¹ : Algebra R A
inst✝ : StarModule R A
toSubalgebra✝ : Subalgebra R A
star_mem'✝ : ∀ {a : A}, a ∈ toSubalgebra✝.carrier → star a ∈ toSubalgebra✝.carrier
⊢ { toSubalgebra := toSubalgebra✝, star_mem' := star_mem'✝ }.toNonUnitalStarSubalgebra.toStarSubalgebra ⋯ =
    { toSubalgebra := toSubalgebra✝, star_mem' := star_mem'✝ }

Tactic:
rfl

Result:
no goals
-- Mathlib/RingTheory/WittVector/Basic.lean
private lemma ghostFun_zsmul (m : ℤ) (x : WittVector p R) : ghostFun (m • x) = m • ghostFun x

Proof state:
p : ℕ
R : Type u_1
inst✝¹ : CommRing R
inst✝ : Fact (Nat.Prime p)
m : ℤ
x : 𝕎 R
⊢ WittVector.ghostFun (m • x) = m • WittVector.ghostFun x

Tactic:
ghost_fun_tac m • (X 0), ![x.coeff]

Result:
no goals
-- Mathlib/Order/Interval/Set/OrdConnectedComponent.lean
theorem ordConnectedComponent_univ : ordConnectedComponent univ x = univ

Proof state:
α : Type u_1
inst✝ : LinearOrder α
x : α
⊢ univ.ordConnectedComponent x = univ

Tactic:
simp [ordConnectedComponent]

Result:
no goals
-- Mathlib/Data/Set/Image.lean
/-- If preimage of each singleton under `f : α → β` is either empty or the whole type,
then `f` is a constant. -/
lemma exists_eq_const_of_preimage_singleton [Nonempty β] {f : α → β}
    (hf : ∀ b : β, f ⁻¹' {b} = ∅ ∨ f ⁻¹' {b} = univ) : ∃ b, f = const α b

Proof state:
case inl.intro
α : Type u_1
β : Type u_2
inst✝ : Nonempty β
f : α → β
hf : ∀ (b : β), f ⁻¹' {b} = ∅ ∨ f ⁻¹' {b} = univ
b : β
hb : f ⁻¹' {b} = univ
⊢ ∃ b, f = const α b

Tactic:
exact ⟨b, funext fun x ↦ eq_univ_iff_forall.1 hb x⟩

Result:
no goals

Proof state:
case inr
α : Type u_1
β : Type u_2
inst✝ : Nonempty β
f : α → β
hf : ∀ (b : β), f ⁻¹' {b} = ∅ ∨ f ⁻¹' {b} = univ
hf' : ¬∃ b, f ⁻¹' {b} = univ
⊢ ∃ b, f = const α b

Tactic:
have : ∀ x b, f x ≠ b := fun x b ↦
  eq_empty_iff_forall_not_mem.1 ((hf b).resolve_right fun h ↦ hf' ⟨b, h⟩) x

Result:
case inr
α : Type u_1
β : Type u_2
inst✝ : Nonempty β
f : α → β
hf : ∀ (b : β), f ⁻¹' {b} = ∅ ∨ f ⁻¹' {b} = univ
hf' : ¬∃ b, f ⁻¹' {b} = univ
this : ∀ (x : α) (b : β), f x ≠ b
⊢ ∃ b, f = const α b

Proof state:
α : Type u_1
β : Type u_2
inst✝ : Nonempty β
f : α → β
hf : ∀ (b : β), f ⁻¹' {b} = ∅ ∨ f ⁻¹' {b} = univ
⊢ ∃ b, f = const α b

Tactic:
rcases em (∃ b, f ⁻¹' {b} = univ) with ⟨b, hb⟩ | hf'

Result:
case inl.intro
α : Type u_1
β : Type u_2
inst✝ : Nonempty β
f : α → β
hf : ∀ (b : β), f ⁻¹' {b} = ∅ ∨ f ⁻¹' {b} = univ
b : β
hb : f ⁻¹' {b} = univ
⊢ ∃ b, f = const α b

case inr
α : Type u_1
β : Type u_2
inst✝ : Nonempty β
f : α → β
hf : ∀ (b : β), f ⁻¹' {b} = ∅ ∨ f ⁻¹' {b} = univ
hf' : ¬∃ b, f ⁻¹' {b} = univ
⊢ ∃ b, f = const α b

Proof state:
case inr
α : Type u_1
β : Type u_2
inst✝ : Nonempty β
f : α → β
hf : ∀ (b : β), f ⁻¹' {b} = ∅ ∨ f ⁻¹' {b} = univ
hf' : ¬∃ b, f ⁻¹' {b} = univ
this : ∀ (x : α) (b : β), f x ≠ b
⊢ ∃ b, f = const α b

Tactic:
exact ⟨Classical.arbitrary β, funext fun x ↦ absurd rfl (this x _)⟩

Result:
no goals
-- Mathlib/Data/Set/Insert.lean
theorem inter_singleton_nonempty : (s ∩ {a}).Nonempty ↔ a ∈ s

Proof state:
α : Type u
s : Set α
a : α
⊢ (s ∩ {a}).Nonempty ↔ a ∈ s

Tactic:
rw [inter_comm, singleton_inter_nonempty]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/MapIdx.lean
theorem mem_zipIdx_iff_le_and_getElem?_sub {x : α × Nat} {l : Array α} {k : Nat} :
    x ∈ zipIdx l k ↔ k ≤ x.2 ∧ l[x.2 - k]? = some x.1

Proof state:
case mk
α : Type u_1
l : Array α
k : Nat
fst✝ : α
snd✝ : Nat
⊢ (fst✝, snd✝) ∈ l.zipIdx k ↔ k ≤ (fst✝, snd✝).snd ∧ l[(fst✝, snd✝).snd - k]? = some (fst✝, snd✝).fst

Tactic:
simp [mk_mem_zipIdx_iff_le_and_getElem?_sub]

Result:
no goals

Proof state:
α : Type u_1
x : α × Nat
l : Array α
k : Nat
⊢ x ∈ l.zipIdx k ↔ k ≤ x.snd ∧ l[x.snd - k]? = some x.fst

Tactic:
cases x

Result:
case mk
α : Type u_1
l : Array α
k : Nat
fst✝ : α
snd✝ : Nat
⊢ (fst✝, snd✝) ∈ l.zipIdx k ↔ k ≤ (fst✝, snd✝).snd ∧ l[(fst✝, snd✝).snd - k]? = some (fst✝, snd✝).fst
-- Mathlib/Topology/Algebra/Valued/ValuationTopology.lean
theorem hasBasis_uniformity : (uniformity R).HasBasis (fun _ => True)
    fun γ : Γ₀ˣ => { p : R × R | v (p.2 - p.1) < (γ : Γ₀) }

Proof state:
R : Type u
inst✝¹ : Ring R
Γ₀ : Type v
inst✝ : LinearOrderedCommGroupWithZero Γ₀
_i : Valued R Γ₀
⊢ (uniformity R).HasBasis (fun x => True) fun γ => {p | v (p.2 - p.1) < ↑γ}

Tactic:
rw [uniformity_eq_comap_nhds_zero]

Result:
R : Type u
inst✝¹ : Ring R
Γ₀ : Type v
inst✝ : LinearOrderedCommGroupWithZero Γ₀
_i : Valued R Γ₀
⊢ (Filter.comap (fun x => x.2 - x.1) (𝓝 0)).HasBasis (fun x => True) fun γ => {p | v (p.2 - p.1) < ↑γ}

Proof state:
R : Type u
inst✝¹ : Ring R
Γ₀ : Type v
inst✝ : LinearOrderedCommGroupWithZero Γ₀
_i : Valued R Γ₀
⊢ (Filter.comap (fun x => x.2 - x.1) (𝓝 0)).HasBasis (fun x => True) fun γ => {p | v (p.2 - p.1) < ↑γ}

Tactic:
exact (hasBasis_nhds_zero R Γ₀).comap _

Result:
no goals
-- Mathlib/Data/Matroid/Closure.lean
lemma closure_iUnion_closure_eq_closure_iUnion (M : Matroid α) (Xs : ι → Set α) :
    M.closure (⋃ i, M.closure (Xs i)) = M.closure (⋃ i, Xs i)

Proof state:
ι : Type u_1
α : Type u_2
M : Matroid α
Xs : ι → Set α
⊢ M.closure (⋃ i, M.closure (Xs i)) = M.closure (⋃ i, Xs i)

Tactic:
simp_rw [closure_eq_subtypeClosure, iUnion_inter, Subtype.coe_inj]

Result:
ι : Type u_1
α : Type u_2
M : Matroid α
Xs : ι → Set α
⊢ M.subtypeClosure ⟨⋃ i, ↑(M.subtypeClosure ⟨Xs i ∩ M.E, ⋯⟩) ∩ M.E, ⋯⟩ = M.subtypeClosure ⟨⋃ i, Xs i ∩ M.E, ⋯⟩

Proof state:
ι : Type u_1
α : Type u_2
M : Matroid α
Xs : ι → Set α
⊢ M.subtypeClosure ⟨⋃ i, ↑(M.subtypeClosure ⟨Xs i ∩ M.E, ⋯⟩) ∩ M.E, ⋯⟩ = M.subtypeClosure ⟨⋃ i, Xs i ∩ M.E, ⋯⟩

Tactic:
convert M.subtypeClosure.closure_iSup_closure (fun i ↦ ⟨Xs i ∩ M.E, inter_subset_right⟩) <;>
simp [← iUnion_inter, subtypeClosure]

Result:
no goals
-- Mathlib/Data/Nat/Cast/Order/Basic.lean
theorem cast_le_one : (n : α) ≤ 1 ↔ n ≤ 1

Proof state:
α : Type u_1
inst✝⁴ : AddMonoidWithOne α
inst✝³ : PartialOrder α
inst✝² : AddLeftMono α
inst✝¹ : ZeroLEOneClass α
inst✝ : CharZero α
n : ℕ
⊢ ↑n ≤ 1 ↔ n ≤ 1

Tactic:
rw [← cast_one, cast_le]

Result:
no goals
-- Mathlib/Algebra/Polynomial/Degree/Operations.lean
theorem degree_smul_le (a : R) (p : R[X]) : degree (a • p) ≤ degree p

Proof state:
R : Type u
inst✝ : Semiring R
a : R
p : R[X]
m : ℕ
hm : p.degree < ↑m
⊢ (a • p).coeff m = 0

Tactic:
rw [degree_lt_iff_coeff_zero] at hm

Result:
R : Type u
inst✝ : Semiring R
a : R
p : R[X]
m : ℕ
hm : ∀ (m_1 : ℕ), m ≤ m_1 → p.coeff m_1 = 0
⊢ (a • p).coeff m = 0

Proof state:
R : Type u
inst✝ : Semiring R
a : R
p : R[X]
⊢ (a • p).degree ≤ p.degree

Tactic:
refine (degree_le_iff_coeff_zero _ _).2 fun m hm => ?_

Result:
R : Type u
inst✝ : Semiring R
a : R
p : R[X]
m : ℕ
hm : p.degree < ↑m
⊢ (a • p).coeff m = 0

Proof state:
R : Type u
inst✝ : Semiring R
a : R
p : R[X]
m : ℕ
hm : ∀ (m_1 : ℕ), m ≤ m_1 → p.coeff m_1 = 0
⊢ (a • p).coeff m = 0

Tactic:
simp [hm m le_rfl]

Result:
no goals
-- Mathlib/Topology/Instances/ENNReal/Lemmas.lean
theorem biInf_le_nhds : ∀ x : ℝ≥0∞, ⨅ ε > 0, 𝓟 (Icc (x - ε) (x + ε)) ≤ 𝓝 x
  | ∞ => iInf₂_le_of_le 1 one_pos <| by
    simpa only [← coe_one, top_sub_coe, top_add, Icc_self, principal_singleton] using pure_le_nhds _
  | (x : ℝ≥0) => (nhds_of_ne_top coe_ne_top).ge

Proof state:
⊢ 𝓟 (Icc (⊤ - 1) (⊤ + 1)) ≤ 𝓝 ⊤

Tactic:
simpa only [← coe_one, top_sub_coe, top_add, Icc_self, principal_singleton] using pure_le_nhds _

Result:
no goals
-- Mathlib/Order/Iterate.lean
theorem iterate_pos_le_iff_map_le' (h : Commute f g) (hf : StrictMono f) (hg : Monotone g) {x n}
    (hn : 0 < n) : f^[n] x ≤ g^[n] x ↔ f x ≤ g x

Proof state:
α : Type u_1
inst✝ : LinearOrder α
f g : α → α
h : Commute f g
hf : StrictMono f
hg : Monotone g
x : α
n : ℕ
hn : 0 < n
⊢ f^[n] x ≤ g^[n] x ↔ f x ≤ g x

Tactic:
simpa only [not_lt] using not_congr (h.symm.iterate_pos_lt_iff_map_lt hg hf hn)

Result:
no goals
-- Mathlib/Data/Finset/Lattice/Fold.lean
theorem mem_sup {α β} [DecidableEq β] {s : Finset α} {f : α → Multiset β} {x : β} :
    x ∈ s.sup f ↔ ∃ v ∈ s, x ∈ f v

Proof state:
α : Type u_7
β : Type u_8
inst✝ : DecidableEq β
s : Finset α
f : α → Multiset β
x : β
⊢ x ∈ s.sup f ↔ ∃ v ∈ s, x ∈ f v

Tactic:
induction s using Finset.cons_induction <;> simp [*]

Result:
no goals
-- Mathlib/FieldTheory/Perfect.lean
theorem separable_iff_squarefree {g : K[X]} : g.Separable ↔ Squarefree g

Proof state:
K : Type u_1
inst✝¹ : Field K
inst✝ : PerfectField K
p : K[X]
h : Irreducible p
q : K[X]
sqf : Squarefree (p * q)
dvd : p ∣ derivative (p * q)
⊢ p ∣ q

Tactic:
rw [derivative_mul, dvd_add_left (dvd_mul_right p _)] at dvd

Result:
K : Type u_1
inst✝¹ : Field K
inst✝ : PerfectField K
p : K[X]
h : Irreducible p
q : K[X]
sqf : Squarefree (p * q)
dvd : p ∣ derivative p * q
⊢ p ∣ q

Proof state:
K : Type u_1
inst✝¹ : Field K
inst✝ : PerfectField K
p : K[X]
h : Irreducible p
q : K[X]
sqf : Squarefree (p * q)
dvd : p ∣ derivative p * q
⊢ p ∣ q

Tactic:
exact (separable_of_irreducible h).dvd_of_dvd_mul_left dvd

Result:
no goals

Proof state:
case intro
K : Type u_1
inst✝¹ : Field K
inst✝ : PerfectField K
p : K[X]
h : Irreducible p
q : K[X]
sqf : Squarefree (p * q)
dvd : p ∣ derivative (p * q)
⊢ False

Tactic:
replace dvd : p ∣ q := by
  rw [derivative_mul, dvd_add_left (dvd_mul_right p _)] at dvd
  exact (separable_of_irreducible h).dvd_of_dvd_mul_left dvd

Result:
case intro
K : Type u_1
inst✝¹ : Field K
inst✝ : PerfectField K
p : K[X]
h : Irreducible p
q : K[X]
sqf : Squarefree (p * q)
dvd : p ∣ q
⊢ False

Proof state:
case intro
K : Type u_1
inst✝¹ : Field K
inst✝ : PerfectField K
p : K[X]
h : Irreducible p
q : K[X]
sqf : Squarefree (p * q)
dvd : p ∣ q
⊢ False

Tactic:
exact (h.1 : ¬ IsUnit p) (sqf _ <| mul_dvd_mul_left _ dvd)

Result:
no goals

Proof state:
K : Type u_1
inst✝¹ : Field K
inst✝ : PerfectField K
g : K[X]
sqf : Squarefree g
⊢ ∀ (z : K[X]), Irreducible z → z ∣ g → ¬z ∣ derivative g

Tactic:
rintro p (h : Irreducible p) ⟨q, rfl⟩ (dvd : p ∣ derivative (p * q))

Result:
case intro
K : Type u_1
inst✝¹ : Field K
inst✝ : PerfectField K
p : K[X]
h : Irreducible p
q : K[X]
sqf : Squarefree (p * q)
dvd : p ∣ derivative (p * q)
⊢ False
-- Mathlib/Topology/ContinuousMap/ContinuousMapZero.lean
lemma isClosedEmbedding_toContinuousMap [T1Space R] :
    IsClosedEmbedding ((↑) : C(X, R)₀ → C(X, R)) where
  toIsEmbedding := isEmbedding_toContinuousMap
  isClosed_range

Proof state:
X : Type u_1
R : Type u_3
inst✝⁴ : Zero X
inst✝³ : Zero R
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace R
inst✝ : T1Space R
⊢ IsClosed (range _root_.toContinuousMap)

Tactic:
rw [range_toContinuousMap]

Result:
X : Type u_1
R : Type u_3
inst✝⁴ : Zero X
inst✝³ : Zero R
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace R
inst✝ : T1Space R
⊢ IsClosed {f | f 0 = 0}

Proof state:
X : Type u_1
R : Type u_3
inst✝⁴ : Zero X
inst✝³ : Zero R
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace R
inst✝ : T1Space R
⊢ IsClosed {f | f 0 = 0}

Tactic:
exact isClosed_singleton.preimage <| continuous_eval_const 0

Result:
no goals