harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem getLsbD_or {x y : BitVec v} : (x ||| y).getLsbD i = (x.getLsbD i || y.getLsbD i)

Proof state:
v i : Nat
x y : BitVec v
⊢ (x ||| y).toNat.testBit i = (x.toNat.testBit i || y.toNat.testBit i)

Tactic:
simp

Result:
no goals

Proof state:
v i : Nat
x y : BitVec v
⊢ (x ||| y).getLsbD i = (x.getLsbD i || y.getLsbD i)

Tactic:
rw [← testBit_toNat, getLsbD, getLsbD]

Result:
v i : Nat
x y : BitVec v
⊢ (x ||| y).toNat.testBit i = (x.toNat.testBit i || y.toNat.testBit i)
-- Mathlib/RingTheory/PowerSeries/Basic.lean
theorem coeff_zero_eq_constantCoeff_apply (φ : R⟦X⟧) : coeff R 0 φ = constantCoeff R φ

Proof state:
R : Type u_1
inst✝ : Semiring R
φ : R⟦X⟧
⊢ (coeff R 0) φ = (constantCoeff R) φ

Tactic:
rw [coeff_zero_eq_constantCoeff]

Result:
no goals
-- Mathlib/Order/Category/BddOrd.lean
lemma hom_inv_apply {X Y : BddOrd} (e : X ≅ Y) (s : Y) : e.hom (e.inv s) = s

Proof state:
X Y : BddOrd
e : X ≅ Y
s : ↑Y.toPartOrd
⊢ (ConcreteCategory.hom e.hom) ((ConcreteCategory.hom e.inv) s) = s

Tactic:
simp

Result:
no goals
-- Mathlib/MeasureTheory/Covering/Differentiation.lean
theorem ae_tendsto_limRatio :
    ∀ᵐ x ∂μ, Tendsto (fun a => ρ a / μ a) (v.filterAt x) (𝓝 (v.limRatio ρ x))

Proof state:
case h
α : Type u_1
inst✝⁴ : PseudoMetricSpace α
m0 : MeasurableSpace α
μ : Measure α
v : VitaliFamily μ
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ : Measure α
inst✝ : IsLocallyFiniteMeasure ρ
hρ : ρ ≪ μ
x : α
hx : ∃ c, Tendsto (fun a => ρ a / μ a) (v.filterAt x) (𝓝 c)
⊢ Tendsto (fun a => ρ a / μ a) (v.filterAt x) (𝓝 (v.limRatio ρ x))

Tactic:
exact tendsto_nhds_limUnder hx

Result:
no goals

Proof state:
α : Type u_1
inst✝⁴ : PseudoMetricSpace α
m0 : MeasurableSpace α
μ : Measure α
v : VitaliFamily μ
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ : Measure α
inst✝ : IsLocallyFiniteMeasure ρ
hρ : ρ ≪ μ
⊢ ∀ᵐ (x : α) ∂μ, Tendsto (fun a => ρ a / μ a) (v.filterAt x) (𝓝 (v.limRatio ρ x))

Tactic:
filter_upwards [v.ae_tendsto_div hρ]

Result:
case h
α : Type u_1
inst✝⁴ : PseudoMetricSpace α
m0 : MeasurableSpace α
μ : Measure α
v : VitaliFamily μ
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ : Measure α
inst✝ : IsLocallyFiniteMeasure ρ
hρ : ρ ≪ μ
⊢ ∀ (a : α),
    (∃ c, Tendsto (fun a => ρ a / μ a) (v.filterAt a) (𝓝 c)) →
      Tendsto (fun a => ρ a / μ a) (v.filterAt a) (𝓝 (v.limRatio ρ a))

Proof state:
case h
α : Type u_1
inst✝⁴ : PseudoMetricSpace α
m0 : MeasurableSpace α
μ : Measure α
v : VitaliFamily μ
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ : Measure α
inst✝ : IsLocallyFiniteMeasure ρ
hρ : ρ ≪ μ
⊢ ∀ (a : α),
    (∃ c, Tendsto (fun a => ρ a / μ a) (v.filterAt a) (𝓝 c)) →
      Tendsto (fun a => ρ a / μ a) (v.filterAt a) (𝓝 (v.limRatio ρ a))

Tactic:
intro x hx

Result:
case h
α : Type u_1
inst✝⁴ : PseudoMetricSpace α
m0 : MeasurableSpace α
μ : Measure α
v : VitaliFamily μ
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ : Measure α
inst✝ : IsLocallyFiniteMeasure ρ
hρ : ρ ≪ μ
x : α
hx : ∃ c, Tendsto (fun a => ρ a / μ a) (v.filterAt x) (𝓝 c)
⊢ Tendsto (fun a => ρ a / μ a) (v.filterAt x) (𝓝 (v.limRatio ρ x))
-- Mathlib/CategoryTheory/Monoidal/Category.lean
theorem pentagon_inv_hom_hom_hom_inv :
    (α_ (W ⊗ X) Y Z).inv ≫ (α_ W X Y).hom ▷ Z ≫ (α_ W (X ⊗ Y) Z).hom =
      (α_ W X (Y ⊗ Z)).hom ≫ W ◁ (α_ X Y Z).inv :=
  eq_of_inv_eq_inv (by simp)

Proof state:
C : Type u
𝒞 : Category.{v, u} C
inst✝ : MonoidalCategory C
W X Y Z : C
⊢ inv ((α_ (W ⊗ X) Y Z).inv ≫ (α_ W X Y).hom ▷ Z ≫ (α_ W (X ⊗ Y) Z).hom) =
    inv ((α_ W X (Y ⊗ Z)).hom ≫ W ◁ (α_ X Y Z).inv)

Tactic:
simp

Result:
no goals
-- Mathlib/Analysis/SpecificLimits/Basic.lean
theorem lt_geom {u : ℕ → ℝ} {c : ℝ} (hc : 0 ≤ c) {n : ℕ} (hn : 0 < n)
    (h : ∀ k < n, u (k + 1) < c * u k) : u n < c ^ n * u 0

Proof state:
u : ℕ → ℝ
c : ℝ
hc : 0 ≤ c
n : ℕ
hn : 0 < n
h : ∀ k < n, u (k + 1) < c * u k
⊢ u n < c ^ n * u 0

Tactic:
apply (monotone_mul_left_of_nonneg hc).seq_pos_lt_seq_of_lt_of_le hn _ h _

Result:
u : ℕ → ℝ
c : ℝ
hc : 0 ≤ c
n : ℕ
hn : 0 < n
h : ∀ k < n, u (k + 1) < c * u k
⊢ u 0 ≤ c ^ 0 * u 0

u : ℕ → ℝ
c : ℝ
hc : 0 ≤ c
n : ℕ
hn : 0 < n
h : ∀ k < n, u (k + 1) < c * u k
⊢ ∀ k < n, c * (c ^ k * u 0) ≤ c ^ (k + 1) * u 0

Proof state:
u : ℕ → ℝ
c : ℝ
hc : 0 ≤ c
n : ℕ
hn : 0 < n
h : ∀ k < n, u (k + 1) < c * u k
⊢ u 0 ≤ c ^ 0 * u 0

Tactic:
simp

Result:
no goals

Proof state:
u : ℕ → ℝ
c : ℝ
hc : 0 ≤ c
n : ℕ
hn : 0 < n
h : ∀ k < n, u (k + 1) < c * u k
⊢ ∀ k < n, c * (c ^ k * u 0) ≤ c ^ (k + 1) * u 0

Tactic:
simp [_root_.pow_succ', mul_assoc, le_refl]

Result:
no goals
-- Mathlib/Algebra/Group/Subgroup/ZPowers/Basic.lean
@[simp]
lemma Int.zmultiples_one : AddSubgroup.zmultiples (1 : ℤ) = ⊤

Proof state:
case h
z : ℤ
⊢ z ∈ AddSubgroup.zmultiples 1 ↔ z ∈ ⊤

Tactic:
simpa only [AddSubgroup.mem_top, iff_true] using ⟨z, zsmul_int_one z⟩

Result:
no goals

Proof state:
⊢ AddSubgroup.zmultiples 1 = ⊤

Tactic:
ext z

Result:
case h
z : ℤ
⊢ z ∈ AddSubgroup.zmultiples 1 ↔ z ∈ ⊤
-- Mathlib/Data/Matrix/PEquiv.lean
lemma toMatrix_toPEquiv_mulVec [DecidableEq n] [Fintype n]
    [NonAssocSemiring α] (σ : m ≃ n) (a : n → α) :
    σ.toPEquiv.toMatrix *ᵥ a = a ∘ σ

Proof state:
case h
m : Type u_3
n : Type u_4
α : Type u_5
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : NonAssocSemiring α
σ : m ≃ n
a : n → α
j : m
⊢ (σ.toPEquiv.toMatrix *ᵥ a) j = (a ∘ ⇑σ) j

Tactic:
simp [toMatrix, mulVec, dotProduct]

Result:
no goals

Proof state:
m : Type u_3
n : Type u_4
α : Type u_5
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : NonAssocSemiring α
σ : m ≃ n
a : n → α
⊢ σ.toPEquiv.toMatrix *ᵥ a = a ∘ ⇑σ

Tactic:
ext j

Result:
case h
m : Type u_3
n : Type u_4
α : Type u_5
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : NonAssocSemiring α
σ : m ≃ n
a : n → α
j : m
⊢ (σ.toPEquiv.toMatrix *ᵥ a) j = (a ∘ ⇑σ) j
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Find.lean
theorem findSome?_guard (l : Vector α n) : findSome? (Option.guard fun x => p x) l = find? p l

Proof state:
case mk
α : Type
n : Nat
p : α → Bool
toArray✝ : Array α
size_toArray✝ : toArray✝.size = n
⊢ findSome? (Option.guard fun x => p x = true) { toArray := toArray✝, size_toArray := size_toArray✝ } =
    find? p { toArray := toArray✝, size_toArray := size_toArray✝ }

Tactic:
simp

Result:
no goals

Proof state:
α : Type
n : Nat
p : α → Bool
l : Vector α n
⊢ findSome? (Option.guard fun x => p x = true) l = find? p l

Tactic:
cases l

Result:
case mk
α : Type
n : Nat
p : α → Bool
toArray✝ : Array α
size_toArray✝ : toArray✝.size = n
⊢ findSome? (Option.guard fun x => p x = true) { toArray := toArray✝, size_toArray := size_toArray✝ } =
    find? p { toArray := toArray✝, size_toArray := size_toArray✝ }
-- Mathlib/RingTheory/GradedAlgebra/Homogeneous/Ideal.lean
theorem toIdeal_iInf₂ {κ : Sort*} {κ' : κ → Sort*} (s : ∀ i, κ' i → HomogeneousIdeal 𝒜) :
    (⨅ (i) (j), s i j).toIdeal = ⨅ (i) (j), (s i j).toIdeal

Proof state:
ι : Type u_1
σ : Type u_2
A : Type u_3
inst✝⁵ : Semiring A
inst✝⁴ : DecidableEq ι
inst✝³ : AddMonoid ι
inst✝² : SetLike σ A
inst✝¹ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝ : GradedRing 𝒜
κ : Sort u_4
κ' : κ → Sort u_5
s : (i : κ) → κ' i → HomogeneousIdeal 𝒜
⊢ (⨅ i, ⨅ j, s i j).toIdeal = ⨅ i, ⨅ j, (s i j).toIdeal

Tactic:
simp_rw [toIdeal_iInf]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Tactic/BVDecide/Normalize/BitVec.lean
theorem BitVec.one_plus_not_eq_not_plus_one (x : BitVec w) : (1#w + ~~~x) = (~~~x + 1#w)

Proof state:
w : Nat
x : BitVec w
⊢ 1#w + ~~~x = ~~~x + 1#w

Tactic:
rw [BitVec.add_comm]

Result:
no goals
-- Mathlib/MeasureTheory/Measure/MeasureSpace.lean
theorem sum_apply_eq_zero [Countable ι] {μ : ι → Measure α} {s : Set α} :
    sum μ s = 0 ↔ ∀ i, μ i s = 0

Proof state:
α : Type u_1
ι : Type u_5
m0 : MeasurableSpace α
inst✝ : Countable ι
μ : ι → Measure α
s : Set α
⊢ (sum μ) s = 0 ↔ ∀ (i : ι), (μ i) s = 0

Tactic:
simp [sum_apply_of_countable]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/PropLemmas.lean
theorem exists_eq_or_imp : (∃ a, (a = a' ∨ q a) ∧ p a) ↔ p a' ∨ ∃ a, q a ∧ p a

Proof state:
α : Sort u_1
p q : α → Prop
a' : α
⊢ (∃ a, (a = a' ∨ q a) ∧ p a) ↔ p a' ∨ ∃ a, q a ∧ p a

Tactic:
simp only [or_and_right, exists_or, exists_eq_left]

Result:
no goals
-- Mathlib/Topology/Algebra/ClosedSubgroup.lean
theorem toSubgroup_injective : Function.Injective
    (ClosedSubgroup.toSubgroup : ClosedSubgroup G → Subgroup G) :=
  fun A B h ↦ by
  ext
  rw [h]

Proof state:
case carrier.h
G : Type u
inst✝¹ : Group G
inst✝ : TopologicalSpace G
A B : ClosedSubgroup G
h : ↑A = ↑B
x✝ : G
⊢ x✝ ∈ (↑A).carrier ↔ x✝ ∈ (↑B).carrier

Tactic:
rw [h]

Result:
no goals

Proof state:
G : Type u
inst✝¹ : Group G
inst✝ : TopologicalSpace G
A B : ClosedSubgroup G
h : ↑A = ↑B
⊢ A = B

Tactic:
ext

Result:
case carrier.h
G : Type u
inst✝¹ : Group G
inst✝ : TopologicalSpace G
A B : ClosedSubgroup G
h : ↑A = ↑B
x✝ : G
⊢ x✝ ∈ (↑A).carrier ↔ x✝ ∈ (↑B).carrier
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Fin/Lemmas.lean
theorem one_eq_zero_iff {n : Nat} [NeZero n] : (1 : Fin n) = 0 ↔ n = 1

Proof state:
n : Nat
inst✝ : NeZero n
⊢ 0 = 1 ↔ n = 1

Tactic:
simp

Result:
no goals

Proof state:
n : Nat
inst✝ : NeZero n
⊢ 1 = 0 ↔ n = 1

Tactic:
rw [eq_comm]

Result:
n : Nat
inst✝ : NeZero n
⊢ 0 = 1 ↔ n = 1
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/List/Associative.lean
theorem getValue?_insertEntry_of_false [BEq α] [PartialEquivBEq α] {l : List ((_ : α) × β)}
    {k a : α} {v : β} (h : (k == a) = false) : getValue? a (insertEntry k v l) = getValue? a l

Proof state:
case false
α : Type u
β : Type v
inst✝¹ : BEq α
inst✝ : PartialEquivBEq α
l : List ((_ : α) × β)
k a : α
v : β
h : (k == a) = false
h' : containsKey k l = false
⊢ getValue? a (insertEntry k v l) = getValue? a l

Tactic:
rw [insertEntry_of_containsKey_eq_false h', getValue?_cons_of_false h]

Result:
no goals

Proof state:
α : Type u
β : Type v
inst✝¹ : BEq α
inst✝ : PartialEquivBEq α
l : List ((_ : α) × β)
k a : α
v : β
h : (k == a) = false
⊢ getValue? a (insertEntry k v l) = getValue? a l

Tactic:
cases h' : containsKey k l

Result:
case false
α : Type u
β : Type v
inst✝¹ : BEq α
inst✝ : PartialEquivBEq α
l : List ((_ : α) × β)
k a : α
v : β
h : (k == a) = false
h' : containsKey k l = false
⊢ getValue? a (insertEntry k v l) = getValue? a l

case true
α : Type u
β : Type v
inst✝¹ : BEq α
inst✝ : PartialEquivBEq α
l : List ((_ : α) × β)
k a : α
v : β
h : (k == a) = false
h' : containsKey k l = true
⊢ getValue? a (insertEntry k v l) = getValue? a l

Proof state:
case true
α : Type u
β : Type v
inst✝¹ : BEq α
inst✝ : PartialEquivBEq α
l : List ((_ : α) × β)
k a : α
v : β
h : (k == a) = false
h' : containsKey k l = true
⊢ getValue? a (insertEntry k v l) = getValue? a l

Tactic:
rw [insertEntry_of_containsKey h', getValue?_replaceEntry_of_false h]

Result:
no goals
-- Mathlib/RingTheory/MvPolynomial/Homogeneous.lean
theorem rename_isHomogeneous {f : σ → τ} (h : φ.IsHomogeneous n) :
    (rename f φ).IsHomogeneous n

Proof state:
σ : Type u_1
τ : Type u_2
R : Type u_3
inst✝ : CommSemiring R
φ : MvPolynomial σ R
n : ℕ
f : σ → τ
h : φ.IsHomogeneous n
d : σ →₀ ℕ
hd : d ∈ φ.support
⊢ (mapDomain f d).degree = n

Tactic:
apply (Finsupp.sum_mapDomain_index_addMonoidHom fun _ ↦ .id ℕ).trans

Result:
σ : Type u_1
τ : Type u_2
R : Type u_3
inst✝ : CommSemiring R
φ : MvPolynomial σ R
n : ℕ
f : σ → τ
h : φ.IsHomogeneous n
d : σ →₀ ℕ
hd : d ∈ φ.support
⊢ (d.sum fun a m => (AddMonoidHom.id ℕ) m) = n

Proof state:
σ : Type u_1
τ : Type u_2
R : Type u_3
inst✝ : CommSemiring R
φ : MvPolynomial σ R
n : ℕ
f : σ → τ
h : φ.IsHomogeneous n
⊢ (∑ x ∈ φ.support, (rename f) ((monomial x) (coeff x φ))).IsHomogeneous n

Tactic:
simp_rw [rename_monomial]

Result:
σ : Type u_1
τ : Type u_2
R : Type u_3
inst✝ : CommSemiring R
φ : MvPolynomial σ R
n : ℕ
f : σ → τ
h : φ.IsHomogeneous n
⊢ (∑ x ∈ φ.support, (monomial (mapDomain f x)) (coeff x φ)).IsHomogeneous n

Proof state:
σ : Type u_1
τ : Type u_2
R : Type u_3
inst✝ : CommSemiring R
φ : MvPolynomial σ R
n : ℕ
f : σ → τ
h : φ.IsHomogeneous n
⊢ (∑ x ∈ φ.support, (monomial (mapDomain f x)) (coeff x φ)).IsHomogeneous n

Tactic:
apply IsHomogeneous.sum _ _ _ fun d hd ↦ isHomogeneous_monomial _ _

Result:
σ : Type u_1
τ : Type u_2
R : Type u_3
inst✝ : CommSemiring R
φ : MvPolynomial σ R
n : ℕ
f : σ → τ
h : φ.IsHomogeneous n
⊢ ∀ d ∈ φ.support, (mapDomain f d).degree = n

Proof state:
σ : Type u_1
τ : Type u_2
R : Type u_3
inst✝ : CommSemiring R
φ : MvPolynomial σ R
n : ℕ
f : σ → τ
h : φ.IsHomogeneous n
⊢ ∀ d ∈ φ.support, (mapDomain f d).degree = n

Tactic:
intro d hd

Result:
σ : Type u_1
τ : Type u_2
R : Type u_3
inst✝ : CommSemiring R
φ : MvPolynomial σ R
n : ℕ
f : σ → τ
h : φ.IsHomogeneous n
d : σ →₀ ℕ
hd : d ∈ φ.support
⊢ (mapDomain f d).degree = n

Proof state:
σ : Type u_1
τ : Type u_2
R : Type u_3
inst✝ : CommSemiring R
φ : MvPolynomial σ R
n : ℕ
f : σ → τ
h : φ.IsHomogeneous n
⊢ ((rename f) φ).IsHomogeneous n

Tactic:
rw [← φ.support_sum_monomial_coeff, map_sum]

Result:
σ : Type u_1
τ : Type u_2
R : Type u_3
inst✝ : CommSemiring R
φ : MvPolynomial σ R
n : ℕ
f : σ → τ
h : φ.IsHomogeneous n
⊢ (∑ x ∈ φ.support, (rename f) ((monomial x) (coeff x φ))).IsHomogeneous n

Proof state:
σ : Type u_1
τ : Type u_2
R : Type u_3
inst✝ : CommSemiring R
φ : MvPolynomial σ R
n : ℕ
f : σ → τ
h : φ.IsHomogeneous n
d : σ →₀ ℕ
hd : d ∈ φ.support
⊢ (d.sum fun a m => (AddMonoidHom.id ℕ) m) = n

Tactic:
convert h (mem_support_iff.mp hd)

Result:
case h.e'_2
σ : Type u_1
τ : Type u_2
R : Type u_3
inst✝ : CommSemiring R
φ : MvPolynomial σ R
n : ℕ
f : σ → τ
h : φ.IsHomogeneous n
d : σ →₀ ℕ
hd : d ∈ φ.support
⊢ (d.sum fun a m => (AddMonoidHom.id ℕ) m) = (weight 1) d

Proof state:
case h.e'_2
σ : Type u_1
τ : Type u_2
R : Type u_3
inst✝ : CommSemiring R
φ : MvPolynomial σ R
n : ℕ
f : σ → τ
h : φ.IsHomogeneous n
d : σ →₀ ℕ
hd : d ∈ φ.support
⊢ (d.sum fun a m => (AddMonoidHom.id ℕ) m) = (weight 1) d

Tactic:
simp only [weight_apply, AddMonoidHom.id_apply, Pi.one_apply, smul_eq_mul, mul_one]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem foldl_reverse' (l : Array α) (f : β → α → β) (b) (w : stop = l.size) :
    l.reverse.foldl f b 0 stop = l.foldr (fun x y => f y x) b

Proof state:
α : Type u_1
β : Type u_2
stop : Nat
l : Array α
f : β → α → β
b : β
w : stop = l.size
⊢ foldl f b l.reverse 0 stop = foldr (fun x y => f y x) b l

Tactic:
simp [w, foldl_eq_foldlM, foldr_eq_foldrM]

Result:
no goals
-- Mathlib/GroupTheory/Complement.lean
@[to_additive]
lemma IsComplement.mul_eq (h : IsComplement S T) : S * T = univ :=
  eq_univ_of_forall fun x ↦ by simpa [mem_mul] using (h.existsUnique x).exists

Proof state:
G : Type u_1
inst✝ : Group G
S T : Set G
h : IsComplement S T
x : G
⊢ x ∈ S * T

Tactic:
simpa [mem_mul] using (h.existsUnique x).exists

Result:
no goals
-- Mathlib/RingTheory/MvPowerSeries/Order.lean
theorem order_le {d : σ →₀ ℕ} (h : coeff R d f ≠ 0) : f.order ≤ degree d

Proof state:
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
f : MvPowerSeries σ R
d : σ →₀ ℕ
h : (coeff R d) f ≠ 0
⊢ f.order ≤ ↑d.degree

Tactic:
rw [degree_eq_weight_one]

Result:
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
f : MvPowerSeries σ R
d : σ →₀ ℕ
h : (coeff R d) f ≠ 0
⊢ f.order ≤ ↑((weight fun x => 1) d)

Proof state:
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
f : MvPowerSeries σ R
d : σ →₀ ℕ
h : (coeff R d) f ≠ 0
⊢ f.order ≤ ↑((weight fun x => 1) d)

Tactic:
exact weightedOrder_le _ h

Result:
no goals
-- Mathlib/Algebra/Polynomial/Coeff.lean
theorem coeff_mul (p q : R[X]) (n : ℕ) :
    coeff (p * q) n = ∑ x ∈ antidiagonal n, coeff p x.1 * coeff q x.2

Proof state:
case ofFinsupp.ofFinsupp
R : Type u
inst✝ : Semiring R
n : ℕ
p q : R[ℕ]
⊢ ({ toFinsupp := p } * { toFinsupp := q }).coeff n =
    ∑ x ∈ antidiagonal n, { toFinsupp := p }.coeff x.1 * { toFinsupp := q }.coeff x.2

Tactic:
simp_rw [← ofFinsupp_mul, coeff]

Result:
case ofFinsupp.ofFinsupp
R : Type u
inst✝ : Semiring R
n : ℕ
p q : R[ℕ]
⊢ (p * q) n = ∑ x ∈ antidiagonal n, p x.1 * q x.2

Proof state:
R : Type u
inst✝ : Semiring R
p q : R[X]
n : ℕ
⊢ (p * q).coeff n = ∑ x ∈ antidiagonal n, p.coeff x.1 * q.coeff x.2

Tactic:
rcases p with ⟨p⟩

Result:
case ofFinsupp
R : Type u
inst✝ : Semiring R
q : R[X]
n : ℕ
p : R[ℕ]
⊢ ({ toFinsupp := p } * q).coeff n = ∑ x ∈ antidiagonal n, { toFinsupp := p }.coeff x.1 * q.coeff x.2

Proof state:
case ofFinsupp.ofFinsupp
R : Type u
inst✝ : Semiring R
n : ℕ
p q : R[ℕ]
⊢ (p * q) n = ∑ x ∈ antidiagonal n, p x.1 * q x.2

Tactic:
exact AddMonoidAlgebra.mul_apply_antidiagonal p q n _ Finset.mem_antidiagonal

Result:
no goals

Proof state:
case ofFinsupp
R : Type u
inst✝ : Semiring R
q : R[X]
n : ℕ
p : R[ℕ]
⊢ ({ toFinsupp := p } * q).coeff n = ∑ x ∈ antidiagonal n, { toFinsupp := p }.coeff x.1 * q.coeff x.2

Tactic:
rcases q with ⟨q⟩

Result:
case ofFinsupp.ofFinsupp
R : Type u
inst✝ : Semiring R
n : ℕ
p q : R[ℕ]
⊢ ({ toFinsupp := p } * { toFinsupp := q }).coeff n =
    ∑ x ∈ antidiagonal n, { toFinsupp := p }.coeff x.1 * { toFinsupp := q }.coeff x.2
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Nat/Linear.lean
theorem PolyCnstr.eq_true_of_isValid (ctx : Context) {c : PolyCnstr} : c.isValid → c.denote ctx = True

Proof state:
case mk
ctx : Context
eq : Bool
lhs rhs : Poly
⊢ { eq := eq, lhs := lhs, rhs := rhs }.isValid = true → denote ctx { eq := eq, lhs := lhs, rhs := rhs } = True

Tactic:
simp [isValid]

Result:
case mk
ctx : Context
eq : Bool
lhs rhs : Poly
⊢ (bif eq then lhs.isZero && rhs.isZero else lhs.isZero) = true → denote ctx { eq := eq, lhs := lhs, rhs := rhs }

Proof state:
case pos
ctx : Context
eq : Bool
lhs rhs : Poly
he : eq = true
h₁ : lhs.isZero = true
h₂ : rhs.isZero = true
⊢ Poly.denote ctx lhs = Poly.denote ctx rhs

Tactic:
simp [Poly.of_isZero, h₁, h₂]

Result:
no goals

Proof state:
case mk
ctx : Context
eq✝ : Bool
lhs✝ rhs✝ : Poly
⊢ { eq := eq✝, lhs := lhs✝, rhs := rhs✝ }.isValid = true → denote ctx { eq := eq✝, lhs := lhs✝, rhs := rhs✝ } = True

Tactic:
rename_i eq lhs rhs

Result:
case mk
ctx : Context
eq : Bool
lhs rhs : Poly
⊢ { eq := eq, lhs := lhs, rhs := rhs }.isValid = true → denote ctx { eq := eq, lhs := lhs, rhs := rhs } = True

Proof state:
ctx : Context
c : PolyCnstr
⊢ c.isValid = true → denote ctx c = True

Tactic:
cases c

Result:
case mk
ctx : Context
eq✝ : Bool
lhs✝ rhs✝ : Poly
⊢ { eq := eq✝, lhs := lhs✝, rhs := rhs✝ }.isValid = true → denote ctx { eq := eq✝, lhs := lhs✝, rhs := rhs✝ } = True

Proof state:
case neg
ctx : Context
eq : Bool
lhs rhs : Poly
he : ¬eq = true
⊢ lhs.isZero = true → Poly.denote ctx lhs ≤ Poly.denote ctx rhs

Tactic:
intro h

Result:
case neg
ctx : Context
eq : Bool
lhs rhs : Poly
he : ¬eq = true
h : lhs.isZero = true
⊢ Poly.denote ctx lhs ≤ Poly.denote ctx rhs

Proof state:
case mk
ctx : Context
eq : Bool
lhs rhs : Poly
⊢ (bif eq then lhs.isZero && rhs.isZero else lhs.isZero) = true → denote ctx { eq := eq, lhs := lhs, rhs := rhs }

Tactic:
by_cases he : eq = true <;> simp [he, denote, Poly.denote_eq, Poly.denote_le, -and_imp]

Result:
case pos
ctx : Context
eq : Bool
lhs rhs : Poly
he : eq = true
⊢ lhs.isZero = true ∧ rhs.isZero = true → Poly.denote ctx lhs = Poly.denote ctx rhs

case neg
ctx : Context
eq : Bool
lhs rhs : Poly
he : ¬eq = true
⊢ lhs.isZero = true → Poly.denote ctx lhs ≤ Poly.denote ctx rhs

Proof state:
case neg
ctx : Context
eq : Bool
lhs rhs : Poly
he : ¬eq = true
h : lhs.isZero = true
⊢ Poly.denote ctx lhs ≤ Poly.denote ctx rhs

Tactic:
simp [Poly.of_isZero, h]

Result:
no goals

Proof state:
case pos
ctx : Context
eq : Bool
lhs rhs : Poly
he : eq = true
⊢ lhs.isZero = true ∧ rhs.isZero = true → Poly.denote ctx lhs = Poly.denote ctx rhs

Tactic:
intro ⟨h₁, h₂⟩

Result:
case pos
ctx : Context
eq : Bool
lhs rhs : Poly
he : eq = true
h₁ : lhs.isZero = true
h₂ : rhs.isZero = true
⊢ Poly.denote ctx lhs = Poly.denote ctx rhs
-- Mathlib/RingTheory/Idempotents.lean
lemma CompleteOrthogonalIdempotents.map (he : CompleteOrthogonalIdempotents e) :
    CompleteOrthogonalIdempotents (f ∘ e) where
  __ := he.toOrthogonalIdempotents.map f
  complete

Proof state:
R : Type u_1
S : Type u_2
inst✝² : Semiring R
inst✝¹ : Semiring S
f : R →+* S
I : Type u_3
e : I → R
inst✝ : Fintype I
he : CompleteOrthogonalIdempotents e
⊢ ∑ i : I, (⇑f ∘ e) i = 1

Tactic:
simp only [Function.comp_apply, ← map_sum, he.complete, map_one]

Result:
no goals
-- Mathlib/Order/Filter/Germ/Basic.lean
/-- If `f : α → β` is constant w.r.t. `l` and `g : β → γ`, then `g ∘ f : α → γ` also is. -/
lemma isConstant_comp {l : Filter α} {f : α → β} {g : β → γ}
    (h : (f : Germ l β).IsConstant) : ((g ∘ f) : Germ l γ).IsConstant

Proof state:
case intro
α : Type u_1
β : Type u_2
γ : Type u_3
l : Filter α
f : α → β
g : β → γ
b : β
hb : f =ᶠ[l] fun x => b
⊢ (↑(g ∘ f)).IsConstant

Tactic:
exact ⟨g b, hb.fun_comp g⟩

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
l : Filter α
f : α → β
g : β → γ
h : (↑f).IsConstant
⊢ (↑(g ∘ f)).IsConstant

Tactic:
obtain ⟨b, hb⟩ := h

Result:
case intro
α : Type u_1
β : Type u_2
γ : Type u_3
l : Filter α
f : α → β
g : β → γ
b : β
hb : f =ᶠ[l] fun x => b
⊢ (↑(g ∘ f)).IsConstant
-- Mathlib/Data/Matroid/Map.lean
@[simp] lemma comap_loopyOn (f : α → β) (E : Set β) : comap (loopyOn E) f = loopyOn (f ⁻¹' E)

Proof state:
α : Type u_1
β : Type u_2
f : α → β
E : Set β
⊢ ((loopyOn E).comap f).E = f ⁻¹' E ∧ ∀ X ⊆ ((loopyOn E).comap f).E, ((loopyOn E).comap f).Indep X → X = ∅

Tactic:
aesop

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
f : α → β
E : Set β
⊢ (loopyOn E).comap f = loopyOn (f ⁻¹' E)

Tactic:
rw [eq_loopyOn_iff]

Result:
α : Type u_1
β : Type u_2
f : α → β
E : Set β
⊢ ((loopyOn E).comap f).E = f ⁻¹' E ∧ ∀ X ⊆ ((loopyOn E).comap f).E, ((loopyOn E).comap f).Indep X → X = ∅
-- Mathlib/RingTheory/Ideal/Quotient/Basic.lean
theorem isDomain_iff_prime : IsDomain (R ⧸ I) ↔ I.IsPrime

Proof state:
case refine_2
R : Type u
inst✝¹ : Ring R
I : Ideal R
inst✝ : I.IsTwoSided
H : IsDomain (R ⧸ I)
x y : R
h : (mk I) x * (mk I) y = 0
⊢ (mk I) x = 0 ∨ (mk I) y = 0

Tactic:
haveI := @IsDomain.to_noZeroDivisors (R ⧸ I) _ H

Result:
case refine_2
R : Type u
inst✝¹ : Ring R
I : Ideal R
inst✝ : I.IsTwoSided
H : IsDomain (R ⧸ I)
x y : R
h : (mk I) x * (mk I) y = 0
this : NoZeroDivisors (R ⧸ I)
⊢ (mk I) x = 0 ∨ (mk I) y = 0

Proof state:
case refine_1
R : Type u
inst✝¹ : Ring R
I : Ideal R
inst✝ : I.IsTwoSided
H : IsDomain (R ⧸ I)
⊢ 0 ≠ 1

Tactic:
haveI : Nontrivial (R ⧸ I) := ⟨H.2.1⟩

Result:
case refine_1
R : Type u
inst✝¹ : Ring R
I : Ideal R
inst✝ : I.IsTwoSided
H : IsDomain (R ⧸ I)
this : Nontrivial (R ⧸ I)
⊢ 0 ≠ 1

Proof state:
case refine_2
R : Type u
inst✝¹ : Ring R
I : Ideal R
inst✝ : I.IsTwoSided
H : IsDomain (R ⧸ I)
x y : R
h : (mk I) x * (mk I) y = 0
this : NoZeroDivisors (R ⧸ I)
⊢ (mk I) x = 0 ∨ (mk I) y = 0

Tactic:
exact eq_zero_or_eq_zero_of_mul_eq_zero h

Result:
no goals

Proof state:
R : Type u
inst✝¹ : Ring R
I : Ideal R
inst✝ : I.IsTwoSided
⊢ IsDomain (R ⧸ I) ↔ I.IsPrime

Tactic:
refine ⟨fun H => ⟨zero_ne_one_iff.1 ?_, fun {x y} h => ?_⟩, fun h => inferInstance⟩

Result:
case refine_1
R : Type u
inst✝¹ : Ring R
I : Ideal R
inst✝ : I.IsTwoSided
H : IsDomain (R ⧸ I)
⊢ 0 ≠ 1

case refine_2
R : Type u
inst✝¹ : Ring R
I : Ideal R
inst✝ : I.IsTwoSided
H : IsDomain (R ⧸ I)
x y : R
h : x * y ∈ I
⊢ x ∈ I ∨ y ∈ I

Proof state:
case refine_2
R : Type u
inst✝¹ : Ring R
I : Ideal R
inst✝ : I.IsTwoSided
H : IsDomain (R ⧸ I)
x y : R
h : x * y ∈ I
⊢ x ∈ I ∨ y ∈ I

Tactic:
simp only [← eq_zero_iff_mem, (mk I).map_mul] at h ⊢

Result:
case refine_2
R : Type u
inst✝¹ : Ring R
I : Ideal R
inst✝ : I.IsTwoSided
H : IsDomain (R ⧸ I)
x y : R
h : (mk I) x * (mk I) y = 0
⊢ (mk I) x = 0 ∨ (mk I) y = 0

Proof state:
case refine_1
R : Type u
inst✝¹ : Ring R
I : Ideal R
inst✝ : I.IsTwoSided
H : IsDomain (R ⧸ I)
this : Nontrivial (R ⧸ I)
⊢ 0 ≠ 1

Tactic:
exact zero_ne_one

Result:
no goals