harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Data/Set/Finite/Basic.lean
theorem toFinset_subset {t : Finset α} : hs.toFinset ⊆ t ↔ s ⊆ t

Proof state:
α : Type u
s : Set α
hs : s.Finite
t : Finset α
⊢ hs.toFinset ⊆ t ↔ s ⊆ ↑t

Tactic:
rw [← Finset.coe_subset, Finite.coe_toFinset]

Result:
no goals
-- Mathlib/Analysis/SumOverResidueClass.lean
/-- If `f : ℕ → ℝ` is decreasing and has a negative term, then `f` restricted to a residue
class is not summable. -/
lemma not_summable_indicator_mod_of_antitone_of_neg {m : ℕ} [hm : NeZero m] {f : ℕ → ℝ}
    (hf : Antitone f) {n : ℕ} (hn : f n < 0) (k : ZMod m) :
    ¬ Summable ({n : ℕ | (n : ZMod m) = k}.indicator f)

Proof state:
m : ℕ
hm : NeZero m
f : ℕ → ℝ
hf : Antitone f
n : ℕ
hn : f n < 0
k : ZMod m
⊢ ¬Summable fun n => f (m * n + k.val)

Tactic:
exact not_summable_of_antitone_of_neg
  (hf.comp_monotone <| (Covariant.monotone_of_const m).add_const k.val) <|
  (hf <| (Nat.le_mul_of_pos_left n Fin.pos').trans <| Nat.le_add_right ..).trans_lt hn

Result:
no goals

Proof state:
m : ℕ
hm : NeZero m
f : ℕ → ℝ
hf : Antitone f
n : ℕ
hn : f n < 0
k : ZMod m
⊢ ¬Summable ({n | ↑n = k}.indicator f)

Tactic:
rw [← ZMod.natCast_zmod_val k, summable_indicator_mod_iff_summable]

Result:
m : ℕ
hm : NeZero m
f : ℕ → ℝ
hf : Antitone f
n : ℕ
hn : f n < 0
k : ZMod m
⊢ ¬Summable fun n => f (m * n + k.val)
-- Mathlib/Order/SymmDiff.lean
theorem disjoint_symmDiff_inf : Disjoint (a ∆ b) (a ⊓ b)

Proof state:
α : Type u_2
inst✝ : GeneralizedBooleanAlgebra α
a b : α
⊢ Disjoint ((a ⊔ b) \ (a ⊓ b)) (a ⊓ b)

Tactic:
exact disjoint_sdiff_self_left

Result:
no goals

Proof state:
α : Type u_2
inst✝ : GeneralizedBooleanAlgebra α
a b : α
⊢ Disjoint (a ∆ b) (a ⊓ b)

Tactic:
rw [symmDiff_eq_sup_sdiff_inf]

Result:
α : Type u_2
inst✝ : GeneralizedBooleanAlgebra α
a b : α
⊢ Disjoint ((a ⊔ b) \ (a ⊓ b)) (a ⊓ b)
-- Mathlib/Probability/ProbabilityMassFunction/Binomial.lean
theorem binomial_one_eq_bernoulli (p : ℝ≥0∞) (h : p ≤ 1) :
    binomial p h 1 = (bernoulli p h).map (cond · 1 0)

Proof state:
case h
p : ℝ≥0∞
h : p ≤ 1
i : Fin (1 + 1)
⊢ (binomial p h 1) i = (map (fun x => bif x then 1 else 0) (bernoulli p h)) i

Tactic:
fin_cases i <;> simp [tsum_bool, binomial_apply]

Result:
no goals

Proof state:
p : ℝ≥0∞
h : p ≤ 1
⊢ binomial p h 1 = map (fun x => bif x then 1 else 0) (bernoulli p h)

Tactic:
ext i

Result:
case h
p : ℝ≥0∞
h : p ≤ 1
i : Fin (1 + 1)
⊢ (binomial p h 1) i = (map (fun x => bif x then 1 else 0) (bernoulli p h)) i
-- Mathlib/Topology/Constructions.lean
theorem isOpenMap_sigmaMk {i : ι} : IsOpenMap (@Sigma.mk ι σ i)

Proof state:
ι : Type u_5
σ : ι → Type u_7
inst✝ : (i : ι) → TopologicalSpace (σ i)
i : ι
s : Set (σ i)
hs : IsOpen s
j : ι
⊢ IsOpen (Sigma.mk j ⁻¹' (Sigma.mk i '' s))

Tactic:
rcases eq_or_ne j i with (rfl | hne)

Result:
case inl
ι : Type u_5
σ : ι → Type u_7
inst✝ : (i : ι) → TopologicalSpace (σ i)
j : ι
s : Set (σ j)
hs : IsOpen s
⊢ IsOpen (Sigma.mk j ⁻¹' (Sigma.mk j '' s))

case inr
ι : Type u_5
σ : ι → Type u_7
inst✝ : (i : ι) → TopologicalSpace (σ i)
i : ι
s : Set (σ i)
hs : IsOpen s
j : ι
hne : j ≠ i
⊢ IsOpen (Sigma.mk j ⁻¹' (Sigma.mk i '' s))

Proof state:
case inl
ι : Type u_5
σ : ι → Type u_7
inst✝ : (i : ι) → TopologicalSpace (σ i)
j : ι
s : Set (σ j)
hs : IsOpen s
⊢ IsOpen (Sigma.mk j ⁻¹' (Sigma.mk j '' s))

Tactic:
rwa [preimage_image_eq _ sigma_mk_injective]

Result:
no goals

Proof state:
case inr
ι : Type u_5
σ : ι → Type u_7
inst✝ : (i : ι) → TopologicalSpace (σ i)
i : ι
s : Set (σ i)
hs : IsOpen s
j : ι
hne : j ≠ i
⊢ IsOpen ∅

Tactic:
exact isOpen_empty

Result:
no goals

Proof state:
ι : Type u_5
σ : ι → Type u_7
inst✝ : (i : ι) → TopologicalSpace (σ i)
i : ι
s : Set (σ i)
hs : IsOpen s
⊢ IsOpen (Sigma.mk i '' s)

Tactic:
rw [isOpen_sigma_iff]

Result:
ι : Type u_5
σ : ι → Type u_7
inst✝ : (i : ι) → TopologicalSpace (σ i)
i : ι
s : Set (σ i)
hs : IsOpen s
⊢ ∀ (i_1 : ι), IsOpen (Sigma.mk i_1 ⁻¹' (Sigma.mk i '' s))

Proof state:
ι : Type u_5
σ : ι → Type u_7
inst✝ : (i : ι) → TopologicalSpace (σ i)
i : ι
⊢ IsOpenMap (Sigma.mk i)

Tactic:
intro s hs

Result:
ι : Type u_5
σ : ι → Type u_7
inst✝ : (i : ι) → TopologicalSpace (σ i)
i : ι
s : Set (σ i)
hs : IsOpen s
⊢ IsOpen (Sigma.mk i '' s)

Proof state:
case inr
ι : Type u_5
σ : ι → Type u_7
inst✝ : (i : ι) → TopologicalSpace (σ i)
i : ι
s : Set (σ i)
hs : IsOpen s
j : ι
hne : j ≠ i
⊢ IsOpen (Sigma.mk j ⁻¹' (Sigma.mk i '' s))

Tactic:
rw [preimage_image_sigmaMk_of_ne hne]

Result:
case inr
ι : Type u_5
σ : ι → Type u_7
inst✝ : (i : ι) → TopologicalSpace (σ i)
i : ι
s : Set (σ i)
hs : IsOpen s
j : ι
hne : j ≠ i
⊢ IsOpen ∅

Proof state:
ι : Type u_5
σ : ι → Type u_7
inst✝ : (i : ι) → TopologicalSpace (σ i)
i : ι
s : Set (σ i)
hs : IsOpen s
⊢ ∀ (i_1 : ι), IsOpen (Sigma.mk i_1 ⁻¹' (Sigma.mk i '' s))

Tactic:
intro j

Result:
ι : Type u_5
σ : ι → Type u_7
inst✝ : (i : ι) → TopologicalSpace (σ i)
i : ι
s : Set (σ i)
hs : IsOpen s
j : ι
⊢ IsOpen (Sigma.mk j ⁻¹' (Sigma.mk i '' s))
-- Mathlib/Algebra/Order/GroupWithZero/Unbundled.lean
theorem posMulStrictMono_iff_mulPosStrictMono : PosMulStrictMono α ↔ MulPosStrictMono α

Proof state:
α : Type u_3
inst✝³ : Mul α
inst✝² : Std.Commutative fun x1 x2 => x1 * x2
inst✝¹ : Zero α
inst✝ : Preorder α
⊢ PosMulStrictMono α ↔ MulPosStrictMono α

Tactic:
simp only [posMulStrictMono_iff, mulPosStrictMono_iff, Std.Commutative.comm]

Result:
no goals
-- Mathlib/Topology/Connected/Clopen.lean
theorem isClopen_iff [PreconnectedSpace α] {s : Set α} : IsClopen s ↔ s = ∅ ∨ s = univ :=
  ⟨fun hs =>
    by_contradiction fun h =>
      have h1 : s ≠ ∅ ∧ sᶜ ≠ ∅ :=
        ⟨mt Or.inl h,
          mt (fun h2 => Or.inr <| (by rw [← compl_compl s, h2, compl_empty] : s = univ)) h⟩
      let ⟨_, h2, h3⟩ :=
        nonempty_inter hs.2 hs.1.isOpen_compl (union_compl_self s) (nonempty_iff_ne_empty.2 h1.1)
          (nonempty_iff_ne_empty.2 h1.2)
      h3 h2,
    by rintro (rfl | rfl) <;> [exact isClopen_empty; exact isClopen_univ]⟩

Proof state:
α : Type u
inst✝¹ : TopologicalSpace α
inst✝ : PreconnectedSpace α
s : Set α
⊢ s = ∅ ∨ s = univ → IsClopen s

Tactic:
rintro (rfl | rfl) <;> [exact isClopen_empty; exact isClopen_univ]

Result:
no goals

Proof state:
α : Type u
inst✝¹ : TopologicalSpace α
inst✝ : PreconnectedSpace α
s : Set α
hs : IsClopen s
h : ¬(s = ∅ ∨ s = univ)
h2 : sᶜ = ∅
⊢ s = univ

Tactic:
rw [← compl_compl s, h2, compl_empty]

Result:
no goals
-- Mathlib/RingTheory/HahnSeries/Basic.lean
theorem coeff_single : (single a r).coeff b = if b = a then r else 0

Proof state:
Γ : Type u_1
R : Type u_3
inst✝¹ : PartialOrder Γ
inst✝ : Zero R
a b : Γ
r : R
⊢ ((single a) r).coeff b = if b = a then r else 0

Tactic:
split_ifs with h <;> simp [h]

Result:
no goals
-- Mathlib/Topology/Bornology/Absorbs.lean
@[simp]
protected lemma Absorbs.univ : Absorbs G₀ univ s :=
  (eventually_ne_cobounded 0).mono fun a ha ↦ by rw [smul_set_univ₀ ha]; apply subset_univ

Proof state:
G₀ : Type u_1
α : Type u_2
inst✝² : GroupWithZero G₀
inst✝¹ : Bornology G₀
inst✝ : MulAction G₀ α
s : Set α
a : G₀
ha : a ≠ 0
⊢ s ⊆ univ

Tactic:
apply subset_univ

Result:
no goals

Proof state:
G₀ : Type u_1
α : Type u_2
inst✝² : GroupWithZero G₀
inst✝¹ : Bornology G₀
inst✝ : MulAction G₀ α
s : Set α
a : G₀
ha : a ≠ 0
⊢ s ⊆ a • univ

Tactic:
rw [smul_set_univ₀ ha]

Result:
G₀ : Type u_1
α : Type u_2
inst✝² : GroupWithZero G₀
inst✝¹ : Bornology G₀
inst✝ : MulAction G₀ α
s : Set α
a : G₀
ha : a ≠ 0
⊢ s ⊆ univ
-- Mathlib/Probability/Kernel/Disintegration/CDFToKernel.lean
lemma setLIntegral_toKernel_Iic [IsFiniteKernel κ] (hf : IsCondKernelCDF f κ ν)
    (a : α) (x : ℝ) {s : Set β} (hs : MeasurableSet s) :
    ∫⁻ b in s, hf.toKernel f (a, b) (Iic x) ∂(ν a) = κ a (s ×ˢ Iic x)

Proof state:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α (β × ℝ)
ν : Kernel α β
f : α × β → StieltjesFunction
inst✝ : IsFiniteKernel κ
hf : IsCondKernelCDF f κ ν
a : α
x : ℝ
s : Set β
hs : MeasurableSet s
⊢ ∫⁻ (b : β) in s, ((IsCondKernelCDF.toKernel f hf) (a, b)) (Iic x) ∂ν a = (κ a) (s ×ˢ Iic x)

Tactic:
simp_rw [IsCondKernelCDF.toKernel_Iic]

Result:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α (β × ℝ)
ν : Kernel α β
f : α × β → StieltjesFunction
inst✝ : IsFiniteKernel κ
hf : IsCondKernelCDF f κ ν
a : α
x : ℝ
s : Set β
hs : MeasurableSet s
⊢ ∫⁻ (b : β) in s, ENNReal.ofReal (↑(f (a, b)) x) ∂ν a = (κ a) (s ×ˢ Iic x)

Proof state:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α (β × ℝ)
ν : Kernel α β
f : α × β → StieltjesFunction
inst✝ : IsFiniteKernel κ
hf : IsCondKernelCDF f κ ν
a : α
x : ℝ
s : Set β
hs : MeasurableSet s
⊢ ∫⁻ (b : β) in s, ENNReal.ofReal (↑(f (a, b)) x) ∂ν a = (κ a) (s ×ˢ Iic x)

Tactic:
exact hf.setLIntegral _ hs _

Result:
no goals
-- Mathlib/Algebra/GroupWithZero/Associated.lean
theorem prime_mul_iff [CancelCommMonoidWithZero M] {x y : M} :
    Prime (x * y) ↔ (Prime x ∧ IsUnit y) ∨ (IsUnit x ∧ Prime y)

Proof state:
case refine_1
M : Type u_1
inst✝ : CancelCommMonoidWithZero M
x y : M
h : Prime (x * y)
⊢ Prime x ∧ IsUnit y ∨ IsUnit x ∧ Prime y

Tactic:
rcases of_irreducible_mul h.irreducible with hx | hy

Result:
case refine_1.inl
M : Type u_1
inst✝ : CancelCommMonoidWithZero M
x y : M
h : Prime (x * y)
hx : IsUnit x
⊢ Prime x ∧ IsUnit y ∨ IsUnit x ∧ Prime y

case refine_1.inr
M : Type u_1
inst✝ : CancelCommMonoidWithZero M
x y : M
h : Prime (x * y)
hy : IsUnit y
⊢ Prime x ∧ IsUnit y ∨ IsUnit x ∧ Prime y

Proof state:
case refine_1.inl
M : Type u_1
inst✝ : CancelCommMonoidWithZero M
x y : M
h : Prime (x * y)
hx : IsUnit x
⊢ Prime x ∧ IsUnit y ∨ IsUnit x ∧ Prime y

Tactic:
exact Or.inr ⟨hx, (associated_unit_mul_left y x hx).prime h⟩

Result:
no goals

Proof state:
M : Type u_1
inst✝ : CancelCommMonoidWithZero M
x y : M
⊢ Prime (x * y) ↔ Prime x ∧ IsUnit y ∨ IsUnit x ∧ Prime y

Tactic:
refine ⟨fun h ↦ ?_, ?_⟩

Result:
case refine_1
M : Type u_1
inst✝ : CancelCommMonoidWithZero M
x y : M
h : Prime (x * y)
⊢ Prime x ∧ IsUnit y ∨ IsUnit x ∧ Prime y

case refine_2
M : Type u_1
inst✝ : CancelCommMonoidWithZero M
x y : M
⊢ Prime x ∧ IsUnit y ∨ IsUnit x ∧ Prime y → Prime (x * y)

Proof state:
case refine_2.inr.intro
M : Type u_1
inst✝ : CancelCommMonoidWithZero M
x y : M
hx : IsUnit x
hy : Prime y
⊢ Prime (x * y)

Tactic:
exact (associated_unit_mul_right y x hx).prime hy

Result:
no goals

Proof state:
case refine_2
M : Type u_1
inst✝ : CancelCommMonoidWithZero M
x y : M
⊢ Prime x ∧ IsUnit y ∨ IsUnit x ∧ Prime y → Prime (x * y)

Tactic:
rintro (⟨hx, hy⟩ | ⟨hx, hy⟩)

Result:
case refine_2.inl.intro
M : Type u_1
inst✝ : CancelCommMonoidWithZero M
x y : M
hx : Prime x
hy : IsUnit y
⊢ Prime (x * y)

case refine_2.inr.intro
M : Type u_1
inst✝ : CancelCommMonoidWithZero M
x y : M
hx : IsUnit x
hy : Prime y
⊢ Prime (x * y)

Proof state:
case refine_2.inl.intro
M : Type u_1
inst✝ : CancelCommMonoidWithZero M
x y : M
hx : Prime x
hy : IsUnit y
⊢ Prime (x * y)

Tactic:
exact (associated_mul_unit_left x y hy).symm.prime hx

Result:
no goals

Proof state:
case refine_1.inr
M : Type u_1
inst✝ : CancelCommMonoidWithZero M
x y : M
h : Prime (x * y)
hy : IsUnit y
⊢ Prime x ∧ IsUnit y ∨ IsUnit x ∧ Prime y

Tactic:
exact Or.inl ⟨(associated_mul_unit_left x y hy).prime h, hy⟩

Result:
no goals
-- Mathlib/Data/Nat/Choose/Factorization.lean
theorem prod_pow_factorization_choose (n k : ℕ) (hkn : k ≤ n) :
    (∏ p ∈ Finset.range (n + 1), p ^ (Nat.choose n k).factorization p) = choose n k

Proof state:
n k : ℕ
hkn : k ≤ n
⊢ ((n.choose k).factorization.prod fun x1 x2 => x1 ^ x2) = ∏ p ∈ Finset.range (n + 1), p ^ (n.choose k).factorization p

Tactic:
apply Finset.prod_subset

Result:
case h
n k : ℕ
hkn : k ≤ n
⊢ (n.choose k).factorization.support ⊆ Finset.range (n + 1)

case hf
n k : ℕ
hkn : k ≤ n
⊢ ∀ x ∈ Finset.range (n + 1),
    x ∉ (n.choose k).factorization.support → (fun x1 x2 => x1 ^ x2) x ((n.choose k).factorization x) = 1

Proof state:
case hf
n k : ℕ
hkn : k ≤ n
⊢ ∀ x ∈ Finset.range (n + 1),
    x ∉ (n.choose k).factorization.support → (fun x1 x2 => x1 ^ x2) x ((n.choose k).factorization x) = 1

Tactic:
intro p _ h2

Result:
case hf
n k : ℕ
hkn : k ≤ n
p : ℕ
a✝ : p ∈ Finset.range (n + 1)
h2 : p ∉ (n.choose k).factorization.support
⊢ (fun x1 x2 => x1 ^ x2) p ((n.choose k).factorization p) = 1

Proof state:
case h
n k : ℕ
hkn : k ≤ n
p : ℕ
hp : p ∈ (n.choose k).factorization.support
⊢ p ∈ Finset.range (n + 1)

Tactic:
rw [Finset.mem_range]

Result:
case h
n k : ℕ
hkn : k ≤ n
p : ℕ
hp : p ∈ (n.choose k).factorization.support
⊢ p < n + 1

Proof state:
n k : ℕ
hkn : k ≤ n
⊢ ∏ p ∈ Finset.range (n + 1), p ^ (n.choose k).factorization p = n.choose k

Tactic:
conv => rhs
  rw [← factorization_prod_pow_eq_self (choose_pos hkn).ne']

Result:
n k : ℕ
hkn : k ≤ n
⊢ ∏ p ∈ Finset.range (n + 1), p ^ (n.choose k).factorization p = (n.choose k).factorization.prod fun x1 x2 => x1 ^ x2

Proof state:
n k : ℕ
hkn : k ≤ n
⊢ ∏ p ∈ Finset.range (n + 1), p ^ (n.choose k).factorization p = (n.choose k).factorization.prod fun x1 x2 => x1 ^ x2

Tactic:
rw [eq_comm]

Result:
n k : ℕ
hkn : k ≤ n
⊢ ((n.choose k).factorization.prod fun x1 x2 => x1 ^ x2) = ∏ p ∈ Finset.range (n + 1), p ^ (n.choose k).factorization p

Proof state:
case h
n k : ℕ
hkn : k ≤ n
p : ℕ
hp : p ∈ (n.choose k).factorization.support
⊢ p < n + 1

Tactic:
contrapose! hp

Result:
case h
n k : ℕ
hkn : k ≤ n
p : ℕ
hp : n + 1 ≤ p
⊢ p ∉ (n.choose k).factorization.support

Proof state:
case h
n k : ℕ
hkn : k ≤ n
p : ℕ
hp : n + 1 ≤ p
⊢ p ∉ (n.choose k).factorization.support

Tactic:
rw [Finsupp.mem_support_iff, Classical.not_not, factorization_choose_eq_zero_of_lt hp]

Result:
no goals

Proof state:
case h
n k : ℕ
hkn : k ≤ n
⊢ (n.choose k).factorization.support ⊆ Finset.range (n + 1)

Tactic:
intro p hp

Result:
case h
n k : ℕ
hkn : k ≤ n
p : ℕ
hp : p ∈ (n.choose k).factorization.support
⊢ p ∈ Finset.range (n + 1)

Proof state:
case hf
n k : ℕ
hkn : k ≤ n
p : ℕ
a✝ : p ∈ Finset.range (n + 1)
h2 : p ∉ (n.choose k).factorization.support
⊢ (fun x1 x2 => x1 ^ x2) p ((n.choose k).factorization p) = 1

Tactic:
simp [Classical.not_not.1 (mt Finsupp.mem_support_iff.2 h2)]

Result:
no goals
-- Mathlib/RingTheory/Ideal/Maximal.lean
theorem span_singleton_lt_span_singleton [IsDomain α] {x y : α} :
    span ({x} : Set α) < span ({y} : Set α) ↔ DvdNotUnit y x

Proof state:
α : Type u
inst✝¹ : CommSemiring α
inst✝ : IsDomain α
x y : α
⊢ span {x} < span {y} ↔ DvdNotUnit y x

Tactic:
rw [lt_iff_le_not_le, span_singleton_le_span_singleton, span_singleton_le_span_singleton,
  dvd_and_not_dvd_iff]

Result:
no goals
-- Mathlib/CategoryTheory/Action/Basic.lean
theorem ρ_one {G : Type u} [Monoid G] (A : Action V G) : A.ρ 1 = 𝟙 A.V

Proof state:
V : Type (u + 1)
inst✝¹ : LargeCategory V
G : Type u
inst✝ : Monoid G
A : Action V G
⊢ A.ρ 1 = 𝟙 A.V

Tactic:
simp

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Finite.lean
/-- If `G` is a subgraph of `H` then `G.minDegree ≤ H.minDegree`. -/
lemma minDegree_le_minDegree {H : SimpleGraph V} [DecidableRel G.Adj] [DecidableRel H.Adj]
    (hle : G ≤ H) : G.minDegree ≤ H.minDegree

Proof state:
case pos.h
V : Type u_1
G : SimpleGraph V
inst✝² : Fintype V
H : SimpleGraph V
inst✝¹ : DecidableRel G.Adj
inst✝ : DecidableRel H.Adj
hle : G ≤ H
hne : Nonempty V
⊢ ∀ (v : V), G.minDegree ≤ H.degree v

Tactic:
exact fun v ↦ (G.minDegree_le_degree v).trans (G.degree_le_of_le hle)

Result:
no goals

Proof state:
case neg
V : Type u_1
G : SimpleGraph V
inst✝² : Fintype V
H : SimpleGraph V
inst✝¹ : DecidableRel G.Adj
inst✝ : DecidableRel H.Adj
hle : G ≤ H
hne : ¬Nonempty V
⊢ G.minDegree ≤ H.minDegree

Tactic:
rw [not_nonempty_iff] at hne

Result:
case neg
V : Type u_1
G : SimpleGraph V
inst✝² : Fintype V
H : SimpleGraph V
inst✝¹ : DecidableRel G.Adj
inst✝ : DecidableRel H.Adj
hle : G ≤ H
hne : IsEmpty V
⊢ G.minDegree ≤ H.minDegree

Proof state:
case neg
V : Type u_1
G : SimpleGraph V
inst✝² : Fintype V
H : SimpleGraph V
inst✝¹ : DecidableRel G.Adj
inst✝ : DecidableRel H.Adj
hle : G ≤ H
hne : IsEmpty V
⊢ G.minDegree ≤ H.minDegree

Tactic:
simp

Result:
no goals

Proof state:
V : Type u_1
G : SimpleGraph V
inst✝² : Fintype V
H : SimpleGraph V
inst✝¹ : DecidableRel G.Adj
inst✝ : DecidableRel H.Adj
hle : G ≤ H
⊢ G.minDegree ≤ H.minDegree

Tactic:
by_cases hne : Nonempty V

Result:
case pos
V : Type u_1
G : SimpleGraph V
inst✝² : Fintype V
H : SimpleGraph V
inst✝¹ : DecidableRel G.Adj
inst✝ : DecidableRel H.Adj
hle : G ≤ H
hne : Nonempty V
⊢ G.minDegree ≤ H.minDegree

case neg
V : Type u_1
G : SimpleGraph V
inst✝² : Fintype V
H : SimpleGraph V
inst✝¹ : DecidableRel G.Adj
inst✝ : DecidableRel H.Adj
hle : G ≤ H
hne : ¬Nonempty V
⊢ G.minDegree ≤ H.minDegree

Proof state:
case pos
V : Type u_1
G : SimpleGraph V
inst✝² : Fintype V
H : SimpleGraph V
inst✝¹ : DecidableRel G.Adj
inst✝ : DecidableRel H.Adj
hle : G ≤ H
hne : Nonempty V
⊢ G.minDegree ≤ H.minDegree

Tactic:
apply le_minDegree_of_forall_le_degree

Result:
case pos.h
V : Type u_1
G : SimpleGraph V
inst✝² : Fintype V
H : SimpleGraph V
inst✝¹ : DecidableRel G.Adj
inst✝ : DecidableRel H.Adj
hle : G ≤ H
hne : Nonempty V
⊢ ∀ (v : V), G.minDegree ≤ H.degree v
-- Mathlib/Data/Set/Enumerate.lean
theorem enumerate_mem (h_sel : ∀ s a, sel s = some a → a ∈ s) :
    ∀ {s n a}, enumerate sel s n = some a → a ∈ s
  | s, 0, a => h_sel s a
  | s, n + 1, a => by
    cases h : sel s with
    | none => simp [enumerate_eq_none_of_sel, h]
    | some a' =>
      simp only [enumerate, h, Nat.add_eq, add_zero]
      exact fun h' : enumerate sel (s \ {a'}) n = some a ↦
        have : a ∈ s \ {a'} := enumerate_mem h_sel h'
        this.left

Proof state:
case some
α : Type u_1
sel : Set α → Option α
h_sel : ∀ (s : Set α) (a : α), sel s = some a → a ∈ s
s : Set α
n : ℕ
a a' : α
h : sel s = some a'
⊢ (do
        let a ← some a'
        enumerate sel (s \ {a}) n) =
      some a →
    a ∈ s

Tactic:
exact fun h' : enumerate sel (s \ {a'}) n = some a ↦
  have : a ∈ s \ {a'} := enumerate_mem h_sel h'
  this.left

Result:
no goals

Proof state:
case some
α : Type u_1
sel : Set α → Option α
h_sel : ∀ (s : Set α) (a : α), sel s = some a → a ∈ s
s : Set α
n : ℕ
a a' : α
h : sel s = some a'
⊢ enumerate sel s (n + 1) = some a → a ∈ s

Tactic:
simp only [enumerate, h, Nat.add_eq, add_zero]

Result:
case some
α : Type u_1
sel : Set α → Option α
h_sel : ∀ (s : Set α) (a : α), sel s = some a → a ∈ s
s : Set α
n : ℕ
a a' : α
h : sel s = some a'
⊢ (do
        let a ← some a'
        enumerate sel (s \ {a}) n) =
      some a →
    a ∈ s

Proof state:
case none
α : Type u_1
sel : Set α → Option α
h_sel : ∀ (s : Set α) (a : α), sel s = some a → a ∈ s
s : Set α
n : ℕ
a : α
h : sel s = none
⊢ enumerate sel s (n + 1) = some a → a ∈ s

Tactic:
simp [enumerate_eq_none_of_sel, h]

Result:
no goals

Proof state:
α : Type u_1
sel : Set α → Option α
h_sel : ∀ (s : Set α) (a : α), sel s = some a → a ∈ s
s : Set α
n : ℕ
a : α
⊢ enumerate sel s (n + 1) = some a → a ∈ s

Tactic:
cases h : sel s with
| none => simp [enumerate_eq_none_of_sel, h]
| some a' =>
  simp only [enumerate, h, Nat.add_eq, add_zero]
  exact fun h' : enumerate sel (s \ {a'}) n = some a ↦
    have : a ∈ s \ {a'} := enumerate_mem h_sel h'
    this.left

Result:
no goals
-- Mathlib/RingTheory/Generators.lean
@[simp]
lemma toAlgHom_ofComp_rename (Q : Generators S T) (P : Generators R S) (p : P.Ring) :
    (Q.ofComp P).toAlgHom ((rename Sum.inr) p) = C (algebraMap _ _ p) :=
  have : (Q.ofComp P).toAlgHom.comp (rename Sum.inr) =
    (IsScalarTower.toAlgHom R S Q.Ring).comp (IsScalarTower.toAlgHom R P.Ring S)

Proof state:
case hf.a
R : Type u
S : Type v
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
T : Type u_2
inst✝³ : CommRing T
inst✝² : Algebra R T
inst✝¹ : Algebra S T
inst✝ : IsScalarTower R S T
Q : Generators S T
P : Generators R S
p : P.Ring
i✝ : P.vars
m✝ : Q.vars →₀ ℕ
⊢ coeff m✝ (((Q.ofComp P).toAlgHom.comp (rename Sum.inr)) (X i✝)) =
    coeff m✝ (((IsScalarTower.toAlgHom R S Q.Ring).comp (IsScalarTower.toAlgHom R P.Ring S)) (X i✝))

Tactic:
simp

Result:
no goals

Proof state:
R : Type u
S : Type v
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
T : Type u_2
inst✝³ : CommRing T
inst✝² : Algebra R T
inst✝¹ : Algebra S T
inst✝ : IsScalarTower R S T
Q : Generators S T
P : Generators R S
p : P.Ring
⊢ (Q.ofComp P).toAlgHom.comp (rename Sum.inr) =
    (IsScalarTower.toAlgHom R S Q.Ring).comp (IsScalarTower.toAlgHom R P.Ring S)

Tactic:
ext

Result:
case hf.a
R : Type u
S : Type v
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
T : Type u_2
inst✝³ : CommRing T
inst✝² : Algebra R T
inst✝¹ : Algebra S T
inst✝ : IsScalarTower R S T
Q : Generators S T
P : Generators R S
p : P.Ring
i✝ : P.vars
m✝ : Q.vars →₀ ℕ
⊢ coeff m✝ (((Q.ofComp P).toAlgHom.comp (rename Sum.inr)) (X i✝)) =
    coeff m✝ (((IsScalarTower.toAlgHom R S Q.Ring).comp (IsScalarTower.toAlgHom R P.Ring S)) (X i✝))
-- Mathlib/MeasureTheory/Function/L2Space.lean
theorem mem_L1_inner (f g : α →₂[μ] E) :
    AEEqFun.mk (fun x => ⟪f x, g x⟫)
        ((Lp.aestronglyMeasurable f).inner (Lp.aestronglyMeasurable g)) ∈
      Lp 𝕜 1 μ

Proof state:
α : Type u_1
E : Type u_2
𝕜 : Type u_4
inst✝³ : RCLike 𝕜
inst✝² : MeasurableSpace α
μ : Measure α
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
f g : ↥(Lp E 2 μ)
⊢ AEEqFun.mk (fun x => inner (↑↑f x) (↑↑g x)) ⋯ ∈ Lp 𝕜 1 μ

Tactic:
simp_rw [mem_Lp_iff_eLpNorm_lt_top, eLpNorm_aeeqFun]

Result:
α : Type u_1
E : Type u_2
𝕜 : Type u_4
inst✝³ : RCLike 𝕜
inst✝² : MeasurableSpace α
μ : Measure α
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
f g : ↥(Lp E 2 μ)
⊢ eLpNorm (fun x => inner (↑↑f x) (↑↑g x)) 1 μ < ⊤

Proof state:
α : Type u_1
E : Type u_2
𝕜 : Type u_4
inst✝³ : RCLike 𝕜
inst✝² : MeasurableSpace α
μ : Measure α
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
f g : ↥(Lp E 2 μ)
⊢ eLpNorm (fun x => inner (↑↑f x) (↑↑g x)) 1 μ < ⊤

Tactic:
exact eLpNorm_inner_lt_top f g

Result:
no goals
-- Mathlib/Algebra/Order/Field/Basic.lean
theorem one_div_lt_one_div_of_neg_of_lt (hb : b < 0) (h : a < b) : 1 / b < 1 / a

Proof state:
α : Type u_2
inst✝ : LinearOrderedField α
a b : α
hb : b < 0
h : a < b
⊢ 1 / b < 1 / a

Tactic:
rwa [div_lt_iff_of_neg' hb, ← div_eq_mul_one_div, div_lt_one_of_neg (h.trans hb)]

Result:
no goals
-- Mathlib/Data/Nat/Init.lean
lemma mod_eq_iff_lt (hn : n ≠ 0) : m % n = m ↔ m < n :=
  ⟨fun h ↦ by rw [← h]; exact mod_lt _ <| Nat.pos_iff_ne_zero.2 hn, mod_eq_of_lt⟩

Proof state:
m n : ℕ
hn : n ≠ 0
h : m % n = m
⊢ m % n < n

Tactic:
exact mod_lt _ <| Nat.pos_iff_ne_zero.2 hn

Result:
no goals

Proof state:
m n : ℕ
hn : n ≠ 0
h : m % n = m
⊢ m < n

Tactic:
rw [← h]

Result:
m n : ℕ
hn : n ≠ 0
h : m % n = m
⊢ m % n < n
-- Mathlib/MeasureTheory/VectorMeasure/Basic.lean
theorem add [ContinuousAdd M] {v₁ v₂ : VectorMeasure α M} {w : VectorMeasure α N} (hv₁ : v₁ ≪ᵥ w)
    (hv₂ : v₂ ≪ᵥ w) : v₁ + v₂ ≪ᵥ w

Proof state:
α : Type u_1
m : MeasurableSpace α
M : Type u_4
N : Type u_5
inst✝⁴ : AddCommMonoid M
inst✝³ : TopologicalSpace M
inst✝² : AddCommMonoid N
inst✝¹ : TopologicalSpace N
inst✝ : ContinuousAdd M
v₁ v₂ : VectorMeasure α M
w : VectorMeasure α N
hv₁ : v₁ ≪ᵥ w
hv₂ : v₂ ≪ᵥ w
s : Set α
hs : ↑w s = 0
⊢ ↑(v₁ + v₂) s = 0

Tactic:
rw [add_apply, hv₁ hs, hv₂ hs, zero_add]

Result:
no goals

Proof state:
α : Type u_1
m : MeasurableSpace α
M : Type u_4
N : Type u_5
inst✝⁴ : AddCommMonoid M
inst✝³ : TopologicalSpace M
inst✝² : AddCommMonoid N
inst✝¹ : TopologicalSpace N
inst✝ : ContinuousAdd M
v₁ v₂ : VectorMeasure α M
w : VectorMeasure α N
hv₁ : v₁ ≪ᵥ w
hv₂ : v₂ ≪ᵥ w
⊢ v₁ + v₂ ≪ᵥ w

Tactic:
intro s hs

Result:
α : Type u_1
m : MeasurableSpace α
M : Type u_4
N : Type u_5
inst✝⁴ : AddCommMonoid M
inst✝³ : TopologicalSpace M
inst✝² : AddCommMonoid N
inst✝¹ : TopologicalSpace N
inst✝ : ContinuousAdd M
v₁ v₂ : VectorMeasure α M
w : VectorMeasure α N
hv₁ : v₁ ≪ᵥ w
hv₂ : v₂ ≪ᵥ w
s : Set α
hs : ↑w s = 0
⊢ ↑(v₁ + v₂) s = 0