harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/.lake/packages/batteries/Batteries/Data/List/Lemmas.lean
theorem set_eq_modify (a : α) : ∀ n (l : List α), set l n a = modify (fun _ => a) n l
  | 0, l => by cases l <;> rfl
  | _+1, [] => rfl
  | _+1, _ :: _ => congrArg (cons _) (set_eq_modify _ _ _)

Proof state:
α : Type u_1
a : α
l : List α
⊢ l.set 0 a = modify (fun x => a) 0 l

Tactic:
cases l <;> rfl

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Lemmas.lean
theorem getElem?_set {l : List α} {i j : Nat} {a : α} :
    (l.set i a)[j]? = if i = j then if i < l.length then some a else none else l[j]?

Proof state:
case isFalse
α : Type u_1
l : List α
i : Nat
a : α
h : ¬i < l.length
⊢ (l.set i a)[i]? = none

Tactic:
simp_all

Result:
no goals

Proof state:
α : Type u_1
l : List α
i : Nat
a : α
h : i < l.length
⊢ ?m.67460 < length ?m.67459

Tactic:
simpa

Result:
no goals

Proof state:
α : Type u_1
l : List α
i : Nat
a : α
⊢ (l.set i a)[i]? = if i < l.length then some a else none

Tactic:
split <;> rename_i h

Result:
case isTrue
α : Type u_1
l : List α
i : Nat
a : α
h : i < l.length
⊢ (l.set i a)[i]? = some a

case isFalse
α : Type u_1
l : List α
i : Nat
a : α
h : ¬i < l.length
⊢ (l.set i a)[i]? = none

Proof state:
α : Type u_1
l : List α
i : Nat
a : α
⊢ (l.set i a)[i]? = if i = i then if i < l.length then some a else none else l[i]?

Tactic:
rw [if_pos rfl]

Result:
α : Type u_1
l : List α
i : Nat
a : α
⊢ (l.set i a)[i]? = if i < l.length then some a else none

Proof state:
α : Type u_1
l : List α
i j : Nat
a : α
h : i = j
⊢ (l.set i a)[j]? = if i = j then if i < l.length then some a else none else l[j]?

Tactic:
subst h

Result:
α : Type u_1
l : List α
i : Nat
a : α
⊢ (l.set i a)[i]? = if i = i then if i < l.length then some a else none else l[i]?

Proof state:
α : Type u_1
l : List α
i j : Nat
a : α
h : ¬i = j
⊢ (l.set i a)[j]? = if i = j then if i < l.length then some a else none else l[j]?

Tactic:
simp [h]

Result:
no goals

Proof state:
case isTrue
α : Type u_1
l : List α
i : Nat
a : α
h : i < l.length
⊢ (l.set i a)[i]? = some a

Tactic:
simp only [getElem?_set_self (by simpa), h]

Result:
no goals
-- Mathlib/Data/Set/Function.lean
theorem BijOn.subset_right {r : Set β} (hf : BijOn f s t) (hrt : r ⊆ t) :
    BijOn f (s ∩ f ⁻¹' r) r

Proof state:
case intro.intro
α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : α → β
r : Set β
hf : BijOn f s t
hrt : r ⊆ t
y : α
hy : y ∈ s
hx : f y ∈ r
⊢ f y ∈ f '' (s ∩ f ⁻¹' r)

Tactic:
exact ⟨y, ⟨hy, hx⟩, rfl⟩

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : α → β
r : Set β
hf : BijOn f s t
hrt : r ⊆ t
x : β
hx : x ∈ r
⊢ x ∈ f '' (s ∩ f ⁻¹' r)

Tactic:
obtain ⟨y, hy, rfl⟩ := hf.surjOn (hrt hx)

Result:
case intro.intro
α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : α → β
r : Set β
hf : BijOn f s t
hrt : r ⊆ t
y : α
hy : y ∈ s
hx : f y ∈ r
⊢ f y ∈ f '' (s ∩ f ⁻¹' r)

Proof state:
α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : α → β
r : Set β
hf : BijOn f s t
hrt : r ⊆ t
⊢ BijOn f (s ∩ f ⁻¹' r) r

Tactic:
refine ⟨inter_subset_right, hf.injOn.mono inter_subset_left, fun x hx ↦ ?_⟩

Result:
α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : α → β
r : Set β
hf : BijOn f s t
hrt : r ⊆ t
x : β
hx : x ∈ r
⊢ x ∈ f '' (s ∩ f ⁻¹' r)
-- Mathlib/MeasureTheory/Measure/ProbabilityMeasure.lean
theorem apply_mono (μ : ProbabilityMeasure Ω) {s₁ s₂ : Set Ω} (h : s₁ ⊆ s₂) : μ s₁ ≤ μ s₂

Proof state:
Ω : Type u_1
inst✝ : MeasurableSpace Ω
μ : ProbabilityMeasure Ω
s₁ s₂ : Set Ω
h : s₁ ⊆ s₂
⊢ μ.toFiniteMeasure s₁ ≤ μ.toFiniteMeasure s₂

Tactic:
exact MeasureTheory.FiniteMeasure.apply_mono _ h

Result:
no goals

Proof state:
Ω : Type u_1
inst✝ : MeasurableSpace Ω
μ : ProbabilityMeasure Ω
s₁ s₂ : Set Ω
h : s₁ ⊆ s₂
⊢ μ s₁ ≤ μ s₂

Tactic:
rw [← coeFn_comp_toFiniteMeasure_eq_coeFn]

Result:
Ω : Type u_1
inst✝ : MeasurableSpace Ω
μ : ProbabilityMeasure Ω
s₁ s₂ : Set Ω
h : s₁ ⊆ s₂
⊢ μ.toFiniteMeasure s₁ ≤ μ.toFiniteMeasure s₂
-- Mathlib/NumberTheory/Modular.lean
theorem coe_T_zpow_smul_eq {n : ℤ} : (↑(T ^ n • z) : ℂ) = z + n

Proof state:
z : ℍ
n : ℤ
⊢ ↑(T ^ n • z) = ↑z + ↑n

Tactic:
rw [sl_moeb, UpperHalfPlane.coe_smul]

Result:
z : ℍ
n : ℤ
⊢ num (↑(T ^ n)) z / denom (↑(T ^ n)) z = ↑z + ↑n

Proof state:
z : ℍ
n : ℤ
⊢ num (↑(T ^ n)) z / denom (↑(T ^ n)) z = ↑z + ↑n

Tactic:
simp [coe_T_zpow, denom, num, -map_zpow]

Result:
no goals
-- Mathlib/Topology/Category/LightProfinite/AsLimit.lean
lemma surjective_transitionMap (n : ℕ) : Function.Surjective (S.transitionMap n)

Proof state:
S : LightProfinite
n : ℕ
⊢ Function.Surjective (⇑(ConcreteCategory.hom (S.transitionMap n)) ∘ ⇑(ConcreteCategory.hom (S.proj (n + 1))))

Tactic:
simpa only [proj_comp_transitionMap'] using S.proj_surjective n

Result:
no goals

Proof state:
S : LightProfinite
n : ℕ
⊢ Function.Surjective ⇑(ConcreteCategory.hom (S.transitionMap n))

Tactic:
apply Function.Surjective.of_comp (g := S.proj (n + 1))

Result:
S : LightProfinite
n : ℕ
⊢ Function.Surjective (⇑(ConcreteCategory.hom (S.transitionMap n)) ∘ ⇑(ConcreteCategory.hom (S.proj (n + 1))))
-- Mathlib/Data/Nat/Find.lean
@[simp] lemma findGreatest_eq : ∀ {n}, P n → Nat.findGreatest P n = n
  | 0, _ => rfl
  | n + 1, h => by simp [Nat.findGreatest, h]

Proof state:
P : ℕ → Prop
inst✝ : DecidablePred P
n : ℕ
h : P (n + 1)
⊢ findGreatest P (n + 1) = n + 1

Tactic:
simp [Nat.findGreatest, h]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Option/Lemmas.lean
theorem map_congr {x : Option α} (h : ∀ a, a ∈ x → f a = g a) : x.map f = x.map g

Proof state:
α : Type u_1
α✝ : Type u_2
f g : α → α✝
x : Option α
h : ∀ (a : α), a ∈ x → f a = g a
⊢ Option.map f x = Option.map g x

Tactic:
cases x <;> simp only [map_none', map_some', h, mem_def]

Result:
no goals
-- Mathlib/Algebra/Category/ModuleCat/Monoidal/Basic.lean
theorem triangle (M N : ModuleCat.{u} R) :
    (associator M (ModuleCat.of R R) N).hom ≫ tensorHom (𝟙 M) (leftUnitor N).hom =
      tensorHom (rightUnitor M).hom (𝟙 N)

Proof state:
case hf.H
R : Type u
inst✝ : CommRing R
M N : ModuleCat R
⊢ ∀ (x : ↑M) (y : ↑(of R R)) (z : ↑N),
    (Hom.hom ((associator M (of R R) N).hom ≫ tensorHom (𝟙 M) (leftUnitor N).hom)) ((x ⊗ₜ[R] y) ⊗ₜ[R] z) =
      (Hom.hom (tensorHom (rightUnitor M).hom (𝟙 N))) ((x ⊗ₜ[R] y) ⊗ₜ[R] z)

Tactic:
intro x y z

Result:
case hf.H
R : Type u
inst✝ : CommRing R
M N : ModuleCat R
x : ↑M
y : ↑(of R R)
z : ↑N
⊢ (Hom.hom ((associator M (of R R) N).hom ≫ tensorHom (𝟙 M) (leftUnitor N).hom)) ((x ⊗ₜ[R] y) ⊗ₜ[R] z) =
    (Hom.hom (tensorHom (rightUnitor M).hom (𝟙 N))) ((x ⊗ₜ[R] y) ⊗ₜ[R] z)

Proof state:
R : Type u
inst✝ : CommRing R
M N : ModuleCat R
⊢ (associator M (of R R) N).hom ≫ tensorHom (𝟙 M) (leftUnitor N).hom = tensorHom (rightUnitor M).hom (𝟙 N)

Tactic:
ext : 1

Result:
case hf
R : Type u
inst✝ : CommRing R
M N : ModuleCat R
⊢ Hom.hom ((associator M (of R R) N).hom ≫ tensorHom (𝟙 M) (leftUnitor N).hom) =
    Hom.hom (tensorHom (rightUnitor M).hom (𝟙 N))

Proof state:
case hf
R : Type u
inst✝ : CommRing R
M N : ModuleCat R
⊢ Hom.hom ((associator M (of R R) N).hom ≫ tensorHom (𝟙 M) (leftUnitor N).hom) =
    Hom.hom (tensorHom (rightUnitor M).hom (𝟙 N))

Tactic:
apply TensorProduct.ext_threefold

Result:
case hf.H
R : Type u
inst✝ : CommRing R
M N : ModuleCat R
⊢ ∀ (x : ↑M) (y : ↑(of R R)) (z : ↑N),
    (Hom.hom ((associator M (of R R) N).hom ≫ tensorHom (𝟙 M) (leftUnitor N).hom)) ((x ⊗ₜ[R] y) ⊗ₜ[R] z) =
      (Hom.hom (tensorHom (rightUnitor M).hom (𝟙 N))) ((x ⊗ₜ[R] y) ⊗ₜ[R] z)

Proof state:
case hf.H
R : Type u
inst✝ : CommRing R
M N : ModuleCat R
x : ↑M
y : ↑(of R R)
z : ↑N
⊢ x ⊗ₜ[R] (ConcreteCategory.hom (leftUnitor N).hom) (y ⊗ₜ[R] z) =
    (ConcreteCategory.hom (rightUnitor M).hom) (x ⊗ₜ[R] y) ⊗ₜ[R] z

Tactic:
erw [TensorProduct.lid_tmul, TensorProduct.rid_tmul]

Result:
case hf.H
R : Type u
inst✝ : CommRing R
M N : ModuleCat R
x : ↑M
y : ↑(of R R)
z : ↑N
⊢ x ⊗ₜ[R] (y • z) = (y • x) ⊗ₜ[R] z

Proof state:
case hf.H
R : Type u
inst✝ : CommRing R
M N : ModuleCat R
x : ↑M
y : ↑(of R R)
z : ↑N
⊢ x ⊗ₜ[R] (y • z) = (y • x) ⊗ₜ[R] z

Tactic:
exact (TensorProduct.smul_tmul _ _ _).symm

Result:
no goals

Proof state:
case hf.H
R : Type u
inst✝ : CommRing R
M N : ModuleCat R
x : ↑M
y : ↑(of R R)
z : ↑N
⊢ (Hom.hom ((associator M (of R R) N).hom ≫ tensorHom (𝟙 M) (leftUnitor N).hom)) ((x ⊗ₜ[R] y) ⊗ₜ[R] z) =
    (Hom.hom (tensorHom (rightUnitor M).hom (𝟙 N))) ((x ⊗ₜ[R] y) ⊗ₜ[R] z)

Tactic:
change x ⊗ₜ[R] ((leftUnitor N).hom) (y ⊗ₜ[R] z) = ((rightUnitor M).hom) (x ⊗ₜ[R] y) ⊗ₜ[R] z

Result:
case hf.H
R : Type u
inst✝ : CommRing R
M N : ModuleCat R
x : ↑M
y : ↑(of R R)
z : ↑N
⊢ x ⊗ₜ[R] (ConcreteCategory.hom (leftUnitor N).hom) (y ⊗ₜ[R] z) =
    (ConcreteCategory.hom (rightUnitor M).hom) (x ⊗ₜ[R] y) ⊗ₜ[R] z
-- Mathlib/Probability/Independence/Conditional.lean
lemma iCondIndep_iff (m : ι → MeasurableSpace Ω) (hm : ∀ i, m i ≤ mΩ)
    (μ : @Measure Ω mΩ) [IsFiniteMeasure μ] :
    iCondIndep m' hm' m μ
      ↔ ∀ (s : Finset ι) {f : ι → Set Ω} (_H : ∀ i, i ∈ s → MeasurableSet[m i] (f i)),
      μ⟦⋂ i ∈ s, f i | m'⟧ =ᵐ[μ] ∏ i ∈ s, (μ⟦f i | m'⟧)

Proof state:
Ω : Type u_1
ι : Type u_2
m' mΩ : MeasurableSpace Ω
inst✝¹ : StandardBorelSpace Ω
hm' : m' ≤ mΩ
m : ι → MeasurableSpace Ω
hm : ∀ (i : ι), m i ≤ mΩ
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
⊢ (∀ (s : Finset ι) {f : ι → Set Ω},
      (∀ i ∈ s, f i ∈ {s | MeasurableSet s}) →
        μ[(⋂ i ∈ s, f i).indicator fun ω => 1|m'] =ᶠ[ae μ] ∏ i ∈ s, μ[(f i).indicator fun ω => 1|m']) ↔
    ∀ (s : Finset ι) {f : ι → Set Ω},
      (∀ i ∈ s, MeasurableSet (f i)) →
        μ[(⋂ i ∈ s, f i).indicator fun ω => 1|m'] =ᶠ[ae μ] ∏ i ∈ s, μ[(f i).indicator fun ω => 1|m']

Tactic:
rfl

Result:
no goals

Proof state:
Ω : Type u_1
ι : Type u_2
m' mΩ : MeasurableSpace Ω
inst✝¹ : StandardBorelSpace Ω
hm' : m' ≤ mΩ
m : ι → MeasurableSpace Ω
hm : ∀ (i : ι), m i ≤ mΩ
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
⊢ iCondIndep m' hm' m μ ↔
    ∀ (s : Finset ι) {f : ι → Set Ω},
      (∀ i ∈ s, MeasurableSet (f i)) →
        μ[(⋂ i ∈ s, f i).indicator fun ω => 1|m'] =ᶠ[ae μ] ∏ i ∈ s, μ[(f i).indicator fun ω => 1|m']

Tactic:
rw [iCondIndep_iff_iCondIndepSets, iCondIndepSets_iff]

Result:
Ω : Type u_1
ι : Type u_2
m' mΩ : MeasurableSpace Ω
inst✝¹ : StandardBorelSpace Ω
hm' : m' ≤ mΩ
m : ι → MeasurableSpace Ω
hm : ∀ (i : ι), m i ≤ mΩ
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
⊢ (∀ (s : Finset ι) {f : ι → Set Ω},
      (∀ i ∈ s, f i ∈ {s | MeasurableSet s}) →
        μ[(⋂ i ∈ s, f i).indicator fun ω => 1|m'] =ᶠ[ae μ] ∏ i ∈ s, μ[(f i).indicator fun ω => 1|m']) ↔
    ∀ (s : Finset ι) {f : ι → Set Ω},
      (∀ i ∈ s, MeasurableSet (f i)) →
        μ[(⋂ i ∈ s, f i).indicator fun ω => 1|m'] =ᶠ[ae μ] ∏ i ∈ s, μ[(f i).indicator fun ω => 1|m']

case hπ
Ω : Type u_1
ι : Type u_2
m' mΩ : MeasurableSpace Ω
inst✝¹ : StandardBorelSpace Ω
hm' : m' ≤ mΩ
m : ι → MeasurableSpace Ω
hm : ∀ (i : ι), m i ≤ mΩ
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
⊢ ∀ (i : ι), ∀ s ∈ {s | MeasurableSet s}, MeasurableSet s

Proof state:
case hπ
Ω : Type u_1
ι : Type u_2
m' mΩ : MeasurableSpace Ω
inst✝¹ : StandardBorelSpace Ω
hm' : m' ≤ mΩ
m : ι → MeasurableSpace Ω
hm : ∀ (i : ι), m i ≤ mΩ
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
⊢ ∀ (i : ι), ∀ s ∈ {s | MeasurableSet s}, MeasurableSet s

Tactic:
exact hm

Result:
no goals
-- Mathlib/Order/Filter/Map.lean
theorem comap_surjective_eq_bot {f : Filter β} {m : α → β} (hm : Surjective m) :
    comap m f = ⊥ ↔ f = ⊥

Proof state:
α : Type u_1
β : Type u_2
f : Filter β
m : α → β
hm : Surjective m
⊢ comap m f = ⊥ ↔ f = ⊥

Tactic:
rw [comap_eq_bot_iff_compl_range, hm.range_eq, compl_univ, empty_mem_iff_bot]

Result:
no goals
-- Mathlib/Data/Setoid/Basic.lean
theorem Quot.subsingleton_iff (r : α → α → Prop) :
    Subsingleton (Quot r) ↔ Relation.EqvGen r = ⊤

Proof state:
α : Type u_1
r : α → α → Prop
⊢ (∀ (x y : Quot r), x = y) ↔ ∀ (i i_1 : α), ⊤ ≤ Relation.EqvGen r i i_1

Tactic:
refine Quot.mk_surjective.forall.trans (forall_congr' fun a => ?_)

Result:
α : Type u_1
r : α → α → Prop
a : α
⊢ (∀ (y : Quot r), mk r a = y) ↔ ∀ (i : α), ⊤ ≤ Relation.EqvGen r a i

Proof state:
α : Type u_1
r : α → α → Prop
a : α
⊢ (∀ (y : Quot r), mk r a = y) ↔ ∀ (i : α), ⊤ ≤ Relation.EqvGen r a i

Tactic:
refine Quot.mk_surjective.forall.trans (forall_congr' fun b => ?_)

Result:
α : Type u_1
r : α → α → Prop
a b : α
⊢ mk r a = mk r b ↔ ⊤ ≤ Relation.EqvGen r a b

Proof state:
α : Type u_1
r : α → α → Prop
a b : α
⊢ mk r a = mk r b ↔ ⊤ ≤ Relation.EqvGen r a b

Tactic:
rw [Quot.eq]

Result:
α : Type u_1
r : α → α → Prop
a b : α
⊢ Relation.EqvGen r a b ↔ ⊤ ≤ Relation.EqvGen r a b

Proof state:
α : Type u_1
r : α → α → Prop
a b : α
⊢ Relation.EqvGen r a b ↔ ⊤ ≤ Relation.EqvGen r a b

Tactic:
simp only [forall_const, le_Prop_eq, Pi.top_apply, Prop.top_eq_true, true_implies]

Result:
no goals

Proof state:
α : Type u_1
r : α → α → Prop
⊢ Subsingleton (Quot r) ↔ Relation.EqvGen r = ⊤

Tactic:
simp only [_root_.subsingleton_iff, _root_.eq_top_iff, Pi.le_def, Pi.top_apply, forall_const]

Result:
α : Type u_1
r : α → α → Prop
⊢ (∀ (x y : Quot r), x = y) ↔ ∀ (i i_1 : α), ⊤ ≤ Relation.EqvGen r i i_1
-- Mathlib/RingTheory/MvPolynomial/MonomialOrder.lean
theorem degree_mul_of_isRegular_left {f g : MvPolynomial σ R}
    (hf : IsRegular (m.leadingCoeff f)) (hg : g ≠ 0) :
    m.degree (f * g) = m.degree f + m.degree g

Proof state:
case hfg
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
f g : MvPolynomial σ R
hf : IsRegular (m.leadingCoeff f)
hg : g ≠ 0
⊢ m.leadingCoeff f * m.leadingCoeff g ≠ 0

Tactic:
simp only [ne_eq, hf, IsRegular.left, IsLeftRegular.mul_left_eq_zero_iff,
  leadingCoeff_eq_zero_iff]

Result:
case hfg
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
f g : MvPolynomial σ R
hf : IsRegular (m.leadingCoeff f)
hg : g ≠ 0
⊢ ¬g = 0

Proof state:
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
f g : MvPolynomial σ R
hf : IsRegular (m.leadingCoeff f)
hg : g ≠ 0
⊢ m.degree (f * g) = m.degree f + m.degree g

Tactic:
apply degree_mul_of_mul_leadingCoeff_ne_zero

Result:
case hfg
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
f g : MvPolynomial σ R
hf : IsRegular (m.leadingCoeff f)
hg : g ≠ 0
⊢ m.leadingCoeff f * m.leadingCoeff g ≠ 0

Proof state:
case hfg
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
f g : MvPolynomial σ R
hf : IsRegular (m.leadingCoeff f)
hg : g ≠ 0
⊢ ¬g = 0

Tactic:
exact hg

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem _root_.List.all_toArray (p : α → Bool) (l : List α) : l.toArray.all p = l.all p

Proof state:
α : Type u_1
p : α → Bool
l : List α
⊢ l.toArray.all p = l.all p

Tactic:
rw [all_toList]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/RawLemmas.lean
theorem insertManyIfNewUnit_cons (h : m.WF) {l : List α} {k : α} :
    insertManyIfNewUnit m (k :: l) = insertManyIfNewUnit (m.insertIfNew k ()) l

Proof state:
α : Type u
inst✝¹ : BEq α
inst✝ : Hashable α
m : Raw α fun x => Unit
h : m.WF
l : List α
k : α
⊢ insertManyIfNewUnit m (k :: l) = insertManyIfNewUnit (m.insertIfNew k ()) l

Tactic:
simp_to_raw

Result:
α : Type u
inst✝¹ : BEq α
inst✝ : Hashable α
m : Raw α fun x => Unit
h : m.WF
l : List α
k : α
⊢ (Raw₀.Const.insertManyIfNewUnit ⟨m, ⋯⟩ (k :: l)).val.val =
    (Raw₀.Const.insertManyIfNewUnit (Raw₀.insertIfNew ⟨m, ⋯⟩ k ()) l).val.val

Proof state:
α : Type u
inst✝¹ : BEq α
inst✝ : Hashable α
m : Raw α fun x => Unit
h : m.WF
l : List α
k : α
⊢ (Raw₀.Const.insertManyIfNewUnit ⟨m, ⋯⟩ (k :: l)).val.val =
    (Raw₀.Const.insertManyIfNewUnit (Raw₀.insertIfNew ⟨m, ⋯⟩ k ()) l).val.val

Tactic:
rw [Raw₀.Const.insertManyIfNewUnit_cons]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Option/Monadic.lean
theorem forIn'_id_yield_eq_pelim
    (o : Option α) (f : (a : α) → a ∈ o → β → β) (b : β) :
    forIn' (m := Id) o b (fun a m b => .yield (f a m b)) =
      o.pelim b (fun a h => f a h b)

Proof state:
α : Type u_1
β : Type u_2
o : Option α
f : (a : α) → a ∈ o → β → β
b : β
⊢ (forIn' o b fun a m b => ForInStep.yield (f a m b)) = o.pelim b fun a h => f a h b

Tactic:
cases o <;> simp

Result:
no goals
-- Mathlib/GroupTheory/Perm/List.lean
theorem mem_of_formPerm_ne_self (l : List α) (x : α) (h : formPerm l x ≠ x) : x ∈ l

Proof state:
α : Type u_1
inst✝ : DecidableEq α
l : List α
x : α
h : l.formPerm x ≠ x
this : x ∈ {y | l.formPerm y ≠ y}
⊢ x ∈ l.toFinset

Tactic:
exact support_formPerm_le' _ this

Result:
no goals

Proof state:
α : Type u_1
inst✝ : DecidableEq α
l : List α
x : α
h : l.formPerm x ≠ x
⊢ x ∈ l

Tactic:
suffices x ∈ { y | formPerm l y ≠ y } by
  rw [← mem_toFinset]
  exact support_formPerm_le' _ this

Result:
α : Type u_1
inst✝ : DecidableEq α
l : List α
x : α
h : l.formPerm x ≠ x
⊢ x ∈ {y | l.formPerm y ≠ y}

Proof state:
α : Type u_1
inst✝ : DecidableEq α
l : List α
x : α
h : l.formPerm x ≠ x
⊢ x ∈ {y | l.formPerm y ≠ y}

Tactic:
simpa using h

Result:
no goals

Proof state:
α : Type u_1
inst✝ : DecidableEq α
l : List α
x : α
h : l.formPerm x ≠ x
this : x ∈ {y | l.formPerm y ≠ y}
⊢ x ∈ l

Tactic:
rw [← mem_toFinset]

Result:
α : Type u_1
inst✝ : DecidableEq α
l : List α
x : α
h : l.formPerm x ≠ x
this : x ∈ {y | l.formPerm y ≠ y}
⊢ x ∈ l.toFinset
-- Mathlib/RingTheory/Polynomial/Cyclotomic/Basic.lean
theorem X_pow_sub_one_mul_prod_cyclotomic_eq_X_pow_sub_one_of_dvd (R) [CommRing R] {d n : ℕ}
    (h : d ∈ n.properDivisors) :
    ((X ^ d - 1) * ∏ x ∈ n.divisors \ d.divisors, cyclotomic x R) = X ^ n - 1

Proof state:
case intro
R : Type u_1
inst✝ : CommRing R
d n : ℕ
h : d ∈ n.properDivisors
hd : d ∣ n
hdn : d < n
h0n : 0 < n
h0d : 0 < d
⊢ (X ^ d - 1) * ∏ x ∈ n.divisors \ d.divisors, cyclotomic x R = X ^ n - 1

Tactic:
rw [← prod_cyclotomic_eq_X_pow_sub_one h0d, ← prod_cyclotomic_eq_X_pow_sub_one h0n, mul_comm,
  Finset.prod_sdiff (Nat.divisors_subset_of_dvd h0n.ne' hd)]

Result:
no goals

Proof state:
case intro
R : Type u_1
inst✝ : CommRing R
d n : ℕ
h : d ∈ n.properDivisors
hd : d ∣ n
hdn : d < n
⊢ (X ^ d - 1) * ∏ x ∈ n.divisors \ d.divisors, cyclotomic x R = X ^ n - 1

Tactic:
have h0n : 0 < n := pos_of_gt hdn

Result:
case intro
R : Type u_1
inst✝ : CommRing R
d n : ℕ
h : d ∈ n.properDivisors
hd : d ∣ n
hdn : d < n
h0n : 0 < n
⊢ (X ^ d - 1) * ∏ x ∈ n.divisors \ d.divisors, cyclotomic x R = X ^ n - 1

Proof state:
R : Type u_1
inst✝ : CommRing R
d n : ℕ
h : d ∈ n.properDivisors
⊢ (X ^ d - 1) * ∏ x ∈ n.divisors \ d.divisors, cyclotomic x R = X ^ n - 1

Tactic:
obtain ⟨hd, hdn⟩ := Nat.mem_properDivisors.mp h

Result:
case intro
R : Type u_1
inst✝ : CommRing R
d n : ℕ
h : d ∈ n.properDivisors
hd : d ∣ n
hdn : d < n
⊢ (X ^ d - 1) * ∏ x ∈ n.divisors \ d.divisors, cyclotomic x R = X ^ n - 1

Proof state:
case intro
R : Type u_1
inst✝ : CommRing R
d n : ℕ
h : d ∈ n.properDivisors
hd : d ∣ n
hdn : d < n
h0n : 0 < n
⊢ (X ^ d - 1) * ∏ x ∈ n.divisors \ d.divisors, cyclotomic x R = X ^ n - 1

Tactic:
have h0d : 0 < d := Nat.pos_of_dvd_of_pos hd h0n

Result:
case intro
R : Type u_1
inst✝ : CommRing R
d n : ℕ
h : d ∈ n.properDivisors
hd : d ∣ n
hdn : d < n
h0n : 0 < n
h0d : 0 < d
⊢ (X ^ d - 1) * ∏ x ∈ n.divisors \ d.divisors, cyclotomic x R = X ^ n - 1
-- Mathlib/Data/Fin/Tuple/NatAntidiagonal.lean
theorem antidiagonalTuple_zero_right : ∀ k, antidiagonalTuple k 0 = [0]
  | 0 => (congr_arg fun x => [x]) <| Subsingleton.elim _ _
  | k + 1 => by
    rw [antidiagonalTuple, antidiagonal_zero, List.flatMap_singleton,
      antidiagonalTuple_zero_right k, List.map_singleton]
    exact congr_arg (fun x => [x]) Matrix.cons_zero_zero

Proof state:
k : ℕ
⊢ antidiagonalTuple (k + 1) 0 = [0]

Tactic:
rw [antidiagonalTuple, antidiagonal_zero, List.flatMap_singleton,
  antidiagonalTuple_zero_right k, List.map_singleton]

Result:
k : ℕ
⊢ [Fin.cons (0, 0).1 0] = [0]

Proof state:
k : ℕ
⊢ [Fin.cons (0, 0).1 0] = [0]

Tactic:
exact congr_arg (fun x => [x]) Matrix.cons_zero_zero

Result:
no goals
-- Mathlib/AlgebraicGeometry/EllipticCurve/Jacobian.lean
lemma negAddY_self (P : Fin 3 → R) : W'.negAddY P P = 0

Proof state:
R : Type r
inst✝ : CommRing R
W' : Jacobian R
P : Fin 3 → R
⊢ -P y * P x ^ 3 * P z ^ 3 + 2 * P y * P y ^ 2 * P z ^ 3 - 3 * P x ^ 2 * P x * P y * P z ^ 2 * P z +
                                      3 * P x * P y * P x ^ 2 * P z * P z ^ 2 +
                                    P x ^ 3 * P y * P z ^ 3 -
                                  2 * P y ^ 2 * P y * P z ^ 3 +
                                W'.a₁ * P x * P y ^ 2 * P z ^ 4 +
                              W'.a₁ * P y * P x * P y * P z ^ 3 * P z -
                            W'.a₁ * P x * P y * P y * P z * P z ^ 3 -
                          W'.a₁ * P y ^ 2 * P x * P z ^ 4 -
                        2 * W'.a₂ * P x * P x * P y * P z ^ 4 * P z +
                      2 * W'.a₂ * P x * P y * P x * P z * P z ^ 4 +
                    W'.a₃ * P y ^ 2 * P z ^ 6 -
                  W'.a₃ * P y ^ 2 * P z ^ 6 -
                W'.a₄ * P x * P y * P z ^ 6 * P z -
              W'.a₄ * P x * P y * P z ^ 4 * P z ^ 3 +
            W'.a₄ * P y * P x * P z ^ 3 * P z ^ 4 +
          W'.a₄ * P x * P y * P z * P z ^ 6 -
        2 * W'.a₆ * P y * P z ^ 6 * P z ^ 3 +
      2 * W'.a₆ * P y * P z ^ 3 * P z ^ 6 =
    0

Tactic:
ring1

Result:
no goals

Proof state:
R : Type r
inst✝ : CommRing R
W' : Jacobian R
P : Fin 3 → R
⊢ W'.negAddY P P = 0

Tactic:
rw [negAddY]

Result:
R : Type r
inst✝ : CommRing R
W' : Jacobian R
P : Fin 3 → R
⊢ -P y * P x ^ 3 * P z ^ 3 + 2 * P y * P y ^ 2 * P z ^ 3 - 3 * P x ^ 2 * P x * P y * P z ^ 2 * P z +
                                      3 * P x * P y * P x ^ 2 * P z * P z ^ 2 +
                                    P x ^ 3 * P y * P z ^ 3 -
                                  2 * P y ^ 2 * P y * P z ^ 3 +
                                W'.a₁ * P x * P y ^ 2 * P z ^ 4 +
                              W'.a₁ * P y * P x * P y * P z ^ 3 * P z -
                            W'.a₁ * P x * P y * P y * P z * P z ^ 3 -
                          W'.a₁ * P y ^ 2 * P x * P z ^ 4 -
                        2 * W'.a₂ * P x * P x * P y * P z ^ 4 * P z +
                      2 * W'.a₂ * P x * P y * P x * P z * P z ^ 4 +
                    W'.a₃ * P y ^ 2 * P z ^ 6 -
                  W'.a₃ * P y ^ 2 * P z ^ 6 -
                W'.a₄ * P x * P y * P z ^ 6 * P z -
              W'.a₄ * P x * P y * P z ^ 4 * P z ^ 3 +
            W'.a₄ * P y * P x * P z ^ 3 * P z ^ 4 +
          W'.a₄ * P x * P y * P z * P z ^ 6 -
        2 * W'.a₆ * P y * P z ^ 6 * P z ^ 3 +
      2 * W'.a₆ * P y * P z ^ 3 * P z ^ 6 =
    0
-- Mathlib/NumberTheory/LSeries/AbstractFuncEq.lean
theorem functional_equation (s : ℂ) :
    P.Λ (P.k - s) = P.ε • P.symm.Λ s

Proof state:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
P : WeakFEPair E
s : ℂ
⊢ P.Λ (↑P.k - s) = P.ε • P.symm.Λ s

Tactic:
linear_combination (norm := module) P.functional_equation₀ s - P.Λ₀_eq (P.k - s)
  + congr(P.ε • $(P.symm_Λ₀_eq s)) + congr(($(mul_inv_cancel₀ P.hε) / ((P.k:ℂ) - s)) • P.f₀)

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/RawLemmas.lean
theorem getKey!_modify [EquivBEq α] [LawfulHashable α] [Inhabited α] {k k' : α} {f : β → β}
    (h : m.WF) : (Const.modify m k f).getKey! k' =
      if k == k' then
        if k ∈ m then k else default
      else
        m.getKey! k'

Proof state:
α : Type u
inst✝⁴ : BEq α
inst✝³ : Hashable α
β : Type v
m : Raw α fun x => β
inst✝² : EquivBEq α
inst✝¹ : LawfulHashable α
inst✝ : Inhabited α
k k' : α
f : β → β
h : m.WF
⊢ (modify m k f).getKey! k' = if (k == k') = true then if k ∈ m then k else default else m.getKey! k'

Tactic:
simp only [mem_iff_contains]

Result:
α : Type u
inst✝⁴ : BEq α
inst✝³ : Hashable α
β : Type v
m : Raw α fun x => β
inst✝² : EquivBEq α
inst✝¹ : LawfulHashable α
inst✝ : Inhabited α
k k' : α
f : β → β
h : m.WF
⊢ (modify m k f).getKey! k' = if (k == k') = true then if m.contains k = true then k else default else m.getKey! k'

Proof state:
α : Type u
inst✝⁴ : BEq α
inst✝³ : Hashable α
β : Type v
m : Raw α fun x => β
inst✝² : EquivBEq α
inst✝¹ : LawfulHashable α
inst✝ : Inhabited α
k k' : α
f : β → β
h : m.WF
⊢ (modify m k f).getKey! k' = if (k == k') = true then if m.contains k = true then k else default else m.getKey! k'

Tactic:
simp_to_raw using Raw₀.Const.getKey!_modify

Result:
no goals