harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Data/Finset/NatAntidiagonal.lean
theorem antidiagonal_succ_succ' {n : ℕ} :
    antidiagonal (n + 2) =
      cons (0, n + 2)
        (cons (n + 2, 0)
            ((antidiagonal n).map
              (Embedding.prodMap ⟨Nat.succ, Nat.succ_injective⟩
                ⟨Nat.succ, Nat.succ_injective⟩)) <|
          by simp)
        (by simp)

Proof state:
n : ℕ
⊢ antidiagonal (n + 2) =
    cons (0, n + 2)
      (cons (n + 2, 0)
        (map
          ({ toFun := Nat.succ, inj' := Nat.succ_injective }.prodMap { toFun := Nat.succ, inj' := Nat.succ_injective })
          (antidiagonal n))
        ⋯)
      ⋯

Tactic:
simp_rw [antidiagonal_succ (n + 1), antidiagonal_succ', Finset.map_cons, map_map]

Result:
n : ℕ
⊢ cons (0, n + 1 + 1)
      (cons (({ toFun := Nat.succ, inj' := Nat.succ_injective }.prodMap (Embedding.refl ℕ)) (n + 1, 0))
        (map
          (((Embedding.refl ℕ).prodMap { toFun := Nat.succ, inj' := Nat.succ_injective }).trans
            ({ toFun := Nat.succ, inj' := Nat.succ_injective }.prodMap (Embedding.refl ℕ)))
          (antidiagonal n))
        ⋯)
      ⋯ =
    cons (0, n + 2)
      (cons (n + 2, 0)
        (map
          ({ toFun := Nat.succ, inj' := Nat.succ_injective }.prodMap { toFun := Nat.succ, inj' := Nat.succ_injective })
          (antidiagonal n))
        ⋯)
      ⋯

Proof state:
n : ℕ
⊢ (n + 2, 0) ∉
    map ({ toFun := Nat.succ, inj' := Nat.succ_injective }.prodMap { toFun := Nat.succ, inj' := Nat.succ_injective })
      (antidiagonal n)

Tactic:
simp

Result:
no goals

Proof state:
n : ℕ
⊢ cons (0, n + 1 + 1)
      (cons (({ toFun := Nat.succ, inj' := Nat.succ_injective }.prodMap (Embedding.refl ℕ)) (n + 1, 0))
        (map
          (((Embedding.refl ℕ).prodMap { toFun := Nat.succ, inj' := Nat.succ_injective }).trans
            ({ toFun := Nat.succ, inj' := Nat.succ_injective }.prodMap (Embedding.refl ℕ)))
          (antidiagonal n))
        ⋯)
      ⋯ =
    cons (0, n + 2)
      (cons (n + 2, 0)
        (map
          ({ toFun := Nat.succ, inj' := Nat.succ_injective }.prodMap { toFun := Nat.succ, inj' := Nat.succ_injective })
          (antidiagonal n))
        ⋯)
      ⋯

Tactic:
rfl

Result:
no goals

Proof state:
n : ℕ
⊢ (0, n + 2) ∉
    cons (n + 2, 0)
      (map ({ toFun := Nat.succ, inj' := Nat.succ_injective }.prodMap { toFun := Nat.succ, inj' := Nat.succ_injective })
        (antidiagonal n))
      ⋯

Tactic:
simp

Result:
no goals
-- Mathlib/Topology/Bornology/Basic.lean
theorem isBounded_ofBounded_iff (B : Set (Set α)) {empty_mem subset_mem union_mem sUnion_univ} :
    @IsBounded _ (ofBounded B empty_mem subset_mem union_mem sUnion_univ) s ↔ s ∈ B

Proof state:
α : Type u_2
s : Set α
B : Set (Set α)
empty_mem : ∅ ∈ B
subset_mem : ∀ s₁ ∈ B, ∀ s₂ ⊆ s₁, s₂ ∈ B
union_mem : ∀ s₁ ∈ B, ∀ s₂ ∈ B, s₁ ∪ s₂ ∈ B
sUnion_univ : ∀ (x : α), {x} ∈ B
⊢ IsBounded s ↔ s ∈ B

Tactic:
rw [isBounded_def, ofBounded_cobounded, compl_mem_comk]

Result:
no goals
-- Mathlib/MeasureTheory/Integral/SetIntegral.lean
theorem setIntegral_indicator (ht : MeasurableSet t) :
    ∫ x in s, t.indicator f x ∂μ = ∫ x in s ∩ t, f x ∂μ

Proof state:
X : Type u_1
E : Type u_3
mX : MeasurableSpace X
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : X → E
s t : Set X
μ : Measure X
ht : MeasurableSet t
⊢ ∫ (x : X) in s, t.indicator f x ∂μ = ∫ (x : X) in s ∩ t, f x ∂μ

Tactic:
rw [integral_indicator ht, Measure.restrict_restrict ht, Set.inter_comm]

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Coloring.lean
lemma chromaticNumber_eq_iInf {G : SimpleGraph V} :
    G.chromaticNumber = ⨅ n : {m | G.Colorable m}, (n : ℕ∞)

Proof state:
V : Type u
G : SimpleGraph V
⊢ G.chromaticNumber = ⨅ n, ↑↑n

Tactic:
rw [chromaticNumber, iInf_subtype]

Result:
no goals
-- Mathlib/MeasureTheory/Measure/FiniteMeasure.lean
theorem smul_testAgainstNN_apply (c : ℝ≥0) (μ : FiniteMeasure Ω) (f : Ω →ᵇ ℝ≥0) :
    (c • μ).testAgainstNN f = c • μ.testAgainstNN f

Proof state:
Ω : Type u_1
inst✝¹ : MeasurableSpace Ω
inst✝ : TopologicalSpace Ω
c : ℝ≥0
μ : FiniteMeasure Ω
f : Ω →ᵇ ℝ≥0
⊢ (c • μ).testAgainstNN f = c • μ.testAgainstNN f

Tactic:
simp only [testAgainstNN, toMeasure_smul, smul_eq_mul, ← ENNReal.smul_toNNReal, ENNReal.smul_def,
  lintegral_smul_measure]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/AssocList/Lemmas.lean
theorem contains_eq [BEq α] {l : AssocList α β} {a : α} :
    l.contains a = containsKey a l.toList

Proof state:
α : Type u
β : α → Type v
inst✝ : BEq α
l : AssocList α β
a : α
⊢ contains a l = containsKey a l.toList

Tactic:
induction l <;> simp_all [contains, List.containsKey]

Result:
no goals
-- Mathlib/Analysis/Convex/Between.lean
theorem Wbtw.trans_left {w x y z : P} (h₁ : Wbtw R w y z) (h₂ : Wbtw R w x y) : Wbtw R w x z

Proof state:
R : Type u_1
V : Type u_2
P : Type u_4
inst✝³ : OrderedRing R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
w x y z : P
h₁ : Wbtw R w y z
h₂ : Wbtw R w x y
⊢ Wbtw R w x z

Tactic:
rcases h₁ with ⟨t₁, ht₁, rfl⟩

Result:
case intro.intro
R : Type u_1
V : Type u_2
P : Type u_4
inst✝³ : OrderedRing R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
w x z : P
t₁ : R
ht₁ : t₁ ∈ Set.Icc 0 1
h₂ : Wbtw R w x ((lineMap w z) t₁)
⊢ Wbtw R w x z

Proof state:
case intro.intro.intro.intro
R : Type u_1
V : Type u_2
P : Type u_4
inst✝³ : OrderedRing R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
w z : P
t₁ : R
ht₁ : t₁ ∈ Set.Icc 0 1
t₂ : R
ht₂ : t₂ ∈ Set.Icc 0 1
⊢ (lineMap w z) (t₂ * t₁) = (lineMap w ((lineMap w z) t₁)) t₂

Tactic:
rw [lineMap_apply, lineMap_apply, lineMap_vsub_left, smul_smul]

Result:
no goals

Proof state:
case intro.intro.intro.intro
R : Type u_1
V : Type u_2
P : Type u_4
inst✝³ : OrderedRing R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
w z : P
t₁ : R
ht₁ : t₁ ∈ Set.Icc 0 1
t₂ : R
ht₂ : t₂ ∈ Set.Icc 0 1
⊢ Wbtw R w ((lineMap w ((lineMap w z) t₁)) t₂) z

Tactic:
refine ⟨t₂ * t₁, ⟨mul_nonneg ht₂.1 ht₁.1, mul_le_one₀ ht₂.2 ht₁.1 ht₁.2⟩, ?_⟩

Result:
case intro.intro.intro.intro
R : Type u_1
V : Type u_2
P : Type u_4
inst✝³ : OrderedRing R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
w z : P
t₁ : R
ht₁ : t₁ ∈ Set.Icc 0 1
t₂ : R
ht₂ : t₂ ∈ Set.Icc 0 1
⊢ (lineMap w z) (t₂ * t₁) = (lineMap w ((lineMap w z) t₁)) t₂

Proof state:
case intro.intro
R : Type u_1
V : Type u_2
P : Type u_4
inst✝³ : OrderedRing R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
w x z : P
t₁ : R
ht₁ : t₁ ∈ Set.Icc 0 1
h₂ : Wbtw R w x ((lineMap w z) t₁)
⊢ Wbtw R w x z

Tactic:
rcases h₂ with ⟨t₂, ht₂, rfl⟩

Result:
case intro.intro.intro.intro
R : Type u_1
V : Type u_2
P : Type u_4
inst✝³ : OrderedRing R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
w z : P
t₁ : R
ht₁ : t₁ ∈ Set.Icc 0 1
t₂ : R
ht₂ : t₂ ∈ Set.Icc 0 1
⊢ Wbtw R w ((lineMap w ((lineMap w z) t₁)) t₂) z
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/MapIdx.lean
theorem mapIdx_eq_mapIdx_iff {l : Vector α n} :
    mapIdx f l = mapIdx g l ↔ ∀ (i : Nat) (h : i < n), f i l[i] = g i l[i]

Proof state:
case mk
α : Type u_1
α✝ : Type u_2
f g : Nat → α → α✝
l : Array α
⊢ mapIdx f { toArray := l, size_toArray := ⋯ } = mapIdx g { toArray := l, size_toArray := ⋯ } ↔
    ∀ (i : Nat) (h : i < l.size),
      f i { toArray := l, size_toArray := ⋯ }[i] = g i { toArray := l, size_toArray := ⋯ }[i]

Tactic:
simp [Array.mapIdx_eq_mapIdx_iff]

Result:
no goals

Proof state:
α : Type u_1
n : Nat
α✝ : Type u_2
f g : Nat → α → α✝
l : Vector α n
⊢ mapIdx f l = mapIdx g l ↔ ∀ (i : Nat) (h : i < n), f i l[i] = g i l[i]

Tactic:
rcases l with ⟨l, rfl⟩

Result:
case mk
α : Type u_1
α✝ : Type u_2
f g : Nat → α → α✝
l : Array α
⊢ mapIdx f { toArray := l, size_toArray := ⋯ } = mapIdx g { toArray := l, size_toArray := ⋯ } ↔
    ∀ (i : Nat) (h : i < l.size),
      f i { toArray := l, size_toArray := ⋯ }[i] = g i { toArray := l, size_toArray := ⋯ }[i]
-- Mathlib/GroupTheory/CoprodI.lean
theorem ext_hom (f g : CoprodI M →* N) (h : ∀ i, f.comp (of : M i →* _) = g.comp of) : f = g :=
  (MonoidHom.cancel_right Con.mk'_surjective).mp <|
    FreeMonoid.hom_eq fun ⟨i, x⟩ => by
      -- This used to be `rw`, but we need `erw` after https://github.com/leanprover/lean4/pull/2644
      erw [MonoidHom.comp_apply, MonoidHom.comp_apply, ← of_apply, ← MonoidHom.comp_apply, ←
        MonoidHom.comp_apply, h]; rfl

Proof state:
ι : Type u_1
M : ι → Type u_2
inst✝¹ : (i : ι) → Monoid (M i)
N : Type u_3
inst✝ : Monoid N
f g : CoprodI M →* N
h : ∀ (i : ι), f.comp of = g.comp of
x✝ : (i : ι) × M i
i : ι
x : M i
⊢ (g.comp of) x = (g.comp (conGen (Rel M)).mk') (FreeMonoid.of ⟨i, x⟩)

Tactic:
rfl

Result:
no goals

Proof state:
ι : Type u_1
M : ι → Type u_2
inst✝¹ : (i : ι) → Monoid (M i)
N : Type u_3
inst✝ : Monoid N
f g : CoprodI M →* N
h : ∀ (i : ι), f.comp of = g.comp of
x✝ : (i : ι) × M i
i : ι
x : M i
⊢ (f.comp (conGen (Rel M)).mk') (FreeMonoid.of ⟨i, x⟩) = (g.comp (conGen (Rel M)).mk') (FreeMonoid.of ⟨i, x⟩)

Tactic:
erw [MonoidHom.comp_apply, MonoidHom.comp_apply, ← of_apply, ← MonoidHom.comp_apply, ←
  MonoidHom.comp_apply, h]

Result:
ι : Type u_1
M : ι → Type u_2
inst✝¹ : (i : ι) → Monoid (M i)
N : Type u_3
inst✝ : Monoid N
f g : CoprodI M →* N
h : ∀ (i : ι), f.comp of = g.comp of
x✝ : (i : ι) × M i
i : ι
x : M i
⊢ (g.comp of) x = (g.comp (conGen (Rel M)).mk') (FreeMonoid.of ⟨i, x⟩)
-- Mathlib/Algebra/Homology/Embedding/Extend.lean
lemma mapX_some {i : Option ι} {a : ι} (hi : i = some a) :
    mapX φ i = (XIso K hi).hom ≫ φ.f a ≫ (XIso L hi).inv

Proof state:
ι : Type u_1
c : ComplexShape ι
C : Type u_3
inst✝² : Category.{u_4, u_3} C
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
K L : HomologicalComplex C c
φ : K ⟶ L
a : ι
⊢ mapX φ (some a) = φ.f a

Tactic:
rfl

Result:
no goals

Proof state:
ι : Type u_1
c : ComplexShape ι
C : Type u_3
inst✝² : Category.{u_4, u_3} C
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
K L : HomologicalComplex C c
φ : K ⟶ L
a : ι
⊢ mapX φ (some a) = (XIso K ⋯).hom ≫ φ.f a ≫ (XIso L ⋯).inv

Tactic:
dsimp [XIso]

Result:
ι : Type u_1
c : ComplexShape ι
C : Type u_3
inst✝² : Category.{u_4, u_3} C
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
K L : HomologicalComplex C c
φ : K ⟶ L
a : ι
⊢ mapX φ (some a) = 𝟙 (X K (some a)) ≫ φ.f a ≫ 𝟙 (X L (some a))

Proof state:
ι : Type u_1
c : ComplexShape ι
C : Type u_3
inst✝² : Category.{u_4, u_3} C
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
K L : HomologicalComplex C c
φ : K ⟶ L
a : ι
⊢ mapX φ (some a) = 𝟙 (X K (some a)) ≫ φ.f a ≫ 𝟙 (X L (some a))

Tactic:
erw [id_comp, comp_id]

Result:
ι : Type u_1
c : ComplexShape ι
C : Type u_3
inst✝² : Category.{u_4, u_3} C
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
K L : HomologicalComplex C c
φ : K ⟶ L
a : ι
⊢ mapX φ (some a) = φ.f a

Proof state:
ι : Type u_1
c : ComplexShape ι
C : Type u_3
inst✝² : Category.{u_4, u_3} C
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
K L : HomologicalComplex C c
φ : K ⟶ L
i : Option ι
a : ι
hi : i = some a
⊢ mapX φ i = (XIso K hi).hom ≫ φ.f a ≫ (XIso L hi).inv

Tactic:
subst hi

Result:
ι : Type u_1
c : ComplexShape ι
C : Type u_3
inst✝² : Category.{u_4, u_3} C
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
K L : HomologicalComplex C c
φ : K ⟶ L
a : ι
⊢ mapX φ (some a) = (XIso K ⋯).hom ≫ φ.f a ≫ (XIso L ⋯).inv
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Basic.lean
theorem zipWithAll_nil :
    zipWithAll f as [] = as.map fun a => f (some a) none

Proof state:
α✝² : Type u_1
α✝¹ : Type u_2
α✝ : Type u_3
f : Option α✝² → Option α✝¹ → α✝
as : List α✝²
⊢ zipWithAll f as nil = map (fun a => f (some a) none) as

Tactic:
cases as <;> rfl

Result:
no goals
-- Mathlib/NumberTheory/Divisors.lean
theorem filter_dvd_eq_properDivisors (h : n ≠ 0) : {d ∈ range n | d ∣ n} = n.properDivisors

Proof state:
case h
n : ℕ
h : n ≠ 0
a✝ : ℕ
⊢ a✝ ∣ n → a✝ < n → 1 ≤ a✝

Tactic:
exact fun ha _ => succ_le_iff.mpr (pos_of_dvd_of_pos ha h.bot_lt)

Result:
no goals

Proof state:
case h
n : ℕ
h : n ≠ 0
a✝ : ℕ
⊢ a✝ ∈ filter (fun d => d ∣ n) (range n) ↔ a✝ ∈ n.properDivisors

Tactic:
simp only [properDivisors, mem_filter, mem_range, mem_Ico, and_congr_left_iff, iff_and_self]

Result:
case h
n : ℕ
h : n ≠ 0
a✝ : ℕ
⊢ a✝ ∣ n → a✝ < n → 1 ≤ a✝

Proof state:
n : ℕ
h : n ≠ 0
⊢ filter (fun d => d ∣ n) (range n) = n.properDivisors

Tactic:
ext

Result:
case h
n : ℕ
h : n ≠ 0
a✝ : ℕ
⊢ a✝ ∈ filter (fun d => d ∣ n) (range n) ↔ a✝ ∈ n.properDivisors
-- Mathlib/Data/List/Basic.lean
theorem forall_iff_forall_mem : ∀ {l : List α}, Forall p l ↔ ∀ x ∈ l, p x
  | [] => (iff_true_intro <| forall_mem_nil _).symm
  | x :: l => by rw [forall_mem_cons, forall_cons, forall_iff_forall_mem]

Proof state:
α : Type u
p : α → Prop
x : α
l : List α
⊢ Forall p (x :: l) ↔ ∀ (x_1 : α), x_1 ∈ x :: l → p x_1

Tactic:
rw [forall_mem_cons, forall_cons, forall_iff_forall_mem]

Result:
no goals
-- Mathlib/GroupTheory/Coprod/Basic.lean
theorem mrange_eq (f : M ∗ N →* P) :
    MonoidHom.mrange f = MonoidHom.mrange (f.comp inl) ⊔ MonoidHom.mrange (f.comp inr)

Proof state:
M : Type u_1
N : Type u_2
P : Type u_5
inst✝² : MulOneClass M
inst✝¹ : MulOneClass N
inst✝ : MulOneClass P
f : M ∗ N →* P
⊢ MonoidHom.mrange f = MonoidHom.mrange (f.comp inl) ⊔ MonoidHom.mrange (f.comp inr)

Tactic:
rw [MonoidHom.mrange_eq_map, ← mrange_inl_sup_mrange_inr, Submonoid.map_sup, MonoidHom.map_mrange,
  MonoidHom.map_mrange]

Result:
no goals
-- Mathlib/Topology/Order/PartialSups.lean
protected lemma partialSups (hf : ∀ k ≤ n, Tendsto (f k) l (𝓝 (g k))) :
    Tendsto (partialSups f n) l (𝓝 (partialSups g n))

Proof state:
L : Type u_1
inst✝² : SemilatticeSup L
inst✝¹ : TopologicalSpace L
inst✝ : ContinuousSup L
α : Type u_2
l : Filter α
f : ℕ → α → L
g : ℕ → L
n : ℕ
hf : ∀ k ≤ n, Tendsto (f k) l (𝓝 (g k))
⊢ ∀ i ∈ Finset.range (n + 1), Tendsto (f i) l (𝓝 (g i))

Tactic:
simpa [Nat.lt_succ_iff]

Result:
no goals

Proof state:
L : Type u_1
inst✝² : SemilatticeSup L
inst✝¹ : TopologicalSpace L
inst✝ : ContinuousSup L
α : Type u_2
l : Filter α
f : ℕ → α → L
g : ℕ → L
n : ℕ
hf : ∀ k ≤ n, Tendsto (f k) l (𝓝 (g k))
⊢ Tendsto ((Finset.range (n + 1)).sup' ⋯ f) l (𝓝 ((Finset.range (n + 1)).sup' ⋯ g))

Tactic:
refine finset_sup'_nhds _ ?_

Result:
L : Type u_1
inst✝² : SemilatticeSup L
inst✝¹ : TopologicalSpace L
inst✝ : ContinuousSup L
α : Type u_2
l : Filter α
f : ℕ → α → L
g : ℕ → L
n : ℕ
hf : ∀ k ≤ n, Tendsto (f k) l (𝓝 (g k))
⊢ ∀ i ∈ Finset.range (n + 1), Tendsto (f i) l (𝓝 (g i))

Proof state:
L : Type u_1
inst✝² : SemilatticeSup L
inst✝¹ : TopologicalSpace L
inst✝ : ContinuousSup L
α : Type u_2
l : Filter α
f : ℕ → α → L
g : ℕ → L
n : ℕ
hf : ∀ k ≤ n, Tendsto (f k) l (𝓝 (g k))
⊢ Tendsto ((partialSups f) n) l (𝓝 ((partialSups g) n))

Tactic:
simp only [partialSups_eq_sup'_range]

Result:
L : Type u_1
inst✝² : SemilatticeSup L
inst✝¹ : TopologicalSpace L
inst✝ : ContinuousSup L
α : Type u_2
l : Filter α
f : ℕ → α → L
g : ℕ → L
n : ℕ
hf : ∀ k ≤ n, Tendsto (f k) l (𝓝 (g k))
⊢ Tendsto ((Finset.range (n + 1)).sup' ⋯ f) l (𝓝 ((Finset.range (n + 1)).sup' ⋯ g))
-- Mathlib/Data/Finsupp/BigOperators.lean
theorem Multiset.support_sum_subset [AddCommMonoid M] (s : Multiset (ι →₀ M)) :
    s.sum.support ⊆ (s.map Finsupp.support).sup

Proof state:
ι : Type u_1
M : Type u_2
inst✝¹ : DecidableEq ι
inst✝ : AddCommMonoid M
s : Multiset (ι →₀ M)
⊢ s.sum.support ⊆ (map Finsupp.support s).sup

Tactic:
induction s using Quot.inductionOn

Result:
case h
ι : Type u_1
M : Type u_2
inst✝¹ : DecidableEq ι
inst✝ : AddCommMonoid M
a✝ : List (ι →₀ M)
⊢ (sum (Quot.mk (⇑(List.isSetoid (ι →₀ M))) a✝)).support ⊆
    (map Finsupp.support (Quot.mk (⇑(List.isSetoid (ι →₀ M))) a✝)).sup

Proof state:
case h
ι : Type u_1
M : Type u_2
inst✝¹ : DecidableEq ι
inst✝ : AddCommMonoid M
a✝ : List (ι →₀ M)
⊢ (sum (Quot.mk (⇑(List.isSetoid (ι →₀ M))) a✝)).support ⊆
    (map Finsupp.support (Quot.mk (⇑(List.isSetoid (ι →₀ M))) a✝)).sup

Tactic:
simpa only [Multiset.quot_mk_to_coe'', Multiset.sum_coe, Multiset.map_coe, Multiset.sup_coe,
  List.foldr_map] using List.support_sum_subset _

Result:
no goals
-- Mathlib/RingTheory/LocalRing/ResidueField/Basic.lean
lemma residue_ne_zero_iff_isUnit (x : R) : residue R x ≠ 0 ↔ IsUnit x

Proof state:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsLocalRing R
x : R
⊢ (residue R) x ≠ 0 ↔ IsUnit x

Tactic:
simp

Result:
no goals
-- Mathlib/Algebra/GroupWithZero/Basic.lean
theorem mul_left_surjective₀ {a : G₀} (h : a ≠ 0) : Surjective fun g => a * g := fun g =>
  ⟨a⁻¹ * g, by simp [← mul_assoc, mul_inv_cancel₀ h]⟩

Proof state:
G₀ : Type u_2
inst✝ : GroupWithZero G₀
a : G₀
h : a ≠ 0
g : G₀
⊢ (fun g => a * g) (a⁻¹ * g) = g

Tactic:
simp [← mul_assoc, mul_inv_cancel₀ h]

Result:
no goals
-- Mathlib/RingTheory/Coprime/Basic.lean
lemma abs_left_iff (x y : R) : IsCoprime |x| y ↔ IsCoprime x y

Proof state:
R : Type u
inst✝² : CommRing R
inst✝¹ : LinearOrder R
inst✝ : AddLeftMono R
x y : R
⊢ IsCoprime |x| y ↔ IsCoprime x y

Tactic:
cases le_or_lt 0 x with
| inl h => rw [abs_of_nonneg h]
| inr h => rw [abs_of_neg h, IsCoprime.neg_left_iff]

Result:
no goals

Proof state:
case inl
R : Type u
inst✝² : CommRing R
inst✝¹ : LinearOrder R
inst✝ : AddLeftMono R
x y : R
h : 0 ≤ x
⊢ IsCoprime |x| y ↔ IsCoprime x y

Tactic:
rw [abs_of_nonneg h]

Result:
no goals

Proof state:
case inr
R : Type u
inst✝² : CommRing R
inst✝¹ : LinearOrder R
inst✝ : AddLeftMono R
x y : R
h : x < 0
⊢ IsCoprime |x| y ↔ IsCoprime x y

Tactic:
rw [abs_of_neg h, IsCoprime.neg_left_iff]

Result:
no goals
-- Mathlib/GroupTheory/GroupAction/FixingSubgroup.lean
theorem mem_fixingSubgroup_iff_subset_fixedBy {s : Set α} {m : M} :
    m ∈ fixingSubgroup M s ↔ s ⊆ fixedBy α m

Proof state:
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
s : Set α
m : M
⊢ m ∈ fixingSubgroup M s ↔ s ⊆ fixedBy α m

Tactic:
simp_rw [mem_fixingSubgroup_iff, Set.subset_def, mem_fixedBy]

Result:
no goals
-- Mathlib/Order/CompleteLattice.lean
theorem biSup_sup {p : ι → Prop} {f : ∀ i, p i → α} {a : α} (h : ∃ i, p i) :
    (⨆ (i) (h : p i), f i h) ⊔ a = ⨆ (i) (h : p i), f i h ⊔ a

Proof state:
α : Type u_1
ι : Sort u_4
inst✝ : CompleteLattice α
p : ι → Prop
f : (i : ι) → p i → α
a : α
h : ∃ i, p i
⊢ (⨆ i, ⨆ (h : p i), f i h) ⊔ a = ⨆ i, ⨆ (h : p i), f i h ⊔ a

Tactic:
haveI : Nonempty { i // p i } :=
  let ⟨i, hi⟩ := h
  ⟨⟨i, hi⟩⟩

Result:
α : Type u_1
ι : Sort u_4
inst✝ : CompleteLattice α
p : ι → Prop
f : (i : ι) → p i → α
a : α
h : ∃ i, p i
this : Nonempty { i // p i }
⊢ (⨆ i, ⨆ (h : p i), f i h) ⊔ a = ⨆ i, ⨆ (h : p i), f i h ⊔ a

Proof state:
α : Type u_1
ι : Sort u_4
inst✝ : CompleteLattice α
p : ι → Prop
f : (i : ι) → p i → α
a : α
h : ∃ i, p i
this : Nonempty { i // p i }
⊢ (⨆ i, ⨆ (h : p i), f i h) ⊔ a = ⨆ i, ⨆ (h : p i), f i h ⊔ a

Tactic:
rw [iSup_subtype', iSup_subtype', iSup_sup]

Result:
no goals
-- Mathlib/Topology/MetricSpace/Isometry.lean
theorem preimage_emetric_closedBall (h : Isometry f) (x : α) (r : ℝ≥0∞) :
    f ⁻¹' EMetric.closedBall (f x) r = EMetric.closedBall x r

Proof state:
case h
α : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
f : α → β
h : Isometry f
x : α
r : ℝ≥0∞
y : α
⊢ y ∈ f ⁻¹' EMetric.closedBall (f x) r ↔ y ∈ EMetric.closedBall x r

Tactic:
simp [h.edist_eq]

Result:
no goals

Proof state:
α : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
f : α → β
h : Isometry f
x : α
r : ℝ≥0∞
⊢ f ⁻¹' EMetric.closedBall (f x) r = EMetric.closedBall x r

Tactic:
ext y

Result:
case h
α : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
f : α → β
h : Isometry f
x : α
r : ℝ≥0∞
y : α
⊢ y ∈ f ⁻¹' EMetric.closedBall (f x) r ↔ y ∈ EMetric.closedBall x r
-- Mathlib/Data/DFinsupp/Interval.lean
lemma card_Iio : #(Iio f) = (∏ i ∈ f.support, #(Iic (f i))) - 1

Proof state:
ι : Type u_1
α : ι → Type u_2
inst✝⁵ : DecidableEq ι
inst✝⁴ : (i : ι) → DecidableEq (α i)
inst✝³ : (i : ι) → AddCommMonoid (α i)
inst✝² : (i : ι) → PartialOrder (α i)
inst✝¹ : ∀ (i : ι), CanonicallyOrderedAdd (α i)
inst✝ : (i : ι) → LocallyFiniteOrder (α i)
f : Π₀ (i : ι), α i
⊢ #(Iio f) = ∏ i ∈ f.support, #(Iic (f i)) - 1

Tactic:
rw [card_Iio_eq_card_Iic_sub_one, card_Iic]

Result:
no goals
-- Mathlib/NumberTheory/Harmonic/ZetaAsymp.lean
lemma _root_.isBigO_riemannZeta_sub_one_div {F : Type*} [Norm F] [One F] [NormOneClass F] :
    (fun s : ℂ ↦ riemannZeta s - 1 / (s - 1)) =O[𝓝 1] (fun _ ↦ 1 : ℂ → F)

Proof state:
F : Type u_1
inst✝² : Norm F
inst✝¹ : One F
inst✝ : NormOneClass F
⊢ (fun s => riemannZeta s - 1 / (s - 1)) =O[𝓝 1] fun x => 1

Tactic:
simpa only [Asymptotics.isBigO_one_nhds_ne_iff] using
   tendsto_riemannZeta_sub_one_div.isBigO_one (F := F)

Result:
no goals
-- Mathlib/FieldTheory/AbelRuffini.lean
theorem gal_X_isSolvable : IsSolvable (X : F[X]).Gal

Proof state:
F : Type u_1
inst✝ : Field F
⊢ IsSolvable X.Gal

Tactic:
infer_instance

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Option/Lemmas.lean
theorem guard_true {α} :
    guard (fun (_ : α) => True) = some

Proof state:
case h
α : Type u_1
a : α
⊢ guard (fun x => True) a = some a

Tactic:
simp [guard]

Result:
no goals

Proof state:
α : Type u_1
⊢ (guard fun x => True) = some

Tactic:
funext a

Result:
case h
α : Type u_1
a : α
⊢ guard (fun x => True) a = some a
-- Mathlib/RingTheory/Localization/Away/Basic.lean
lemma algebraMap_pow_isUnit (n : ℕ) : IsUnit (algebraMap R S x ^ n) :=
  IsUnit.pow _ <| IsLocalization.map_units _ (⟨x, 1, by simp⟩ : Submonoid.powers x)

Proof state:
R : Type u_1
inst✝³ : CommSemiring R
S : Type u_2
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
x : R
inst✝ : Away x S
n : ℕ
⊢ (fun x_1 => x ^ x_1) 1 = x

Tactic:
simp

Result:
no goals
-- Mathlib/NumberTheory/LegendreSymbol/ZModChar.lean
theorem χ₈_nat_mod_eight (n : ℕ) : χ₈ n = χ₈ (n % 8 : ℕ)

Proof state:
n : ℕ
⊢ χ₈ ↑n = χ₈ ↑(n % 8)

Tactic:
rw [← ZMod.natCast_mod n 8]

Result:
no goals
-- Mathlib/Order/Compare.lean
theorem cmp_compares [LinearOrder α] (a b : α) : (cmp a b).Compares a b

Proof state:
α : Type u_1
inst✝ : LinearOrder α
a b : α
⊢ (cmp a b).Compares a b

Tactic:
obtain h | h | h := lt_trichotomy a b <;> simp [cmp, cmpUsing, h, h.not_lt]

Result:
no goals
-- Mathlib/Algebra/Order/Group/Abs.lean
theorem le_abs' : a ≤ |b| ↔ b ≤ -a ∨ a ≤ b

Proof state:
α : Type u_1
inst✝ : LinearOrderedAddCommGroup α
a b : α
⊢ a ≤ |b| ↔ b ≤ -a ∨ a ≤ b

Tactic:
rw [le_abs, or_comm, le_neg]

Result:
no goals
-- Mathlib/MeasureTheory/MeasurableSpace/Card.lean
theorem cardinal_generateMeasurable_le_continuum {s : Set (Set α)} (hs : #s ≤ 𝔠) :
    #{ t | GenerateMeasurable s t } ≤ 𝔠

Proof state:
α : Type u
s : Set (Set α)
hs : #↑s ≤ 𝔠
⊢ (#↑s ⊔ 2) ^ ℵ₀ ≤ 𝔠

Tactic:
rw [← continuum_power_aleph0]

Result:
α : Type u
s : Set (Set α)
hs : #↑s ≤ 𝔠
⊢ (#↑s ⊔ 2) ^ ℵ₀ ≤ 𝔠 ^ ℵ₀

Proof state:
α : Type u
s : Set (Set α)
hs : #↑s ≤ 𝔠
⊢ (#↑s ⊔ 2) ^ ℵ₀ ≤ 𝔠 ^ ℵ₀

Tactic:
exact_mod_cast power_le_power_right (max_le hs (nat_lt_continuum 2).le)

Result:
no goals

Proof state:
α : Type u
s : Set (Set α)
hs : #↑s ≤ 𝔠
⊢ #↑{t | GenerateMeasurable s t} ≤ 𝔠

Tactic:
apply (cardinal_generateMeasurable_le s).trans

Result:
α : Type u
s : Set (Set α)
hs : #↑s ≤ 𝔠
⊢ (#↑s ⊔ 2) ^ ℵ₀ ≤ 𝔠
-- Mathlib/Analysis/Asymptotics/SpecificAsymptotics.lean
theorem tendsto_pow_div_pow_atTop_zero [TopologicalSpace 𝕜] [OrderTopology 𝕜] {p q : ℕ}
    (hpq : p < q) : Tendsto (fun x : 𝕜 => x ^ p / x ^ q) atTop (𝓝 0)

Proof state:
case hn
𝕜 : Type u_1
inst✝² : LinearOrderedField 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
p q : ℕ
hpq : p < q
⊢ ↑p - ↑q < 0

Tactic:
omega

Result:
no goals

Proof state:
𝕜 : Type u_1
inst✝² : LinearOrderedField 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
p q : ℕ
hpq : p < q
⊢ Tendsto (fun x => x ^ p / x ^ q) atTop (𝓝 0)

Tactic:
rw [tendsto_congr' pow_div_pow_eventuallyEq_atTop]

Result:
𝕜 : Type u_1
inst✝² : LinearOrderedField 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
p q : ℕ
hpq : p < q
⊢ Tendsto (fun x => x ^ (↑p - ↑q)) atTop (𝓝 0)

Proof state:
𝕜 : Type u_1
inst✝² : LinearOrderedField 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
p q : ℕ
hpq : p < q
⊢ Tendsto (fun x => x ^ (↑p - ↑q)) atTop (𝓝 0)

Tactic:
apply tendsto_zpow_atTop_zero

Result:
case hn
𝕜 : Type u_1
inst✝² : LinearOrderedField 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
p q : ℕ
hpq : p < q
⊢ ↑p - ↑q < 0