harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Topology/Algebra/Support.lean
@[to_additive]
lemma isCompact_preimage [TopologicalSpace β]
    (h'f : HasCompactMulSupport f) (hf : Continuous f) {k : Set β} (hk : IsClosed k)
    (h'k : 1 ∉ k) : IsCompact (f ⁻¹' k)

Proof state:
α : Type u_2
β : Type u_4
inst✝² : TopologicalSpace α
inst✝¹ : One β
f : α → β
inst✝ : TopologicalSpace β
h'f : HasCompactMulSupport f
hf : Continuous f
k : Set β
hk : IsClosed k
h'k : 1 ∉ k
⊢ IsCompact (f ⁻¹' k)

Tactic:
apply IsCompact.of_isClosed_subset h'f (hk.preimage hf) (fun x hx ↦ ?_)

Result:
α : Type u_2
β : Type u_4
inst✝² : TopologicalSpace α
inst✝¹ : One β
f : α → β
inst✝ : TopologicalSpace β
h'f : HasCompactMulSupport f
hf : Continuous f
k : Set β
hk : IsClosed k
h'k : 1 ∉ k
x : α
hx : x ∈ f ⁻¹' k
⊢ x ∈ mulTSupport f

Proof state:
case a
α : Type u_2
β : Type u_4
inst✝² : TopologicalSpace α
inst✝¹ : One β
f : α → β
inst✝ : TopologicalSpace β
h'f : HasCompactMulSupport f
hf : Continuous f
k : Set β
hk : IsClosed k
h'k : 1 ∉ k
x : α
hx : x ∈ f ⁻¹' k
⊢ x ∈ mulSupport f

Tactic:
aesop

Result:
no goals

Proof state:
α : Type u_2
β : Type u_4
inst✝² : TopologicalSpace α
inst✝¹ : One β
f : α → β
inst✝ : TopologicalSpace β
h'f : HasCompactMulSupport f
hf : Continuous f
k : Set β
hk : IsClosed k
h'k : 1 ∉ k
x : α
hx : x ∈ f ⁻¹' k
⊢ x ∈ mulTSupport f

Tactic:
apply subset_mulTSupport

Result:
case a
α : Type u_2
β : Type u_4
inst✝² : TopologicalSpace α
inst✝¹ : One β
f : α → β
inst✝ : TopologicalSpace β
h'f : HasCompactMulSupport f
hf : Continuous f
k : Set β
hk : IsClosed k
h'k : 1 ∉ k
x : α
hx : x ∈ f ⁻¹' k
⊢ x ∈ mulSupport f
-- Mathlib/AlgebraicTopology/AlternatingFaceMapComplex.lean
theorem d_squared (n : ℕ) : objD X n ≫ objD X (n + 1) = 0

Proof state:
C : Type u_1
inst✝¹ : Category.{u_3, u_1} C
inst✝ : Preadditive C
X : CosimplicialObject C
n : ℕ
⊢ objD X n ≫ objD X (n + 1) = 0

Tactic:
simp only [d_eq_unop_d, ← unop_comp, AlternatingFaceMapComplex.d_squared, unop_zero]

Result:
no goals
-- Mathlib/CategoryTheory/Shift/SingleFunctors.lean
@[reassoc (attr := simp)]
lemma inv_hom_id_hom (e : F ≅ G) (n : A) : e.inv.hom n ≫ e.hom.hom n = 𝟙 _

Proof state:
C : Type u_1
D : Type u_2
inst✝³ : Category.{u_7, u_1} C
inst✝² : Category.{u_6, u_2} D
A : Type u_5
inst✝¹ : AddMonoid A
inst✝ : HasShift D A
F G : SingleFunctors C D A
e : F ≅ G
n : A
⊢ e.inv.hom n ≫ e.hom.hom n = 𝟙 (G.functor n)

Tactic:
rw [← comp_hom, e.inv_hom_id, id_hom]

Result:
no goals
-- Mathlib/LinearAlgebra/ExteriorPower/Pairing.lean
theorem alternatingMapToDual_apply_ιMulti {n : ℕ}
    (f : (_ : Fin n) → Module.Dual R M) (v : Fin n → M) :
    alternatingMapToDual R M n f (ιMulti _ _ v) =
      Matrix.det (n := Fin n) (.of (fun i j ↦ f j (v i)))

Proof state:
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
n : ℕ
f : Fin n → Module.Dual R M
v : Fin n → M
⊢ ((alternatingMapToDual R M n) f) ((ιMulti R n) v) = (Matrix.of fun i j => (f j) (v i)).det

Tactic:
simp [alternatingMapToDual, Matrix.det_apply]

Result:
no goals
-- Mathlib/Data/Fintype/Prod.lean
theorem toFinset_off_diag {s : Set α} [DecidableEq α] [Fintype s] [Fintype s.offDiag] :
    s.offDiag.toFinset = s.toFinset.offDiag :=
  Finset.ext <| by simp

Proof state:
α : Type u_1
s : Set α
inst✝² : DecidableEq α
inst✝¹ : Fintype ↑s
inst✝ : Fintype ↑s.offDiag
⊢ ∀ (a : α × α), a ∈ s.offDiag.toFinset ↔ a ∈ s.toFinset.offDiag

Tactic:
simp

Result:
no goals
-- Mathlib/CategoryTheory/Limits/Shapes/Pullback/HasPullback.lean
theorem map_lift_pullbackComparison (f : X ⟶ Z) (g : Y ⟶ Z) [HasPullback f g]
    [HasPullback (G.map f) (G.map g)] {W : C} {h : W ⟶ X} {k : W ⟶ Y} (w : h ≫ f = k ≫ g) :
    G.map (pullback.lift _ _ w) ≫ pullbackComparison G f g =
      pullback.lift (G.map h) (G.map k) (by simp only [← G.map_comp, w])

Proof state:
C : Type u
inst✝³ : Category.{v, u} C
X Y Z : C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
G : C ⥤ D
f : X ⟶ Z
g : Y ⟶ Z
inst✝¹ : HasPullback f g
inst✝ : HasPullback (G.map f) (G.map g)
W : C
h : W ⟶ X
k : W ⟶ Y
w : h ≫ f = k ≫ g
⊢ G.map (pullback.lift h k w) ≫ pullbackComparison G f g = pullback.lift (G.map h) (G.map k) ⋯

Tactic:
ext <;> simp [← G.map_comp]

Result:
no goals

Proof state:
C : Type u
inst✝³ : Category.{v, u} C
W✝ X Y Z : C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
G : C ⥤ D
f : X ⟶ Z
g : Y ⟶ Z
inst✝¹ : HasPullback f g
inst✝ : HasPullback (G.map f) (G.map g)
W : C
h : W ⟶ X
k : W ⟶ Y
w : h ≫ f = k ≫ g
⊢ G.map h ≫ G.map f = G.map k ≫ G.map g

Tactic:
simp only [← G.map_comp, w]

Result:
no goals
-- Mathlib/Combinatorics/SetFamily/AhlswedeZhang.lean
@[simp] lemma truncatedInf_empty (a : α) : truncatedInf ∅ a = ⊥ := truncatedInf_of_not_mem (by simp)

Proof state:
α : Type u_1
inst✝² : SemilatticeInf α
inst✝¹ : DecidableRel fun x1 x2 => x1 ≤ x2
inst✝ : BoundedOrder α
a : α
⊢ a ∉ upperClosure ↑∅

Tactic:
simp

Result:
no goals
-- Mathlib/Probability/ProbabilityMassFunction/Basic.lean
theorem toMeasure_mono {s t : Set α} (hs : MeasurableSet s) (ht : MeasurableSet t)
    (h : s ∩ p.support ⊆ t) : p.toMeasure s ≤ p.toMeasure t

Proof state:
α : Type u_1
inst✝ : MeasurableSpace α
p : PMF α
s t : Set α
hs : MeasurableSet s
ht : MeasurableSet t
h : s ∩ p.support ⊆ t
⊢ p.toMeasure s ≤ p.toMeasure t

Tactic:
simpa only [p.toMeasure_apply_eq_toOuterMeasure_apply, hs, ht] using toOuterMeasure_mono p h

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Nat/Bitwise/Lemmas.lean
theorem testBit_or (x y i : Nat) : (x ||| y).testBit i = (x.testBit i || y.testBit i)

Proof state:
x y i : Nat
⊢ (x ||| y).testBit i = (x.testBit i || y.testBit i)

Tactic:
simp [HOr.hOr, OrOp.or, lor, testBit_bitwise ]

Result:
no goals
-- Mathlib/Logic/Equiv/Fintype.lean
theorem extendSubtype_not_mem (e : { x // p x } ≃ { x // q x }) (x) (hx : ¬p x) :
    ¬q (e.extendSubtype x)

Proof state:
case h.e'_1.h.e'_1
α : Type u_1
inst✝² : Finite α
p q : α → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
e : { x // p x } ≃ { x // q x }
x : α
hx : ¬p x
⊢ e.extendSubtype x = ↑(e.toCompl ⟨x, hx⟩)

Tactic:
rw [e.extendSubtype_apply_of_not_mem _ hx]

Result:
no goals

Proof state:
α : Type u_1
inst✝² : Finite α
p q : α → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
e : { x // p x } ≃ { x // q x }
x : α
hx : ¬p x
⊢ ¬q (e.extendSubtype x)

Tactic:
convert (e.toCompl ⟨x, hx⟩).2

Result:
case h.e'_1.h.e'_1
α : Type u_1
inst✝² : Finite α
p q : α → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
e : { x // p x } ≃ { x // q x }
x : α
hx : ¬p x
⊢ e.extendSubtype x = ↑(e.toCompl ⟨x, hx⟩)
-- Mathlib/Data/Num/Lemmas.lean
theorem dvd_to_nat (m n : Num) : (m : ℕ) ∣ n ↔ m ∣ n :=
  ⟨fun ⟨k, e⟩ => ⟨k, by rw [← of_to_nat n, e]; simp⟩, fun ⟨k, e⟩ => ⟨k, by simp [e, mul_to_nat]⟩⟩

Proof state:
m n : Num
x✝ : ↑m ∣ ↑n
k : ℕ
e : ↑n = ↑m * k
⊢ n = m * ↑k

Tactic:
rw [← of_to_nat n, e]

Result:
m n : Num
x✝ : ↑m ∣ ↑n
k : ℕ
e : ↑n = ↑m * k
⊢ ↑(↑m * k) = m * ↑k

Proof state:
m n : Num
x✝ : m ∣ n
k : Num
e : n = m * k
⊢ ↑n = ↑m * ↑k

Tactic:
simp [e, mul_to_nat]

Result:
no goals

Proof state:
m n : Num
x✝ : ↑m ∣ ↑n
k : ℕ
e : ↑n = ↑m * k
⊢ ↑(↑m * k) = m * ↑k

Tactic:
simp

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/RawLemmas.lean
theorem getKey_insertMany_list_of_contains_eq_false [EquivBEq α] [LawfulHashable α] (h : m.1.WF)
    {l : List (α × β)} {k : α}
    (h₁ : (l.map Prod.fst).contains k = false)
    {h'} :
    (insertMany m l).1.getKey k h' =
    m.getKey k (contains_of_contains_insertMany_list _ h h' h₁)

Proof state:
α : Type u
inst✝³ : BEq α
inst✝² : Hashable α
β : Type v
m : Raw₀ α fun x => β
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
h : m.val.WF
l : List (α × β)
k : α
h₁ : (List.map Prod.fst l).contains k = false
h' : (insertMany m l).val.contains k = true
⊢ (insertMany m l).val.getKey k h' = m.getKey k ⋯

Tactic:
simp_to_model [Const.insertMany] using List.getKey_insertListConst_of_contains_eq_false

Result:
no goals
-- Mathlib/RingTheory/MvPolynomial/Symmetric/Defs.lean
theorem hsymm_one : hsymm σ R 1 = ∑ i, X i

Proof state:
case h
σ : Type u_5
R : Type u_6
inst✝² : CommSemiring R
inst✝¹ : Fintype σ
inst✝ : DecidableEq σ
⊢ ∀ (x : σ), X x = (Multiset.map X ↑(oneEquiv x)).prod

Tactic:
simp only [oneEquiv_apply, Multiset.map_singleton, Multiset.prod_singleton, implies_true]

Result:
no goals

Proof state:
σ : Type u_5
R : Type u_6
inst✝² : CommSemiring R
inst✝¹ : Fintype σ
inst✝ : DecidableEq σ
⊢ ∑ i : σ, X i = hsymm σ R 1

Tactic:
apply Fintype.sum_equiv oneEquiv

Result:
case h
σ : Type u_5
R : Type u_6
inst✝² : CommSemiring R
inst✝¹ : Fintype σ
inst✝ : DecidableEq σ
⊢ ∀ (x : σ), X x = (Multiset.map X ↑(oneEquiv x)).prod

Proof state:
σ : Type u_5
R : Type u_6
inst✝² : CommSemiring R
inst✝¹ : Fintype σ
inst✝ : DecidableEq σ
⊢ hsymm σ R 1 = ∑ i : σ, X i

Tactic:
symm

Result:
σ : Type u_5
R : Type u_6
inst✝² : CommSemiring R
inst✝¹ : Fintype σ
inst✝ : DecidableEq σ
⊢ ∑ i : σ, X i = hsymm σ R 1
-- Mathlib/Topology/Instances/AddCircle.lean
lemma eq_coe_Ico (a : AddCircle p) : ∃ b, b ∈ Ico 0 p ∧ ↑b = a

Proof state:
𝕜 : Type u_1
inst✝¹ : LinearOrderedAddCommGroup 𝕜
p : 𝕜
hp : Fact (0 < p)
inst✝ : Archimedean 𝕜
a : AddCircle p
⊢ ∃ b ∈ Ico 0 p, ↑b = a

Tactic:
let b := QuotientAddGroup.equivIcoMod hp.out 0 a

Result:
𝕜 : Type u_1
inst✝¹ : LinearOrderedAddCommGroup 𝕜
p : 𝕜
hp : Fact (0 < p)
inst✝ : Archimedean 𝕜
a : AddCircle p
b : ↑(Ico 0 (0 + p)) := (QuotientAddGroup.equivIcoMod ⋯ 0) a
⊢ ∃ b ∈ Ico 0 p, ↑b = a

Proof state:
𝕜 : Type u_1
inst✝¹ : LinearOrderedAddCommGroup 𝕜
p : 𝕜
hp : Fact (0 < p)
inst✝ : Archimedean 𝕜
a : AddCircle p
b : ↑(Ico 0 (0 + p)) := (QuotientAddGroup.equivIcoMod ⋯ 0) a
⊢ ∃ b ∈ Ico 0 p, ↑b = a

Tactic:
exact ⟨b.1, by simpa only [zero_add] using b.2,
  (QuotientAddGroup.equivIcoMod hp.out 0).symm_apply_apply a⟩

Result:
no goals

Proof state:
𝕜 : Type u_1
inst✝¹ : LinearOrderedAddCommGroup 𝕜
p : 𝕜
hp : Fact (0 < p)
inst✝ : Archimedean 𝕜
a : AddCircle p
b : ↑(Ico 0 (0 + p)) := (QuotientAddGroup.equivIcoMod ⋯ 0) a
⊢ ↑b ∈ Ico 0 p

Tactic:
simpa only [zero_add] using b.2

Result:
no goals
-- Mathlib/Data/Set/Card.lean
/-- Given a subset `s` of a set `t`, of sizes at most and at least `n` respectively, there exists a
set `u` of size `n` which is both a superset of `s` and a subset of `t`. -/
lemma exists_subsuperset_card_eq {n : ℕ} (hst : s ⊆ t) (hsn : s.ncard ≤ n) (hnt : n ≤ t.ncard) :
    ∃ u, s ⊆ u ∧ u ⊆ t ∧ u.ncard = n

Proof state:
α : Type u_1
s t : Set α
n : ℕ
hst : s ⊆ t
hsn : s.ncard ≤ n
hnt : n ≤ t.ncard
⊢ ∃ u, s ⊆ u ∧ u ⊆ t ∧ u.ncard = n

Tactic:
obtain ht | ht := t.infinite_or_finite

Result:
case inl
α : Type u_1
s t : Set α
n : ℕ
hst : s ⊆ t
hsn : s.ncard ≤ n
hnt : n ≤ t.ncard
ht : t.Infinite
⊢ ∃ u, s ⊆ u ∧ u ⊆ t ∧ u.ncard = n

case inr
α : Type u_1
s t : Set α
n : ℕ
hst : s ⊆ t
hsn : s.ncard ≤ n
hnt : n ≤ t.ncard
ht : t.Finite
⊢ ∃ u, s ⊆ u ∧ u ⊆ t ∧ u.ncard = n

Proof state:
case inl
α : Type u_1
s t : Set α
n : ℕ
hst : s ⊆ t
hsn : s.ncard ≤ n
hnt : n ≤ t.ncard
ht : t.Infinite
⊢ ∃ u, s ⊆ u ∧ u ⊆ t ∧ u.ncard = n

Tactic:
rw [ht.ncard, Nat.le_zero, ← ht.ncard] at hnt

Result:
case inl
α : Type u_1
s t : Set α
n : ℕ
hst : s ⊆ t
hsn : s.ncard ≤ n
hnt : n = t.ncard
ht : t.Infinite
⊢ ∃ u, s ⊆ u ∧ u ⊆ t ∧ u.ncard = n

Proof state:
α : Type u_1
n : ℕ
s : Finset α
hsn : (↑s).ncard ≤ n
t : Finset α
hnt : n ≤ (↑t).ncard
hst : ↑s ⊆ ↑t
⊢ s.card ≤ n

Tactic:
simpa using hsn

Result:
no goals

Proof state:
case inl
α : Type u_1
s t : Set α
n : ℕ
hst : s ⊆ t
hsn : s.ncard ≤ n
hnt : n = t.ncard
ht : t.Infinite
⊢ ∃ u, s ⊆ u ∧ u ⊆ t ∧ u.ncard = n

Tactic:
exact ⟨t, hst, Subset.rfl, hnt.symm⟩

Result:
no goals

Proof state:
case inr.intro.intro.intro.intro.intro
α : Type u_1
n : ℕ
s : Finset α
hsn : (↑s).ncard ≤ n
t : Finset α
hnt : n ≤ (↑t).ncard
hst : ↑s ⊆ ↑t
u : Finset α
hsu : s ⊆ u
hut : u ⊆ t
hu : u.card = n
⊢ ∃ u, ↑s ⊆ u ∧ u ⊆ ↑t ∧ u.ncard = n

Tactic:
exact ⟨u, mod_cast hsu, mod_cast hut, mod_cast hu⟩

Result:
no goals

Proof state:
case inr
α : Type u_1
s t : Set α
n : ℕ
hst : s ⊆ t
hsn : s.ncard ≤ n
hnt : n ≤ t.ncard
ht : t.Finite
⊢ ∃ u, s ⊆ u ∧ u ⊆ t ∧ u.ncard = n

Tactic:
lift s to Finset α using ht.subset hst

Result:
case inr.intro
α : Type u_1
t : Set α
n : ℕ
hnt : n ≤ t.ncard
ht : t.Finite
s : Finset α
hst : ↑s ⊆ t
hsn : (↑s).ncard ≤ n
⊢ ∃ u, ↑s ⊆ u ∧ u ⊆ t ∧ u.ncard = n

Proof state:
case inr.intro.intro
α : Type u_1
n : ℕ
s : Finset α
hsn : (↑s).ncard ≤ n
t : Finset α
hnt : n ≤ (↑t).ncard
hst : ↑s ⊆ ↑t
⊢ ∃ u, ↑s ⊆ u ∧ u ⊆ ↑t ∧ u.ncard = n

Tactic:
obtain ⟨u, hsu, hut, hu⟩ := Finset.exists_subsuperset_card_eq (mod_cast hst) (by simpa using hsn)
  (mod_cast hnt)

Result:
case inr.intro.intro.intro.intro.intro
α : Type u_1
n : ℕ
s : Finset α
hsn : (↑s).ncard ≤ n
t : Finset α
hnt : n ≤ (↑t).ncard
hst : ↑s ⊆ ↑t
u : Finset α
hsu : s ⊆ u
hut : u ⊆ t
hu : u.card = n
⊢ ∃ u, ↑s ⊆ u ∧ u ⊆ ↑t ∧ u.ncard = n

Proof state:
case inr.intro
α : Type u_1
t : Set α
n : ℕ
hnt : n ≤ t.ncard
ht : t.Finite
s : Finset α
hst : ↑s ⊆ t
hsn : (↑s).ncard ≤ n
⊢ ∃ u, ↑s ⊆ u ∧ u ⊆ t ∧ u.ncard = n

Tactic:
lift t to Finset α using ht

Result:
case inr.intro.intro
α : Type u_1
n : ℕ
s : Finset α
hsn : (↑s).ncard ≤ n
t : Finset α
hnt : n ≤ (↑t).ncard
hst : ↑s ⊆ ↑t
⊢ ∃ u, ↑s ⊆ u ∧ u ⊆ ↑t ∧ u.ncard = n
-- Mathlib/Tactic/Positivity/Core.lean
lemma pos_of_isRat {n : ℤ} {d : ℕ} [LinearOrderedRing A] :
    (NormNum.IsRat e n d) → (decide (0 < n)) → ((0 : A) < (e : A))
  | ⟨inv, eq⟩, h => by
    have pos_invOf_d : (0 < ⅟ (d : A)) := pos_invOf_of_invertible_cast d
    have pos_n : (0 < (n : A)) := Int.cast_pos (n := n) |>.2 (of_decide_eq_true h)
    rw [eq]
    exact mul_pos pos_n pos_invOf_d

Proof state:
A : Type u_1
e : A
n : ℤ
d : ℕ
inst✝ : LinearOrderedRing A
inv : Invertible ↑d
eq : e = ↑n * ⅟↑d
h : decide (0 < n) = true
pos_invOf_d : 0 < ⅟↑d
pos_n : 0 < ↑n
⊢ 0 < ↑n * ⅟↑d

Tactic:
exact mul_pos pos_n pos_invOf_d

Result:
no goals

Proof state:
A : Type u_1
e : A
n : ℤ
d : ℕ
inst✝ : LinearOrderedRing A
inv : Invertible ↑d
eq : e = ↑n * ⅟↑d
h : decide (0 < n) = true
⊢ 0 < e

Tactic:
have pos_invOf_d : (0 < ⅟ (d : A)) := pos_invOf_of_invertible_cast d

Result:
A : Type u_1
e : A
n : ℤ
d : ℕ
inst✝ : LinearOrderedRing A
inv : Invertible ↑d
eq : e = ↑n * ⅟↑d
h : decide (0 < n) = true
pos_invOf_d : 0 < ⅟↑d
⊢ 0 < e

Proof state:
A : Type u_1
e : A
n : ℤ
d : ℕ
inst✝ : LinearOrderedRing A
inv : Invertible ↑d
eq : e = ↑n * ⅟↑d
h : decide (0 < n) = true
pos_invOf_d : 0 < ⅟↑d
pos_n : 0 < ↑n
⊢ 0 < e

Tactic:
rw [eq]

Result:
A : Type u_1
e : A
n : ℤ
d : ℕ
inst✝ : LinearOrderedRing A
inv : Invertible ↑d
eq : e = ↑n * ⅟↑d
h : decide (0 < n) = true
pos_invOf_d : 0 < ⅟↑d
pos_n : 0 < ↑n
⊢ 0 < ↑n * ⅟↑d

Proof state:
A : Type u_1
e : A
n : ℤ
d : ℕ
inst✝ : LinearOrderedRing A
inv : Invertible ↑d
eq : e = ↑n * ⅟↑d
h : decide (0 < n) = true
pos_invOf_d : 0 < ⅟↑d
⊢ 0 < e

Tactic:
have pos_n : (0 < (n : A)) := Int.cast_pos (n := n) |>.2 (of_decide_eq_true h)

Result:
A : Type u_1
e : A
n : ℤ
d : ℕ
inst✝ : LinearOrderedRing A
inv : Invertible ↑d
eq : e = ↑n * ⅟↑d
h : decide (0 < n) = true
pos_invOf_d : 0 < ⅟↑d
pos_n : 0 < ↑n
⊢ 0 < e
-- Mathlib/Data/Set/NAry.lean
theorem image2_subset_iff_right : image2 f s t ⊆ u ↔ ∀ b ∈ t, (fun a => f a b) '' s ⊆ u

Proof state:
α : Type u_1
β : Type u_3
γ : Type u_5
f : α → β → γ
s : Set α
t : Set β
u : Set γ
⊢ image2 f s t ⊆ u ↔ ∀ b ∈ t, (fun a => f a b) '' s ⊆ u

Tactic:
simp_rw [image2_subset_iff, image_subset_iff, subset_def, mem_preimage, @forall₂_swap α]

Result:
no goals
-- Mathlib/GroupTheory/Perm/Cycle/Type.lean
theorem filter_parts_partition_eq_cycleType {σ : Perm α} :
    ((partition σ).parts.filter fun n => 2 ≤ n) = σ.cycleType

Proof state:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
a : ℕ
h : a ∈ Multiset.replicate (Fintype.card α - σ.support.card) 1
⊢ ¬2 ≤ 1

Tactic:
decide

Result:
no goals

Proof state:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
a : ℕ
h : a ∈ Multiset.replicate (Fintype.card α - σ.support.card) 1
⊢ ¬2 ≤ a

Tactic:
rw [Multiset.eq_of_mem_replicate h]

Result:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
a : ℕ
h : a ∈ Multiset.replicate (Fintype.card α - σ.support.card) 1
⊢ ¬2 ≤ 1

Proof state:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
⊢ Multiset.filter (fun n => 2 ≤ n) σ.partition.parts = σ.cycleType

Tactic:
rw [parts_partition, filter_add, Multiset.filter_eq_self.2 fun _ => two_le_of_mem_cycleType,
  Multiset.filter_eq_nil.2 fun a h => ?_, add_zero]

Result:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
a : ℕ
h : a ∈ Multiset.replicate (Fintype.card α - σ.support.card) 1
⊢ ¬2 ≤ a
-- Mathlib/Topology/UniformSpace/Defs.lean
theorem mem_nhds_uniformity_iff_left {x : α} {s : Set α} :
    s ∈ 𝓝 x ↔ { p : α × α | p.2 = x → p.1 ∈ s } ∈ 𝓤 α

Proof state:
α : Type ua
inst✝ : UniformSpace α
x : α
s : Set α
⊢ s ∈ 𝓝 x ↔ {p | p.2 = x → p.1 ∈ s} ∈ 𝓤 α

Tactic:
rw [uniformity_eq_symm, mem_nhds_uniformity_iff_right]

Result:
α : Type ua
inst✝ : UniformSpace α
x : α
s : Set α
⊢ {p | p.1 = x → p.2 ∈ s} ∈ 𝓤 α ↔ {p | p.2 = x → p.1 ∈ s} ∈ Prod.swap <$> 𝓤 α

Proof state:
α : Type ua
inst✝ : UniformSpace α
x : α
s : Set α
⊢ {p | p.1 = x → p.2 ∈ s} ∈ 𝓤 α ↔ {p | p.2 = x → p.1 ∈ s} ∈ Prod.swap <$> 𝓤 α

Tactic:
simp only [map_def, mem_map, preimage_setOf_eq, Prod.snd_swap, Prod.fst_swap]

Result:
no goals
-- Mathlib/MeasureTheory/Measure/Haar/Basic.lean
theorem index_defined {K V : Set G} (hK : IsCompact K) (hV : (interior V).Nonempty) :
    ∃ n : ℕ, n ∈ Finset.card '' { t : Finset G | K ⊆ ⋃ g ∈ t, (fun h => g * h) ⁻¹' V }

Proof state:
G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : IsTopologicalGroup G
K V : Set G
hK : IsCompact K
hV : (interior V).Nonempty
⊢ ∃ n, n ∈ Finset.card '' {t | K ⊆ ⋃ g ∈ t, (fun h => g * h) ⁻¹' V}

Tactic:
rcases compact_covered_by_mul_left_translates hK hV with ⟨t, ht⟩

Result:
case intro
G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : IsTopologicalGroup G
K V : Set G
hK : IsCompact K
hV : (interior V).Nonempty
t : Finset G
ht : K ⊆ ⋃ g ∈ t, (fun x => g * x) ⁻¹' V
⊢ ∃ n, n ∈ Finset.card '' {t | K ⊆ ⋃ g ∈ t, (fun h => g * h) ⁻¹' V}

Proof state:
case intro
G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : IsTopologicalGroup G
K V : Set G
hK : IsCompact K
hV : (interior V).Nonempty
t : Finset G
ht : K ⊆ ⋃ g ∈ t, (fun x => g * x) ⁻¹' V
⊢ ∃ n, n ∈ Finset.card '' {t | K ⊆ ⋃ g ∈ t, (fun h => g * h) ⁻¹' V}

Tactic:
exact ⟨t.card, t, ht, rfl⟩

Result:
no goals
-- Mathlib/MeasureTheory/Function/LpSpace/Basic.lean
theorem norm_le_norm_of_ae_le {f : Lp E p μ} {g : Lp F p μ} (h : ∀ᵐ x ∂μ, ‖f x‖ ≤ ‖g x‖) :
    ‖f‖ ≤ ‖g‖

Proof state:
α : Type u_1
E : Type u_4
F : Type u_5
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedAddCommGroup F
f : ↥(Lp E p μ)
g : ↥(Lp F p μ)
h : ∀ᵐ (x : α) ∂μ, ‖↑↑f x‖ ≤ ‖↑↑g x‖
⊢ (eLpNorm (↑↑f) p μ).toReal ≤ (eLpNorm (↑↑g) p μ).toReal

Tactic:
exact ENNReal.toReal_mono (eLpNorm_ne_top _) (eLpNorm_mono_ae h)

Result:
no goals

Proof state:
α : Type u_1
E : Type u_4
F : Type u_5
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedAddCommGroup F
f : ↥(Lp E p μ)
g : ↥(Lp F p μ)
h : ∀ᵐ (x : α) ∂μ, ‖↑↑f x‖ ≤ ‖↑↑g x‖
⊢ ‖f‖ ≤ ‖g‖

Tactic:
rw [norm_def, norm_def]

Result:
α : Type u_1
E : Type u_4
F : Type u_5
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedAddCommGroup F
f : ↥(Lp E p μ)
g : ↥(Lp F p μ)
h : ∀ᵐ (x : α) ∂μ, ‖↑↑f x‖ ≤ ‖↑↑g x‖
⊢ (eLpNorm (↑↑f) p μ).toReal ≤ (eLpNorm (↑↑g) p μ).toReal
-- Mathlib/Algebra/Polynomial/Degree/Definitions.lean
theorem degree_update_le (p : R[X]) (n : ℕ) (a : R) : degree (p.update n a) ≤ max (degree p) n

Proof state:
R : Type u
inst✝ : Semiring R
p : R[X]
n : ℕ
a : R
⊢ (if a = 0 then p.support.erase n else insert n p.support).max ≤ p.degree ⊔ ↑n

Tactic:
split_ifs

Result:
case pos
R : Type u
inst✝ : Semiring R
p : R[X]
n : ℕ
a : R
h✝ : a = 0
⊢ (p.support.erase n).max ≤ p.degree ⊔ ↑n

case neg
R : Type u
inst✝ : Semiring R
p : R[X]
n : ℕ
a : R
h✝ : ¬a = 0
⊢ (insert n p.support).max ≤ p.degree ⊔ ↑n

Proof state:
case neg
R : Type u
inst✝ : Semiring R
p : R[X]
n : ℕ
a : R
h✝ : ¬a = 0
⊢ (insert n p.support).max ≤ p.degree ⊔ ↑n

Tactic:
rw [max_insert, max_comm]

Result:
case neg
R : Type u
inst✝ : Semiring R
p : R[X]
n : ℕ
a : R
h✝ : ¬a = 0
⊢ p.support.max ⊔ ↑n ≤ p.degree ⊔ ↑n

Proof state:
case neg
R : Type u
inst✝ : Semiring R
p : R[X]
n : ℕ
a : R
h✝ : ¬a = 0
⊢ p.support.max ⊔ ↑n ≤ p.degree ⊔ ↑n

Tactic:
exact le_rfl

Result:
no goals

Proof state:
R : Type u
inst✝ : Semiring R
p : R[X]
n : ℕ
a : R
⊢ (p.update n a).degree ≤ p.degree ⊔ ↑n

Tactic:
rw [degree, support_update]

Result:
R : Type u
inst✝ : Semiring R
p : R[X]
n : ℕ
a : R
⊢ (if a = 0 then p.support.erase n else insert n p.support).max ≤ p.degree ⊔ ↑n

Proof state:
case pos
R : Type u
inst✝ : Semiring R
p : R[X]
n : ℕ
a : R
h✝ : a = 0
⊢ (p.support.erase n).max ≤ p.degree ⊔ ↑n

Tactic:
exact (Finset.max_mono (erase_subset _ _)).trans (le_max_left _ _)

Result:
no goals
-- Mathlib/MeasureTheory/MeasurableSpace/Basic.lean
theorem measurable_update'  {a : δ} [DecidableEq δ] :
    Measurable (fun p : (∀ i, π i) × π a ↦ update p.1 a p.2)

Proof state:
case pos
δ : Type u_4
π : δ → Type u_6
inst✝¹ : (a : δ) → MeasurableSpace (π a)
a : δ
inst✝ : DecidableEq δ
j : δ
h : j = a
⊢ Measurable fun x => ⋯ ▸ x.2

Tactic:
subst h

Result:
case pos
δ : Type u_4
π : δ → Type u_6
inst✝¹ : (a : δ) → MeasurableSpace (π a)
inst✝ : DecidableEq δ
j : δ
⊢ Measurable fun x => ⋯ ▸ x.2

Proof state:
δ : Type u_4
π : δ → Type u_6
inst✝¹ : (a : δ) → MeasurableSpace (π a)
a : δ
inst✝ : DecidableEq δ
j : δ
⊢ Measurable fun x => update x.1 a x.2 j

Tactic:
dsimp [update]

Result:
δ : Type u_4
π : δ → Type u_6
inst✝¹ : (a : δ) → MeasurableSpace (π a)
a : δ
inst✝ : DecidableEq δ
j : δ
⊢ Measurable fun x => if h : j = a then ⋯ ▸ x.2 else x.1 j

Proof state:
δ : Type u_4
π : δ → Type u_6
inst✝¹ : (a : δ) → MeasurableSpace (π a)
a : δ
inst✝ : DecidableEq δ
j : δ
⊢ Measurable fun x => if h : j = a then ⋯ ▸ x.2 else x.1 j

Tactic:
split_ifs with h

Result:
case pos
δ : Type u_4
π : δ → Type u_6
inst✝¹ : (a : δ) → MeasurableSpace (π a)
a : δ
inst✝ : DecidableEq δ
j : δ
h : j = a
⊢ Measurable fun x => ⋯ ▸ x.2

case neg
δ : Type u_4
π : δ → Type u_6
inst✝¹ : (a : δ) → MeasurableSpace (π a)
a : δ
inst✝ : DecidableEq δ
j : δ
h : ¬j = a
⊢ Measurable fun x => x.1 j

Proof state:
δ : Type u_4
π : δ → Type u_6
inst✝¹ : (a : δ) → MeasurableSpace (π a)
a : δ
inst✝ : DecidableEq δ
⊢ ∀ (a_1 : δ), Measurable fun x => update x.1 a x.2 a_1

Tactic:
intro j

Result:
δ : Type u_4
π : δ → Type u_6
inst✝¹ : (a : δ) → MeasurableSpace (π a)
a : δ
inst✝ : DecidableEq δ
j : δ
⊢ Measurable fun x => update x.1 a x.2 j

Proof state:
δ : Type u_4
π : δ → Type u_6
inst✝¹ : (a : δ) → MeasurableSpace (π a)
a : δ
inst✝ : DecidableEq δ
⊢ Measurable fun p => update p.1 a p.2

Tactic:
rw [measurable_pi_iff]

Result:
δ : Type u_4
π : δ → Type u_6
inst✝¹ : (a : δ) → MeasurableSpace (π a)
a : δ
inst✝ : DecidableEq δ
⊢ ∀ (a_1 : δ), Measurable fun x => update x.1 a x.2 a_1

Proof state:
case pos
δ : Type u_4
π : δ → Type u_6
inst✝¹ : (a : δ) → MeasurableSpace (π a)
inst✝ : DecidableEq δ
j : δ
⊢ Measurable fun x => ⋯ ▸ x.2

Tactic:
dsimp

Result:
case pos
δ : Type u_4
π : δ → Type u_6
inst✝¹ : (a : δ) → MeasurableSpace (π a)
inst✝ : DecidableEq δ
j : δ
⊢ Measurable fun x => x.2

Proof state:
case pos
δ : Type u_4
π : δ → Type u_6
inst✝¹ : (a : δ) → MeasurableSpace (π a)
inst✝ : DecidableEq δ
j : δ
⊢ Measurable fun x => x.2

Tactic:
exact measurable_snd

Result:
no goals

Proof state:
case neg
δ : Type u_4
π : δ → Type u_6
inst✝¹ : (a : δ) → MeasurableSpace (π a)
a : δ
inst✝ : DecidableEq δ
j : δ
h : ¬j = a
⊢ Measurable fun x => x.1 j

Tactic:
exact measurable_pi_iff.1 measurable_fst _

Result:
no goals