harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Algebra/Pointwise/Stabilizer.lean
@[to_additive (attr := simp)]
lemma stabilizer_singleton (b : α) : stabilizer G ({b} : Set α) = stabilizer G b

Proof state:
G : Type u_1
α : Type u_3
inst✝¹ : Group G
inst✝ : MulAction G α
b : α
⊢ stabilizer G {b} = stabilizer G b

Tactic:
ext

Result:
case h
G : Type u_1
α : Type u_3
inst✝¹ : Group G
inst✝ : MulAction G α
b : α
x✝ : G
⊢ x✝ ∈ stabilizer G {b} ↔ x✝ ∈ stabilizer G b

Proof state:
case h
G : Type u_1
α : Type u_3
inst✝¹ : Group G
inst✝ : MulAction G α
b : α
x✝ : G
⊢ x✝ ∈ stabilizer G {b} ↔ x✝ ∈ stabilizer G b

Tactic:
simp

Result:
no goals
-- Mathlib/Data/Seq/Seq.lean
theorem length_map {s : Seq α} {f : α → β} (h : (s.map f).Terminates) :
    (s.map f).length h = s.length (terminates_map_iff.1 h)

Proof state:
α : Type u
β : Type v
s : Seq α
f : α → β
h : (map f s).Terminates
⊢ Nat.find h = s.length ⋯

Tactic:
congr

Result:
case e_p
α : Type u
β : Type v
s : Seq α
f : α → β
h : (map f s).Terminates
⊢ (map f s).TerminatedAt = s.TerminatedAt

Proof state:
case e_p
α : Type u
β : Type v
s : Seq α
f : α → β
h : (map f s).Terminates
⊢ (map f s).TerminatedAt = s.TerminatedAt

Tactic:
ext

Result:
case e_p.h.a
α : Type u
β : Type v
s : Seq α
f : α → β
h : (map f s).Terminates
x✝ : ℕ
⊢ (map f s).TerminatedAt x✝ ↔ s.TerminatedAt x✝

Proof state:
case e_p.h.a
α : Type u
β : Type v
s : Seq α
f : α → β
h : (map f s).Terminates
x✝ : ℕ
⊢ (map f s).TerminatedAt x✝ ↔ s.TerminatedAt x✝

Tactic:
simp

Result:
no goals

Proof state:
α : Type u
β : Type v
s : Seq α
f : α → β
h : (map f s).Terminates
⊢ (map f s).length h = s.length ⋯

Tactic:
rw [length]

Result:
α : Type u
β : Type v
s : Seq α
f : α → β
h : (map f s).Terminates
⊢ Nat.find h = s.length ⋯
-- Mathlib/Analysis/LocallyConvex/Polar.lean
theorem polar_eq_biInter_preimage (s : Set E) :
    B.polar s = ⋂ x ∈ s, ((B x) ⁻¹' Metric.closedBall (0 : 𝕜) 1)

Proof state:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NormedCommRing 𝕜
inst✝³ : AddCommMonoid E
inst✝² : AddCommMonoid F
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 F
B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜
s : Set E
⊢ B.polar s = ⋂ x ∈ s, ⇑(B x) ⁻¹' Metric.closedBall 0 1

Tactic:
aesop

Result:
no goals
-- Mathlib/Algebra/BigOperators/Expect.lean
lemma expect_mul [IsScalarTower ℚ≥0 M M] (s : Finset ι) (f : ι → M) (a : M) :
    (𝔼 i ∈ s, f i) * a = 𝔼 i ∈ s, f i * a

Proof state:
ι : Type u_1
M : Type u_3
inst✝² : Semiring M
inst✝¹ : Module ℚ≥0 M
inst✝ : IsScalarTower ℚ≥0 M M
s : Finset ι
f : ι → M
a : M
⊢ (𝔼 i ∈ s, f i) * a = 𝔼 i ∈ s, f i * a

Tactic:
rw [expect, expect, smul_mul_assoc, sum_mul]

Result:
no goals
-- Mathlib/SetTheory/Cardinal/Cofinality.lean
theorem le_cof_type [IsWellOrder α r] {c} : c ≤ cof (type r) ↔ ∀ S, Unbounded r S → c ≤ #S :=
  (le_csInf_iff'' (Order.cof_nonempty _)).trans
    ⟨fun H S h => H _ ⟨S, h, rfl⟩, by
      rintro H d ⟨S, h, rfl⟩
      exact H _ h⟩

Proof state:
case intro.intro
α : Type u
r : α → α → Prop
inst✝ : IsWellOrder α r
c : Cardinal.{u}
H : ∀ (S : Set α), Unbounded r S → c ≤ #↑S
S : Set { α := α, r := r, wo := inst✝ }.α
h : ∀ (a : { α := α, r := r, wo := inst✝ }.α), ∃ b ∈ S, swap { α := α, r := r, wo := inst✝ }.rᶜ a b
⊢ c ≤ #↑S

Tactic:
exact H _ h

Result:
no goals

Proof state:
α : Type u
r : α → α → Prop
inst✝ : IsWellOrder α r
c : Cardinal.{u}
⊢ (∀ (S : Set α), Unbounded r S → c ≤ #↑S) →
    ∀
      b ∈
        {c |
          ∃ S,
            (∀ (a : { α := α, r := r, wo := inst✝ }.α), ∃ b ∈ S, swap { α := α, r := r, wo := inst✝ }.rᶜ a b) ∧
              #↑S = c},
      c ≤ b

Tactic:
rintro H d ⟨S, h, rfl⟩

Result:
case intro.intro
α : Type u
r : α → α → Prop
inst✝ : IsWellOrder α r
c : Cardinal.{u}
H : ∀ (S : Set α), Unbounded r S → c ≤ #↑S
S : Set { α := α, r := r, wo := inst✝ }.α
h : ∀ (a : { α := α, r := r, wo := inst✝ }.α), ∃ b ∈ S, swap { α := α, r := r, wo := inst✝ }.rᶜ a b
⊢ c ≤ #↑S
-- Mathlib/Topology/UniformSpace/Defs.lean
theorem ball_eq_of_symmetry {V : Set (β × β)} (hV : SymmetricRel V) {x} :
    ball x V = { y | (y, x) ∈ V }

Proof state:
case h
β : Type ub
V : Set (β × β)
hV : SymmetricRel V
x y : β
⊢ x ∈ ball y V ↔ y ∈ {y | (y, x) ∈ V}

Tactic:
exact Iff.rfl

Result:
no goals

Proof state:
case h
β : Type ub
V : Set (β × β)
hV : SymmetricRel V
x y : β
⊢ y ∈ ball x V ↔ y ∈ {y | (y, x) ∈ V}

Tactic:
rw [mem_ball_symmetry hV]

Result:
case h
β : Type ub
V : Set (β × β)
hV : SymmetricRel V
x y : β
⊢ x ∈ ball y V ↔ y ∈ {y | (y, x) ∈ V}

Proof state:
β : Type ub
V : Set (β × β)
hV : SymmetricRel V
x : β
⊢ ball x V = {y | (y, x) ∈ V}

Tactic:
ext y

Result:
case h
β : Type ub
V : Set (β × β)
hV : SymmetricRel V
x y : β
⊢ y ∈ ball x V ↔ y ∈ {y | (y, x) ∈ V}
-- Mathlib/Algebra/Prime/Defs.lean
theorem Irreducible.prime_of_isPrimal {a : M}
    (irr : Irreducible a) (primal : IsPrimal a) : Prime a :=
  ⟨irr.ne_zero, irr.not_unit, fun a b dvd ↦ by
    obtain ⟨d₁, d₂, h₁, h₂, rfl⟩ := primal dvd
    exact (of_irreducible_mul irr).symm.imp (·.mul_right_dvd.mpr h₁) (·.mul_left_dvd.mpr h₂)⟩

Proof state:
M : Type u_1
inst✝ : CommMonoidWithZero M
a✝ : M
irr : Irreducible a✝
primal : IsPrimal a✝
a b : M
dvd : a✝ ∣ a * b
⊢ a✝ ∣ a ∨ a✝ ∣ b

Tactic:
obtain ⟨d₁, d₂, h₁, h₂, rfl⟩ := primal dvd

Result:
case intro.intro.intro.intro
M : Type u_1
inst✝ : CommMonoidWithZero M
a b d₁ d₂ : M
h₁ : d₁ ∣ a
h₂ : d₂ ∣ b
irr : Irreducible (d₁ * d₂)
primal : IsPrimal (d₁ * d₂)
dvd : d₁ * d₂ ∣ a * b
⊢ d₁ * d₂ ∣ a ∨ d₁ * d₂ ∣ b
-- Mathlib/RingTheory/WittVector/MulCoeff.lean
theorem polyOfInterest_vars (n : ℕ) : (polyOfInterest p n).vars ⊆ univ ×ˢ range (n + 1)

Proof state:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
⊢ (↑p ^ (n + 1) *
        (wittMul p (n + 1) + ↑p ^ (n + 1) * X (0, n + 1) * X (1, n + 1) -
            X (0, n + 1) * (rename (Prod.mk 1)) (wittPolynomial p ℤ (n + 1)) -
          X (1, n + 1) * (rename (Prod.mk 0)) (wittPolynomial p ℤ (n + 1)))).vars ⊆
    univ ×ˢ range (n + 1)

Tactic:
apply mul_polyOfInterest_vars

Result:
no goals

Proof state:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
⊢ (polyOfInterest p n).vars ⊆ univ ×ˢ range (n + 1)

Tactic:
rw [polyOfInterest_vars_eq]

Result:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
⊢ (↑p ^ (n + 1) *
        (wittMul p (n + 1) + ↑p ^ (n + 1) * X (0, n + 1) * X (1, n + 1) -
            X (0, n + 1) * (rename (Prod.mk 1)) (wittPolynomial p ℤ (n + 1)) -
          X (1, n + 1) * (rename (Prod.mk 0)) (wittPolynomial p ℤ (n + 1)))).vars ⊆
    univ ×ˢ range (n + 1)
-- Mathlib/Data/Multiset/Basic.lean
theorem strongDownwardInductionOn_eq {p : Multiset α → Sort*} (s : Multiset α) {n : ℕ}
    (H : ∀ t₁, (∀ {t₂ : Multiset α}, card t₂ ≤ n → t₁ < t₂ → p t₂) → card t₁ ≤ n → p t₁) :
    s.strongDownwardInductionOn H = H s fun {t} ht _h => t.strongDownwardInductionOn H ht

Proof state:
α : Type u_1
p : Multiset α → Sort u_3
s : Multiset α
n : ℕ
H : (t₁ : Multiset α) → ({t₂ : Multiset α} → t₂.card ≤ n → t₁ < t₂ → p t₂) → t₁.card ≤ n → p t₁
⊢ (fun a => s.strongDownwardInductionOn H a) = H s fun {t} ht _h => t.strongDownwardInductionOn H ht

Tactic:
dsimp only [strongDownwardInductionOn]

Result:
α : Type u_1
p : Multiset α → Sort u_3
s : Multiset α
n : ℕ
H : (t₁ : Multiset α) → ({t₂ : Multiset α} → t₂.card ≤ n → t₁ < t₂ → p t₂) → t₁.card ≤ n → p t₁
⊢ (fun a => strongDownwardInduction H s a) = H s fun {t} ht _h => strongDownwardInduction H t ht

Proof state:
α : Type u_1
p : Multiset α → Sort u_3
s : Multiset α
n : ℕ
H : (t₁ : Multiset α) → ({t₂ : Multiset α} → t₂.card ≤ n → t₁ < t₂ → p t₂) → t₁.card ≤ n → p t₁
⊢ (fun a => strongDownwardInduction H s a) = H s fun {t} ht _h => strongDownwardInduction H t ht

Tactic:
rw [strongDownwardInduction]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem toInt_xor (x y : BitVec w) :
    BitVec.toInt (x ^^^ y) = Int.bmod (BitVec.toNat x ^^^ BitVec.toNat y) (2^w)

Proof state:
w : Nat
x y : BitVec w
⊢ (x ^^^ y).toInt = (↑(x.toNat ^^^ y.toNat)).bmod (2 ^ w)

Tactic:
rw_mod_cast [Int.bmod_def, BitVec.toInt, toNat_xor, Nat.mod_eq_of_lt
  (Nat.xor_lt_two_pow (BitVec.isLt x) (BitVec.isLt y))]

Result:
w : Nat
x y : BitVec w
⊢ (if 2 * (x.toNat ^^^ y.toNat) < 2 ^ w then ↑(x.toNat ^^^ y.toNat) else ↑(x.toNat ^^^ y.toNat) - ↑(2 ^ w)) =
    if x.toNat ^^^ y.toNat < (2 ^ w + 1) / 2 then ↑(x.toNat ^^^ y.toNat) else ↑(x.toNat ^^^ y.toNat) - ↑(2 ^ w)

Proof state:
w : Nat
x y : BitVec w
⊢ (if 2 * (x.toNat ^^^ y.toNat) < 2 ^ w then ↑(x.toNat ^^^ y.toNat) else ↑(x.toNat ^^^ y.toNat) - ↑(2 ^ w)) =
    if x.toNat ^^^ y.toNat < (2 ^ w + 1) / 2 then ↑(x.toNat ^^^ y.toNat) else ↑(x.toNat ^^^ y.toNat) - ↑(2 ^ w)

Tactic:
omega

Result:
no goals
-- Mathlib/Data/Sym/Card.lean
theorem card_sym_eq_multichoose (α : Type*) (k : ℕ) [Fintype α] [Fintype (Sym α k)] :
    card (Sym α k) = multichoose (card α) k

Proof state:
α : Type u_2
k : ℕ
inst✝¹ : Fintype α
inst✝ : Fintype (Sym α k)
⊢ Fintype.card (Sym α k) = (Fintype.card α).multichoose k

Tactic:
rw [← card_sym_fin_eq_multichoose]

Result:
α : Type u_2
k : ℕ
inst✝¹ : Fintype α
inst✝ : Fintype (Sym α k)
⊢ Fintype.card (Sym α k) = Fintype.card (Sym (Fin (Fintype.card α)) k)

Proof state:
α : Type u_2
k : ℕ
inst✝¹ : Fintype α
inst✝ : Fintype (Sym α k)
⊢ Fintype.card (Sym α k) = Fintype.card (Sym (Fin (Fintype.card α)) k)

Tactic:
exact Fintype.card_congr (equivCongr (equivFin α))

Result:
no goals
-- Mathlib/Probability/Kernel/Composition/MeasureCompProd.lean
lemma lintegral_compProd [SFinite μ] [IsSFiniteKernel κ]
    {f : α × β → ℝ≥0∞} (hf : Measurable f) :
    ∫⁻ x, f x ∂(μ ⊗ₘ κ) = ∫⁻ a, ∫⁻ b, f (a, b) ∂(κ a) ∂μ

Proof state:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
κ : Kernel α β
inst✝¹ : SFinite μ
inst✝ : IsSFiniteKernel κ
f : α × β → ℝ≥0∞
hf : Measurable f
⊢ ∫⁻ (x : α × β), f x ∂μ ⊗ₘ κ = ∫⁻ (a : α), ∫⁻ (b : β), f (a, b) ∂κ a ∂μ

Tactic:
rw [compProd, Kernel.lintegral_compProd _ _ _ hf]

Result:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
κ : Kernel α β
inst✝¹ : SFinite μ
inst✝ : IsSFiniteKernel κ
f : α × β → ℝ≥0∞
hf : Measurable f
⊢ ∫⁻ (b : α), ∫⁻ (c : β), f (b, c) ∂(Kernel.prodMkLeft Unit κ) ((), b) ∂(Kernel.const Unit μ) () =
    ∫⁻ (a : α), ∫⁻ (b : β), f (a, b) ∂κ a ∂μ

Proof state:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
κ : Kernel α β
inst✝¹ : SFinite μ
inst✝ : IsSFiniteKernel κ
f : α × β → ℝ≥0∞
hf : Measurable f
⊢ ∫⁻ (b : α), ∫⁻ (c : β), f (b, c) ∂(Kernel.prodMkLeft Unit κ) ((), b) ∂(Kernel.const Unit μ) () =
    ∫⁻ (a : α), ∫⁻ (b : β), f (a, b) ∂κ a ∂μ

Tactic:
simp

Result:
no goals
-- Mathlib/CategoryTheory/Localization/CalculusOfFractions.lean
lemma homMk_comp_homMk {X Y Z : C} (z₁ : W.LeftFraction X Y) (z₂ : W.LeftFraction Y Z)
    (z₃ : W.LeftFraction z₁.Y' z₂.Y') (h₃ : z₂.f ≫ z₃.s = z₁.s ≫ z₃.f) :
    homMk z₁ ≫ homMk z₂ = homMk (z₁.comp₀ z₂ z₃)

Proof state:
C : Type u_1
inst✝¹ : Category.{u_3, u_1} C
W : MorphismProperty C
inst✝ : W.HasLeftCalculusOfFractions
X Y Z : C
z₁ : W.LeftFraction X Y
z₂ : W.LeftFraction Y Z
z₃ : W.LeftFraction z₁.Y' z₂.Y'
h₃ : z₂.f ≫ z₃.s = z₁.s ≫ z₃.f
⊢ Hom.comp (homMk z₁) (homMk z₂) = homMk (z₁.comp₀ z₂ z₃)

Tactic:
rw [Hom.comp_eq, comp_eq z₁ z₂ z₃ h₃]

Result:
no goals

Proof state:
C : Type u_1
inst✝¹ : Category.{u_3, u_1} C
W : MorphismProperty C
inst✝ : W.HasLeftCalculusOfFractions
X Y Z : C
z₁ : W.LeftFraction X Y
z₂ : W.LeftFraction Y Z
z₃ : W.LeftFraction z₁.Y' z₂.Y'
h₃ : z₂.f ≫ z₃.s = z₁.s ≫ z₃.f
⊢ homMk z₁ ≫ homMk z₂ = homMk (z₁.comp₀ z₂ z₃)

Tactic:
change Hom.comp _ _ = _

Result:
C : Type u_1
inst✝¹ : Category.{u_3, u_1} C
W : MorphismProperty C
inst✝ : W.HasLeftCalculusOfFractions
X Y Z : C
z₁ : W.LeftFraction X Y
z₂ : W.LeftFraction Y Z
z₃ : W.LeftFraction z₁.Y' z₂.Y'
h₃ : z₂.f ≫ z₃.s = z₁.s ≫ z₃.f
⊢ Hom.comp (homMk z₁) (homMk z₂) = homMk (z₁.comp₀ z₂ z₃)
-- Mathlib/RingTheory/SimpleModule/Basic.lean
theorem IsSemisimpleModule.sup {p q : Submodule R M}
    (_ : IsSemisimpleModule R p) (_ : IsSemisimpleModule R q) :
    IsSemisimpleModule R ↥(p ⊔ q)

Proof state:
R : Type u_2
inst✝² : Ring R
M : Type u_4
inst✝¹ : AddCommGroup M
inst✝ : Module R M
p q : Submodule R M
x✝¹ : IsSemisimpleModule R ↥p
x✝ : IsSemisimpleModule R ↥q
f : Bool → Submodule R M := fun t => Bool.rec q p t
⊢ IsSemisimpleModule R ↥(⨆ i ∈ Set.univ, f i)

Tactic:
exact isSemisimpleModule_biSup_of_isSemisimpleModule_submodule (by rintro (_|_) _ <;> assumption)

Result:
no goals

Proof state:
R : Type u_2
inst✝² : Ring R
M : Type u_4
inst✝¹ : AddCommGroup M
inst✝ : Module R M
p q : Submodule R M
x✝¹ : IsSemisimpleModule R ↥p
x✝ : IsSemisimpleModule R ↥q
f : Bool → Submodule R M := fun t => Bool.rec q p t
⊢ ∀ i ∈ Set.univ, IsSemisimpleModule R ↥(f i)

Tactic:
rintro (_|_) _ <;> assumption

Result:
no goals

Proof state:
R : Type u_2
inst✝² : Ring R
M : Type u_4
inst✝¹ : AddCommGroup M
inst✝ : Module R M
p q : Submodule R M
x✝¹ : IsSemisimpleModule R ↥p
x✝ : IsSemisimpleModule R ↥q
f : Bool → Submodule R M := fun t => Bool.rec q p t
⊢ p ⊔ q = ⨆ i ∈ Set.univ, f i

Tactic:
rw [iSup_univ, iSup_bool_eq]

Result:
no goals

Proof state:
R : Type u_2
inst✝² : Ring R
M : Type u_4
inst✝¹ : AddCommGroup M
inst✝ : Module R M
p q : Submodule R M
x✝¹ : IsSemisimpleModule R ↥p
x✝ : IsSemisimpleModule R ↥q
⊢ IsSemisimpleModule R ↥(p ⊔ q)

Tactic:
let f : Bool → Submodule R M := Bool.rec q p

Result:
R : Type u_2
inst✝² : Ring R
M : Type u_4
inst✝¹ : AddCommGroup M
inst✝ : Module R M
p q : Submodule R M
x✝¹ : IsSemisimpleModule R ↥p
x✝ : IsSemisimpleModule R ↥q
f : Bool → Submodule R M := fun t => Bool.rec q p t
⊢ IsSemisimpleModule R ↥(p ⊔ q)

Proof state:
R : Type u_2
inst✝² : Ring R
M : Type u_4
inst✝¹ : AddCommGroup M
inst✝ : Module R M
p q : Submodule R M
x✝¹ : IsSemisimpleModule R ↥p
x✝ : IsSemisimpleModule R ↥q
f : Bool → Submodule R M := fun t => Bool.rec q p t
⊢ IsSemisimpleModule R ↥(p ⊔ q)

Tactic:
rw [show p ⊔ q = ⨆ i ∈ Set.univ, f i by rw [iSup_univ, iSup_bool_eq]]

Result:
R : Type u_2
inst✝² : Ring R
M : Type u_4
inst✝¹ : AddCommGroup M
inst✝ : Module R M
p q : Submodule R M
x✝¹ : IsSemisimpleModule R ↥p
x✝ : IsSemisimpleModule R ↥q
f : Bool → Submodule R M := fun t => Bool.rec q p t
⊢ IsSemisimpleModule R ↥(⨆ i ∈ Set.univ, f i)
-- Mathlib/Data/Num/Lemmas.lean
theorem cast_le [LinearOrderedRing α] {m n : ZNum} : (m : α) ≤ n ↔ m ≤ n

Proof state:
α : Type u_1
inst✝ : LinearOrderedRing α
m n : ZNum
⊢ ↑m ≤ ↑n ↔ m ≤ n

Tactic:
rw [← not_lt]

Result:
α : Type u_1
inst✝ : LinearOrderedRing α
m n : ZNum
⊢ ¬↑n < ↑m ↔ m ≤ n

Proof state:
α : Type u_1
inst✝ : LinearOrderedRing α
m n : ZNum
⊢ ¬↑n < ↑m ↔ m ≤ n

Tactic:
exact not_congr cast_lt

Result:
no goals
-- Mathlib/Algebra/BigOperators/Group/Finset/Basic.lean
theorem prod_union [DecidableEq α] (h : Disjoint s₁ s₂) :
    ∏ x ∈ s₁ ∪ s₂, f x = (∏ x ∈ s₁, f x) * ∏ x ∈ s₂, f x

Proof state:
α : Type u_3
β : Type u_4
s₁ s₂ : Finset α
f : α → β
inst✝¹ : CommMonoid β
inst✝ : DecidableEq α
h : Disjoint s₁ s₂
⊢ ∏ x ∈ s₁ ∪ s₂, f x = (∏ x ∈ s₁, f x) * ∏ x ∈ s₂, f x

Tactic:
rw [← prod_union_inter, disjoint_iff_inter_eq_empty.mp h]

Result:
α : Type u_3
β : Type u_4
s₁ s₂ : Finset α
f : α → β
inst✝¹ : CommMonoid β
inst✝ : DecidableEq α
h : Disjoint s₁ s₂
⊢ ∏ x ∈ s₁ ∪ s₂, f x = (∏ x ∈ s₁ ∪ s₂, f x) * ∏ x ∈ ∅, f x

Proof state:
α : Type u_3
β : Type u_4
s₁ s₂ : Finset α
f : α → β
inst✝¹ : CommMonoid β
inst✝ : DecidableEq α
h : Disjoint s₁ s₂
⊢ ∏ x ∈ s₁ ∪ s₂, f x = (∏ x ∈ s₁ ∪ s₂, f x) * ∏ x ∈ ∅, f x

Tactic:
exact (mul_one _).symm

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Int/Pow.lean
theorem two_pow_pred_sub_two_pow {w : Nat} (h : 0 < w) :
    ((2 ^ (w - 1) : Nat) - (2 ^ w : Nat) : Int) = - ((2 ^ (w - 1) : Nat) : Int)

Proof state:
w : Nat
h : 0 < w
⊢ ↑(2 ^ (w - 1)) - ↑(2 ^ (w - 1) + 2 ^ (w - 1)) = -↑(2 ^ (w - 1))

Tactic:
omega

Result:
no goals

Proof state:
w : Nat
h : 0 < w
⊢ ↑(2 ^ (w - 1)) - ↑(2 ^ w) = -↑(2 ^ (w - 1))

Tactic:
rw [← Nat.two_pow_pred_add_two_pow_pred h]

Result:
w : Nat
h : 0 < w
⊢ ↑(2 ^ (w - 1)) - ↑(2 ^ (w - 1) + 2 ^ (w - 1)) = -↑(2 ^ (w - 1))
-- Mathlib/NumberTheory/LegendreSymbol/GaussEisensteinLemmas.lean
theorem gauss_lemma_aux (p : ℕ) [hp : Fact p.Prime] {a : ℤ} (hap : (a : ZMod p) ≠ 0) :
    (a ^ (p / 2) : ZMod p) =
      ((-1) ^ #{x ∈ Ico 1 (p / 2).succ | p / 2 < (a * x.cast : ZMod p).val} :) :=
  (mul_left_inj' (show ((p / 2)! : ZMod p) ≠ 0 by
    rw [Ne, CharP.cast_eq_zero_iff (ZMod p) p, hp.1.dvd_factorial, not_le]
    exact Nat.div_lt_self hp.1.pos (by decide))).1 <| by
      simpa using gauss_lemma_aux₁ p hap

Proof state:
p : ℕ
hp : Fact (Nat.Prime p)
a : ℤ
hap : ↑a ≠ 0
⊢ ↑(p / 2)! ≠ 0

Tactic:
rw [Ne, CharP.cast_eq_zero_iff (ZMod p) p, hp.1.dvd_factorial, not_le]

Result:
p : ℕ
hp : Fact (Nat.Prime p)
a : ℤ
hap : ↑a ≠ 0
⊢ p / 2 < p

Proof state:
p : ℕ
hp : Fact (Nat.Prime p)
a : ℤ
hap : ↑a ≠ 0
⊢ p / 2 < p

Tactic:
exact Nat.div_lt_self hp.1.pos (by decide)

Result:
no goals

Proof state:
p : ℕ
hp : Fact (Nat.Prime p)
a : ℤ
hap : ↑a ≠ 0
⊢ ↑a ^ (p / 2) * ↑(p / 2)! = ↑((-1) ^ #(filter (fun x => p / 2 < (↑a * ↑x).val) (Ico 1 (p / 2).succ))) * ↑(p / 2)!

Tactic:
simpa using gauss_lemma_aux₁ p hap

Result:
no goals

Proof state:
p : ℕ
hp : Fact (Nat.Prime p)
a : ℤ
hap : ↑a ≠ 0
⊢ 1 < 2

Tactic:
decide

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Lemmas.lean
theorem getElem?_insert_succ (l : List α) (a : α) (i : Nat) :
    (l.insert a)[i+1]? = if a ∈ l then l[i+1]? else l[i]?

Proof state:
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
l : List α
a : α
i : Nat
⊢ (List.insert a l)[i + 1]? = if a ∈ l then l[i + 1]? else l[i]?

Tactic:
simp only [insert_eq]

Result:
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
l : List α
a : α
i : Nat
⊢ (if a ∈ l then l else a :: l)[i + 1]? = if a ∈ l then l[i + 1]? else l[i]?

Proof state:
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
l : List α
a : α
i : Nat
⊢ (if a ∈ l then l else a :: l)[i + 1]? = if a ∈ l then l[i + 1]? else l[i]?

Tactic:
split <;> simp

Result:
no goals
-- Mathlib/Topology/ContinuousMap/StoneWeierstrass.lean
theorem subalgebra_topologicalClosure_eq_top_of_separatesPoints (A : Subalgebra ℝ C(X, ℝ))
    (w : A.SeparatesPoints) : A.topologicalClosure = ⊤

Proof state:
case h
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : CompactSpace X
A : Subalgebra ℝ C(X, ℝ)
w : A.SeparatesPoints
L : Subalgebra ℝ C(X, ℝ) := A.topologicalClosure
⊢ ↑A.topologicalClosure = ↑⊤

Tactic:
have n : Set.Nonempty (L : Set C(X, ℝ)) := ⟨(1 : C(X, ℝ)), A.le_topologicalClosure A.one_mem⟩

Result:
case h
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : CompactSpace X
A : Subalgebra ℝ C(X, ℝ)
w : A.SeparatesPoints
L : Subalgebra ℝ C(X, ℝ) := A.topologicalClosure
n : (↑L).Nonempty
⊢ ↑A.topologicalClosure = ↑⊤

Proof state:
case h
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : CompactSpace X
A : Subalgebra ℝ C(X, ℝ)
w : A.SeparatesPoints
L : Subalgebra ℝ C(X, ℝ) := A.topologicalClosure
n : (↑L).Nonempty
⊢ ↑A.topologicalClosure = ↑⊤

Tactic:
convert
  sublattice_closure_eq_top (L : Set C(X, ℝ)) n
    (fun f fm g gm => inf_mem_closed_subalgebra L A.isClosed_topologicalClosure ⟨f, fm⟩ ⟨g, gm⟩)
    (fun f fm g gm => sup_mem_closed_subalgebra L A.isClosed_topologicalClosure ⟨f, fm⟩ ⟨g, gm⟩)
    (Subalgebra.SeparatesPoints.strongly
      (Subalgebra.separatesPoints_monotone A.le_topologicalClosure w))

Result:
case h.e'_2
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : CompactSpace X
A : Subalgebra ℝ C(X, ℝ)
w : A.SeparatesPoints
L : Subalgebra ℝ C(X, ℝ) := A.topologicalClosure
n : (↑L).Nonempty
⊢ ↑A.topologicalClosure = closure ↑L

Proof state:
case h.e'_2
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : CompactSpace X
A : Subalgebra ℝ C(X, ℝ)
w : A.SeparatesPoints
L : Subalgebra ℝ C(X, ℝ) := A.topologicalClosure
n : (↑L).Nonempty
⊢ ↑A.topologicalClosure = closure ↑L

Tactic:
simp [L]

Result:
no goals

Proof state:
case h
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : CompactSpace X
A : Subalgebra ℝ C(X, ℝ)
w : A.SeparatesPoints
⊢ ↑A.topologicalClosure = ↑⊤

Tactic:
let L := A.topologicalClosure

Result:
case h
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : CompactSpace X
A : Subalgebra ℝ C(X, ℝ)
w : A.SeparatesPoints
L : Subalgebra ℝ C(X, ℝ) := A.topologicalClosure
⊢ ↑A.topologicalClosure = ↑⊤

Proof state:
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : CompactSpace X
A : Subalgebra ℝ C(X, ℝ)
w : A.SeparatesPoints
⊢ A.topologicalClosure = ⊤

Tactic:
apply SetLike.ext'

Result:
case h
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : CompactSpace X
A : Subalgebra ℝ C(X, ℝ)
w : A.SeparatesPoints
⊢ ↑A.topologicalClosure = ↑⊤
-- Mathlib/Order/KrullDimension.lean
lemma coheight_le_krullDim (a : α) : coheight a ≤ krullDim α

Proof state:
α : Type u_1
inst✝ : Preorder α
a : α
⊢ ↑(coheight a) ≤ krullDim α

Tactic:
simpa using height_le_krullDim (α := αᵒᵈ) a

Result:
no goals
-- Mathlib/RingTheory/WittVector/Basic.lean
theorem pow (n : ℕ) : mapFun f (x ^ n) = mapFun f x ^ n

Proof state:
p : ℕ
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Fact (Nat.Prime p)
f : R →+* S
x : 𝕎 R
n : ℕ
⊢ mapFun (⇑f) (x ^ n) = mapFun (⇑f) x ^ n

Tactic:
map_fun_tac

Result:
no goals
-- Mathlib/Data/Ordmap/Ordset.lean
theorem Valid'.node4L_lemma₁ {a b c d : ℕ} (lr₂ : 3 * (b + c + 1 + d) ≤ 16 * a + 9)
    (mr₂ : b + c + 1 ≤ 3 * d) (mm₁ : b ≤ 3 * c) : b < 3 * a + 1

Proof state:
a b c d : ℕ
lr₂ : 3 * (b + c + 1 + d) ≤ 16 * a + 9
mr₂ : b + c + 1 ≤ 3 * d
mm₁ : b ≤ 3 * c
⊢ b < 3 * a + 1

Tactic:
omega

Result:
no goals
-- Mathlib/.lake/packages/batteries/Batteries/Data/Array/Monadic.lean
theorem toList_flatMapM [Monad m] [LawfulMonad m] (a : Array α) (f : α → m (Array β)) :
    toList <$> a.flatMapM f = a.toList.flatMapM (fun a => toList <$> f a)

Proof state:
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
a : Array α
f : α → m (Array β)
⊢ toList <$> flatMapM f a = List.flatMapM (fun a => toList <$> f a) a.toList

Tactic:
rw [List.flatMapM_toArray]

Result:
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
a : Array α
f : α → m (Array β)
⊢ toList <$> List.toArray <$> List.flatMapM (fun a => toList <$> f a) a.toList =
    List.flatMapM (fun a => toList <$> f a) a.toList

Proof state:
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
a : Array α
f : α → m (Array β)
⊢ toList <$> List.toArray <$> List.flatMapM (fun a => toList <$> f a) a.toList =
    List.flatMapM (fun a => toList <$> f a) a.toList

Tactic:
simp only [Functor.map_map, id_map']

Result:
no goals
-- Mathlib/CategoryTheory/Bicategory/Adjunction/Basic.lean
theorem rightZigzagIso_inv : (rightZigzagIso η ε).inv = leftZigzag ε.inv η.inv

Proof state:
B : Type u
inst✝ : Bicategory B
a b : B
f : a ⟶ b
g : b ⟶ a
η : 𝟙 a ≅ f ≫ g
ε : g ≫ f ≅ 𝟙 b
⊢ (rightZigzagIso η ε).inv = leftZigzag ε.inv η.inv

Tactic:
simp [bicategoricalComp, bicategoricalIsoComp]

Result:
no goals
-- Mathlib/SetTheory/Cardinal/Basic.lean
theorem bddAbove_image (f : Cardinal.{u} → Cardinal.{max u v}) {s : Set Cardinal.{u}}
    (hs : BddAbove s) : BddAbove (f '' s)

Proof state:
f : Cardinal.{u} → Cardinal.{max u v}
s : Set Cardinal.{u}
hs : BddAbove s
⊢ BddAbove (f '' s)

Tactic:
rw [bddAbove_iff_small] at hs ⊢

Result:
f : Cardinal.{u} → Cardinal.{max u v}
s : Set Cardinal.{u}
hs : Small.{u, u + 1} ↑s
⊢ Small.{max u v, (max u v) + 1} ↑(f '' s)

Proof state:
f : Cardinal.{u} → Cardinal.{max u v}
s : Set Cardinal.{u}
hs : Small.{u, u + 1} ↑s
⊢ Small.{max u v, (max u v) + 1} ↑(f '' s)

Tactic:
exact small_lift _

Result:
no goals
-- Mathlib/Probability/Kernel/Composition/MapComap.lean
@[simp]
lemma prodMkLeft_zero : Kernel.prodMkLeft α (0 : Kernel β γ) = 0

Proof state:
case h.h
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
x : α × β
s : Set γ
a✝ : MeasurableSet s
⊢ ((prodMkLeft α 0) x) s = (0 x) s

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
⊢ prodMkLeft α 0 = 0

Tactic:
ext x s _

Result:
case h.h
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
x : α × β
s : Set γ
a✝ : MeasurableSet s
⊢ ((prodMkLeft α 0) x) s = (0 x) s