harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Topology/Connected/Basic.lean
theorem IsPreconnected.subset_left_of_subset_union (hu : IsOpen u) (hv : IsOpen v)
    (huv : Disjoint u v) (hsuv : s ⊆ u ∪ v) (hsu : (s ∩ u).Nonempty) (hs : IsPreconnected s) :
    s ⊆ u :=
  Disjoint.subset_left_of_subset_union hsuv
    (by
      by_contra hsv
      rw [not_disjoint_iff_nonempty_inter] at hsv
      obtain ⟨x, _, hx⟩ := hs u v hu hv hsuv hsu hsv
      exact Set.disjoint_iff.1 huv hx)

Proof state:
α : Type u
inst✝ : TopologicalSpace α
s u v : Set α
hu : IsOpen u
hv : IsOpen v
huv : Disjoint u v
hsuv : s ⊆ u ∪ v
hsu : (s ∩ u).Nonempty
hs : IsPreconnected s
hsv : (s ∩ v).Nonempty
⊢ False

Tactic:
obtain ⟨x, _, hx⟩ := hs u v hu hv hsuv hsu hsv

Result:
case intro.intro
α : Type u
inst✝ : TopologicalSpace α
s u v : Set α
hu : IsOpen u
hv : IsOpen v
huv : Disjoint u v
hsuv : s ⊆ u ∪ v
hsu : (s ∩ u).Nonempty
hs : IsPreconnected s
hsv : (s ∩ v).Nonempty
x : α
left✝ : x ∈ s
hx : x ∈ u ∩ v
⊢ False

Proof state:
case intro.intro
α : Type u
inst✝ : TopologicalSpace α
s u v : Set α
hu : IsOpen u
hv : IsOpen v
huv : Disjoint u v
hsuv : s ⊆ u ∪ v
hsu : (s ∩ u).Nonempty
hs : IsPreconnected s
hsv : (s ∩ v).Nonempty
x : α
left✝ : x ∈ s
hx : x ∈ u ∩ v
⊢ False

Tactic:
exact Set.disjoint_iff.1 huv hx

Result:
no goals

Proof state:
α : Type u
inst✝ : TopologicalSpace α
s u v : Set α
hu : IsOpen u
hv : IsOpen v
huv : Disjoint u v
hsuv : s ⊆ u ∪ v
hsu : (s ∩ u).Nonempty
hs : IsPreconnected s
⊢ Disjoint s v

Tactic:
by_contra hsv

Result:
α : Type u
inst✝ : TopologicalSpace α
s u v : Set α
hu : IsOpen u
hv : IsOpen v
huv : Disjoint u v
hsuv : s ⊆ u ∪ v
hsu : (s ∩ u).Nonempty
hs : IsPreconnected s
hsv : ¬Disjoint s v
⊢ False

Proof state:
α : Type u
inst✝ : TopologicalSpace α
s u v : Set α
hu : IsOpen u
hv : IsOpen v
huv : Disjoint u v
hsuv : s ⊆ u ∪ v
hsu : (s ∩ u).Nonempty
hs : IsPreconnected s
hsv : ¬Disjoint s v
⊢ False

Tactic:
rw [not_disjoint_iff_nonempty_inter] at hsv

Result:
α : Type u
inst✝ : TopologicalSpace α
s u v : Set α
hu : IsOpen u
hv : IsOpen v
huv : Disjoint u v
hsuv : s ⊆ u ∪ v
hsu : (s ∩ u).Nonempty
hs : IsPreconnected s
hsv : (s ∩ v).Nonempty
⊢ False
-- Mathlib/Topology/Basic.lean
lemma not_mem_closure_iff_nhdsWithin_eq_bot : x ∉ closure s ↔ 𝓝[s] x = ⊥

Proof state:
X : Type u
x : X
s : Set X
inst✝ : TopologicalSpace X
⊢ x ∉ closure s ↔ 𝓝[s] x = ⊥

Tactic:
rw [mem_closure_iff_nhdsWithin_neBot, not_neBot]

Result:
no goals
-- Mathlib/MeasureTheory/MeasurableSpace/CountablyGenerated.lean
lemma countableOrCountablyGenerated_right_of_prod_left_of_nonempty [Nonempty α]
    [h : CountableOrCountablyGenerated (α × β) γ] :
    CountableOrCountablyGenerated β γ

Proof state:
β : Type u_2
α : Type u_3
γ : Type u_4
inst✝³ : MeasurableSpace α
inst✝² : MeasurableSpace β
inst✝¹ : MeasurableSpace γ
inst✝ : Nonempty α
h : CountableOrCountablyGenerated (α × β) γ
⊢ CountableOrCountablyGenerated β γ

Tactic:
rcases h.countableOrCountablyGenerated with (h | h)

Result:
case inl
β : Type u_2
α : Type u_3
γ : Type u_4
inst✝³ : MeasurableSpace α
inst✝² : MeasurableSpace β
inst✝¹ : MeasurableSpace γ
inst✝ : Nonempty α
h✝ : CountableOrCountablyGenerated (α × β) γ
h : Countable (α × β)
⊢ CountableOrCountablyGenerated β γ

case inr
β : Type u_2
α : Type u_3
γ : Type u_4
inst✝³ : MeasurableSpace α
inst✝² : MeasurableSpace β
inst✝¹ : MeasurableSpace γ
inst✝ : Nonempty α
h✝ : CountableOrCountablyGenerated (α × β) γ
h : CountablyGenerated γ
⊢ CountableOrCountablyGenerated β γ

Proof state:
case inr
β : Type u_2
α : Type u_3
γ : Type u_4
inst✝³ : MeasurableSpace α
inst✝² : MeasurableSpace β
inst✝¹ : MeasurableSpace γ
inst✝ : Nonempty α
h✝ : CountableOrCountablyGenerated (α × β) γ
h : CountablyGenerated γ
⊢ CountableOrCountablyGenerated β γ

Tactic:
infer_instance

Result:
no goals

Proof state:
case inl
β : Type u_2
α : Type u_3
γ : Type u_4
inst✝³ : MeasurableSpace α
inst✝² : MeasurableSpace β
inst✝¹ : MeasurableSpace γ
inst✝ : Nonempty α
h✝ : CountableOrCountablyGenerated (α × β) γ
h : Countable (α × β)
this : Countable β
⊢ CountableOrCountablyGenerated β γ

Tactic:
infer_instance

Result:
no goals

Proof state:
case inl
β : Type u_2
α : Type u_3
γ : Type u_4
inst✝³ : MeasurableSpace α
inst✝² : MeasurableSpace β
inst✝¹ : MeasurableSpace γ
inst✝ : Nonempty α
h✝ : CountableOrCountablyGenerated (α × β) γ
h : Countable (α × β)
⊢ CountableOrCountablyGenerated β γ

Tactic:
have := countable_right_of_prod_of_nonempty h

Result:
case inl
β : Type u_2
α : Type u_3
γ : Type u_4
inst✝³ : MeasurableSpace α
inst✝² : MeasurableSpace β
inst✝¹ : MeasurableSpace γ
inst✝ : Nonempty α
h✝ : CountableOrCountablyGenerated (α × β) γ
h : Countable (α × β)
this : Countable β
⊢ CountableOrCountablyGenerated β γ
-- Mathlib/Data/Complex/Trigonometric.lean
theorem sin_pos_of_pos_of_le_two {x : ℝ} (hx0 : 0 < x) (hx : x ≤ 2) : 0 < sin x :=
  have : x / 2 ≤ 1 := (div_le_iff₀ (by norm_num)).mpr (by simpa)
  calc
    0 < 2 * sin (x / 2) * cos (x / 2) :=
      mul_pos (mul_pos (by norm_num) (sin_pos_of_pos_of_le_one (half_pos hx0) this))
        (cos_pos_of_le_one (by rwa [abs_of_nonneg (le_of_lt (half_pos hx0))]))
    _ = sin x

Proof state:
x : ℝ
hx0 : 0 < x
hx : x ≤ 2
this : x / 2 ≤ 1
⊢ 0 < 2

Tactic:
norm_num

Result:
no goals

Proof state:
x : ℝ
hx0 : 0 < x
hx : x ≤ 2
⊢ x ≤ 1 * 2

Tactic:
simpa

Result:
no goals

Proof state:
x : ℝ
hx0 : 0 < x
hx : x ≤ 2
this : x / 2 ≤ 1
⊢ 2 * sin (x / 2) * cos (x / 2) = sin x

Tactic:
rw [← sin_two_mul, two_mul, add_halves]

Result:
no goals

Proof state:
x : ℝ
hx0 : 0 < x
hx : x ≤ 2
this : x / 2 ≤ 1
⊢ |x / 2| ≤ 1

Tactic:
rwa [abs_of_nonneg (le_of_lt (half_pos hx0))]

Result:
no goals

Proof state:
x : ℝ
hx0 : 0 < x
hx : x ≤ 2
⊢ 0 < 2

Tactic:
norm_num

Result:
no goals
-- Mathlib/Analysis/SpecificLimits/FloorPow.lean
theorem mul_pow_le_nat_floor_pow {c : ℝ} (hc : 1 < c) (i : ℕ) : (1 - c⁻¹) * c ^ i ≤ ⌊c ^ i⌋₊

Proof state:
c : ℝ
hc : 1 < c
i : ℕ
cpos : 0 < c
⊢ (1 - c⁻¹) * c ^ i ≤ ↑⌊c ^ i⌋₊

Tactic:
rcases eq_or_ne i 0 with (rfl | hi)

Result:
case inl
c : ℝ
hc : 1 < c
cpos : 0 < c
⊢ (1 - c⁻¹) * c ^ 0 ≤ ↑⌊c ^ 0⌋₊

case inr
c : ℝ
hc : 1 < c
i : ℕ
cpos : 0 < c
hi : i ≠ 0
⊢ (1 - c⁻¹) * c ^ i ≤ ↑⌊c ^ i⌋₊

Proof state:
case inr
c : ℝ
hc : 1 < c
i : ℕ
cpos : 0 < c
hi : i ≠ 0
⊢ (1 - c⁻¹) * c ^ i ≤ ↑⌊c ^ i⌋₊

Tactic:
calc
  (1 - c⁻¹) * c ^ i = c ^ i - c ^ i * c⁻¹ := by ring
  _ ≤ c ^ i - 1 := by
    gcongr
    simpa only [← div_eq_mul_inv, one_le_div cpos, pow_one] using le_self_pow₀ hc.le hi
  _ ≤ ⌊c ^ i⌋₊ := (Nat.sub_one_lt_floor _).le

Result:
no goals

Proof state:
case inl
c : ℝ
hc : 1 < c
cpos : 0 < c
⊢ (1 - c⁻¹) * c ^ 0 ≤ ↑⌊c ^ 0⌋₊

Tactic:
simp only [pow_zero, Nat.floor_one, Nat.cast_one, mul_one, sub_le_self_iff, inv_nonneg, cpos.le]

Result:
no goals

Proof state:
c : ℝ
hc : 1 < c
i : ℕ
cpos : 0 < c
hi : i ≠ 0
⊢ c ^ i - c ^ i * c⁻¹ ≤ c ^ i - 1

Tactic:
gcongr

Result:
case h
c : ℝ
hc : 1 < c
i : ℕ
cpos : 0 < c
hi : i ≠ 0
⊢ 1 ≤ c ^ i * c⁻¹

Proof state:
c : ℝ
hc : 1 < c
i : ℕ
⊢ (1 - c⁻¹) * c ^ i ≤ ↑⌊c ^ i⌋₊

Tactic:
have cpos : 0 < c := zero_lt_one.trans hc

Result:
c : ℝ
hc : 1 < c
i : ℕ
cpos : 0 < c
⊢ (1 - c⁻¹) * c ^ i ≤ ↑⌊c ^ i⌋₊

Proof state:
c : ℝ
hc : 1 < c
i : ℕ
cpos : 0 < c
hi : i ≠ 0
⊢ (1 - c⁻¹) * c ^ i = c ^ i - c ^ i * c⁻¹

Tactic:
ring

Result:
no goals

Proof state:
case h
c : ℝ
hc : 1 < c
i : ℕ
cpos : 0 < c
hi : i ≠ 0
⊢ 1 ≤ c ^ i * c⁻¹

Tactic:
simpa only [← div_eq_mul_inv, one_le_div cpos, pow_one] using le_self_pow₀ hc.le hi

Result:
no goals
-- Mathlib/Data/Nat/Factors.lean
theorem eq_prime_pow_of_unique_prime_dvd {n p : ℕ} (hpos : n ≠ 0)
    (h : ∀ {d}, Nat.Prime d → d ∣ n → d = p) : n = p ^ n.primeFactorsList.length

Proof state:
n p : ℕ
hpos : n ≠ 0
h : ∀ {d : ℕ}, Prime d → d ∣ n → d = p
k : ℕ := n.primeFactorsList.length
⊢ n = p ^ k

Tactic:
rw [← prod_primeFactorsList hpos, ← prod_replicate k p, eq_replicate_of_mem fun d hd =>
  h (prime_of_mem_primeFactorsList hd) (dvd_of_mem_primeFactorsList hd)]

Result:
no goals

Proof state:
n p : ℕ
hpos : n ≠ 0
h : ∀ {d : ℕ}, Prime d → d ∣ n → d = p
⊢ n = p ^ n.primeFactorsList.length

Tactic:
set k := n.primeFactorsList.length

Result:
n p : ℕ
hpos : n ≠ 0
h : ∀ {d : ℕ}, Prime d → d ∣ n → d = p
k : ℕ := n.primeFactorsList.length
⊢ n = p ^ k
-- Mathlib/Topology/Category/TopCat/Limits/Products.lean
theorem sigmaIsoSigma_hom_ι {ι : Type v} (α : ι → TopCat.{max v u}) (i : ι) :
    Sigma.ι α i ≫ (sigmaIsoSigma α).hom = sigmaι α i

Proof state:
ι : Type v
α : ι → TopCat
i : ι
⊢ Sigma.ι α i ≫ (sigmaIsoSigma α).hom = sigmaι α i

Tactic:
simp [sigmaIsoSigma]

Result:
no goals
-- Mathlib/Algebra/Order/Antidiag/Nat.lean
theorem dvd_of_mem_finMulAntidiag {n d : ℕ} {f : Fin d → ℕ} (hf : f ∈ finMulAntidiag d n)
    (i : Fin d) : f i ∣ n

Proof state:
n d : ℕ
f : Fin d → ℕ
hf : ∏ i : Fin d, f i = n ∧ n ≠ 0
i : Fin d
⊢ f i ∣ ∏ i : Fin d, f i

Tactic:
exact dvd_prod_of_mem f (mem_univ i)

Result:
no goals

Proof state:
n d : ℕ
f : Fin d → ℕ
hf : f ∈ d.finMulAntidiag n
i : Fin d
⊢ f i ∣ n

Tactic:
rw [mem_finMulAntidiag] at hf

Result:
n d : ℕ
f : Fin d → ℕ
hf : ∏ i : Fin d, f i = n ∧ n ≠ 0
i : Fin d
⊢ f i ∣ n

Proof state:
n d : ℕ
f : Fin d → ℕ
hf : ∏ i : Fin d, f i = n ∧ n ≠ 0
i : Fin d
⊢ f i ∣ n

Tactic:
rw [← hf.1]

Result:
n d : ℕ
f : Fin d → ℕ
hf : ∏ i : Fin d, f i = n ∧ n ≠ 0
i : Fin d
⊢ f i ∣ ∏ i : Fin d, f i
-- Mathlib/SetTheory/Cardinal/Arithmetic.lean
theorem mk_embedding_eq_arrow_of_lift_le (lle : lift.{u} #β' ≤ lift.{v} #α) :
    #(β' ↪ α) = #(β' → α) :=
  (mk_embedding_le_arrow _ _).antisymm <| by
    conv_rhs => rw [← (Equiv.embeddingCongr (.refl _)
      (Cardinal.eq.mp <| mul_eq_self <| aleph0_le_mk α).some).cardinal_eq]
    obtain ⟨e⟩ := lift_mk_le'.mp lle
    exact ⟨⟨fun f ↦ ⟨fun b ↦ ⟨e b, f b⟩, fun _ _ h ↦ e.injective congr(Prod.fst $h)⟩,
      fun f g h ↦ funext fun b ↦ congr(Prod.snd <| $h b)⟩⟩

Proof state:
case intro
α : Type u
β' : Type v
inst✝ : Infinite α
lle : lift.{u, v} #β' ≤ lift.{v, u} #α
e : β' ↪ α
⊢ #(β' → α) ≤ #(β' ↪ α × α)

Tactic:
exact ⟨⟨fun f ↦ ⟨fun b ↦ ⟨e b, f b⟩, fun _ _ h ↦ e.injective congr(Prod.fst $h)⟩,
  fun f g h ↦ funext fun b ↦ congr(Prod.snd <| $h b)⟩⟩

Result:
no goals

Proof state:
α : Type u
β' : Type v
inst✝ : Infinite α
lle : lift.{u, v} #β' ≤ lift.{v, u} #α
⊢ #(β' → α) ≤ #(β' ↪ α)

Tactic:
conv_rhs => rw [← (Equiv.embeddingCongr (.refl _)
  (Cardinal.eq.mp <| mul_eq_self <| aleph0_le_mk α).some).cardinal_eq]

Result:
α : Type u
β' : Type v
inst✝ : Infinite α
lle : lift.{u, v} #β' ≤ lift.{v, u} #α
⊢ #(β' → α) ≤ #(β' ↪ α × α)

Proof state:
α : Type u
β' : Type v
inst✝ : Infinite α
lle : lift.{u, v} #β' ≤ lift.{v, u} #α
⊢ #(β' → α) ≤ #(β' ↪ α × α)

Tactic:
obtain ⟨e⟩ := lift_mk_le'.mp lle

Result:
case intro
α : Type u
β' : Type v
inst✝ : Infinite α
lle : lift.{u, v} #β' ≤ lift.{v, u} #α
e : β' ↪ α
⊢ #(β' → α) ≤ #(β' ↪ α × α)
-- Mathlib/AlgebraicTopology/DoldKan/SplitSimplicialObject.lean
theorem ιSummand_comp_d_comp_πSummand_eq_zero (j k : ℕ) (A : IndexSet (op ⦋j⦌)) (hA : ¬A.EqId) :
    (s.cofan _).inj A ≫ K[X].d j k ≫ s.πSummand (IndexSet.id (op ⦋k⦌)) = 0

Proof state:
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
X : SimplicialObject C
s : Splitting X
inst✝ : Preadditive C
j k : ℕ
A : IndexSet (op ⦋j⦌)
hA : ¬A.EqId
⊢ (s.cofan (op ⦋j⦌)).inj A ≫ K[X].d j k ≫ s.πSummand (IndexSet.id (op ⦋k⦌)) = 0

Tactic:
rw [A.eqId_iff_mono] at hA

Result:
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
X : SimplicialObject C
s : Splitting X
inst✝ : Preadditive C
j k : ℕ
A : IndexSet (op ⦋j⦌)
hA : ¬Mono A.e
⊢ (s.cofan (op ⦋j⦌)).inj A ≫ K[X].d j k ≫ s.πSummand (IndexSet.id (op ⦋k⦌)) = 0

Proof state:
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
X : SimplicialObject C
s : Splitting X
inst✝ : Preadditive C
j k : ℕ
A : IndexSet (op ⦋j⦌)
hA : ¬Mono A.e
⊢ (s.cofan (op ⦋j⦌)).inj A ≫ K[X].d j k ≫ s.πSummand (IndexSet.id (op ⦋k⦌)) = 0

Tactic:
rw [← assoc, ← s.comp_PInfty_eq_zero_iff, assoc, ← PInfty.comm j k, s.cofan_inj_eq, assoc,
  degeneracy_comp_PInfty_assoc X j A.e hA, zero_comp, comp_zero]

Result:
no goals
-- Mathlib/Algebra/DirectSum/Module.lean
theorem isInternal_submodule_iff_isCompl (A : ι → Submodule R M) {i j : ι} (hij : i ≠ j)
    (h : (Set.univ : Set ι) = {i, j}) : IsInternal A ↔ IsCompl (A i) (A j)

Proof state:
R : Type u
inst✝² : Ring R
ι : Type v
dec_ι : DecidableEq ι
M : Type u_1
inst✝¹ : AddCommGroup M
inst✝ : Module R M
A : ι → Submodule R M
i j : ι
hij : i ≠ j
h : Set.univ = {i, j}
this : ∀ (k : ι), k = i ∨ k = j
⊢ Disjoint (A i) (A j) ∧ A i ⊔ A j = ⊤ ↔ IsCompl (A i) (A j)

Tactic:
exact ⟨fun ⟨hd, ht⟩ ↦ ⟨hd, codisjoint_iff.mpr ht⟩, fun ⟨hd, ht⟩ ↦ ⟨hd, ht.eq_top⟩⟩

Result:
no goals

Proof state:
R : Type u
inst✝² : Ring R
ι : Type v
dec_ι : DecidableEq ι
M : Type u_1
inst✝¹ : AddCommGroup M
inst✝ : Module R M
A : ι → Submodule R M
i j : ι
hij : i ≠ j
h : Set.univ = {i, j}
k : ι
⊢ k = i ∨ k = j

Tactic:
simpa using Set.ext_iff.mp h k

Result:
no goals

Proof state:
R : Type u
inst✝² : Ring R
ι : Type v
dec_ι : DecidableEq ι
M : Type u_1
inst✝¹ : AddCommGroup M
inst✝ : Module R M
A : ι → Submodule R M
i j : ι
hij : i ≠ j
h : Set.univ = {i, j}
this : ∀ (k : ι), k = i ∨ k = j
⊢ IsInternal A ↔ IsCompl (A i) (A j)

Tactic:
rw [isInternal_submodule_iff_iSupIndep_and_iSup_eq_top, iSup, ← Set.image_univ, h,
  Set.image_insert_eq, Set.image_singleton, sSup_pair, iSupIndep_pair hij this]

Result:
R : Type u
inst✝² : Ring R
ι : Type v
dec_ι : DecidableEq ι
M : Type u_1
inst✝¹ : AddCommGroup M
inst✝ : Module R M
A : ι → Submodule R M
i j : ι
hij : i ≠ j
h : Set.univ = {i, j}
this : ∀ (k : ι), k = i ∨ k = j
⊢ Disjoint (A i) (A j) ∧ A i ⊔ A j = ⊤ ↔ IsCompl (A i) (A j)

Proof state:
R : Type u
inst✝² : Ring R
ι : Type v
dec_ι : DecidableEq ι
M : Type u_1
inst✝¹ : AddCommGroup M
inst✝ : Module R M
A : ι → Submodule R M
i j : ι
hij : i ≠ j
h : Set.univ = {i, j}
⊢ IsInternal A ↔ IsCompl (A i) (A j)

Tactic:
have : ∀ k, k = i ∨ k = j := fun k ↦ by simpa using Set.ext_iff.mp h k

Result:
R : Type u
inst✝² : Ring R
ι : Type v
dec_ι : DecidableEq ι
M : Type u_1
inst✝¹ : AddCommGroup M
inst✝ : Module R M
A : ι → Submodule R M
i j : ι
hij : i ≠ j
h : Set.univ = {i, j}
this : ∀ (k : ι), k = i ∨ k = j
⊢ IsInternal A ↔ IsCompl (A i) (A j)
-- Mathlib/GroupTheory/Perm/Cycle/Type.lean
theorem cycleType_eq' {σ : Perm α} (s : Finset (Perm α)) (h1 : ∀ f : Perm α, f ∈ s → f.IsCycle)
    (h2 : (s : Set (Perm α)).Pairwise Disjoint)
    (h0 : s.noncommProd id (h2.imp fun _ _ => Disjoint.commute) = σ) :
    σ.cycleType = s.1.map (Finset.card ∘ support)

Proof state:
case e_s.e_self
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
s : Finset (Perm α)
h1 : ∀ f ∈ s, f.IsCycle
h2 : (↑s).Pairwise Disjoint
h0 : s.noncommProd id ⋯ = σ
⊢ σ.cycleFactorsFinset = s

Tactic:
rw [cycleFactorsFinset_eq_finset]

Result:
case e_s.e_self
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
s : Finset (Perm α)
h1 : ∀ f ∈ s, f.IsCycle
h2 : (↑s).Pairwise Disjoint
h0 : s.noncommProd id ⋯ = σ
⊢ (∀ f ∈ s, f.IsCycle) ∧ ∃ (h : (↑s).Pairwise Disjoint), s.noncommProd id ⋯ = σ

Proof state:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
s : Finset (Perm α)
h1 : ∀ f ∈ s, f.IsCycle
h2 : (↑s).Pairwise Disjoint
h0 : s.noncommProd id ⋯ = σ
⊢ σ.cycleType = Multiset.map (Finset.card ∘ support) s.val

Tactic:
rw [cycleType_def]

Result:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
s : Finset (Perm α)
h1 : ∀ f ∈ s, f.IsCycle
h2 : (↑s).Pairwise Disjoint
h0 : s.noncommProd id ⋯ = σ
⊢ Multiset.map (Finset.card ∘ support) σ.cycleFactorsFinset.val = Multiset.map (Finset.card ∘ support) s.val

Proof state:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
s : Finset (Perm α)
h1 : ∀ f ∈ s, f.IsCycle
h2 : (↑s).Pairwise Disjoint
h0 : s.noncommProd id ⋯ = σ
⊢ Multiset.map (Finset.card ∘ support) σ.cycleFactorsFinset.val = Multiset.map (Finset.card ∘ support) s.val

Tactic:
congr

Result:
case e_s.e_self
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
s : Finset (Perm α)
h1 : ∀ f ∈ s, f.IsCycle
h2 : (↑s).Pairwise Disjoint
h0 : s.noncommProd id ⋯ = σ
⊢ σ.cycleFactorsFinset = s

Proof state:
case e_s.e_self
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
s : Finset (Perm α)
h1 : ∀ f ∈ s, f.IsCycle
h2 : (↑s).Pairwise Disjoint
h0 : s.noncommProd id ⋯ = σ
⊢ (∀ f ∈ s, f.IsCycle) ∧ ∃ (h : (↑s).Pairwise Disjoint), s.noncommProd id ⋯ = σ

Tactic:
exact ⟨h1, h2, h0⟩

Result:
no goals
-- Mathlib/NumberTheory/LSeries/Dirichlet.lean
lemma not_LSeriesSummable_moebius_at_one : ¬ LSeriesSummable ↗μ 1

Proof state:
case neg
h : LSeriesSummable (fun n => ↑(μ n)) 1
n : ℕ
hn : ¬Nat.Prime n
⊢ {n | Nat.Prime n}.indicator (term (fun n => ↑(μ n)) 1) n = -↑({p | Nat.Prime p}.indicator (fun n => 1 / ↑n) n)

Tactic:
simp [hn]

Result:
no goals

Proof state:
h : LSeriesSummable (fun n => ↑(μ n)) 1
⊢ Summable fun b => -↑({p | Nat.Prime p}.indicator (fun n => 1 / ↑n) b)

Tactic:
refine (h.indicator {n | n.Prime}).congr fun n ↦ ?_

Result:
h : LSeriesSummable (fun n => ↑(μ n)) 1
n : ℕ
⊢ {n | Nat.Prime n}.indicator (term (fun n => ↑(μ n)) 1) n = -↑({p | Nat.Prime p}.indicator (fun n => 1 / ↑n) n)

Proof state:
h : LSeriesSummable (fun n => ↑(μ n)) 1
n : ℕ
⊢ {n | Nat.Prime n}.indicator (term (fun n => ↑(μ n)) 1) n = -↑({p | Nat.Prime p}.indicator (fun n => 1 / ↑n) n)

Tactic:
by_cases hn : n.Prime

Result:
case pos
h : LSeriesSummable (fun n => ↑(μ n)) 1
n : ℕ
hn : Nat.Prime n
⊢ {n | Nat.Prime n}.indicator (term (fun n => ↑(μ n)) 1) n = -↑({p | Nat.Prime p}.indicator (fun n => 1 / ↑n) n)

case neg
h : LSeriesSummable (fun n => ↑(μ n)) 1
n : ℕ
hn : ¬Nat.Prime n
⊢ {n | Nat.Prime n}.indicator (term (fun n => ↑(μ n)) 1) n = -↑({p | Nat.Prime p}.indicator (fun n => 1 / ↑n) n)

Proof state:
case pos
h : LSeriesSummable (fun n => ↑(μ n)) 1
n : ℕ
hn : Nat.Prime n
⊢ {n | Nat.Prime n}.indicator (term (fun n => ↑(μ n)) 1) n = -↑({p | Nat.Prime p}.indicator (fun n => 1 / ↑n) n)

Tactic:
simp [hn, hn.ne_zero, moebius_apply_prime hn, push_cast, neg_div]

Result:
no goals

Proof state:
⊢ ¬LSeriesSummable (fun n => ↑(μ n)) 1

Tactic:
refine fun h ↦ not_summable_one_div_on_primes <| summable_ofReal.mp <| .of_neg ?_

Result:
h : LSeriesSummable (fun n => ↑(μ n)) 1
⊢ Summable fun b => -↑({p | Nat.Prime p}.indicator (fun n => 1 / ↑n) b)
-- Mathlib/MeasureTheory/Integral/SetIntegral.lean
theorem integrableOn_iUnion_of_summable_norm_restrict {f : C(X, E)} {s : ι → Compacts X}
    (hf : Summable fun i : ι => ‖f.restrict (s i)‖ * ENNReal.toReal (μ <| s i)) :
    IntegrableOn f (⋃ i : ι, s i) μ

Proof state:
X : Type u_1
E : Type u_3
mX : MeasurableSpace X
ι : Type u_5
inst✝⁵ : Countable ι
μ : Measure X
inst✝⁴ : NormedAddCommGroup E
inst✝³ : TopologicalSpace X
inst✝² : BorelSpace X
inst✝¹ : MetrizableSpace X
inst✝ : IsLocallyFiniteMeasure μ
f : C(X, E)
s : ι → Compacts X
hf : Summable fun i => ‖ContinuousMap.restrict (↑(s i)) f‖ * (μ ↑(s i)).toReal
i : ι
⊢ ‖∫ (x : X) in ↑(s i), ‖f x‖ ∂μ‖ ≤ ‖ContinuousMap.restrict (↑(s i)) f‖ * (μ ↑(s i)).toReal

Tactic:
exact
  norm_setIntegral_le_of_norm_le_const' (s i).isCompact.measure_lt_top
    (s i).isCompact.isClosed.measurableSet fun x hx =>
    (norm_norm (f x)).symm ▸ (f.restrict (s i : Set X)).norm_coe_le_norm ⟨x, hx⟩

Result:
no goals

Proof state:
X : Type u_1
E : Type u_3
mX : MeasurableSpace X
ι : Type u_5
inst✝⁵ : Countable ι
μ : Measure X
inst✝⁴ : NormedAddCommGroup E
inst✝³ : TopologicalSpace X
inst✝² : BorelSpace X
inst✝¹ : MetrizableSpace X
inst✝ : IsLocallyFiniteMeasure μ
f : C(X, E)
s : ι → Compacts X
hf : Summable fun i => ‖ContinuousMap.restrict (↑(s i)) f‖ * (μ ↑(s i)).toReal
i : ι
⊢ ∫ (x : X) in ↑(s i), ‖f x‖ ∂μ ≤ ‖ContinuousMap.restrict (↑(s i)) f‖ * (μ ↑(s i)).toReal

Tactic:
rw [← (Real.norm_of_nonneg (integral_nonneg fun x => norm_nonneg _) : ‖_‖ = ∫ x in s i, ‖f x‖ ∂μ)]

Result:
X : Type u_1
E : Type u_3
mX : MeasurableSpace X
ι : Type u_5
inst✝⁵ : Countable ι
μ : Measure X
inst✝⁴ : NormedAddCommGroup E
inst✝³ : TopologicalSpace X
inst✝² : BorelSpace X
inst✝¹ : MetrizableSpace X
inst✝ : IsLocallyFiniteMeasure μ
f : C(X, E)
s : ι → Compacts X
hf : Summable fun i => ‖ContinuousMap.restrict (↑(s i)) f‖ * (μ ↑(s i)).toReal
i : ι
⊢ ‖∫ (x : X) in ↑(s i), ‖f x‖ ∂μ‖ ≤ ‖ContinuousMap.restrict (↑(s i)) f‖ * (μ ↑(s i)).toReal

Proof state:
X : Type u_1
E : Type u_3
mX : MeasurableSpace X
ι : Type u_5
inst✝⁵ : Countable ι
μ : Measure X
inst✝⁴ : NormedAddCommGroup E
inst✝³ : TopologicalSpace X
inst✝² : BorelSpace X
inst✝¹ : MetrizableSpace X
inst✝ : IsLocallyFiniteMeasure μ
f : C(X, E)
s : ι → Compacts X
hf : Summable fun i => ‖ContinuousMap.restrict (↑(s i)) f‖ * (μ ↑(s i)).toReal
⊢ IntegrableOn (⇑f) (⋃ i, ↑(s i)) μ

Tactic:
refine
  integrableOn_iUnion_of_summable_integral_norm (fun i => (s i).isCompact.isClosed.measurableSet)
    (fun i => (map_continuous f).continuousOn.integrableOn_compact (s i).isCompact)
    (.of_nonneg_of_le (fun ι => integral_nonneg fun x => norm_nonneg _) (fun i => ?_) hf)

Result:
X : Type u_1
E : Type u_3
mX : MeasurableSpace X
ι : Type u_5
inst✝⁵ : Countable ι
μ : Measure X
inst✝⁴ : NormedAddCommGroup E
inst✝³ : TopologicalSpace X
inst✝² : BorelSpace X
inst✝¹ : MetrizableSpace X
inst✝ : IsLocallyFiniteMeasure μ
f : C(X, E)
s : ι → Compacts X
hf : Summable fun i => ‖ContinuousMap.restrict (↑(s i)) f‖ * (μ ↑(s i)).toReal
i : ι
⊢ ∫ (x : X) in ↑(s i), ‖f x‖ ∂μ ≤ ‖ContinuousMap.restrict (↑(s i)) f‖ * (μ ↑(s i)).toReal
-- Mathlib/CategoryTheory/SmallObject/Iteration/ExtendToSucc.lean
lemma map_comp (i₁ i₂ i₃ : J) (h₁₂ : i₁ ≤ i₂) (h₂₃ : i₂ ≤ i₃) (h : i₃ ≤ Order.succ j) :
    map hj F τ i₁ i₃ (h₁₂.trans h₂₃) h =
      map hj F τ i₁ i₂ h₁₂ (h₂₃.trans h) ≫ map hj F τ i₂ i₃ h₂₃ h

Proof state:
case neg.inl
C : Type u_1
inst✝² : Category.{u_2, u_1} C
J : Type u
inst✝¹ : LinearOrder J
inst✝ : SuccOrder J
j : J
hj : ¬IsMax j
F : ↑(Set.Iic j) ⥤ C
X : C
τ : F.obj ⟨j, ⋯⟩ ⟶ X
i₁ i₂ : J
h₁₂ : i₁ ≤ i₂
h₂₃ : i₂ ≤ Order.succ j
h : Order.succ j ≤ Order.succ j
h₁ : ¬Order.succ j ≤ j
h₂ : i₂ ≤ j
⊢ (if h₁ : Order.succ j ≤ j then (objIso F X ⟨i₁, ⋯⟩).hom ≫ F.map (homOfLE ⋯) ≫ (objIso F X ⟨Order.succ j, h₁⟩).inv
    else
      if h₂ : i₁ ≤ j then
        (objIso F X ⟨i₁, h₂⟩).hom ≫ F.map (homOfLE h₂) ≫ τ ≫ (objSuccIso hj F X).inv ≫ 𝟙 (obj F X ⟨Order.succ j, ⋯⟩)
      else eqToHom ⋯) =
    ((objIso F X ⟨i₁, ⋯⟩).hom ≫ F.map (homOfLE h₁₂) ≫ (objIso F X ⟨i₂, h₂⟩).inv) ≫
      if h₁ : Order.succ j ≤ j then (objIso F X ⟨i₂, ⋯⟩).hom ≫ F.map (homOfLE h₂₃) ≫ (objIso F X ⟨Order.succ j, h₁⟩).inv
      else
        if h₂ : i₂ ≤ j then
          (objIso F X ⟨i₂, h₂⟩).hom ≫ F.map (homOfLE h₂) ≫ τ ≫ (objSuccIso hj F X).inv ≫ 𝟙 (obj F X ⟨Order.succ j, ⋯⟩)
        else eqToHom ⋯

Tactic:
rw [dif_neg h₁, dif_pos (h₁₂.trans h₂), dif_neg h₁, dif_pos h₂, assoc, assoc,
  Iso.inv_hom_id_assoc,comp_id, ← Functor.map_comp_assoc, homOfLE_comp]

Result:
no goals
-- Mathlib/LinearAlgebra/Vandermonde.lean
theorem vandermonde_mul_vandermonde_transpose {n : ℕ} (v w : Fin n → R) (i j) :
    (vandermonde v * (vandermonde w)ᵀ) i j = ∑ k : Fin n, (v i * w j) ^ (k : ℕ)

Proof state:
R : Type u_1
inst✝ : CommRing R
n : ℕ
v w : Fin n → R
i j : Fin n
⊢ (vandermonde v * (vandermonde w)ᵀ) i j = ∑ k : Fin n, (v i * w j) ^ ↑k

Tactic:
simp only [vandermonde_apply, Matrix.mul_apply, Matrix.transpose_apply, mul_pow]

Result:
no goals