harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Combinatorics/Enumerative/DyckWord.lean
@[simp] lemma nest_ne_zero : p.nest ≠ 0

Proof state:
p : DyckWord
⊢ p.nest ≠ 0

Tactic:
simp [← toList_ne_nil, nest]

Result:
no goals
-- Mathlib/RingTheory/Smooth/Kaehler.lean
lemma H1Cotangent.equivOfFormallySmooth_apply {P₁ P₂ : Extension R S} (f : P₁.Hom P₂)
    [FormallySmooth R P₁.Ring] [FormallySmooth R P₂.Ring] (x) :
    H1Cotangent.equivOfFormallySmooth P₁ P₂ x = map f x

Proof state:
R S : Type u
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
P₁ P₂ : Extension R S
f : P₁.Hom P₂
inst✝¹ : FormallySmooth R P₁.Ring
inst✝ : FormallySmooth R P₂.Ring
x : P₁.H1Cotangent
⊢ (equivOfFormallySmooth P₁ P₂) x = (map f) x

Tactic:
rw [← equivOfFormallySmooth_toLinearMap]

Result:
R S : Type u
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
P₁ P₂ : Extension R S
f : P₁.Hom P₂
inst✝¹ : FormallySmooth R P₁.Ring
inst✝ : FormallySmooth R P₂.Ring
x : P₁.H1Cotangent
⊢ (equivOfFormallySmooth P₁ P₂) x = ↑(equivOfFormallySmooth P₁ P₂) x

Proof state:
R S : Type u
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
P₁ P₂ : Extension R S
f : P₁.Hom P₂
inst✝¹ : FormallySmooth R P₁.Ring
inst✝ : FormallySmooth R P₂.Ring
x : P₁.H1Cotangent
⊢ (equivOfFormallySmooth P₁ P₂) x = ↑(equivOfFormallySmooth P₁ P₂) x

Tactic:
rfl

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Option/Lemmas.lean
theorem liftOrGet_none_right {f} {a : Option α} : liftOrGet f a none = a

Proof state:
α : Type u_1
f : α → α → α
a : Option α
⊢ liftOrGet f a none = a

Tactic:
cases a <;> rfl

Result:
no goals
-- Mathlib/Topology/Inseparable.lean
theorem map_mk_nhdsWithin_preimage (s : Set (SeparationQuotient X)) (x : X) :
    map mk (𝓝[mk ⁻¹' s] x) = 𝓝[s] mk x

Proof state:
X : Type u_1
inst✝ : TopologicalSpace X
s : Set (SeparationQuotient X)
x : X
⊢ Filter.map mk (𝓝[mk ⁻¹' s] x) = 𝓝[s] mk x

Tactic:
rw [nhdsWithin, ← comap_principal, Filter.push_pull, nhdsWithin, map_mk_nhds]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/RawLemmas.lean
theorem getKey!_insertMany_list_of_mem [EquivBEq α] [LawfulHashable α] [Inhabited α] (h : m.1.WF)
    {l : List (α × β)}
    {k k' : α} (k_beq : k == k')
    (distinct : l.Pairwise (fun a b => (a.1 == b.1) = false))
    (mem : k ∈ l.map Prod.fst) :
    (insertMany m l).1.getKey! k' = k

Proof state:
α : Type u
inst✝⁴ : BEq α
inst✝³ : Hashable α
β : Type v
m : Raw₀ α fun x => β
inst✝² : EquivBEq α
inst✝¹ : LawfulHashable α
inst✝ : Inhabited α
h : m.val.WF
l : List (α × β)
k k' : α
k_beq : (k == k') = true
distinct : List.Pairwise (fun a b => (a.fst == b.fst) = false) l
mem : k ∈ List.map Prod.fst l
⊢ (insertMany m l).val.getKey! k' = k

Tactic:
simp_to_model [Const.insertMany] using List.getKey!_insertListConst_of_mem

Result:
no goals
-- Mathlib/Analysis/Complex/Basic.lean
@[simp]
lemma natCast_mem_slitPlane {n : ℕ} : ↑n ∈ slitPlane ↔ n ≠ 0

Proof state:
n : ℕ
⊢ ↑n ∈ slitPlane ↔ n ≠ 0

Tactic:
simpa [pos_iff_ne_zero] using @ofReal_mem_slitPlane n

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Clique.lean
theorem isNIndepSet_induce {F : Set α} {s : Finset { x // x ∈ F }} {n : ℕ} :
    ((⊤ : Subgraph G).induce F).coe.IsNIndepSet n ↑s ↔
    G.IsNIndepSet n (Finset.map ⟨Subtype.val, Subtype.val_injective⟩ s)

Proof state:
α : Type u_1
G : SimpleGraph α
F : Set α
s : Finset { x // x ∈ F }
n : ℕ
⊢ (⊤.induce F).coe.IsNIndepSet n s ↔ G.IsNIndepSet n (map { toFun := Subtype.val, inj' := ⋯ } s)

Tactic:
simp [isNIndepSet_iff, (isIndepSet_induce)]

Result:
no goals
-- Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Order.lean
lemma mem_Icc_iff_norm_le_one {x : A} :
    x ∈ Icc 0 1 ↔ 0 ≤ x ∧ ‖x‖ ≤ 1

Proof state:
A : Type u_1
inst✝² : CStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
x : A
⊢ x ∈ Icc 0 1 ↔ 0 ≤ x ∧ ‖x‖ ≤ 1

Tactic:
simpa only [map_one] using mem_Icc_algebraMap_iff_norm_le zero_le_one (A := A)

Result:
no goals
-- Mathlib/Analysis/NormedSpace/Real.lean
theorem norm_smul_of_nonneg {t : ℝ} (ht : 0 ≤ t) (x : E) : ‖t • x‖ = t * ‖x‖

Proof state:
E : Type u_1
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
t : ℝ
ht : 0 ≤ t
x : E
⊢ ‖t • x‖ = t * ‖x‖

Tactic:
rw [norm_smul, Real.norm_eq_abs, abs_of_nonneg ht]

Result:
no goals
-- Mathlib/Algebra/CubicDiscriminant.lean
theorem monic_of_a_eq_one (ha : P.a = 1) : P.toPoly.Monic

Proof state:
R : Type u_1
P : Cubic R
inst✝ : Semiring R
ha : P.a = 1
⊢ P.toPoly.Monic

Tactic:
nontriviality R

Result:
R : Type u_1
P : Cubic R
inst✝ : Semiring R
ha : P.a = 1
a✝ : Nontrivial R
⊢ P.toPoly.Monic

Proof state:
R : Type u_1
P : Cubic R
inst✝ : Semiring R
ha : P.a = 1
a✝ : Nontrivial R
⊢ P.toPoly.Monic

Tactic:
rw [Monic, leadingCoeff_of_a_ne_zero (ha ▸ one_ne_zero), ha]

Result:
no goals
-- Mathlib/Algebra/Ring/Periodic.lean
theorem Periodic.sub_antiperiod [AddGroup α] [InvolutiveNeg β] (h1 : Periodic f c₁)
    (h2 : Antiperiodic f c₂) : Antiperiodic f (c₁ - c₂)

Proof state:
α : Type u_1
β : Type u_2
f : α → β
c₁ c₂ : α
inst✝¹ : AddGroup α
inst✝ : InvolutiveNeg β
h1 : Periodic f c₁
h2 : Antiperiodic f c₂
⊢ Antiperiodic f (c₁ - c₂)

Tactic:
simpa only [sub_eq_add_neg] using h1.add_antiperiod h2.neg

Result:
no goals
-- Mathlib/SetTheory/Ordinal/Basic.lean
theorem enum_le_enum' (a : Ordinal) {o₁ o₂ : Iio (type (· < ·))} :
    enum (· < ·) o₁ ≤ enum (α := a.toType) (· < ·) o₂ ↔ o₁ ≤ o₂

Proof state:
a : Ordinal.{u_1}
o₁ o₂ : ↑(Iio (type fun x1 x2 => x1 < x2))
⊢ (enum fun x1 x2 => x1 < x2) o₁ ≤ (enum fun x1 x2 => x1 < x2) o₂ ↔ o₁ ≤ o₂

Tactic:
rw [← enum_le_enum, not_lt]

Result:
no goals
-- Mathlib/MeasureTheory/Function/SimpleFuncDenseLp.lean
theorem zero_toSimpleFunc : toSimpleFunc (0 : Lp.simpleFunc E p μ) =ᵐ[μ] 0

Proof state:
α : Type u_1
E : Type u_4
inst✝¹ : MeasurableSpace α
inst✝ : NormedAddCommGroup E
p : ℝ≥0∞
μ : Measure α
⊢ ⇑(toSimpleFunc 0) =ᶠ[ae μ] 0

Tactic:
filter_upwards [toSimpleFunc_eq_toFun (0 : Lp.simpleFunc E p μ),
  Lp.coeFn_zero E 1 μ] with _ h₁ _

Result:
case h
α : Type u_1
E : Type u_4
inst✝¹ : MeasurableSpace α
inst✝ : NormedAddCommGroup E
p : ℝ≥0∞
μ : Measure α
a✝¹ : α
h₁ : (toSimpleFunc 0) a✝¹ = ↑↑↑0 a✝¹
a✝ : ↑↑0 a✝¹ = 0 a✝¹
⊢ (toSimpleFunc 0) a✝¹ = 0 a✝¹

Proof state:
case h
α : Type u_1
E : Type u_4
inst✝¹ : MeasurableSpace α
inst✝ : NormedAddCommGroup E
p : ℝ≥0∞
μ : Measure α
a✝¹ : α
h₁ : (toSimpleFunc 0) a✝¹ = ↑↑↑0 a✝¹
a✝ : ↑↑0 a✝¹ = 0 a✝¹
⊢ (toSimpleFunc 0) a✝¹ = 0 a✝¹

Tactic:
rwa [h₁]

Result:
no goals
-- Mathlib/Order/Interval/Set/Basic.lean
theorem left_mem_Ici : a ∈ Ici a

Proof state:
α : Type u_1
inst✝ : Preorder α
a : α
⊢ a ∈ Ici a

Tactic:
simp

Result:
no goals
-- Mathlib/Data/Fintype/Pi.lean
lemma piFinset_image [∀ a, DecidableEq (δ a)] (f : ∀ a, γ a → δ a) (s : ∀ a, Finset (γ a)) :
    piFinset (fun a ↦ (s a).image (f a)) = (piFinset s).image fun b a ↦ f _ (b a)

Proof state:
case h
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Fintype α
γ : α → Type u_3
δ : α → Type u_4
inst✝ : (a : α) → DecidableEq (δ a)
f : (a : α) → γ a → δ a
s : (a : α) → Finset (γ a)
a✝ : (a : α) → δ a
⊢ (a✝ ∈ piFinset fun a => image (f a) (s a)) ↔ a✝ ∈ image (fun b a => f a (b a)) (piFinset s)

Tactic:
simp only [mem_piFinset, mem_image, Classical.skolem, forall_and, funext_iff]

Result:
no goals

Proof state:
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Fintype α
γ : α → Type u_3
δ : α → Type u_4
inst✝ : (a : α) → DecidableEq (δ a)
f : (a : α) → γ a → δ a
s : (a : α) → Finset (γ a)
⊢ (piFinset fun a => image (f a) (s a)) = image (fun b a => f a (b a)) (piFinset s)

Tactic:
ext

Result:
case h
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Fintype α
γ : α → Type u_3
δ : α → Type u_4
inst✝ : (a : α) → DecidableEq (δ a)
f : (a : α) → γ a → δ a
s : (a : α) → Finset (γ a)
a✝ : (a : α) → δ a
⊢ (a✝ ∈ piFinset fun a => image (f a) (s a)) ↔ a✝ ∈ image (fun b a => f a (b a)) (piFinset s)
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Lemmas.lean
theorem forall_mem_singleton {p : α → Prop} {a : α} : (∀ (x) (_ : x ∈ #v[a]), p x) ↔ p a

Proof state:
α : Type u_1
p : α → Prop
a : α
⊢ (∀ (x : α), x ∈ { toArray := #[a], size_toArray := ⋯ } → p x) ↔ p a

Tactic:
simp only [mem_singleton, forall_eq]

Result:
no goals
-- Mathlib/Order/Interval/Set/Image.lean
lemma MonotoneOn.mapsTo_Ici (h : MonotoneOn f (Ici a)) : MapsTo f (Ici a) (Ici (f a)) :=
  fun _ _ ↦ by aesop

Proof state:
α : Type u_1
β : Type u_2
f : α → β
inst✝¹ : Preorder α
inst✝ : Preorder β
a : α
h : MonotoneOn f (Ici a)
x✝¹ : α
x✝ : x✝¹ ∈ Ici a
⊢ f x✝¹ ∈ Ici (f a)

Tactic:
aesop

Result:
no goals
-- Mathlib/RingTheory/AdicCompletion/Functoriality.lean
theorem map_comp_apply (f : M →ₗ[R] N) (g : N →ₗ[R] P) (x : AdicCompletion I M) :
    map I g (map I f x) = map I (g ∘ₗ f) x

Proof state:
R : Type u_1
inst✝⁶ : CommRing R
I : Ideal R
M : Type u_2
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
N : Type u_3
inst✝³ : AddCommGroup N
inst✝² : Module R N
P : Type u_4
inst✝¹ : AddCommGroup P
inst✝ : Module R P
f : M →ₗ[R] N
g : N →ₗ[R] P
x : AdicCompletion I M
⊢ (map I g) ((map I f) x) = (map I (g ∘ₗ f)) x

Tactic:
show (map I g ∘ₗ map I f) x = map I (g ∘ₗ f) x

Result:
R : Type u_1
inst✝⁶ : CommRing R
I : Ideal R
M : Type u_2
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
N : Type u_3
inst✝³ : AddCommGroup N
inst✝² : Module R N
P : Type u_4
inst✝¹ : AddCommGroup P
inst✝ : Module R P
f : M →ₗ[R] N
g : N →ₗ[R] P
x : AdicCompletion I M
⊢ (map I g ∘ₗ map I f) x = (map I (g ∘ₗ f)) x

Proof state:
R : Type u_1
inst✝⁶ : CommRing R
I : Ideal R
M : Type u_2
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
N : Type u_3
inst✝³ : AddCommGroup N
inst✝² : Module R N
P : Type u_4
inst✝¹ : AddCommGroup P
inst✝ : Module R P
f : M →ₗ[R] N
g : N →ₗ[R] P
x : AdicCompletion I M
⊢ (map I g ∘ₗ map I f) x = (map I (g ∘ₗ f)) x

Tactic:
rw [map_comp]

Result:
no goals
-- Mathlib/Algebra/Polynomial/Degree/Lemmas.lean
theorem coeff_sub_eq_neg_right_of_lt (df : p.natDegree < n) : (p - q).coeff n = -q.coeff n

Proof state:
R : Type u
n : ℕ
inst✝ : Ring R
p q : R[X]
df : p.natDegree < n
⊢ (p - q).coeff n = -q.coeff n

Tactic:
rwa [sub_eq_add_neg, coeff_add_eq_right_of_lt, coeff_neg]

Result:
no goals
-- Mathlib/Data/Ordmap/Ordset.lean
theorem size_dual (t : Ordnode α) : size (dual t) = size t

Proof state:
α : Type u_1
t : Ordnode α
⊢ t.dual.size = t.size

Tactic:
cases t <;> rfl

Result:
no goals
-- Mathlib/Algebra/Order/GroupWithZero/Unbundled.lean
@[simp] lemma one_lt_zpow_iff_right_of_lt_one₀ (ha₀ : 0 < a) (ha₁ : a < 1) : 1 < a ^ n ↔ n < 0

Proof state:
G₀ : Type u_2
inst✝⁴ : GroupWithZero G₀
inst✝³ : PartialOrder G₀
inst✝² : ZeroLEOneClass G₀
inst✝¹ : PosMulReflectLT G₀
a : G₀
inst✝ : PosMulStrictMono G₀
n : ℤ
ha₀ : 0 < a
ha₁ : a < 1
⊢ 1 < a ^ n ↔ n < 0

Tactic:
simp [← zpow_lt_zpow_iff_right_of_lt_one₀ ha₀ ha₁]

Result:
no goals
-- Mathlib/Algebra/Order/Group/Unbundled/Basic.lean
theorem Right.one_lt_inv_iff : 1 < a⁻¹ ↔ a < 1

Proof state:
α : Type u
inst✝² : Group α
inst✝¹ : LT α
inst✝ : MulRightStrictMono α
a : α
⊢ 1 < a⁻¹ ↔ a < 1

Tactic:
rw [← mul_lt_mul_iff_right a, inv_mul_cancel, one_mul]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Find.lean
theorem find?_flatMap (xs : List α) (f : α → List β) (p : β → Bool) :
    (xs.flatMap f).find? p = xs.findSome? (fun x => (f x).find? p)

Proof state:
α : Type u_1
β : Type u_2
xs : List α
f : α → List β
p : β → Bool
⊢ findSome? ((fun x => find? p x) ∘ f) xs = findSome? (fun x => find? p (f x)) xs

Tactic:
rfl

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
xs : List α
f : α → List β
p : β → Bool
⊢ find? p (flatMap f xs) = findSome? (fun x => find? p (f x)) xs

Tactic:
simp [flatMap_def, findSome?_map]

Result:
α : Type u_1
β : Type u_2
xs : List α
f : α → List β
p : β → Bool
⊢ findSome? ((fun x => find? p x) ∘ f) xs = findSome? (fun x => find? p (f x)) xs
-- Mathlib/FieldTheory/SeparableClosure.lean
theorem le_separableClosure' {L : IntermediateField F E} (hs : ∀ x : L, IsSeparable F x) :
    L ≤ separableClosure F E := fun x h ↦ by simpa only [IsSeparable, minpoly_eq] using hs ⟨x, h⟩

Proof state:
F : Type u
E : Type v
inst✝² : Field F
inst✝¹ : Field E
inst✝ : Algebra F E
L : IntermediateField F E
hs : ∀ (x : ↥L), IsSeparable F x
x : E
h : x ∈ L
⊢ x ∈ separableClosure F E

Tactic:
simpa only [IsSeparable, minpoly_eq] using hs ⟨x, h⟩

Result:
no goals
-- Mathlib/Analysis/InnerProductSpace/TwoDim.lean
theorem kahler_ne_zero {x y : E} (hx : x ≠ 0) (hy : y ≠ 0) : o.kahler x y ≠ 0

Proof state:
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
x y : E
hx : x ≠ 0
hy : y ≠ 0
⊢ (o.kahler x) y ≠ 0

Tactic:
apply mt o.eq_zero_or_eq_zero_of_kahler_eq_zero

Result:
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
x y : E
hx : x ≠ 0
hy : y ≠ 0
⊢ ¬(x = 0 ∨ y = 0)

Proof state:
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
x y : E
hx : x ≠ 0
hy : y ≠ 0
⊢ ¬(x = 0 ∨ y = 0)

Tactic:
tauto

Result:
no goals
-- Mathlib/Topology/Inseparable.lean
theorem comap_mk_nhdsSet : comap mk (𝓝ˢ t) = 𝓝ˢ (mk ⁻¹' t)

Proof state:
X : Type u_1
inst✝ : TopologicalSpace X
t : Set (SeparationQuotient X)
⊢ comap mk (𝓝ˢ t) = 𝓝ˢ (mk ⁻¹' t)

Tactic:
conv_lhs => rw [← image_preimage_eq t surjective_mk, comap_mk_nhdsSet_image]

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Basic.lean
@[simp] lemma deleteEdges_univ : G.deleteEdges Set.univ = ⊥

Proof state:
V : Type u
G : SimpleGraph V
⊢ G.deleteEdges Set.univ = ⊥

Tactic:
simp [deleteEdges]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/RawLemmas.lean
theorem get?_of_isEmpty [LawfulBEq α] (h : m.1.WF) {a : α} :
    m.1.isEmpty = true → m.get? a = none

Proof state:
α : Type u
β : α → Type v
m : Raw₀ α β
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : LawfulBEq α
h : m.val.WF
a : α
⊢ m.val.isEmpty = true → m.get? a = none

Tactic:
simp_to_model

Result:
α : Type u
β : α → Type v
m : Raw₀ α β
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : LawfulBEq α
h : m.val.WF
a : α
⊢ (toListModel m.val.buckets).isEmpty = true → getValueCast? a (toListModel m.val.buckets) = none

Proof state:
α : Type u
β : α → Type v
m : Raw₀ α β
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : LawfulBEq α
h : m.val.WF
a : α
⊢ (toListModel m.val.buckets).isEmpty = true → getValueCast? a (toListModel m.val.buckets) = none

Tactic:
empty

Result:
no goals
-- Mathlib/Analysis/Normed/Lp/PiLp.lean
theorem edist_equiv_symm_single_same (i : ι) (b₁ b₂ : β i) :
    edist
        ((WithLp.equiv p (∀ i, β i)).symm (Pi.single i b₁))
        ((WithLp.equiv p (∀ i, β i)).symm (Pi.single i b₂)) =
      edist b₁ b₂

Proof state:
p : ℝ≥0∞
ι : Type u_2
β : ι → Type u_4
hp : Fact (1 ≤ p)
inst✝² : Fintype ι
inst✝¹ : (i : ι) → SeminormedAddCommGroup (β i)
inst✝ : DecidableEq ι
i : ι
b₁ b₂ : β i
⊢ edist ((WithLp.equiv p ((i : ι) → β i)).symm (Pi.single i b₁))
      ((WithLp.equiv p ((i : ι) → β i)).symm (Pi.single i b₂)) =
    edist b₁ b₂

Tactic:
simp only [edist_nndist, nndist_equiv_symm_single_same p β i b₁ b₂]

Result:
no goals
-- Mathlib/Algebra/DirectSum/Basic.lean
theorem fromAddMonoid_of_apply (i : ι) (f : γ →+ β i) (x : γ) :
    fromAddMonoid (of _ i f) x = of _ i (f x)

Proof state:
ι : Type v
β : ι → Type w
inst✝² : (i : ι) → AddCommMonoid (β i)
inst✝¹ : DecidableEq ι
γ : Type u₁
inst✝ : AddCommMonoid γ
i : ι
f : γ →+ β i
x : γ
⊢ (fromAddMonoid ((of (fun i => γ →+ β i) i) f)) x = (of β i) (f x)

Tactic:
rw [fromAddMonoid_of, AddMonoidHom.coe_comp, Function.comp]

Result:
no goals
-- Mathlib/Analysis/Convex/Join.lean
theorem convexJoin_empty_left (t : Set E) : convexJoin 𝕜 ∅ t = ∅

Proof state:
𝕜 : Type u_2
E : Type u_3
inst✝² : OrderedSemiring 𝕜
inst✝¹ : AddCommMonoid E
inst✝ : Module 𝕜 E
t : Set E
⊢ convexJoin 𝕜 ∅ t = ∅

Tactic:
simp [convexJoin]

Result:
no goals
-- Mathlib/Combinatorics/Additive/AP/Three/Behrend.lean
theorem lower_bound_le_one' (hN : 2 ≤ N) (hN' : N ≤ 4096) :
    (N : ℝ) * exp (-4 * √(log N)) ≤ 1

Proof state:
N : ℕ
hN : 2 ≤ N
hN' : N ≤ 4096
⊢ ↑N ≤ rexp (4 ^ 2)

Tactic:
norm_num1

Result:
N : ℕ
hN : 2 ≤ N
hN' : N ≤ 4096
⊢ ↑N ≤ rexp 16

Proof state:
N : ℕ
hN : 2 ≤ N
hN' : N ≤ 4096
⊢ ↑N ≤ 4096

Tactic:
exact mod_cast hN'

Result:
no goals

Proof state:
N : ℕ
hN : 2 ≤ N
hN' : N ≤ 4096
⊢ ↑N ≤ rexp 16

Tactic:
apply le_trans _ four_zero_nine_six_lt_exp_sixteen.le

Result:
N : ℕ
hN : 2 ≤ N
hN' : N ≤ 4096
⊢ ↑N ≤ 4096

Proof state:
N : ℕ
hN : 2 ≤ N
hN' : N ≤ 4096
⊢ ↑N * rexp (-4 * √(log ↑N)) ≤ 1

Tactic:
rw [← log_le_log_iff (mul_pos (cast_pos.2 (zero_lt_two.trans_le hN)) (exp_pos _)) zero_lt_one,
  log_one, log_mul (cast_pos.2 (zero_lt_two.trans_le hN)).ne' (exp_pos _).ne', log_exp, neg_mul, ←
  sub_eq_add_neg, sub_nonpos, ←
  div_le_iff₀ (Real.sqrt_pos.2 <| log_pos <| one_lt_cast.2 <| one_lt_two.trans_le hN), div_sqrt,
  sqrt_le_left zero_le_four, log_le_iff_le_exp (cast_pos.2 (zero_lt_two.trans_le hN))]

Result:
N : ℕ
hN : 2 ≤ N
hN' : N ≤ 4096
⊢ ↑N ≤ rexp (4 ^ 2)
-- Mathlib/Analysis/Normed/Group/Basic.lean
@[to_additive (attr := simp) norm_pos_iff]
lemma norm_pos_iff' : 0 < ‖a‖ ↔ a ≠ 1

Proof state:
E : Type u_5
inst✝ : NormedGroup E
a : E
⊢ 0 < ‖a‖ ↔ a ≠ 1

Tactic:
rw [← not_le, norm_le_zero_iff']

Result:
no goals
-- Mathlib/Data/Set/Subset.lean
lemma preimage_val_eq_univ_of_subset (h : A ⊆ B) : A ↓∩ B = univ

Proof state:
α : Type u_2
A B : Set α
h : A ⊆ B
⊢ ∀ (a : α) (b : a ∈ A), ⟨a, b⟩ ∈ A ↓∩ B

Tactic:
exact h

Result:
no goals

Proof state:
α : Type u_2
A B : Set α
h : A ⊆ B
⊢ A ↓∩ B = univ

Tactic:
rw [eq_univ_iff_forall, Subtype.forall]

Result:
α : Type u_2
A B : Set α
h : A ⊆ B
⊢ ∀ (a : α) (b : a ∈ A), ⟨a, b⟩ ∈ A ↓∩ B
-- Mathlib/Probability/Kernel/Composition/MapComap.lean
theorem sum_comap_seq (κ : Kernel α β) [IsSFiniteKernel κ] (hg : Measurable g) :
    (Kernel.sum fun n => comap (seq κ n) g hg) = comap κ g hg

Proof state:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
γ : Type u_4
mγ : MeasurableSpace γ
g : γ → α
κ : Kernel α β
inst✝ : IsSFiniteKernel κ
hg : Measurable g
⊢ (Kernel.sum fun n => (κ.seq n).comap g hg) = κ.comap g hg

Tactic:
ext a s hs

Result:
case h.h
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
γ : Type u_4
mγ : MeasurableSpace γ
g : γ → α
κ : Kernel α β
inst✝ : IsSFiniteKernel κ
hg : Measurable g
a : γ
s : Set β
hs : MeasurableSet s
⊢ ((Kernel.sum fun n => (κ.seq n).comap g hg) a) s = ((κ.comap g hg) a) s

Proof state:
case h.h
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
γ : Type u_4
mγ : MeasurableSpace γ
g : γ → α
κ : Kernel α β
inst✝ : IsSFiniteKernel κ
hg : Measurable g
a : γ
s : Set β
hs : MeasurableSet s
⊢ ∑' (i : ℕ), (((κ.seq i).comap g hg) a) s = ∑' (i : ℕ), ((κ.seq i) (g a)) s

Tactic:
simp_rw [comap_apply' _ hg _ s]

Result:
no goals

Proof state:
case h.h
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
γ : Type u_4
mγ : MeasurableSpace γ
g : γ → α
κ : Kernel α β
inst✝ : IsSFiniteKernel κ
hg : Measurable g
a : γ
s : Set β
hs : MeasurableSet s
⊢ ((Kernel.sum fun n => (κ.seq n).comap g hg) a) s = ((κ.comap g hg) a) s

Tactic:
rw [Kernel.sum_apply, comap_apply' κ hg a s, Measure.sum_apply _ hs, ← measure_sum_seq κ,
  Measure.sum_apply _ hs]

Result:
case h.h
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
γ : Type u_4
mγ : MeasurableSpace γ
g : γ → α
κ : Kernel α β
inst✝ : IsSFiniteKernel κ
hg : Measurable g
a : γ
s : Set β
hs : MeasurableSet s
⊢ ∑' (i : ℕ), (((κ.seq i).comap g hg) a) s = ∑' (i : ℕ), ((κ.seq i) (g a)) s
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Find.lean
theorem find?_mkArray :
    find? p (mkArray n a) = if n = 0 then none else if p a then some a else none

Proof state:
α✝ : Type u_1
p : α✝ → Bool
n : Nat
a : α✝
⊢ find? p (mkArray n a) = if n = 0 then none else if p a = true then some a else none

Tactic:
simp [← List.toArray_replicate, List.find?_replicate]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Lemmas.lean
theorem findRev?_toArray (p : α → Bool) (v : Vector α n) :
    v.toArray.findRev? p = v.findRev? p

Proof state:
α : Type
n : Nat
p : α → Bool
v : Vector α n
⊢ Array.findRev? p v.toArray = findRev? p v

Tactic:
cases v

Result:
case mk
α : Type
n : Nat
p : α → Bool
toArray✝ : Array α
size_toArray✝ : toArray✝.size = n
⊢ Array.findRev? p { toArray := toArray✝, size_toArray := size_toArray✝ }.toArray =
    findRev? p { toArray := toArray✝, size_toArray := size_toArray✝ }

Proof state:
case mk
α : Type
n : Nat
p : α → Bool
toArray✝ : Array α
size_toArray✝ : toArray✝.size = n
⊢ Array.findRev? p { toArray := toArray✝, size_toArray := size_toArray✝ }.toArray =
    findRev? p { toArray := toArray✝, size_toArray := size_toArray✝ }

Tactic:
simp

Result:
no goals
-- Mathlib/Topology/Algebra/Group/Basic.lean
theorem Topology.IsInducing.continuousInv {G H : Type*} [Inv G] [Inv H] [TopologicalSpace G]
    [TopologicalSpace H] [ContinuousInv H] {f : G → H} (hf : IsInducing f)
    (hf_inv : ∀ x, f x⁻¹ = (f x)⁻¹) : ContinuousInv G :=
  ⟨hf.continuous_iff.2 <| by simpa only [Function.comp_def, hf_inv] using hf.continuous.inv⟩

Proof state:
G : Type u_1
H : Type u_2
inst✝⁴ : Inv G
inst✝³ : Inv H
inst✝² : TopologicalSpace G
inst✝¹ : TopologicalSpace H
inst✝ : ContinuousInv H
f : G → H
hf : IsInducing f
hf_inv : ∀ (x : G), f x⁻¹ = (f x)⁻¹
⊢ Continuous (f ∘ fun a => a⁻¹)

Tactic:
simpa only [Function.comp_def, hf_inv] using hf.continuous.inv

Result:
no goals
-- Mathlib/GroupTheory/MonoidLocalization/Basic.lean
theorem mk'_eq_iff_eq {x₁ x₂} {y₁ y₂ : S} :
    f.mk' x₁ y₁ = f.mk' x₂ y₂ ↔ f.toMap (y₂ * x₁) = f.toMap (y₁ * x₂) :=
  ⟨fun H ↦ by
    rw [f.toMap.map_mul, f.toMap.map_mul, f.mk'_eq_iff_eq_mul.1 H,← mul_assoc, mk'_spec',
      mul_comm ((toMap f) x₂) _],
    fun H ↦ by
    rw [mk'_eq_iff_eq_mul, mk', mul_assoc, mul_comm _ (f.toMap y₁), ← mul_assoc, ←
      f.toMap.map_mul, mul_comm x₂, ← H, ← mul_comm x₁, f.toMap.map_mul,
      mul_inv_right f.map_units]⟩

Proof state:
M : Type u_1
inst✝¹ : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝ : CommMonoid N
f : S.LocalizationMap N
x₁ x₂ : M
y₁ y₂ : ↥S
H : f.mk' x₁ y₁ = f.mk' x₂ y₂
⊢ f.toMap (↑y₂ * x₁) = f.toMap (↑y₁ * x₂)

Tactic:
rw [f.toMap.map_mul, f.toMap.map_mul, f.mk'_eq_iff_eq_mul.1 H,← mul_assoc, mk'_spec',
  mul_comm ((toMap f) x₂) _]

Result:
no goals

Proof state:
M : Type u_1
inst✝¹ : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝ : CommMonoid N
f : S.LocalizationMap N
x₁ x₂ : M
y₁ y₂ : ↥S
H : f.toMap (↑y₂ * x₁) = f.toMap (↑y₁ * x₂)
⊢ f.mk' x₁ y₁ = f.mk' x₂ y₂

Tactic:
rw [mk'_eq_iff_eq_mul, mk', mul_assoc, mul_comm _ (f.toMap y₁), ← mul_assoc, ←
  f.toMap.map_mul, mul_comm x₂, ← H, ← mul_comm x₁, f.toMap.map_mul,
  mul_inv_right f.map_units]

Result:
no goals
-- Mathlib/Data/Finsupp/Order.lean
theorem support_inf_union_support_sup : (f ⊓ g).support ∪ (f ⊔ g).support = f.support ∪ g.support :=
  coe_injective <| compl_injective <| by ext; simp [inf_eq_and_sup_eq_iff]

Proof state:
case h
ι : Type u_1
α : Type u_3
inst✝² : Zero α
inst✝¹ : DecidableEq ι
inst✝ : Lattice α
f g : ι →₀ α
x✝ : ι
⊢ x✝ ∈ (↑((f ⊓ g).support ∪ (f ⊔ g).support))ᶜ ↔ x✝ ∈ (↑(f.support ∪ g.support))ᶜ

Tactic:
simp [inf_eq_and_sup_eq_iff]

Result:
no goals

Proof state:
ι : Type u_1
α : Type u_3
inst✝² : Zero α
inst✝¹ : DecidableEq ι
inst✝ : Lattice α
f g : ι →₀ α
⊢ (↑((f ⊓ g).support ∪ (f ⊔ g).support))ᶜ = (↑(f.support ∪ g.support))ᶜ

Tactic:
ext

Result:
case h
ι : Type u_1
α : Type u_3
inst✝² : Zero α
inst✝¹ : DecidableEq ι
inst✝ : Lattice α
f g : ι →₀ α
x✝ : ι
⊢ x✝ ∈ (↑((f ⊓ g).support ∪ (f ⊔ g).support))ᶜ ↔ x✝ ∈ (↑(f.support ∪ g.support))ᶜ