harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/LinearAlgebra/Eigenspace/Basic.lean
@[deprecated genEigenspace_le_smul (since := "2024-10-23")]
lemma iSup_genEigenspace_le_smul (f : Module.End R M) (μ t : R) :
    (⨆ k : ℕ, f.genEigenspace μ k) ≤ ⨆ k : ℕ, (t • f).genEigenspace (t * μ) k

Proof state:
R : Type v
M : Type w
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : End R M
μ t : R
⊢ ⨆ k, (f.genEigenspace μ) ↑k ≤ ⨆ k, ((t • f).genEigenspace (t * μ)) ↑k

Tactic:
rw [iSup_genEigenspace_eq, iSup_genEigenspace_eq]

Result:
R : Type v
M : Type w
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : End R M
μ t : R
⊢ f.maxGenEigenspace μ ≤ (t • f).maxGenEigenspace (t * μ)

Proof state:
R : Type v
M : Type w
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : End R M
μ t : R
⊢ f.maxGenEigenspace μ ≤ (t • f).maxGenEigenspace (t * μ)

Tactic:
apply genEigenspace_le_smul

Result:
no goals
-- Mathlib/Algebra/Star/Pointwise.lean
theorem star_add [AddMonoid α] [StarAddMonoid α] (s t : Set α) : (s + t)⋆ = s⋆ + t⋆

Proof state:
α : Type u_1
inst✝¹ : AddMonoid α
inst✝ : StarAddMonoid α
s t : Set α
⊢ (s + t)⋆ = s⋆ + t⋆

Tactic:
simp_rw [← image_star, ← image2_add, image_image2, image2_image_left, image2_image_right,
  star_add]

Result:
no goals
-- Mathlib/Data/List/MinMax.lean
theorem maximum_ne_bot_of_ne_nil (h : l ≠ []) : l.maximum ≠ ⊥ :=
  match l, h with | _ :: _, _ => by simp [maximum_cons]

Proof state:
α : Type u_1
inst✝ : LinearOrder α
l : List α
h : l ≠ []
head✝ : α
tail✝ : List α
x✝ : head✝ :: tail✝ ≠ []
⊢ (head✝ :: tail✝).maximum ≠ ⊥

Tactic:
simp [maximum_cons]

Result:
no goals
-- Mathlib/RingTheory/MvPowerSeries/Basic.lean
theorem coeff_pow [DecidableEq σ] (f : MvPowerSeries σ R) {n : ℕ} (d : σ →₀ ℕ) :
    coeff R d (f ^ n) =
      ∑ l ∈ finsuppAntidiag (Finset.range n) d,
        ∏ i ∈ Finset.range n, coeff R (l i) f

Proof state:
σ : Type u_1
R : Type u_3
inst✝¹ : CommSemiring R
inst✝ : DecidableEq σ
f : MvPowerSeries σ R
n : ℕ
d : σ →₀ ℕ
⊢ f ^ n = ∏ x ∈ range n, f

Tactic:
rw [Finset.prod_const, card_range]

Result:
no goals

Proof state:
σ : Type u_1
R : Type u_3
inst✝¹ : CommSemiring R
inst✝ : DecidableEq σ
f : MvPowerSeries σ R
n : ℕ
d : σ →₀ ℕ
this : f ^ n = ∏ x ∈ range n, f
⊢ (coeff R d) (f ^ n) = ∑ l ∈ (range n).finsuppAntidiag d, ∏ i ∈ range n, (coeff R (l i)) f

Tactic:
rw [this, coeff_prod]

Result:
no goals

Proof state:
σ : Type u_1
R : Type u_3
inst✝¹ : CommSemiring R
inst✝ : DecidableEq σ
f : MvPowerSeries σ R
n : ℕ
d : σ →₀ ℕ
⊢ (coeff R d) (f ^ n) = ∑ l ∈ (range n).finsuppAntidiag d, ∏ i ∈ range n, (coeff R (l i)) f

Tactic:
suffices f ^ n = (Finset.range n).prod fun _ ↦ f by
  rw [this, coeff_prod]

Result:
σ : Type u_1
R : Type u_3
inst✝¹ : CommSemiring R
inst✝ : DecidableEq σ
f : MvPowerSeries σ R
n : ℕ
d : σ →₀ ℕ
⊢ f ^ n = ∏ x ∈ range n, f
-- Mathlib/Algebra/Order/Sub/Unbundled/Basic.lean
theorem tsub_lt_iff_tsub_lt (hb : AddLECancellable b) (hc : AddLECancellable c)
    (h₁ : b ≤ a) (h₂ : c ≤ a) : a - b < c ↔ a - c < b

Proof state:
α : Type u_1
inst✝⁵ : AddCommSemigroup α
inst✝⁴ : PartialOrder α
inst✝³ : ExistsAddOfLE α
inst✝² : AddLeftMono α
inst✝¹ : Sub α
inst✝ : OrderedSub α
a b c : α
hb : AddLECancellable b
hc : AddLECancellable c
h₁ : b ≤ a
h₂ : c ≤ a
⊢ a - b < c ↔ a - c < b

Tactic:
rw [hb.tsub_lt_iff_left h₁, hc.tsub_lt_iff_right h₂]

Result:
no goals
-- Mathlib/GroupTheory/Perm/Cycle/Concrete.lean
theorem nodup_toCycle (f : Perm α) (hf : IsCycle f) : (toCycle f hf).Nodup

Proof state:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
f : Perm α
hf : f.IsCycle
⊢ (f.toCycle hf).Nodup

Tactic:
obtain ⟨x, hx, -⟩ := id hf

Result:
case intro.intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
f : Perm α
hf : f.IsCycle
x : α
hx : f x ≠ x
⊢ (f.toCycle hf).Nodup

Proof state:
case intro.intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
f : Perm α
hf : f.IsCycle
x : α
hx : f x ≠ x
⊢ (f.toCycle hf).Nodup

Tactic:
simpa [toCycle_eq_toList f hf x hx] using nodup_toList _ _

Result:
no goals
-- Mathlib/Topology/Algebra/Group/Basic.lean
theorem isClosed_setOf_map_inv [Inv G₁] [Inv G₂] [ContinuousInv G₂] :
    IsClosed { f : G₁ → G₂ | ∀ x, f x⁻¹ = (f x)⁻¹ }

Proof state:
G₁ : Type u_2
G₂ : Type u_3
inst✝⁴ : TopologicalSpace G₂
inst✝³ : T2Space G₂
inst✝² : Inv G₁
inst✝¹ : Inv G₂
inst✝ : ContinuousInv G₂
⊢ IsClosed (⋂ i, {x | x i⁻¹ = (x i)⁻¹})

Tactic:
exact isClosed_iInter fun i => isClosed_eq (continuous_apply _) (continuous_apply _).inv

Result:
no goals

Proof state:
G₁ : Type u_2
G₂ : Type u_3
inst✝⁴ : TopologicalSpace G₂
inst✝³ : T2Space G₂
inst✝² : Inv G₁
inst✝¹ : Inv G₂
inst✝ : ContinuousInv G₂
⊢ IsClosed {f | ∀ (x : G₁), f x⁻¹ = (f x)⁻¹}

Tactic:
simp only [setOf_forall]

Result:
G₁ : Type u_2
G₂ : Type u_3
inst✝⁴ : TopologicalSpace G₂
inst✝³ : T2Space G₂
inst✝² : Inv G₁
inst✝¹ : Inv G₂
inst✝ : ContinuousInv G₂
⊢ IsClosed (⋂ i, {x | x i⁻¹ = (x i)⁻¹})
-- Mathlib/Topology/Basic.lean
theorem Dense.open_subset_closure_inter (hs : Dense s) (ht : IsOpen t) :
    t ⊆ closure (t ∩ s) :=
  calc
    t = t ∩ closure s

Proof state:
X : Type u
s t : Set X
inst✝ : TopologicalSpace X
hs : Dense s
ht : IsOpen t
⊢ t = t ∩ closure s

Tactic:
rw [hs.closure_eq, inter_univ]

Result:
no goals
-- Mathlib/RingTheory/Localization/Away/Basic.lean
lemma mapₐ_surjective_of_surjective {f : A →ₐ[R] B} (a : A) [Away a Aₚ] [Away (f a) Bₚ]
    (hf : Function.Surjective f) : Function.Surjective (mapₐ Aₚ Bₚ f a) :=
  have : IsLocalization (Submonoid.map f.toRingHom (Submonoid.powers a)) Bₚ

Proof state:
R : Type u_1
inst✝¹⁴ : CommSemiring R
A : Type u_5
inst✝¹³ : CommSemiring A
inst✝¹² : Algebra R A
B : Type u_6
inst✝¹¹ : CommSemiring B
inst✝¹⁰ : Algebra R B
Aₚ : Type u_7
inst✝⁹ : CommSemiring Aₚ
inst✝⁸ : Algebra A Aₚ
inst✝⁷ : Algebra R Aₚ
inst✝⁶ : IsScalarTower R A Aₚ
Bₚ : Type u_8
inst✝⁵ : CommSemiring Bₚ
inst✝⁴ : Algebra B Bₚ
inst✝³ : Algebra R Bₚ
inst✝² : IsScalarTower R B Bₚ
f : A →ₐ[R] B
a : A
inst✝¹ : Away a Aₚ
inst✝ : Away (f a) Bₚ
hf : Function.Surjective ⇑f
⊢ IsLocalization (Submonoid.map f.toRingHom (Submonoid.powers a)) Bₚ

Tactic:
simp only [AlgHom.toRingHom_eq_coe, Submonoid.map_powers, RingHom.coe_coe]

Result:
R : Type u_1
inst✝¹⁴ : CommSemiring R
A : Type u_5
inst✝¹³ : CommSemiring A
inst✝¹² : Algebra R A
B : Type u_6
inst✝¹¹ : CommSemiring B
inst✝¹⁰ : Algebra R B
Aₚ : Type u_7
inst✝⁹ : CommSemiring Aₚ
inst✝⁸ : Algebra A Aₚ
inst✝⁷ : Algebra R Aₚ
inst✝⁶ : IsScalarTower R A Aₚ
Bₚ : Type u_8
inst✝⁵ : CommSemiring Bₚ
inst✝⁴ : Algebra B Bₚ
inst✝³ : Algebra R Bₚ
inst✝² : IsScalarTower R B Bₚ
f : A →ₐ[R] B
a : A
inst✝¹ : Away a Aₚ
inst✝ : Away (f a) Bₚ
hf : Function.Surjective ⇑f
⊢ IsLocalization (Submonoid.powers (f a)) Bₚ

Proof state:
R : Type u_1
inst✝¹⁴ : CommSemiring R
A : Type u_5
inst✝¹³ : CommSemiring A
inst✝¹² : Algebra R A
B : Type u_6
inst✝¹¹ : CommSemiring B
inst✝¹⁰ : Algebra R B
Aₚ : Type u_7
inst✝⁹ : CommSemiring Aₚ
inst✝⁸ : Algebra A Aₚ
inst✝⁷ : Algebra R Aₚ
inst✝⁶ : IsScalarTower R A Aₚ
Bₚ : Type u_8
inst✝⁵ : CommSemiring Bₚ
inst✝⁴ : Algebra B Bₚ
inst✝³ : Algebra R Bₚ
inst✝² : IsScalarTower R B Bₚ
f : A →ₐ[R] B
a : A
inst✝¹ : Away a Aₚ
inst✝ : Away (f a) Bₚ
hf : Function.Surjective ⇑f
⊢ IsLocalization (Submonoid.powers (f a)) Bₚ

Tactic:
infer_instance

Result:
no goals
-- Mathlib/RingTheory/Polynomial/Cyclotomic/Eval.lean
theorem cyclotomic_eval_le_add_one_pow_totient {q : ℝ} (hq' : 1 < q) :
    ∀ n, (cyclotomic n ℝ).eval q ≤ (q + 1) ^ totient n
  | 0 => by simp
  | 1 => by simp [add_assoc, add_nonneg, zero_le_one]
  | 2 => by simp
  | _ + 3 => (cyclotomic_eval_lt_add_one_pow_totient le_add_self hq').le

Proof state:
q : ℝ
hq' : 1 < q
⊢ eval q (cyclotomic 2 ℝ) ≤ (q + 1) ^ φ 2

Tactic:
simp

Result:
no goals

Proof state:
q : ℝ
hq' : 1 < q
⊢ eval q (cyclotomic 0 ℝ) ≤ (q + 1) ^ φ 0

Tactic:
simp

Result:
no goals

Proof state:
q : ℝ
hq' : 1 < q
⊢ eval q (cyclotomic 1 ℝ) ≤ (q + 1) ^ φ 1

Tactic:
simp [add_assoc, add_nonneg, zero_le_one]

Result:
no goals
-- Mathlib/Algebra/Group/Basic.lean
@[to_additive]
lemma eq_of_mul_inv_eq_one (h : a * b⁻¹ = 1) : a = b

Proof state:
α : Type u_1
inst✝ : DivisionMonoid α
a b : α
h : a * b⁻¹ = 1
⊢ a = b

Tactic:
simpa using eq_inv_of_mul_eq_one_left h

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Zip.lean
theorem zipWith_map_right (l₁ : List α) (l₂ : List β) (f : β → β') (g : α → β' → γ) :
    zipWith g l₁ (l₂.map f) = zipWith (fun a b => g a (f b)) l₁ l₂

Proof state:
α : Type u_1
β : Type u_2
β' : Type u_3
γ : Type u_4
l₁ : List α
l₂ : List β
f : β → β'
g : α → β' → γ
⊢ zipWith g l₁ (map f l₂) = zipWith (fun a b => g a (f b)) l₁ l₂

Tactic:
induction l₁ generalizing l₂ <;> cases l₂ <;> simp_all

Result:
no goals
-- Mathlib/MeasureTheory/Integral/Pi.lean
theorem integral_fintype_prod_eq_pow {E : Type*} (ι : Type*) [Fintype ι] (f : E → 𝕜)
    [MeasureSpace E] [SigmaFinite (volume : Measure E)] :
    ∫ x : ι → E, ∏ i, f (x i) = (∫ x, f x) ^ (card ι)

Proof state:
𝕜 : Type u_1
inst✝³ : RCLike 𝕜
E : Type u_2
ι : Type u_3
inst✝² : Fintype ι
f : E → 𝕜
inst✝¹ : MeasureSpace E
inst✝ : SigmaFinite volume
⊢ ∫ (x : ι → E), ∏ i : ι, f (x i) = (∫ (x : E), f x) ^ card ι

Tactic:
rw [integral_fintype_prod_eq_prod, Finset.prod_const, card]

Result:
no goals
-- Mathlib/Order/Monotone/Defs.lean
theorem StrictAnti.prod_map (hf : StrictAnti f) (hg : StrictAnti g) : StrictAnti (Prod.map f g) :=
  fun a b ↦ by
  simp only [Prod.lt_iff]
  exact Or.imp (And.imp hf.imp hg.antitone.imp) (And.imp hf.antitone.imp hg.imp)

Proof state:
α : Type u
β : Type v
γ : Type w
δ : Type u_2
inst✝³ : PartialOrder α
inst✝² : PartialOrder β
inst✝¹ : Preorder γ
inst✝ : Preorder δ
f : α → γ
g : β → δ
hf : StrictAnti f
hg : StrictAnti g
a b : α × β
⊢ a < b → Prod.map f g b < Prod.map f g a

Tactic:
simp only [Prod.lt_iff]

Result:
α : Type u
β : Type v
γ : Type w
δ : Type u_2
inst✝³ : PartialOrder α
inst✝² : PartialOrder β
inst✝¹ : Preorder γ
inst✝ : Preorder δ
f : α → γ
g : β → δ
hf : StrictAnti f
hg : StrictAnti g
a b : α × β
⊢ a.fst < b.fst ∧ a.snd ≤ b.snd ∨ a.fst ≤ b.fst ∧ a.snd < b.snd →
    (Prod.map f g b).fst < (Prod.map f g a).fst ∧ (Prod.map f g b).snd ≤ (Prod.map f g a).snd ∨
      (Prod.map f g b).fst ≤ (Prod.map f g a).fst ∧ (Prod.map f g b).snd < (Prod.map f g a).snd

Proof state:
α : Type u
β : Type v
γ : Type w
δ : Type u_2
inst✝³ : PartialOrder α
inst✝² : PartialOrder β
inst✝¹ : Preorder γ
inst✝ : Preorder δ
f : α → γ
g : β → δ
hf : StrictAnti f
hg : StrictAnti g
a b : α × β
⊢ a.fst < b.fst ∧ a.snd ≤ b.snd ∨ a.fst ≤ b.fst ∧ a.snd < b.snd →
    (Prod.map f g b).fst < (Prod.map f g a).fst ∧ (Prod.map f g b).snd ≤ (Prod.map f g a).snd ∨
      (Prod.map f g b).fst ≤ (Prod.map f g a).fst ∧ (Prod.map f g b).snd < (Prod.map f g a).snd

Tactic:
exact Or.imp (And.imp hf.imp hg.antitone.imp) (And.imp hf.antitone.imp hg.imp)

Result:
no goals
-- Mathlib/ModelTheory/Semantics.lean
theorem realize_relabel {φ : L.Formula α} {g : α → β} {v : β → M} :
    (φ.relabel g).Realize v ↔ φ.Realize (v ∘ g)

Proof state:
L : Language
M : Type w
inst✝ : L.Structure M
α : Type u'
β : Type v'
φ : L.Formula α
g : α → β
v : β → M
⊢ (relabel g φ).Realize v ↔ φ.Realize (v ∘ g)

Tactic:
rw [Realize, Realize, relabel, BoundedFormula.realize_relabel, iff_eq_eq, Fin.castAdd_zero]

Result:
L : Language
M : Type w
inst✝ : L.Structure M
α : Type u'
β : Type v'
φ : L.Formula α
g : α → β
v : β → M
⊢ BoundedFormula.Realize φ (Sum.elim v (default ∘ Fin.cast ⋯) ∘ Sum.inl ∘ g) (default ∘ natAdd 0) =
    BoundedFormula.Realize φ (v ∘ g) default

Proof state:
L : Language
M : Type w
inst✝ : L.Structure M
α : Type u'
β : Type v'
φ : L.Formula α
g : α → β
v : β → M
⊢ BoundedFormula.Realize φ (Sum.elim v (default ∘ Fin.cast ⋯) ∘ Sum.inl ∘ g) (default ∘ natAdd 0) =
    BoundedFormula.Realize φ (v ∘ g) default

Tactic:
exact congr rfl (funext finZeroElim)

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Int/DivModLemmas.lean
theorem emod_add_cancel_left {m n k i : Int} : (i + m) % n = (i + k) % n ↔ m % n = k % n

Proof state:
m n k i : Int
⊢ (i + m) % n = (i + k) % n ↔ m % n = k % n

Tactic:
rw [Int.add_comm, Int.add_comm i, emod_add_cancel_right]

Result:
no goals
-- Mathlib/Analysis/Asymptotics/SpecificAsymptotics.lean
theorem Asymptotics.isLittleO_pow_pow_atTop_of_lt [OrderTopology 𝕜] {p q : ℕ} (hpq : p < q) :
    (fun x : 𝕜 => x ^ p) =o[atTop] fun x => x ^ q

Proof state:
𝕜 : Type u_1
inst✝¹ : NormedLinearOrderedField 𝕜
inst✝ : OrderTopology 𝕜
p q : ℕ
hpq : p < q
⊢ ∀ᶠ (x : 𝕜) in atTop, x ^ q = 0 → x ^ p = 0

Tactic:
exact (eventually_gt_atTop 0).mono fun x hx hxq => (pow_ne_zero q hx.ne' hxq).elim

Result:
no goals

Proof state:
𝕜 : Type u_1
inst✝¹ : NormedLinearOrderedField 𝕜
inst✝ : OrderTopology 𝕜
p q : ℕ
hpq : p < q
⊢ (fun x => x ^ p) =o[atTop] fun x => x ^ q

Tactic:
refine (isLittleO_iff_tendsto' ?_).mpr (tendsto_pow_div_pow_atTop_zero hpq)

Result:
𝕜 : Type u_1
inst✝¹ : NormedLinearOrderedField 𝕜
inst✝ : OrderTopology 𝕜
p q : ℕ
hpq : p < q
⊢ ∀ᶠ (x : 𝕜) in atTop, x ^ q = 0 → x ^ p = 0
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem exists_push_of_size_eq_add_one {xs : Array α} (h : xs.size = n + 1) :
    ∃ (ys : Array α) (a : α), xs = ys.push a :=
  exists_push_of_size_pos (by simp [h])

Proof state:
α : Type u_1
n : Nat
xs : Array α
h : xs.size = n + 1
⊢ 0 < xs.size

Tactic:
simp [h]

Result:
no goals
-- Mathlib/Data/Fin/Basic.lean
@[simp] lemma castLE_inj {hmn : m ≤ n} {a b : Fin m} : castLE hmn a = castLE hmn b ↔ a = b

Proof state:
n m : ℕ
hmn : m ≤ n
a b : Fin m
⊢ castLE hmn a = castLE hmn b ↔ a = b

Tactic:
simp [Fin.ext_iff]

Result:
no goals
-- Mathlib/Data/Real/EReal.lean
theorem sign_coe (x : ℝ) : sign (x : EReal) = sign x

Proof state:
x : ℝ
⊢ sign ↑x = sign x

Tactic:
simp only [sign, OrderHom.coe_mk, EReal.coe_pos, EReal.coe_neg']

Result:
no goals
-- Mathlib/Algebra/Star/SelfAdjoint.lean
theorem smul [Star R] [AddMonoid A] [StarAddMonoid A] [SMul R A] [StarModule R A]
    {r : R} (hr : IsSelfAdjoint r) {x : A} (hx : IsSelfAdjoint x) :
    IsSelfAdjoint (r • x)

Proof state:
R : Type u_1
A : Type u_2
inst✝⁴ : Star R
inst✝³ : AddMonoid A
inst✝² : StarAddMonoid A
inst✝¹ : SMul R A
inst✝ : StarModule R A
r : R
hr : IsSelfAdjoint r
x : A
hx : IsSelfAdjoint x
⊢ IsSelfAdjoint (r • x)

Tactic:
simp only [isSelfAdjoint_iff, star_smul, hr.star_eq, hx.star_eq]

Result:
no goals
-- Mathlib/Combinatorics/Additive/CovBySMul.lean
@[to_additive]
lemma CovBySMul.subset_right (hB : B₁ ⊆ B₂) (hAB : CovBySMul M K A B₁) :
    CovBySMul M K A B₂

Proof state:
M : Type u_1
X : Type u_3
inst✝¹ : Monoid M
inst✝ : MulAction M X
K : ℝ
A B₁ B₂ : Set X
hB : B₁ ⊆ B₂
hAB : CovBySMul M K A B₁
⊢ CovBySMul M K A B₂

Tactic:
simpa using hAB.trans (.of_subset (M := M) hB)

Result:
no goals
-- Mathlib/Data/Finsupp/Basic.lean
theorem prod_mapDomain_index_inj [CommMonoid N] {f : α → β} {s : α →₀ M} {h : β → M → N}
    (hf : Function.Injective f) : (s.mapDomain f).prod h = s.prod fun a b => h (f a) b

Proof state:
α : Type u_1
β : Type u_2
M : Type u_5
N : Type u_7
inst✝¹ : AddCommMonoid M
inst✝ : CommMonoid N
f : α → β
s : α →₀ M
h : β → M → N
hf : Injective f
⊢ (mapDomain f s).prod h = s.prod fun a b => h (f a) b

Tactic:
rw [← Function.Embedding.coeFn_mk f hf, ← embDomain_eq_mapDomain, prod_embDomain]

Result:
no goals
-- Mathlib/RepresentationTheory/Maschke.lean
theorem equivariantProjection_apply (v : W) :
    π.equivariantProjection G v = Ring.inverse (Fintype.card G : k) • ∑ g : G, π.conjugate g v

Proof state:
k : Type u
inst✝¹⁰ : CommRing k
G : Type u
inst✝⁹ : Group G
V : Type v
inst✝⁸ : AddCommGroup V
inst✝⁷ : Module k V
inst✝⁶ : Module (MonoidAlgebra k G) V
inst✝⁵ : IsScalarTower k (MonoidAlgebra k G) V
W : Type w
inst✝⁴ : AddCommGroup W
inst✝³ : Module k W
inst✝² : Module (MonoidAlgebra k G) W
inst✝¹ : IsScalarTower k (MonoidAlgebra k G) W
π : W →ₗ[k] V
inst✝ : Fintype G
v : W
⊢ (equivariantProjection G π) v = Ring.inverse ↑(Fintype.card G) • ∑ g : G, (π.conjugate g) v

Tactic:
simp only [equivariantProjection, smul_apply, sumOfConjugatesEquivariant_apply]

Result:
no goals
-- Mathlib/Algebra/Polynomial/Basic.lean
theorem mem_coeffs_iff {p : R[X]} {c : R} : c ∈ p.coeffs ↔ ∃ n ∈ p.support, c = p.coeff n

Proof state:
R : Type u
inst✝ : Semiring R
p : R[X]
c : R
⊢ c ∈ p.coeffs ↔ ∃ n ∈ p.support, c = p.coeff n

Tactic:
simp [coeffs, eq_comm, (Finset.mem_image)]

Result:
no goals
-- Mathlib/CategoryTheory/Limits/Shapes/Biproducts.lean
theorem biproduct.fromSubtype_eq_lift [DecidablePred p] :
    biproduct.fromSubtype f p =
      biproduct.lift fun j => if h : p j then biproduct.π (Subtype.restrict p f) ⟨j, h⟩ else 0 :=
  biproduct.hom_ext _ _ (by simp)

Proof state:
J : Type w
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroMorphisms C
f : J → C
inst✝² : HasBiproduct f
p : J → Prop
inst✝¹ : HasBiproduct (Subtype.restrict p f)
inst✝ : DecidablePred p
⊢ ∀ (j : J), fromSubtype f p ≫ π f j = (lift fun j => if h : p j then π (Subtype.restrict p f) ⟨j, h⟩ else 0) ≫ π f j

Tactic:
simp

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/PropLemmas.lean
theorem exists₂_imp {P : (x : α) → p x → Prop} : (∃ x h, P x h) → b ↔ ∀ x h, P x h → b

Proof state:
α : Sort u_1
p : α → Prop
b : Prop
P : (x : α) → p x → Prop
⊢ (∃ x h, P x h) → b ↔ ∀ (x : α) (h : p x), P x h → b

Tactic:
simp

Result:
no goals
-- Mathlib/Order/Filter/AtTopBot/Field.lean
theorem tendsto_mul_const_atTop_of_neg (hr : r < 0) :
    Tendsto (fun x => f x * r) l atTop ↔ Tendsto f l atBot

Proof state:
α : Type u_1
β : Type u_2
inst✝ : LinearOrderedField α
l : Filter β
f : β → α
r : α
hr : r < 0
⊢ Tendsto (fun x => f x * r) l atTop ↔ Tendsto f l atBot

Tactic:
simpa only [mul_comm] using tendsto_const_mul_atTop_of_neg hr

Result:
no goals
-- Mathlib/MeasureTheory/Group/Arithmetic.lean
/-- Compositional version of `Measurable.smul` for use by `fun_prop`. -/
@[to_additive (attr := fun_prop)
"Compositional version of `Measurable.vadd` for use by `fun_prop`."]
lemma Measurable.smul' [MeasurableSMul₂ M X] {f : α → β → M} {g : α → β → X} {h : α → β}
    (hf : Measurable ↿f) (hg : Measurable ↿g) (hh : Measurable h) :
    Measurable fun a ↦ (f a • g a) (h a)

Proof state:
M : Type u_2
X : Type u_3
α : Type u_4
β : Type u_5
inst✝³ : MeasurableSpace M
inst✝² : MeasurableSpace X
inst✝¹ : SMul M X
m : MeasurableSpace α
mβ : MeasurableSpace β
inst✝ : MeasurableSMul₂ M X
f : α → β → M
g : α → β → X
h : α → β
hf : Measurable ↿f
hg : Measurable ↿g
hh : Measurable h
⊢ Measurable fun a => f a (h a) • g a (h a)

Tactic:
fun_prop

Result:
no goals

Proof state:
M : Type u_2
X : Type u_3
α : Type u_4
β : Type u_5
inst✝³ : MeasurableSpace M
inst✝² : MeasurableSpace X
inst✝¹ : SMul M X
m : MeasurableSpace α
mβ : MeasurableSpace β
inst✝ : MeasurableSMul₂ M X
f : α → β → M
g : α → β → X
h : α → β
hf : Measurable ↿f
hg : Measurable ↿g
hh : Measurable h
⊢ Measurable fun a => (f a • g a) (h a)

Tactic:
simp

Result:
M : Type u_2
X : Type u_3
α : Type u_4
β : Type u_5
inst✝³ : MeasurableSpace M
inst✝² : MeasurableSpace X
inst✝¹ : SMul M X
m : MeasurableSpace α
mβ : MeasurableSpace β
inst✝ : MeasurableSMul₂ M X
f : α → β → M
g : α → β → X
h : α → β
hf : Measurable ↿f
hg : Measurable ↿g
hh : Measurable h
⊢ Measurable fun a => f a (h a) • g a (h a)
-- Mathlib/CategoryTheory/Localization/CalculusOfFractions.lean
lemma fac (F : C ⥤ E) (hF : W.IsInvertedBy F) : Q W ⋙ lift F hF = F :=
  Functor.ext (fun _ => rfl) (fun X Y f => by
    dsimp [lift]
    rw [Q_map, Hom.map_mk, id_comp, comp_id, map_ofHom])

Proof state:
C : Type u_1
inst✝² : Category.{u_4, u_1} C
W : MorphismProperty C
inst✝¹ : W.HasLeftCalculusOfFractions
E : Type u_3
inst✝ : Category.{u_5, u_3} E
F : C ⥤ E
hF : W.IsInvertedBy F
X Y : C
f : X ⟶ Y
⊢ (Q W ⋙ lift F hF).map f = eqToHom ⋯ ≫ F.map f ≫ eqToHom ⋯

Tactic:
dsimp [lift]

Result:
C : Type u_1
inst✝² : Category.{u_4, u_1} C
W : MorphismProperty C
inst✝¹ : W.HasLeftCalculusOfFractions
E : Type u_3
inst✝ : Category.{u_5, u_3} E
F : C ⥤ E
hF : W.IsInvertedBy F
X Y : C
f : X ⟶ Y
⊢ Hom.map ((Q W).map f) F hF = 𝟙 (F.obj X) ≫ F.map f ≫ 𝟙 (F.obj Y)

Proof state:
C : Type u_1
inst✝² : Category.{u_4, u_1} C
W : MorphismProperty C
inst✝¹ : W.HasLeftCalculusOfFractions
E : Type u_3
inst✝ : Category.{u_5, u_3} E
F : C ⥤ E
hF : W.IsInvertedBy F
X Y : C
f : X ⟶ Y
⊢ Hom.map ((Q W).map f) F hF = 𝟙 (F.obj X) ≫ F.map f ≫ 𝟙 (F.obj Y)

Tactic:
rw [Q_map, Hom.map_mk, id_comp, comp_id, map_ofHom]

Result:
no goals
-- Mathlib/Topology/Basic.lean
theorem isOpen_iff_forall_mem_open : IsOpen s ↔ ∀ x ∈ s, ∃ t, t ⊆ s ∧ IsOpen t ∧ x ∈ t

Proof state:
X : Type u
s : Set X
inst✝ : TopologicalSpace X
⊢ s ⊆ interior s ↔ ∀ x ∈ s, ∃ t ⊆ s, IsOpen t ∧ x ∈ t

Tactic:
simp only [subset_def, mem_interior]

Result:
no goals

Proof state:
X : Type u
s : Set X
inst✝ : TopologicalSpace X
⊢ IsOpen s ↔ ∀ x ∈ s, ∃ t ⊆ s, IsOpen t ∧ x ∈ t

Tactic:
rw [← subset_interior_iff_isOpen]

Result:
X : Type u
s : Set X
inst✝ : TopologicalSpace X
⊢ s ⊆ interior s ↔ ∀ x ∈ s, ∃ t ⊆ s, IsOpen t ∧ x ∈ t
-- Mathlib/Algebra/Order/SuccPred.lean
lemma strictAntiOn_of_lt_sub_one (hs : s.OrdConnected) :
    (∀ a, ¬ IsMin a → a ∈ s → a - 1 ∈ s → f a < f (a - 1)) → StrictAntiOn f s

Proof state:
α : Type u_2
β : Type u_3
inst✝⁵ : PartialOrder α
inst✝⁴ : Preorder β
inst✝³ : Sub α
inst✝² : One α
inst✝¹ : PredSubOrder α
inst✝ : IsPredArchimedean α
s : Set α
f : α → β
hs : s.OrdConnected
⊢ (∀ (a : α), ¬IsMin a → a ∈ s → a - 1 ∈ s → f a < f (a - 1)) → StrictAntiOn f s

Tactic:
simpa [Order.pred_eq_sub_one] using strictAntiOn_of_lt_pred hs (f := f)

Result:
no goals
-- Mathlib/Geometry/Euclidean/Sphere/Basic.lean
lemma isDiameter_iff_left_mem_and_pointReflection_center_left :
    s.IsDiameter p₁ p₂ ↔ p₁ ∈ s ∧ Equiv.pointReflection s.center p₁ = p₂ :=
  ⟨fun h ↦ ⟨h.1, h.pointReflection_center_left⟩, fun h ↦ ⟨h.1, by simp [← h.2]⟩⟩

Proof state:
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : NormedSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
s : Sphere P
p₁ p₂ : P
h : p₁ ∈ s ∧ (Equiv.pointReflection s.center) p₁ = p₂
⊢ midpoint ℝ p₁ p₂ = s.center

Tactic:
simp [← h.2]

Result:
no goals
-- Mathlib/Algebra/BigOperators/Group/Finset/Basic.lean
theorem prod_update_of_not_mem [DecidableEq α] {s : Finset α} {i : α} (h : i ∉ s) (f : α → β)
    (b : β) : ∏ x ∈ s, Function.update f i b x = ∏ x ∈ s, f x

Proof state:
α : Type u_3
β : Type u_4
inst✝¹ : CommMonoid β
inst✝ : DecidableEq α
s : Finset α
i : α
h : i ∉ s
f : α → β
b : β
⊢ ∀ x ∈ s, update f i b x = f x

Tactic:
intros j hj

Result:
α : Type u_3
β : Type u_4
inst✝¹ : CommMonoid β
inst✝ : DecidableEq α
s : Finset α
i : α
h : i ∉ s
f : α → β
b : β
j : α
hj : j ∈ s
⊢ update f i b j = f j

Proof state:
α : Type u_3
β : Type u_4
inst✝¹ : CommMonoid β
inst✝ : DecidableEq α
s : Finset α
i : α
h : i ∉ s
f : α → β
b : β
j : α
hj : j ∈ s
this : j ≠ i
⊢ update f i b j = f j

Tactic:
simp [this]

Result:
no goals

Proof state:
α : Type u_3
β : Type u_4
inst✝¹ : CommMonoid β
inst✝ : DecidableEq α
s : Finset α
i : α
h : i ∉ s
f : α → β
b : β
⊢ ∏ x ∈ s, update f i b x = ∏ x ∈ s, f x

Tactic:
apply prod_congr rfl

Result:
α : Type u_3
β : Type u_4
inst✝¹ : CommMonoid β
inst✝ : DecidableEq α
s : Finset α
i : α
h : i ∉ s
f : α → β
b : β
⊢ ∀ x ∈ s, update f i b x = f x

Proof state:
α : Type u_3
β : Type u_4
inst✝¹ : CommMonoid β
inst✝ : DecidableEq α
s : Finset α
i : α
h : i ∉ s
f : α → β
b : β
j : α
hj : j ∈ s
⊢ j ≠ i

Tactic:
rintro rfl

Result:
α : Type u_3
β : Type u_4
inst✝¹ : CommMonoid β
inst✝ : DecidableEq α
s : Finset α
f : α → β
b : β
j : α
hj : j ∈ s
h : j ∉ s
⊢ False

Proof state:
α : Type u_3
β : Type u_4
inst✝¹ : CommMonoid β
inst✝ : DecidableEq α
s : Finset α
i : α
h : i ∉ s
f : α → β
b : β
j : α
hj : j ∈ s
⊢ update f i b j = f j

Tactic:
have : j ≠ i := by
  rintro rfl
  exact h hj

Result:
α : Type u_3
β : Type u_4
inst✝¹ : CommMonoid β
inst✝ : DecidableEq α
s : Finset α
i : α
h : i ∉ s
f : α → β
b : β
j : α
hj : j ∈ s
this : j ≠ i
⊢ update f i b j = f j

Proof state:
α : Type u_3
β : Type u_4
inst✝¹ : CommMonoid β
inst✝ : DecidableEq α
s : Finset α
f : α → β
b : β
j : α
hj : j ∈ s
h : j ∉ s
⊢ False

Tactic:
exact h hj

Result:
no goals
-- Mathlib/Data/Num/Lemmas.lean
theorem add_one : ∀ n : Num, n + 1 = succ n
  | 0 => rfl
  | pos p => by cases p <;> rfl

Proof state:
p : PosNum
⊢ pos p + 1 = (pos p).succ

Tactic:
cases p <;> rfl

Result:
no goals