harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Data/Finset/Disjoint.lean
theorem mem_disjUnion {α s t h a} : a ∈ @disjUnion α s t h ↔ a ∈ s ∨ a ∈ t

Proof state:
α : Type u_4
s t : Finset α
h : Disjoint s t
a : α
⊢ a ∈ s.disjUnion t h ↔ a ∈ s ∨ a ∈ t

Tactic:
rcases s with ⟨⟨s⟩⟩

Result:
case mk.mk
α : Type u_4
t : Finset α
a : α
val✝ : Multiset α
s : List α
nodup✝ : Nodup (Quot.mk (⇑(List.isSetoid α)) s)
h : Disjoint { val := Quot.mk (⇑(List.isSetoid α)) s, nodup := nodup✝ } t
⊢ a ∈ { val := Quot.mk (⇑(List.isSetoid α)) s, nodup := nodup✝ }.disjUnion t h ↔
    a ∈ { val := Quot.mk (⇑(List.isSetoid α)) s, nodup := nodup✝ } ∨ a ∈ t

Proof state:
case mk.mk
α : Type u_4
t : Finset α
a : α
val✝ : Multiset α
s : List α
nodup✝ : Nodup (Quot.mk (⇑(List.isSetoid α)) s)
h : Disjoint { val := Quot.mk (⇑(List.isSetoid α)) s, nodup := nodup✝ } t
⊢ a ∈ { val := Quot.mk (⇑(List.isSetoid α)) s, nodup := nodup✝ }.disjUnion t h ↔
    a ∈ { val := Quot.mk (⇑(List.isSetoid α)) s, nodup := nodup✝ } ∨ a ∈ t

Tactic:
rcases t with ⟨⟨t⟩⟩

Result:
case mk.mk.mk.mk
α : Type u_4
a : α
val✝¹ : Multiset α
s : List α
nodup✝¹ : Nodup (Quot.mk (⇑(List.isSetoid α)) s)
val✝ : Multiset α
t : List α
nodup✝ : Nodup (Quot.mk (⇑(List.isSetoid α)) t)
h :
  Disjoint { val := Quot.mk (⇑(List.isSetoid α)) s, nodup := nodup✝¹ }
    { val := Quot.mk (⇑(List.isSetoid α)) t, nodup := nodup✝ }
⊢ a ∈
      { val := Quot.mk (⇑(List.isSetoid α)) s, nodup := nodup✝¹ }.disjUnion
        { val := Quot.mk (⇑(List.isSetoid α)) t, nodup := nodup✝ } h ↔
    a ∈ { val := Quot.mk (⇑(List.isSetoid α)) s, nodup := nodup✝¹ } ∨
      a ∈ { val := Quot.mk (⇑(List.isSetoid α)) t, nodup := nodup✝ }

Proof state:
case mk.mk.mk.mk
α : Type u_4
a : α
val✝¹ : Multiset α
s : List α
nodup✝¹ : Nodup (Quot.mk (⇑(List.isSetoid α)) s)
val✝ : Multiset α
t : List α
nodup✝ : Nodup (Quot.mk (⇑(List.isSetoid α)) t)
h :
  Disjoint { val := Quot.mk (⇑(List.isSetoid α)) s, nodup := nodup✝¹ }
    { val := Quot.mk (⇑(List.isSetoid α)) t, nodup := nodup✝ }
⊢ a ∈
      { val := Quot.mk (⇑(List.isSetoid α)) s, nodup := nodup✝¹ }.disjUnion
        { val := Quot.mk (⇑(List.isSetoid α)) t, nodup := nodup✝ } h ↔
    a ∈ { val := Quot.mk (⇑(List.isSetoid α)) s, nodup := nodup✝¹ } ∨
      a ∈ { val := Quot.mk (⇑(List.isSetoid α)) t, nodup := nodup✝ }

Tactic:
apply List.mem_append

Result:
no goals
-- Mathlib/Probability/Kernel/Composition/CompProd.lean
theorem compProd_null (a : α) (hs : MeasurableSet s) :
    (κ ⊗ₖ η) a s = 0 ↔ (fun b => η (a, b) (Prod.mk b ⁻¹' s)) =ᵐ[κ a] 0

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
s : Set (β × γ)
κ : Kernel α β
inst✝¹ : IsSFiniteKernel κ
η : Kernel (α × β) γ
inst✝ : IsSFiniteKernel η
a : α
hs : MeasurableSet s
⊢ ((κ ⊗ₖ η) a) s = 0 ↔ (fun b => (η (a, b)) (Prod.mk b ⁻¹' s)) =ᶠ[ae (κ a)] 0

Tactic:
rw [Kernel.compProd_apply hs, lintegral_eq_zero_iff]

Result:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
s : Set (β × γ)
κ : Kernel α β
inst✝¹ : IsSFiniteKernel κ
η : Kernel (α × β) γ
inst✝ : IsSFiniteKernel η
a : α
hs : MeasurableSet s
⊢ (fun b => (η (a, b)) {c | (b, c) ∈ s}) =ᶠ[ae (κ a)] 0 ↔ (fun b => (η (a, b)) (Prod.mk b ⁻¹' s)) =ᶠ[ae (κ a)] 0

α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
s : Set (β × γ)
κ : Kernel α β
inst✝¹ : IsSFiniteKernel κ
η : Kernel (α × β) γ
inst✝ : IsSFiniteKernel η
a : α
hs : MeasurableSet s
⊢ Measurable fun b => (η (a, b)) {c | (b, c) ∈ s}

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
s : Set (β × γ)
κ : Kernel α β
inst✝¹ : IsSFiniteKernel κ
η : Kernel (α × β) γ
inst✝ : IsSFiniteKernel η
a : α
hs : MeasurableSet s
⊢ Measurable fun b => (η (a, b)) {c | (b, c) ∈ s}

Tactic:
exact Kernel.measurable_kernel_prod_mk_left' hs a

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
s : Set (β × γ)
κ : Kernel α β
inst✝¹ : IsSFiniteKernel κ
η : Kernel (α × β) γ
inst✝ : IsSFiniteKernel η
a : α
hs : MeasurableSet s
⊢ (fun b => (η (a, b)) {c | (b, c) ∈ s}) =ᶠ[ae (κ a)] 0 ↔ (fun b => (η (a, b)) (Prod.mk b ⁻¹' s)) =ᶠ[ae (κ a)] 0

Tactic:
rfl

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Nat/Lemmas.lean
theorem pow_pred_mul {x w : Nat} (h : 0 < w) :
    x ^ (w - 1) * x = x ^ w

Proof state:
x w : Nat
h : 0 < w
⊢ x ^ (w - 1) * x = x ^ w

Tactic:
simp [← Nat.pow_succ, succ_eq_add_one, Nat.sub_add_cancel h]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Zip.lean
theorem zipWith_self (f : α → α → δ) (l : Array α) : zipWith f l l = l.map fun a => f a a

Proof state:
case mk
α : Type u_1
δ : Type u_2
f : α → α → δ
toList✝ : List α
⊢ zipWith f { toList := toList✝ } { toList := toList✝ } = map (fun a => f a a) { toList := toList✝ }

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
δ : Type u_2
f : α → α → δ
l : Array α
⊢ zipWith f l l = map (fun a => f a a) l

Tactic:
cases l

Result:
case mk
α : Type u_1
δ : Type u_2
f : α → α → δ
toList✝ : List α
⊢ zipWith f { toList := toList✝ } { toList := toList✝ } = map (fun a => f a a) { toList := toList✝ }
-- Mathlib/Data/Nat/Init.lean
/-- special case of `mul_dvd_mul_iff_right` for `ℕ`.
Duplicated here to keep simple imports for this file. -/
protected lemma mul_dvd_mul_iff_right (hc : 0 < c) : a * c ∣ b * c ↔ a ∣ b :=
  exists_congr fun d ↦ by rw [Nat.mul_right_comm, Nat.mul_left_inj <| ne_of_gt hc]

Proof state:
a b c : ℕ
hc : 0 < c
d : ℕ
⊢ b * c = a * c * d ↔ b = a * d

Tactic:
rw [Nat.mul_right_comm, Nat.mul_left_inj <| ne_of_gt hc]

Result:
no goals
-- Mathlib/CategoryTheory/Limits/Shapes/Images.lean
theorem image.map_ι : image.map sq ≫ image.ι g.hom = image.ι f.hom ≫ sq.right

Proof state:
C : Type u
inst✝³ : Category.{v, u} C
f g : Arrow C
inst✝² : HasImage f.hom
inst✝¹ : HasImage g.hom
sq : f ⟶ g
inst✝ : HasImageMap sq
⊢ map sq ≫ ι g.hom = ι f.hom ≫ sq.right

Tactic:
simp

Result:
no goals
-- Mathlib/Analysis/Calculus/ContDiff/Basic.lean
theorem LinearIsometry.norm_iteratedFDeriv_comp_left {f : E → F} (g : F →ₗᵢ[𝕜] G)
    (hf : ContDiffAt 𝕜 n f x) {i : ℕ} (hi : i ≤ n) :
    ‖iteratedFDeriv 𝕜 i (g ∘ f) x‖ = ‖iteratedFDeriv 𝕜 i f x‖

Proof state:
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type uE
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type uF
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
G : Type uG
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
x : E
n : WithTop ℕ∞
f : E → F
g : F →ₗᵢ[𝕜] G
hf : ContDiffAt 𝕜 n f x
i : ℕ
hi : ↑i ≤ n
⊢ ‖iteratedFDeriv 𝕜 i (⇑g ∘ f) x‖ = ‖iteratedFDeriv 𝕜 i f x‖

Tactic:
simp only [← iteratedFDerivWithin_univ]

Result:
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type uE
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type uF
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
G : Type uG
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
x : E
n : WithTop ℕ∞
f : E → F
g : F →ₗᵢ[𝕜] G
hf : ContDiffAt 𝕜 n f x
i : ℕ
hi : ↑i ≤ n
⊢ ‖iteratedFDerivWithin 𝕜 i (⇑g ∘ f) univ x‖ = ‖iteratedFDerivWithin 𝕜 i f univ x‖

Proof state:
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type uE
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type uF
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
G : Type uG
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
x : E
n : WithTop ℕ∞
f : E → F
g : F →ₗᵢ[𝕜] G
hf : ContDiffAt 𝕜 n f x
i : ℕ
hi : ↑i ≤ n
⊢ ‖iteratedFDerivWithin 𝕜 i (⇑g ∘ f) univ x‖ = ‖iteratedFDerivWithin 𝕜 i f univ x‖

Tactic:
exact g.norm_iteratedFDerivWithin_comp_left hf.contDiffWithinAt uniqueDiffOn_univ (mem_univ x) hi

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/SimpLemmas.lean
theorem bne_iff_ne [BEq α] [LawfulBEq α] {a b : α} : a != b ↔ a ≠ b

Proof state:
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
a b : α
⊢ (a == b) = false ↔ ¬a = b

Tactic:
rw [← beq_iff_eq (a := a) (b := b)]

Result:
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
a b : α
⊢ (a == b) = false ↔ ¬(a == b) = true

Proof state:
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
a b : α
⊢ (a == b) = false ↔ ¬(a == b) = true

Tactic:
simp [-beq_iff_eq]

Result:
no goals

Proof state:
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
a b : α
⊢ (a != b) = true ↔ a ≠ b

Tactic:
simp [bne]

Result:
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
a b : α
⊢ (a == b) = false ↔ ¬a = b
-- Mathlib/Data/Finset/Sups.lean
theorem disjSups_union_left : (s₁ ∪ s₂) ○ t = s₁ ○ t ∪ s₂ ○ t

Proof state:
α : Type u_2
inst✝³ : DecidableEq α
inst✝² : SemilatticeSup α
inst✝¹ : OrderBot α
inst✝ : DecidableRel Disjoint
s₁ s₂ t : Finset α
⊢ (s₁ ∪ s₂) ○ t = s₁ ○ t ∪ s₂ ○ t

Tactic:
simp [disjSups, filter_union, image_union]

Result:
no goals
-- Mathlib/Data/Set/Function.lean
lemma BijOn.forall {p : β → Prop} (hf : BijOn f s t) : (∀ b ∈ t, p b) ↔ ∀ a ∈ s, p (f a) where
  mp h _ ha := h _ <| hf.mapsTo ha
  mpr h b hb

Proof state:
α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : α → β
p : β → Prop
hf : BijOn f s t
h : ∀ a ∈ s, p (f a)
b : β
hb : b ∈ t
⊢ p b

Tactic:
obtain ⟨a, ha, rfl⟩ := hf.surjOn hb

Result:
case intro.intro
α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : α → β
p : β → Prop
hf : BijOn f s t
h : ∀ a ∈ s, p (f a)
a : α
ha : a ∈ s
hb : f a ∈ t
⊢ p (f a)

Proof state:
case intro.intro
α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : α → β
p : β → Prop
hf : BijOn f s t
h : ∀ a ∈ s, p (f a)
a : α
ha : a ∈ s
hb : f a ∈ t
⊢ p (f a)

Tactic:
exact h _ ha

Result:
no goals
-- Mathlib/Algebra/Order/BigOperators/Ring/Finset.lean
/-- If each `f i`, `i ∈ s` belongs to `[0, 1]`, then their product is less than or equal to one.
See also `Finset.prod_le_one'` for the case of an ordered commutative multiplicative monoid. -/
lemma prod_le_one (h0 : ∀ i ∈ s, 0 ≤ f i) (h1 : ∀ i ∈ s, f i ≤ 1) : ∏ i ∈ s, f i ≤ 1

Proof state:
ι : Type u_1
R : Type u_2
inst✝³ : CommMonoidWithZero R
inst✝² : PartialOrder R
inst✝¹ : ZeroLEOneClass R
inst✝ : PosMulMono R
f : ι → R
s : Finset ι
h0 : ∀ i ∈ s, 0 ≤ f i
h1 : ∀ i ∈ s, f i ≤ 1
⊢ ∏ i ∈ s, f i ≤ 1

Tactic:
convert ← prod_le_prod h0 h1

Result:
case h.e'_4
ι : Type u_1
R : Type u_2
inst✝³ : CommMonoidWithZero R
inst✝² : PartialOrder R
inst✝¹ : ZeroLEOneClass R
inst✝ : PosMulMono R
f : ι → R
s : Finset ι
h0 : ∀ i ∈ s, 0 ≤ f i
h1 : ∀ i ∈ s, f i ≤ 1
⊢ ∏ i ∈ s, 1 = 1

Proof state:
case h.e'_4
ι : Type u_1
R : Type u_2
inst✝³ : CommMonoidWithZero R
inst✝² : PartialOrder R
inst✝¹ : ZeroLEOneClass R
inst✝ : PosMulMono R
f : ι → R
s : Finset ι
h0 : ∀ i ∈ s, 0 ≤ f i
h1 : ∀ i ∈ s, f i ≤ 1
⊢ ∏ i ∈ s, 1 = 1

Tactic:
exact Finset.prod_const_one

Result:
no goals
-- Mathlib/Topology/Bases.lean
theorem isOpen_biUnion_countable [SecondCountableTopology α] {ι : Type*} (I : Set ι) (s : ι → Set α)
    (H : ∀ i ∈ I, IsOpen (s i)) : ∃ T ⊆ I, T.Countable ∧ ⋃ i ∈ T, s i = ⋃ i ∈ I, s i

Proof state:
α : Type u
t : TopologicalSpace α
inst✝ : SecondCountableTopology α
ι : Type u_1
I : Set ι
s : ι → Set α
H : ∀ i ∈ I, IsOpen (s i)
⊢ ∃ s_1, (Subtype.val '' s_1).Countable ∧ ⋃ y ∈ s_1, s ↑y = ⋃ i ∈ I, s i

Tactic:
rcases isOpen_iUnion_countable (fun i : I ↦ s i) fun i ↦ H i i.2 with ⟨T, hTc, hU⟩

Result:
case intro.intro
α : Type u
t : TopologicalSpace α
inst✝ : SecondCountableTopology α
ι : Type u_1
I : Set ι
s : ι → Set α
H : ∀ i ∈ I, IsOpen (s i)
T : Set ↑I
hTc : T.Countable
hU : ⋃ i ∈ T, s ↑i = ⋃ i, s ↑i
⊢ ∃ s_1, (Subtype.val '' s_1).Countable ∧ ⋃ y ∈ s_1, s ↑y = ⋃ i ∈ I, s i

Proof state:
α : Type u
t : TopologicalSpace α
inst✝ : SecondCountableTopology α
ι : Type u_1
I : Set ι
s : ι → Set α
H : ∀ i ∈ I, IsOpen (s i)
⊢ ∃ T ⊆ I, T.Countable ∧ ⋃ i ∈ T, s i = ⋃ i ∈ I, s i

Tactic:
simp_rw [← Subtype.exists_set_subtype, biUnion_image]

Result:
α : Type u
t : TopologicalSpace α
inst✝ : SecondCountableTopology α
ι : Type u_1
I : Set ι
s : ι → Set α
H : ∀ i ∈ I, IsOpen (s i)
⊢ ∃ s_1, (Subtype.val '' s_1).Countable ∧ ⋃ y ∈ s_1, s ↑y = ⋃ i ∈ I, s i

Proof state:
case intro.intro
α : Type u
t : TopologicalSpace α
inst✝ : SecondCountableTopology α
ι : Type u_1
I : Set ι
s : ι → Set α
H : ∀ i ∈ I, IsOpen (s i)
T : Set ↑I
hTc : T.Countable
hU : ⋃ i ∈ T, s ↑i = ⋃ i, s ↑i
⊢ ∃ s_1, (Subtype.val '' s_1).Countable ∧ ⋃ y ∈ s_1, s ↑y = ⋃ i ∈ I, s i

Tactic:
exact ⟨T, hTc.image _, hU.trans <| iUnion_subtype ..⟩

Result:
no goals
-- Mathlib/Combinatorics/SetFamily/AhlswedeZhang.lean
private lemma upper_aux [DecidableEq α] :
    a ∈ upperClosure ↑(s ∪ t) ↔ a ∈ upperClosure s ∨ a ∈ upperClosure t

Proof state:
α : Type u_1
inst✝¹ : SemilatticeInf α
s t : Finset α
a : α
inst✝ : DecidableEq α
⊢ a ∈ upperClosure ↑(s ∪ t) ↔ a ∈ upperClosure ↑s ∨ a ∈ upperClosure ↑t

Tactic:
rw [coe_union, upperClosure_union, UpperSet.mem_inf_iff]

Result:
no goals
-- Mathlib/Order/Interval/Set/WithBotTop.lean
theorem image_coe_Ico : (some : α → WithBot α) '' Ico a b = Ico (a : WithBot α) b

Proof state:
α : Type u_1
inst✝ : Preorder α
a b : α
⊢ some '' Ico a b = Ico ↑a ↑b

Tactic:
rw [← preimage_coe_Ico, image_preimage_eq_inter_range, range_coe,
  inter_eq_self_of_subset_left
    (Subset.trans Ico_subset_Ici_self <| Ici_subset_Ioi.2 <| bot_lt_coe a)]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Trigonometric/Bounds.lean
lemma lt_sin (hx : x < 0) : x < sin x

Proof state:
x : ℝ
hx : x < 0
⊢ x < sin x

Tactic:
simpa using sin_lt <| neg_pos.2 hx

Result:
no goals
-- Mathlib/CategoryTheory/Products/Basic.lean
@[ext]
lemma prod.hom_ext {X Y : C × D} {f g : X ⟶ Y} (h₁ : f.1 = g.1) (h₂ : f.2 = g.2) : f = g

Proof state:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
X Y : C × D
f g : X ⟶ Y
h₁ : f.1 = g.1
h₂ : f.2 = g.2
⊢ f = g

Tactic:
ext <;> assumption

Result:
no goals
-- Mathlib/RingTheory/Polynomial/Basic.lean
theorem restriction_one : restriction (1 : R[X]) = 1 :=
  ext fun i => Subtype.eq <| by rw [coeff_restriction', coeff_one, coeff_one]; split_ifs <;> rfl

Proof state:
R : Type u
inst✝ : Ring R
i : ℕ
⊢ ↑((restriction 1).coeff i) = ↑(coeff 1 i)

Tactic:
rw [coeff_restriction', coeff_one, coeff_one]

Result:
R : Type u
inst✝ : Ring R
i : ℕ
⊢ (if i = 0 then 1 else 0) = ↑(if i = 0 then 1 else 0)

Proof state:
R : Type u
inst✝ : Ring R
i : ℕ
⊢ (if i = 0 then 1 else 0) = ↑(if i = 0 then 1 else 0)

Tactic:
split_ifs <;> rfl

Result:
no goals
-- Mathlib/Computability/PartrecCode.lean
theorem encode_lt_rfind' (cf) : encode cf < encode (rfind' cf)

Proof state:
cf : Code
⊢ cf.encodeCode < 2 * (2 * cf.encodeCode + 1) + 1 + 4

Tactic:
omega

Result:
no goals

Proof state:
cf : Code
⊢ encode cf < encode cf.rfind'

Tactic:
simp only [encodeCode_eq, encodeCode]

Result:
cf : Code
⊢ cf.encodeCode < 2 * (2 * cf.encodeCode + 1) + 1 + 4
-- Mathlib/Algebra/Group/Submonoid/BigOperators.lean
theorem multiset_noncommProd_mem (S : Submonoid M) (m : Multiset M) (comm) (h : ∀ x ∈ m, x ∈ S) :
    m.noncommProd comm ∈ S

Proof state:
case h
M : Type u_1
inst✝ : Monoid M
S : Submonoid M
l : List M
comm : {x | x ∈ ⟦l⟧}.Pairwise Commute
h : ∀ x ∈ ⟦l⟧, x ∈ S
⊢ l.prod ∈ S

Tactic:
exact Submonoid.list_prod_mem _ h

Result:
no goals

Proof state:
M : Type u_1
inst✝ : Monoid M
S : Submonoid M
m : Multiset M
comm : {x | x ∈ m}.Pairwise Commute
h : ∀ x ∈ m, x ∈ S
⊢ m.noncommProd comm ∈ S

Tactic:
induction m using Quotient.inductionOn with | h l => ?_

Result:
case h
M : Type u_1
inst✝ : Monoid M
S : Submonoid M
l : List M
comm : {x | x ∈ ⟦l⟧}.Pairwise Commute
h : ∀ x ∈ ⟦l⟧, x ∈ S
⊢ Multiset.noncommProd ⟦l⟧ comm ∈ S

Proof state:
case h
M : Type u_1
inst✝ : Monoid M
S : Submonoid M
l : List M
comm : {x | x ∈ ⟦l⟧}.Pairwise Commute
h : ∀ x ∈ ⟦l⟧, x ∈ S
⊢ Multiset.noncommProd ⟦l⟧ comm ∈ S

Tactic:
simp only [Multiset.quot_mk_to_coe, Multiset.noncommProd_coe]

Result:
case h
M : Type u_1
inst✝ : Monoid M
S : Submonoid M
l : List M
comm : {x | x ∈ ⟦l⟧}.Pairwise Commute
h : ∀ x ∈ ⟦l⟧, x ∈ S
⊢ l.prod ∈ S
-- Mathlib/Data/Real/EReal.lean
lemma mul_div_cancel (h₁ : b ≠ ⊥) (h₂ : b ≠ ⊤) (h₃ : b ≠ 0) : b * (a / b) = a

Proof state:
a b : EReal
h₁ : b ≠ ⊥
h₂ : b ≠ ⊤
h₃ : b ≠ 0
⊢ b * (a / b) = a

Tactic:
rw [mul_comm, div_mul_cancel h₁ h₂ h₃]

Result:
no goals
-- Mathlib/RingTheory/Flat/Equalizer.lean
@[simp]
lemma LinearMap.tensorEqLocus_coe (x : M ⊗[R] (LinearMap.eqLocus f g)) :
    (tensorEqLocus S M f g x : M ⊗[R] N) = (eqLocus f g).subtype.lTensor M x

Proof state:
R : Type u_1
S : Type u_2
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing S
inst✝⁸ : Algebra R S
M : Type u_3
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : Module S M
inst✝⁴ : IsScalarTower R S M
N : Type u_4
P : Type u_5
inst✝³ : AddCommGroup N
inst✝² : AddCommGroup P
inst✝¹ : Module R N
inst✝ : Module R P
f g : N →ₗ[R] P
x : M ⊗[R] ↥(eqLocus f g)
⊢ ↑((tensorEqLocus S M f g) x) = (lTensor M (eqLocus f g).subtype) x

Tactic:
induction x <;> simp_all

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Find.lean
theorem findSome?_replicate_of_pos (h : 0 < n) : findSome? f (replicate n a) = f a

Proof state:
n : Nat
α✝¹ : Type u_1
α✝ : Type u_2
f : α✝¹ → Option α✝
a : α✝¹
h : 0 < n
⊢ findSome? f (replicate n a) = f a

Tactic:
simp [findSome?_replicate, Nat.ne_of_gt h]

Result:
no goals
-- Mathlib/RingTheory/MvPolynomial/Symmetric/NewtonIdentities.lean
private lemma filter_pairs_lt (k : ℕ) :
    (pairs σ k).filter (fun (s, _) ↦ #s < k) =
      (range k).disjiUnion (powersetCard · univ) ((pairwise_disjoint_powersetCard _).set_pairwise _)
        ×ˢ univ

Proof state:
σ : Type u_1
inst✝¹ : DecidableEq σ
inst✝ : Fintype σ
k : ℕ
⊢ filter
      (fun x =>
        match x with
        | (s, snd) => #s < k)
      (MvPolynomial.NewtonIdentities.pairs σ k) =
    (range k).disjiUnion (fun x => powersetCard x univ) ⋯ ×ˢ univ

Tactic:
ext

Result:
case h
σ : Type u_1
inst✝¹ : DecidableEq σ
inst✝ : Fintype σ
k : ℕ
a✝ : Finset σ × σ
⊢ a✝ ∈
      filter
        (fun x =>
          match x with
          | (s, snd) => #s < k)
        (MvPolynomial.NewtonIdentities.pairs σ k) ↔
    a✝ ∈ (range k).disjiUnion (fun x => powersetCard x univ) ⋯ ×ˢ univ

Proof state:
case h
σ : Type u_1
inst✝¹ : DecidableEq σ
inst✝ : Fintype σ
k : ℕ
a✝ : Finset σ × σ
⊢ a✝ ∈
      filter
        (fun x =>
          match x with
          | (s, snd) => #s < k)
        (MvPolynomial.NewtonIdentities.pairs σ k) ↔
    a✝ ∈ (range k).disjiUnion (fun x => powersetCard x univ) ⋯ ×ˢ univ

Tactic:
aesop (add unsafe le_of_lt)

Result:
no goals
-- Mathlib/Analysis/Normed/Lp/ProdLp.lean
theorem prod_norm_eq_of_L1 (x : WithLp 1 (α × β)) :
    ‖x‖ = ‖x.fst‖ + ‖x.snd‖

Proof state:
α : Type u_2
β : Type u_3
inst✝¹ : SeminormedAddCommGroup α
inst✝ : SeminormedAddCommGroup β
x : WithLp 1 (α × β)
⊢ ‖x‖ = ‖x.1‖ + ‖x.2‖

Tactic:
simp [prod_norm_eq_add]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/RawLemmas.lean
theorem get?_eq_some_getD [EquivBEq α] [LawfulHashable α] (h : m.WF) {a : α} {fallback : β} :
    a ∈ m → get? m a = some (getD m a fallback)

Proof state:
α : Type u
inst✝³ : BEq α
inst✝² : Hashable α
β : Type v
m : Raw α fun x => β
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
h : m.WF
a : α
fallback : β
⊢ a ∈ m → get? m a = some (getD m a fallback)

Tactic:
simpa [mem_iff_contains] using get?_eq_some_getD_of_contains h

Result:
no goals
-- Mathlib/Order/Interval/Finset/Basic.lean
theorem filter_lt_lt_eq_Ioo [DecidablePred fun j => a < j ∧ j < b] :
    ({j | a < j ∧ j < b} : Finset _) = Ioo a b

Proof state:
case h
α : Type u_2
a b : α
inst✝³ : Preorder α
inst✝² : LocallyFiniteOrder α
inst✝¹ : Fintype α
inst✝ : DecidablePred fun j => a < j ∧ j < b
a✝ : α
⊢ a✝ ∈ filter (fun j => a < j ∧ j < b) univ ↔ a✝ ∈ Ioo a b

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_2
a b : α
inst✝³ : Preorder α
inst✝² : LocallyFiniteOrder α
inst✝¹ : Fintype α
inst✝ : DecidablePred fun j => a < j ∧ j < b
⊢ filter (fun j => a < j ∧ j < b) univ = Ioo a b

Tactic:
ext

Result:
case h
α : Type u_2
a b : α
inst✝³ : Preorder α
inst✝² : LocallyFiniteOrder α
inst✝¹ : Fintype α
inst✝ : DecidablePred fun j => a < j ∧ j < b
a✝ : α
⊢ a✝ ∈ filter (fun j => a < j ∧ j < b) univ ↔ a✝ ∈ Ioo a b
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/RawLemmas.lean
theorem get?_eq_some_get! [EquivBEq α] [LawfulHashable α] [Inhabited β] (h : m.1.WF) {a : α} :
    m.contains a = true → get? m a = some (get! m a)

Proof state:
α : Type u
inst✝⁴ : BEq α
inst✝³ : Hashable α
β : Type v
m : Raw₀ α fun x => β
inst✝² : EquivBEq α
inst✝¹ : LawfulHashable α
inst✝ : Inhabited β
h : m.val.WF
a : α
⊢ m.contains a = true → get? m a = some (get! m a)

Tactic:
simp_to_model using List.getValue?_eq_some_getValue!

Result:
no goals
-- Mathlib/FieldTheory/Minpoly/MinpolyDiv.lean
lemma natDegree_minpolyDiv :
    natDegree (minpolyDiv R x) = natDegree (minpoly R x) - 1

Proof state:
R : Type u_2
S : Type u_1
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
x : S
a✝ : Nontrivial S
⊢ (minpolyDiv R x).natDegree = (minpoly R x).natDegree - 1

Tactic:
by_cases hx : IsIntegral R x

Result:
case pos
R : Type u_2
S : Type u_1
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
x : S
a✝ : Nontrivial S
hx : IsIntegral R x
⊢ (minpolyDiv R x).natDegree = (minpoly R x).natDegree - 1

case neg
R : Type u_2
S : Type u_1
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
x : S
a✝ : Nontrivial S
hx : ¬IsIntegral R x
⊢ (minpolyDiv R x).natDegree = (minpoly R x).natDegree - 1

Proof state:
case pos
R : Type u_2
S : Type u_1
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
x : S
a✝ : Nontrivial S
hx : IsIntegral R x
⊢ (minpolyDiv R x).natDegree = (minpolyDiv R x).natDegree + 1 - 1

Tactic:
rfl

Result:
no goals

Proof state:
case neg
R : Type u_2
S : Type u_1
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
x : S
a✝ : Nontrivial S
hx : ¬IsIntegral R x
⊢ natDegree 0 = natDegree 0 - 1

Tactic:
rfl

Result:
no goals

Proof state:
case neg
R : Type u_2
S : Type u_1
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
x : S
a✝ : Nontrivial S
hx : ¬IsIntegral R x
⊢ (minpolyDiv R x).natDegree = (minpoly R x).natDegree - 1

Tactic:
rw [minpolyDiv_eq_zero hx, minpoly.eq_zero hx]

Result:
case neg
R : Type u_2
S : Type u_1
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
x : S
a✝ : Nontrivial S
hx : ¬IsIntegral R x
⊢ natDegree 0 = natDegree 0 - 1

Proof state:
case pos
R : Type u_2
S : Type u_1
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
x : S
a✝ : Nontrivial S
hx : IsIntegral R x
⊢ (minpolyDiv R x).natDegree = (minpoly R x).natDegree - 1

Tactic:
rw [← natDegree_minpolyDiv_succ hx]

Result:
case pos
R : Type u_2
S : Type u_1
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
x : S
a✝ : Nontrivial S
hx : IsIntegral R x
⊢ (minpolyDiv R x).natDegree = (minpolyDiv R x).natDegree + 1 - 1

Proof state:
R : Type u_2
S : Type u_1
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
x : S
⊢ (minpolyDiv R x).natDegree = (minpoly R x).natDegree - 1

Tactic:
nontriviality S

Result:
R : Type u_2
S : Type u_1
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
x : S
a✝ : Nontrivial S
⊢ (minpolyDiv R x).natDegree = (minpoly R x).natDegree - 1
-- Mathlib/Data/Vector/MapLemmas.lean
theorem map_mapAccumr {s : σ₂} (f₁ : β → γ) :
    (map f₁ (mapAccumr f₂ xs s).snd) = (mapAccumr (fun x s =>
        let r := (f₂ x s); (r.fst, f₁ r.snd)
      ) xs s).snd

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
σ₂ : Type u_7
n : ℕ
xs : Vector α n
f₂ : α → σ₂ → σ₂ × β
s : σ₂
f₁ : β → γ
⊢ map f₁ (mapAccumr f₂ xs s).2 =
    (mapAccumr
        (fun x s =>
          let r := f₂ x s;
          (r.1, f₁ r.2))
        xs s).2

Tactic:
induction xs using Vector.revInductionOn generalizing s <;> simp_all

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Nat/Lcm.lean
theorem lcm_zero_left (m : Nat) : lcm 0 m = 0

Proof state:
m : Nat
⊢ lcm 0 m = 0

Tactic:
simp [lcm]

Result:
no goals