harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/MeasureTheory/Measure/Tilted.lean
lemma tilted_apply_eq_ofReal_integral' {s : Set α} (f : α → ℝ) (hs : MeasurableSet s) :
    μ.tilted f s = ENNReal.ofReal (∫ a in s, exp (f a) / ∫ x, exp (f x) ∂μ ∂μ)

Proof state:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
s : Set α
f : α → ℝ
hs : MeasurableSet s
⊢ (μ.tilted f) s = ENNReal.ofReal (∫ (a : α) in s, rexp (f a) / ∫ (x : α), rexp (f x) ∂μ ∂μ)

Tactic:
by_cases hf : Integrable (fun x ↦ exp (f x)) μ

Result:
case pos
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
s : Set α
f : α → ℝ
hs : MeasurableSet s
hf : Integrable (fun x => rexp (f x)) μ
⊢ (μ.tilted f) s = ENNReal.ofReal (∫ (a : α) in s, rexp (f a) / ∫ (x : α), rexp (f x) ∂μ ∂μ)

case neg
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
s : Set α
f : α → ℝ
hs : MeasurableSet s
hf : ¬Integrable (fun x => rexp (f x)) μ
⊢ (μ.tilted f) s = ENNReal.ofReal (∫ (a : α) in s, rexp (f a) / ∫ (x : α), rexp (f x) ∂μ ∂μ)

Proof state:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
s : Set α
f : α → ℝ
hs : MeasurableSet s
hf : Integrable (fun x => rexp (f x)) μ
x✝ : α
⊢ 0 x✝ ≤ (fun a => rexp (f a) / ∫ (x : α), rexp (f x) ∂μ) x✝

Tactic:
positivity

Result:
no goals

Proof state:
case neg
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
s : Set α
f : α → ℝ
hs : MeasurableSet s
hf : ¬Integrable (fun x => rexp (f x)) μ
⊢ (μ.tilted f) s = ENNReal.ofReal (∫ (a : α) in s, rexp (f a) / ∫ (x : α), rexp (f x) ∂μ ∂μ)

Tactic:
simp only [hf, not_false_eq_true, tilted_of_not_integrable, Measure.coe_zero,
  Pi.zero_apply, integral_undef hf, div_zero, integral_zero, ENNReal.ofReal_zero]

Result:
no goals

Proof state:
case pos.f_nn
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
s : Set α
f : α → ℝ
hs : MeasurableSet s
hf : Integrable (fun x => rexp (f x)) μ
⊢ 0 ≤ᶠ[ae (μ.restrict s)] fun a => rexp (f a) / ∫ (x : α), rexp (f x) ∂μ

Tactic:
exact ae_of_all _ (fun _ ↦ by positivity)

Result:
no goals

Proof state:
case pos.hfi
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
s : Set α
f : α → ℝ
hs : MeasurableSet s
hf : Integrable (fun x => rexp (f x)) μ
⊢ Integrable (fun a => rexp (f a) / ∫ (x : α), rexp (f x) ∂μ) (μ.restrict s)

Tactic:
exact hf.integrableOn.div_const _

Result:
no goals

Proof state:
case pos
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
s : Set α
f : α → ℝ
hs : MeasurableSet s
hf : Integrable (fun x => rexp (f x)) μ
⊢ (μ.tilted f) s = ENNReal.ofReal (∫ (a : α) in s, rexp (f a) / ∫ (x : α), rexp (f x) ∂μ ∂μ)

Tactic:
rw [tilted_apply' _ _ hs, ← ofReal_integral_eq_lintegral_ofReal]

Result:
case pos.hfi
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
s : Set α
f : α → ℝ
hs : MeasurableSet s
hf : Integrable (fun x => rexp (f x)) μ
⊢ Integrable (fun a => rexp (f a) / ∫ (x : α), rexp (f x) ∂μ) (μ.restrict s)

case pos.f_nn
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
s : Set α
f : α → ℝ
hs : MeasurableSet s
hf : Integrable (fun x => rexp (f x)) μ
⊢ 0 ≤ᶠ[ae (μ.restrict s)] fun a => rexp (f a) / ∫ (x : α), rexp (f x) ∂μ
-- Mathlib/Analysis/Calculus/LineDeriv/Basic.lean
theorem lineDerivWithin_univ : lineDerivWithin 𝕜 f univ x v = lineDeriv 𝕜 f x v

Proof state:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
F : Type u_2
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
E : Type u_3
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
f : E → F
x v : E
⊢ lineDerivWithin 𝕜 f univ x v = lineDeriv 𝕜 f x v

Tactic:
simp [lineDerivWithin, lineDeriv]

Result:
no goals
-- Mathlib/Algebra/Ring/Ext.lean
theorem toNonUnitalSemiring_injective :
    Function.Injective (@toNonUnitalSemiring R)

Proof state:
R : Type u
a₁✝ a₂✝ : Semiring R
h : toNonUnitalSemiring = toNonUnitalSemiring
⊢ a₁✝ = a₂✝

Tactic:
ext x y

Result:
case h_add.h.h
R : Type u
a₁✝ a₂✝ : Semiring R
h : toNonUnitalSemiring = toNonUnitalSemiring
x y : R
⊢ x + y = x + y

case h_mul.h.h
R : Type u
a₁✝ a₂✝ : Semiring R
h : toNonUnitalSemiring = toNonUnitalSemiring
x y : R
⊢ x * y = x * y

Proof state:
R : Type u
⊢ Function.Injective (@toNonUnitalSemiring R)

Tactic:
intro _ _ h

Result:
R : Type u
a₁✝ a₂✝ : Semiring R
h : toNonUnitalSemiring = toNonUnitalSemiring
⊢ a₁✝ = a₂✝
-- Mathlib/SetTheory/Surreal/Basic.lean
lemma isOption {x' x} (h : IsOption x' x) (hx : Numeric x) : Numeric x'

Proof state:
x' x : PGame
h : x'.IsOption x
hx : x.Numeric
⊢ x'.Numeric

Tactic:
cases h

Result:
case moveLeft
x : PGame
hx : x.Numeric
i✝ : x.LeftMoves
⊢ (x.moveLeft i✝).Numeric

case moveRight
x : PGame
hx : x.Numeric
i✝ : x.RightMoves
⊢ (x.moveRight i✝).Numeric

Proof state:
case moveRight
x : PGame
hx : x.Numeric
i✝ : x.RightMoves
⊢ (x.moveRight i✝).Numeric

Tactic:
apply hx.moveRight

Result:
no goals

Proof state:
case moveLeft
x : PGame
hx : x.Numeric
i✝ : x.LeftMoves
⊢ (x.moveLeft i✝).Numeric

Tactic:
apply hx.moveLeft

Result:
no goals
-- Mathlib/Algebra/Homology/HomologicalComplex.lean
theorem mk_d_1_0 : (mk X₀ X₁ X₂ d₀ d₁ s succ).d 1 0 = d₀

Proof state:
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
X₀ X₁ X₂ : V
d₀ : X₁ ⟶ X₀
d₁ : X₂ ⟶ X₁
s : d₁ ≫ d₀ = 0
succ : (S : ShortComplex V) → (X₃ : V) ×' (d₂ : X₃ ⟶ S.X₁) ×' d₂ ≫ S.f = 0
⊢ (if 1 = 0 + 1 then 𝟙 X₁ ≫ d₀ else 0) = d₀

Tactic:
rw [if_pos rfl, Category.id_comp]

Result:
no goals

Proof state:
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
X₀ X₁ X₂ : V
d₀ : X₁ ⟶ X₀
d₁ : X₂ ⟶ X₁
s : d₁ ≫ d₀ = 0
succ : (S : ShortComplex V) → (X₃ : V) ×' (d₂ : X₃ ⟶ S.X₁) ×' d₂ ≫ S.f = 0
⊢ (mk X₀ X₁ X₂ d₀ d₁ s succ).d 1 0 = d₀

Tactic:
change ite (1 = 0 + 1) (𝟙 X₁ ≫ d₀) 0 = d₀

Result:
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
X₀ X₁ X₂ : V
d₀ : X₁ ⟶ X₀
d₁ : X₂ ⟶ X₁
s : d₁ ≫ d₀ = 0
succ : (S : ShortComplex V) → (X₃ : V) ×' (d₂ : X₃ ⟶ S.X₁) ×' d₂ ≫ S.f = 0
⊢ (if 1 = 0 + 1 then 𝟙 X₁ ≫ d₀ else 0) = d₀
-- Mathlib/AlgebraicGeometry/GammaSpecAdjunction.lean
theorem Scheme.toSpecΓ_appTop (X : Scheme.{u}) :
    X.toSpecΓ.appTop = (Scheme.ΓSpecIso Γ(X, ⊤)).hom

Proof state:
X : Scheme
this : (Hom.appTop X.toSpecΓ).op = inv (ΓSpecIso Γ(X, ⊤)).inv.op
⊢ Hom.appTop X.toSpecΓ = (ΓSpecIso Γ(X, ⊤)).hom

Tactic:
rw [← Quiver.Hom.op_inj.eq_iff, this, ← op_inv, IsIso.Iso.inv_inv]

Result:
no goals

Proof state:
X : Scheme
this : Γ.rightOp.map (ΓSpec.adjunction.unit.app X) ≫ ΓSpec.adjunction.counit.app (Γ.rightOp.obj X) = 𝟙 (Γ.rightOp.obj X)
⊢ Hom.appTop X.toSpecΓ = (ΓSpecIso Γ(X, ⊤)).hom

Tactic:
dsimp at this

Result:
X : Scheme
this : (Hom.appTop X.toSpecΓ).op ≫ (ΓSpecIso Γ(X, ⊤)).inv.op = 𝟙 (op Γ(X, ⊤))
⊢ Hom.appTop X.toSpecΓ = (ΓSpecIso Γ(X, ⊤)).hom

Proof state:
X : Scheme
⊢ Hom.appTop X.toSpecΓ = (ΓSpecIso Γ(X, ⊤)).hom

Tactic:
have := ΓSpec.adjunction.left_triangle_components X

Result:
X : Scheme
this : Γ.rightOp.map (ΓSpec.adjunction.unit.app X) ≫ ΓSpec.adjunction.counit.app (Γ.rightOp.obj X) = 𝟙 (Γ.rightOp.obj X)
⊢ Hom.appTop X.toSpecΓ = (ΓSpecIso Γ(X, ⊤)).hom

Proof state:
X : Scheme
this : (Hom.appTop X.toSpecΓ).op = 𝟙 (op Γ(X, ⊤)) ≫ inv (ΓSpecIso Γ(X, ⊤)).inv.op
⊢ Hom.appTop X.toSpecΓ = (ΓSpecIso Γ(X, ⊤)).hom

Tactic:
simp only [ΓSpec.adjunction_counit_app, Functor.id_obj, Functor.comp_obj, Functor.rightOp_obj,
  Scheme.Γ_obj, Category.id_comp] at this

Result:
X : Scheme
this : (Hom.appTop X.toSpecΓ).op = inv (ΓSpecIso Γ(X, ⊤)).inv.op
⊢ Hom.appTop X.toSpecΓ = (ΓSpecIso Γ(X, ⊤)).hom

Proof state:
X : Scheme
this : (Hom.appTop X.toSpecΓ).op ≫ (ΓSpecIso Γ(X, ⊤)).inv.op = 𝟙 (op Γ(X, ⊤))
⊢ Hom.appTop X.toSpecΓ = (ΓSpecIso Γ(X, ⊤)).hom

Tactic:
rw [← IsIso.eq_comp_inv] at this

Result:
X : Scheme
this : (Hom.appTop X.toSpecΓ).op = 𝟙 (op Γ(X, ⊤)) ≫ inv (ΓSpecIso Γ(X, ⊤)).inv.op
⊢ Hom.appTop X.toSpecΓ = (ΓSpecIso Γ(X, ⊤)).hom
-- Mathlib/MeasureTheory/Measure/Lebesgue/EqHaar.lean
theorem addHaar_ball_mul [Nontrivial E] (x : E) {r : ℝ} (hr : 0 ≤ r) (s : ℝ) :
    μ (ball x (r * s)) = ENNReal.ofReal (r ^ finrank ℝ E) * μ (ball 0 s)

Proof state:
case inl
E : Type u_1
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : MeasurableSpace E
inst✝³ : BorelSpace E
inst✝² : FiniteDimensional ℝ E
μ : Measure E
inst✝¹ : μ.IsAddHaarMeasure
inst✝ : Nontrivial E
x : E
s : ℝ
hr : 0 ≤ 0
⊢ μ (ball x (0 * s)) = ENNReal.ofReal (0 ^ finrank ℝ E) * μ (ball 0 s)

Tactic:
simp only [zero_pow (finrank_pos (R := ℝ) (M := E)).ne', measure_empty, zero_mul,
  ENNReal.ofReal_zero, ball_zero]

Result:
no goals

Proof state:
case inr
E : Type u_1
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : MeasurableSpace E
inst✝³ : BorelSpace E
inst✝² : FiniteDimensional ℝ E
μ : Measure E
inst✝¹ : μ.IsAddHaarMeasure
inst✝ : Nontrivial E
x : E
r : ℝ
hr : 0 ≤ r
s : ℝ
h : 0 < r
⊢ μ (ball x (r * s)) = ENNReal.ofReal (r ^ finrank ℝ E) * μ (ball 0 s)

Tactic:
exact addHaar_ball_mul_of_pos μ x h s

Result:
no goals

Proof state:
E : Type u_1
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : MeasurableSpace E
inst✝³ : BorelSpace E
inst✝² : FiniteDimensional ℝ E
μ : Measure E
inst✝¹ : μ.IsAddHaarMeasure
inst✝ : Nontrivial E
x : E
r : ℝ
hr : 0 ≤ r
s : ℝ
⊢ μ (ball x (r * s)) = ENNReal.ofReal (r ^ finrank ℝ E) * μ (ball 0 s)

Tactic:
rcases hr.eq_or_lt with (rfl | h)

Result:
case inl
E : Type u_1
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : MeasurableSpace E
inst✝³ : BorelSpace E
inst✝² : FiniteDimensional ℝ E
μ : Measure E
inst✝¹ : μ.IsAddHaarMeasure
inst✝ : Nontrivial E
x : E
s : ℝ
hr : 0 ≤ 0
⊢ μ (ball x (0 * s)) = ENNReal.ofReal (0 ^ finrank ℝ E) * μ (ball 0 s)

case inr
E : Type u_1
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : MeasurableSpace E
inst✝³ : BorelSpace E
inst✝² : FiniteDimensional ℝ E
μ : Measure E
inst✝¹ : μ.IsAddHaarMeasure
inst✝ : Nontrivial E
x : E
r : ℝ
hr : 0 ≤ r
s : ℝ
h : 0 < r
⊢ μ (ball x (r * s)) = ENNReal.ofReal (r ^ finrank ℝ E) * μ (ball 0 s)
-- Mathlib/RingTheory/RootsOfUnity/PrimitiveRoots.lean
theorem isPrimitiveRoot_of_mem_primitiveRoots {ζ : R} (h : ζ ∈ primitiveRoots k R) :
    IsPrimitiveRoot ζ k :=
  k.eq_zero_or_pos.elim (fun hk ↦ by simp [hk] at h) fun hk ↦ (mem_primitiveRoots hk).1 h

Proof state:
R : Type u_4
k : ℕ
inst✝¹ : CommRing R
inst✝ : IsDomain R
ζ : R
h : ζ ∈ primitiveRoots k R
hk : k = 0
⊢ IsPrimitiveRoot ζ k

Tactic:
simp [hk] at h

Result:
no goals
-- Mathlib/RingTheory/Coprime/Basic.lean
theorem neg_left {x y : R} (h : IsCoprime x y) : IsCoprime (-x) y

Proof state:
case h
R : Type u
inst✝ : CommRing R
x y a b : R
h : a * x + b * y = 1
⊢ -a * -x + b * y = 1

Tactic:
rwa [neg_mul_neg]

Result:
no goals

Proof state:
R : Type u
inst✝ : CommRing R
x y : R
h : IsCoprime x y
⊢ IsCoprime (-x) y

Tactic:
obtain ⟨a, b, h⟩ := h

Result:
case intro.intro
R : Type u
inst✝ : CommRing R
x y a b : R
h : a * x + b * y = 1
⊢ IsCoprime (-x) y

Proof state:
case intro.intro
R : Type u
inst✝ : CommRing R
x y a b : R
h : a * x + b * y = 1
⊢ IsCoprime (-x) y

Tactic:
use -a, b

Result:
case h
R : Type u
inst✝ : CommRing R
x y a b : R
h : a * x + b * y = 1
⊢ -a * -x + b * y = 1
-- Mathlib/LinearAlgebra/Matrix/Permanent.lean
theorem permanent_eq_elem_of_subsingleton [Subsingleton n] (A : Matrix n n R) (k : n) :
    permanent A = A k k

Proof state:
n : Type u_1
inst✝³ : DecidableEq n
inst✝² : Fintype n
R : Type u_2
inst✝¹ : CommSemiring R
inst✝ : Subsingleton n
A : Matrix n n R
k : n
this : Unique n
⊢ A.permanent = A k k

Tactic:
convert permanent_unique A

Result:
no goals

Proof state:
n : Type u_1
inst✝³ : DecidableEq n
inst✝² : Fintype n
R : Type u_2
inst✝¹ : CommSemiring R
inst✝ : Subsingleton n
A : Matrix n n R
k : n
⊢ A.permanent = A k k

Tactic:
have := uniqueOfSubsingleton k

Result:
n : Type u_1
inst✝³ : DecidableEq n
inst✝² : Fintype n
R : Type u_2
inst✝¹ : CommSemiring R
inst✝ : Subsingleton n
A : Matrix n n R
k : n
this : Unique n
⊢ A.permanent = A k k
-- Mathlib/Algebra/BigOperators/Ring/Finset.lean
theorem prod_add_prod_eq {s : Finset ι} {i : ι} {f g h : ι → α} (hi : i ∈ s)
    (h1 : g i + h i = f i) (h2 : ∀ j ∈ s, j ≠ i → g j = f j) (h3 : ∀ j ∈ s, j ≠ i → h j = f j) :
    (∏ i ∈ s, g i) + ∏ i ∈ s, h i = ∏ i ∈ s, f i

Proof state:
ι : Type u_1
α : Type u_3
inst✝ : CommSemiring α
s : Finset ι
i : ι
f g h : ι → α
hi : i ∈ s
h1 : g i + h i = f i
h2 : ∀ j ∈ s, j ≠ i → g j = f j
h3 : ∀ j ∈ s, j ≠ i → h j = f j
⊢ g i * ∏ i ∈ s \ {i}, g i + h i * ∏ i ∈ s \ {i}, h i = g i * ∏ i ∈ s \ {i}, f i + h i * ∏ i ∈ s \ {i}, f i

Tactic:
congr 2 <;> apply prod_congr rfl <;> simpa

Result:
no goals

Proof state:
ι : Type u_1
α : Type u_3
inst✝ : CommSemiring α
s : Finset ι
i : ι
f g h : ι → α
hi : i ∈ s
h1 : g i + h i = f i
h2 : ∀ j ∈ s, j ≠ i → g j = f j
h3 : ∀ j ∈ s, j ≠ i → h j = f j
⊢ ∏ i ∈ s, g i + ∏ i ∈ s, h i = ∏ i ∈ s, f i

Tactic:
simp_rw [prod_eq_mul_prod_diff_singleton hi, ← h1, right_distrib]

Result:
ι : Type u_1
α : Type u_3
inst✝ : CommSemiring α
s : Finset ι
i : ι
f g h : ι → α
hi : i ∈ s
h1 : g i + h i = f i
h2 : ∀ j ∈ s, j ≠ i → g j = f j
h3 : ∀ j ∈ s, j ≠ i → h j = f j
⊢ g i * ∏ i ∈ s \ {i}, g i + h i * ∏ i ∈ s \ {i}, h i = g i * ∏ i ∈ s \ {i}, f i + h i * ∏ i ∈ s \ {i}, f i

Proof state:
ι : Type u_1
α : Type u_3
inst✝ : CommSemiring α
s : Finset ι
i : ι
f g h : ι → α
hi : i ∈ s
h1 : g i + h i = f i
h2 : ∀ j ∈ s, j ≠ i → g j = f j
h3 : ∀ j ∈ s, j ≠ i → h j = f j
⊢ ∏ i ∈ s, g i + ∏ i ∈ s, h i = ∏ i ∈ s, f i

Tactic:
classical
  simp_rw [prod_eq_mul_prod_diff_singleton hi, ← h1, right_distrib]
  congr 2 <;> apply prod_congr rfl <;> simpa

Result:
no goals
-- Mathlib/Probability/Moments/Basic.lean
theorem centralMoment_zero (hp : p ≠ 0) : centralMoment 0 p μ = 0

Proof state:
Ω : Type u_1
m : MeasurableSpace Ω
p : ℕ
μ : Measure Ω
hp : p ≠ 0
⊢ centralMoment 0 p μ = 0

Tactic:
simp only [centralMoment, hp, Pi.zero_apply, integral_const, smul_eq_mul,
  mul_zero, zero_sub, Pi.pow_apply, Pi.neg_apply, neg_zero, zero_pow, Ne, not_false_iff]

Result:
no goals
-- Mathlib/Algebra/Polynomial/FieldDivision.lean
theorem map_eq_zero [Semiring S] [Nontrivial S] (f : R →+* S) : p.map f = 0 ↔ p = 0

Proof state:
R : Type u
S : Type v
inst✝² : DivisionRing R
p : R[X]
inst✝¹ : Semiring S
inst✝ : Nontrivial S
f : R →+* S
⊢ (∀ (n : ℕ), (map f p).coeff n = coeff 0 n) ↔ ∀ (n : ℕ), p.coeff n = coeff 0 n

Tactic:
congr!

Result:
case a.h.a
R : Type u
S : Type v
inst✝² : DivisionRing R
p : R[X]
inst✝¹ : Semiring S
inst✝ : Nontrivial S
f : R →+* S
a✝ : ℕ
⊢ (map f p).coeff a✝ = coeff 0 a✝ ↔ p.coeff a✝ = coeff 0 a✝

Proof state:
R : Type u
S : Type v
inst✝² : DivisionRing R
p : R[X]
inst✝¹ : Semiring S
inst✝ : Nontrivial S
f : R →+* S
⊢ map f p = 0 ↔ p = 0

Tactic:
simp only [Polynomial.ext_iff]

Result:
R : Type u
S : Type v
inst✝² : DivisionRing R
p : R[X]
inst✝¹ : Semiring S
inst✝ : Nontrivial S
f : R →+* S
⊢ (∀ (n : ℕ), (map f p).coeff n = coeff 0 n) ↔ ∀ (n : ℕ), p.coeff n = coeff 0 n

Proof state:
case a.h.a
R : Type u
S : Type v
inst✝² : DivisionRing R
p : R[X]
inst✝¹ : Semiring S
inst✝ : Nontrivial S
f : R →+* S
a✝ : ℕ
⊢ (map f p).coeff a✝ = coeff 0 a✝ ↔ p.coeff a✝ = coeff 0 a✝

Tactic:
simp [map_eq_zero, coeff_map, coeff_zero]

Result:
no goals
-- Mathlib/Data/PFun.lean
theorem preimage_asSubtype (f : α →. β) (s : Set β) :
    f.asSubtype ⁻¹' s = Subtype.val ⁻¹' f.preimage s

Proof state:
case h
α : Type u_1
β : Type u_2
f : α →. β
s : Set β
x : ↑f.Dom
⊢ x ∈ f.asSubtype ⁻¹' s ↔ x ∈ Subtype.val ⁻¹' f.preimage s

Tactic:
simp only [Set.mem_preimage, Set.mem_setOf_eq, PFun.asSubtype, PFun.mem_preimage]

Result:
case h
α : Type u_1
β : Type u_2
f : α →. β
s : Set β
x : ↑f.Dom
⊢ f.fn ↑x ⋯ ∈ s ↔ ∃ y ∈ s, y ∈ f ↑x

Proof state:
α : Type u_1
β : Type u_2
f : α →. β
s : Set β
⊢ f.asSubtype ⁻¹' s = Subtype.val ⁻¹' f.preimage s

Tactic:
ext x

Result:
case h
α : Type u_1
β : Type u_2
f : α →. β
s : Set β
x : ↑f.Dom
⊢ x ∈ f.asSubtype ⁻¹' s ↔ x ∈ Subtype.val ⁻¹' f.preimage s

Proof state:
case h
α : Type u_1
β : Type u_2
f : α →. β
s : Set β
x : ↑f.Dom
⊢ f.fn ↑x ⋯ ∈ s ↔ ∃ y ∈ s, y ∈ f ↑x

Tactic:
exact
  Iff.intro (fun h => ⟨_, h, Part.get_mem _⟩) fun ⟨y, ys, fxy⟩ =>
    have : f.fn x.val x.property ∈ f x.val := Part.get_mem _
    Part.mem_unique fxy this ▸ ys

Result:
no goals
-- Mathlib/Order/UpperLower/Basic.lean
theorem coe_iSup₂ (f : ∀ i, κ i → UpperSet α) :
    (↑(⨆ (i) (j), f i j) : Set α) = ⋂ (i) (j), f i j

Proof state:
α : Type u_1
ι : Sort u_4
κ : ι → Sort u_5
inst✝ : LE α
f : (i : ι) → κ i → UpperSet α
⊢ ↑(⨆ i, ⨆ j, f i j) = ⋂ i, ⋂ j, ↑(f i j)

Tactic:
simp_rw [coe_iSup]

Result:
no goals
-- Mathlib/Data/Nat/PartENat.lean
theorem add_one_le_of_lt {x y : PartENat} (h : x < y) : x + 1 ≤ y

Proof state:
case a.intro
n m : ℕ
h : ↑m < ↑n
⊢ ↑m + 1 ≤ ↑n

Tactic:
norm_cast

Result:
case a.intro
n m : ℕ
h : ↑m < ↑n
⊢ m + 1 ≤ n

Proof state:
x y : PartENat
h : x < y
⊢ x + 1 ≤ y

Tactic:
induction' y using PartENat.casesOn with n

Result:
case a
x : PartENat
h : x < ⊤
⊢ x + 1 ≤ ⊤

case a
x : PartENat
n : ℕ
h : x < ↑n
⊢ x + 1 ≤ ↑n

Proof state:
case a.intro
n m : ℕ
h : ↑m < ↑n
⊢ m + 1 ≤ n

Tactic:
apply Nat.succ_le_of_lt

Result:
case a.intro.h
n m : ℕ
h : ↑m < ↑n
⊢ m < n

Proof state:
case a.intro.h
n m : ℕ
h : ↑m < ↑n
⊢ m < n

Tactic:
norm_cast at h

Result:
no goals

Proof state:
case a
x : PartENat
h : x < ⊤
⊢ x + 1 ≤ ⊤

Tactic:
apply le_top

Result:
no goals

Proof state:
case a
x : PartENat
n : ℕ
h : x < ↑n
⊢ x + 1 ≤ ↑n

Tactic:
rcases ne_top_iff.mp (ne_top_of_lt h) with ⟨m, rfl⟩

Result:
case a.intro
n m : ℕ
h : ↑m < ↑n
⊢ ↑m + 1 ≤ ↑n
-- Mathlib/GroupTheory/MonoidLocalization/Basic.lean
theorem r_iff_oreEqv_r {x y : M × S} : r S x y ↔ (OreLocalization.oreEqv S M).r x y

Proof state:
case mp.intro.intro
M : Type u_1
inst✝ : CommMonoid M
S : Submonoid M
x y : M × ↥S
u : M
hu : u ∈ S
e : u * (↑y.2 * x.1) = u * (↑x.2 * y.1)
⊢ ∃ a ∈ S, ∃ v, a * y.1 = v * x.1 ∧ a * ↑y.2 = v * ↑x.2

Tactic:
exact ⟨_, mul_mem hu x.2.2, u * y.2, by rw [mul_assoc, mul_assoc, ← e], mul_right_comm _ _ _⟩

Result:
no goals

Proof state:
M : Type u_1
inst✝ : CommMonoid M
S : Submonoid M
x y : M × ↥S
u : M
hu : u ∈ S
e : u * (↑y.2 * x.1) = u * (↑x.2 * y.1)
⊢ u * ↑x.2 * y.1 = u * ↑y.2 * x.1

Tactic:
rw [mul_assoc, mul_assoc, ← e]

Result:
no goals

Proof state:
M : Type u_1
inst✝ : CommMonoid M
S : Submonoid M
x y : M × ↥S
⊢ (r S) x y ↔ (OreLocalization.oreEqv S M) x y

Tactic:
simp only [r_iff_exists, Subtype.exists, exists_prop, OreLocalization.oreEqv, smul_eq_mul,
  Submonoid.mk_smul]

Result:
M : Type u_1
inst✝ : CommMonoid M
S : Submonoid M
x y : M × ↥S
⊢ (∃ a ∈ S, a * (↑y.2 * x.1) = a * (↑x.2 * y.1)) ↔ ∃ a ∈ S, ∃ v, a * y.1 = v * x.1 ∧ a * ↑y.2 = v * ↑x.2

Proof state:
M : Type u_1
inst✝ : CommMonoid M
S : Submonoid M
x y : M × ↥S
⊢ (∃ a ∈ S, a * (↑y.2 * x.1) = a * (↑x.2 * y.1)) ↔ ∃ a ∈ S, ∃ v, a * y.1 = v * x.1 ∧ a * ↑y.2 = v * ↑x.2

Tactic:
constructor

Result:
case mp
M : Type u_1
inst✝ : CommMonoid M
S : Submonoid M
x y : M × ↥S
⊢ (∃ a ∈ S, a * (↑y.2 * x.1) = a * (↑x.2 * y.1)) → ∃ a ∈ S, ∃ v, a * y.1 = v * x.1 ∧ a * ↑y.2 = v * ↑x.2

case mpr
M : Type u_1
inst✝ : CommMonoid M
S : Submonoid M
x y : M × ↥S
⊢ (∃ a ∈ S, ∃ v, a * y.1 = v * x.1 ∧ a * ↑y.2 = v * ↑x.2) → ∃ a ∈ S, a * (↑y.2 * x.1) = a * (↑x.2 * y.1)

Proof state:
case mp
M : Type u_1
inst✝ : CommMonoid M
S : Submonoid M
x y : M × ↥S
⊢ (∃ a ∈ S, a * (↑y.2 * x.1) = a * (↑x.2 * y.1)) → ∃ a ∈ S, ∃ v, a * y.1 = v * x.1 ∧ a * ↑y.2 = v * ↑x.2

Tactic:
rintro ⟨u, hu, e⟩

Result:
case mp.intro.intro
M : Type u_1
inst✝ : CommMonoid M
S : Submonoid M
x y : M × ↥S
u : M
hu : u ∈ S
e : u * (↑y.2 * x.1) = u * (↑x.2 * y.1)
⊢ ∃ a ∈ S, ∃ v, a * y.1 = v * x.1 ∧ a * ↑y.2 = v * ↑x.2

Proof state:
M : Type u_1
inst✝ : CommMonoid M
S : Submonoid M
x y : M × ↥S
u : M
hu : u ∈ S
v : M
e₁ : u * y.1 = v * x.1
e₂ : u * ↑y.2 = v * ↑x.2
⊢ u * (↑y.2 * x.1) = u * (↑x.2 * y.1)

Tactic:
rw [← mul_assoc, e₂, mul_right_comm, ← e₁, mul_assoc, mul_comm y.1]

Result:
no goals

Proof state:
case mpr.intro.intro.intro.intro
M : Type u_1
inst✝ : CommMonoid M
S : Submonoid M
x y : M × ↥S
u : M
hu : u ∈ S
v : M
e₁ : u * y.1 = v * x.1
e₂ : u * ↑y.2 = v * ↑x.2
⊢ ∃ a ∈ S, a * (↑y.2 * x.1) = a * (↑x.2 * y.1)

Tactic:
exact ⟨u, hu, by rw [← mul_assoc, e₂, mul_right_comm, ← e₁, mul_assoc, mul_comm y.1]⟩

Result:
no goals

Proof state:
case mpr
M : Type u_1
inst✝ : CommMonoid M
S : Submonoid M
x y : M × ↥S
⊢ (∃ a ∈ S, ∃ v, a * y.1 = v * x.1 ∧ a * ↑y.2 = v * ↑x.2) → ∃ a ∈ S, a * (↑y.2 * x.1) = a * (↑x.2 * y.1)

Tactic:
rintro ⟨u, hu, v, e₁, e₂⟩

Result:
case mpr.intro.intro.intro.intro
M : Type u_1
inst✝ : CommMonoid M
S : Submonoid M
x y : M × ↥S
u : M
hu : u ∈ S
v : M
e₁ : u * y.1 = v * x.1
e₂ : u * ↑y.2 = v * ↑x.2
⊢ ∃ a ∈ S, a * (↑y.2 * x.1) = a * (↑x.2 * y.1)
-- Mathlib/GroupTheory/SpecificGroups/Cyclic.lean
theorem card_pow_eq_one_eq_orderOf_aux (a : α) : #{b : α | b ^ orderOf a = 1} = orderOf a :=
  le_antisymm (hn _ (orderOf_pos a))
    (calc
      orderOf a = @Fintype.card (zpowers a) (id _) := Fintype.card_zpowers.symm
      _ ≤
          @Fintype.card (({b : α | b ^ orderOf a = 1} : Finset _) : Set α)
            (Fintype.ofFinset _ fun _ => Iff.rfl) :=
        (@Fintype.card_le_of_injective (zpowers a)
          (({b : α | b ^ orderOf a = 1} : Finset _) : Set α) (id _) (id _)
          (fun b =>
            ⟨b.1,
              mem_filter.2
                ⟨mem_univ _, by
                  let ⟨i, hi⟩ := b.2
                  rw [← hi, ← zpow_natCast, ← zpow_mul, mul_comm, zpow_mul, zpow_natCast,
                    pow_orderOf_eq_one, one_zpow]⟩⟩)
          fun _ _ h => Subtype.eq (Subtype.mk.inj h))
      _ = #{b : α | b ^ orderOf a = 1} := Fintype.card_ofFinset _ _
      )

Proof state:
α : Type u_1
inst✝² : Group α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hn : ∀ (n : ℕ), 0 < n → #(filter (fun a => a ^ n = 1) univ) ≤ n
a : α
b : ↥(zpowers a)
i : ℤ
hi : (fun x => a ^ x) i = ↑b
⊢ ↑b ^ orderOf a = 1

Tactic:
rw [← hi, ← zpow_natCast, ← zpow_mul, mul_comm, zpow_mul, zpow_natCast,
  pow_orderOf_eq_one, one_zpow]

Result:
no goals

Proof state:
α : Type u_1
inst✝² : Group α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hn : ∀ (n : ℕ), 0 < n → #(filter (fun a => a ^ n = 1) univ) ≤ n
a : α
b : ↥(zpowers a)
⊢ ↑b ^ orderOf a = 1

Tactic:
let ⟨i, hi⟩ := b.2

Result:
α : Type u_1
inst✝² : Group α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hn : ∀ (n : ℕ), 0 < n → #(filter (fun a => a ^ n = 1) univ) ≤ n
a : α
b : ↥(zpowers a)
i : ℤ
hi : (fun x => a ^ x) i = ↑b
⊢ ↑b ^ orderOf a = 1
-- Mathlib/Algebra/DirectSum/Internal.lean
theorem coe_mul_of_apply_of_mem_zero [AddMonoid ι] [SetLike.GradedMonoid A] (r : ⨁ i, A i)
    (r' : A 0) (j : ι) : ((r * of (fun i => A i) 0 r') j : R) = r j * r' :=
  coe_mul_of_apply_aux _ _ _ fun _x => by rw [add_zero]

Proof state:
ι : Type u_1
σ : Type u_2
R : Type u_4
inst✝⁵ : DecidableEq ι
inst✝⁴ : Semiring R
inst✝³ : SetLike σ R
inst✝² : AddSubmonoidClass σ R
A : ι → σ
inst✝¹ : AddMonoid ι
inst✝ : SetLike.GradedMonoid A
r : ⨁ (i : ι), ↥(A i)
r' : ↥(A 0)
j _x : ι
⊢ _x + 0 = j ↔ _x = j

Tactic:
rw [add_zero]

Result:
no goals