harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/CategoryTheory/Abelian/Injective/Resolution.lean
@[reassoc]
lemma InjectiveResolution.iso_inv_naturality {X Y : C} (f : X ⟶ Y)
    (I : InjectiveResolution X) (J : InjectiveResolution Y)
    (φ : I.cocomplex ⟶ J.cocomplex) (comm : I.ι.f 0 ≫ φ.f 0 = f ≫ J.ι.f 0) :
    I.iso.inv ≫ (injectiveResolutions C).map f =
      (HomotopyCategory.quotient _ _).map φ ≫ J.iso.inv

Proof state:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasInjectiveResolutions C
X Y : C
f : X ⟶ Y
I : InjectiveResolution X
J : InjectiveResolution Y
φ : I.cocomplex ⟶ J.cocomplex
comm : I.ι.f 0 ≫ φ.f 0 = f ≫ J.ι.f 0
⊢ I.iso.inv ≫ (injectiveResolutions C).map f = (HomotopyCategory.quotient C (ComplexShape.up ℕ)).map φ ≫ J.iso.inv

Tactic:
rw [← cancel_mono (J.iso).hom, Category.assoc, iso_hom_naturality f I J φ comm,
  Iso.inv_hom_id_assoc, Category.assoc, Iso.inv_hom_id, Category.comp_id]

Result:
no goals
-- Mathlib/Data/Num/Lemmas.lean
theorem ofNat'_zero : Num.ofNat' 0 = 0

Proof state:
⊢ ofNat' 0 = 0

Tactic:
simp [Num.ofNat']

Result:
no goals
-- Mathlib/.lake/packages/batteries/Batteries/Classes/SatisfiesM.lean
theorem pure [Applicative m] [LawfulApplicative m]
    (h : p a) : SatisfiesM (m := m) p (pure a) := ⟨pure ⟨_, h⟩, by simp⟩

Proof state:
m : Type u_1 → Type u_2
α✝ : Type u_1
p : α✝ → Prop
a : α✝
inst✝¹ : Applicative m
inst✝ : LawfulApplicative m
h : p a
⊢ Subtype.val <$> pure ⟨a, h⟩ = pure a

Tactic:
simp

Result:
no goals
-- Mathlib/LinearAlgebra/Matrix/ToLin.lean
theorem LinearMap.toMatrix_reindexRange [DecidableEq M₁] (f : M₁ →ₗ[R] M₂) (k : m) (i : n) :
    LinearMap.toMatrix v₁.reindexRange v₂.reindexRange f ⟨v₂ k, Set.mem_range_self k⟩
        ⟨v₁ i, Set.mem_range_self i⟩ =
      LinearMap.toMatrix v₁ v₂ f k i

Proof state:
R : Type u_1
inst✝⁸ : CommSemiring R
m : Type u_3
n : Type u_4
inst✝⁷ : Fintype n
inst✝⁶ : Finite m
inst✝⁵ : DecidableEq n
M₁ : Type u_5
M₂ : Type u_6
inst✝⁴ : AddCommMonoid M₁
inst✝³ : AddCommMonoid M₂
inst✝² : Module R M₁
inst✝¹ : Module R M₂
v₁ : Basis n R M₁
v₂ : Basis m R M₂
inst✝ : DecidableEq M₁
f : M₁ →ₗ[R] M₂
k : m
i : n
⊢ (toMatrix v₁.reindexRange v₂.reindexRange) f ⟨v₂ k, ⋯⟩ ⟨v₁ i, ⋯⟩ = (toMatrix v₁ v₂) f k i

Tactic:
simp_rw [LinearMap.toMatrix_apply, Basis.reindexRange_self, Basis.reindexRange_repr]

Result:
no goals
-- Mathlib/Algebra/BigOperators/Group/Multiset/Defs.lean
theorem prod_pair (a b : α) : ({a, b} : Multiset α).prod = a * b

Proof state:
α : Type u_3
inst✝ : CommMonoid α
a b : α
⊢ {a, b}.prod = a * b

Tactic:
rw [insert_eq_cons, prod_cons, prod_singleton]

Result:
no goals
-- Mathlib/Algebra/AddTorsor/Defs.lean
theorem vsub_sub_vsub_cancel_right (p₁ p₂ p₃ : P) : p₁ -ᵥ p₃ - (p₂ -ᵥ p₃) = p₁ -ᵥ p₂

Proof state:
G : Type u_1
P : Type u_2
inst✝ : AddGroup G
T : AddTorsor G P
p₁ p₂ p₃ : P
⊢ p₁ -ᵥ p₃ - (p₂ -ᵥ p₃) = p₁ -ᵥ p₂

Tactic:
rw [← vsub_vadd_eq_vsub_sub, vsub_vadd]

Result:
no goals
-- Mathlib/MeasureTheory/Integral/Marginal.lean
theorem lmarginal_union' (f : (∀ i, π i) → ℝ≥0∞) (hf : Measurable f) {s t : Finset δ}
    (hst : Disjoint s t) : ∫⋯∫⁻_s ∪ t, f ∂μ = ∫⋯∫⁻_t, ∫⋯∫⁻_s, f ∂μ ∂μ

Proof state:
δ : Type u_1
π : δ → Type u_3
inst✝² : (x : δ) → MeasurableSpace (π x)
μ : (i : δ) → Measure (π i)
inst✝¹ : DecidableEq δ
inst✝ : ∀ (i : δ), SigmaFinite (μ i)
f : ((i : δ) → π i) → ℝ≥0∞
hf : Measurable f
s t : Finset δ
hst : Disjoint s t
⊢ ∫⋯∫⁻_s ∪ t, f ∂μ = ∫⋯∫⁻_t, ∫⋯∫⁻_s, f ∂μ ∂μ

Tactic:
rw [Finset.union_comm, lmarginal_union μ f hf hst.symm]

Result:
no goals
-- Mathlib/LinearAlgebra/AffineSpace/Basis.lean
theorem coord_apply_eq (i : ι) : b.coord i (b i) = 1

Proof state:
ι : Type u_1
k : Type u_5
V : Type u_6
P : Type u_7
inst✝³ : AddCommGroup V
inst✝² : AffineSpace V P
inst✝¹ : Ring k
inst✝ : Module k V
b : AffineBasis ι k P
i : ι
⊢ (b.coord i) (b i) = 1

Tactic:
simp only [coord, Basis.coe_sumCoords, LinearEquiv.map_zero, LinearEquiv.coe_coe, sub_zero,
  AffineMap.coe_mk, Finsupp.sum_zero_index, vsub_self]

Result:
no goals
-- Mathlib/Data/Sign.lean
theorem nonneg_iff {a : SignType} : 0 ≤ a ↔ a = 0 ∨ a = 1

Proof state:
a : SignType
⊢ 0 ≤ a ↔ a = 0 ∨ a = 1

Tactic:
cases a <;> decide

Result:
no goals
-- Mathlib/Data/Int/Cast/Lemmas.lean
@[simp] lemma cast_eq_one : (n : α) = 1 ↔ n = 1

Proof state:
α : Type u_3
inst✝¹ : AddGroupWithOne α
inst✝ : CharZero α
n : ℤ
⊢ ↑n = 1 ↔ n = 1

Tactic:
rw [← cast_one, cast_inj]

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Operations.lean
/-- Except possibly for `t`, the neighbours of `s` in `G.replaceVertex s t` are its neighbours in
`G`. -/
lemma adj_replaceVertex_iff_of_ne_left {w : V} (hw : w ≠ t) :
    (G.replaceVertex s t).Adj s w ↔ G.Adj s w

Proof state:
V : Type u_1
G : SimpleGraph V
s t : V
inst✝ : DecidableEq V
w : V
hw : w ≠ t
⊢ (G.replaceVertex s t).Adj s w ↔ G.Adj s w

Tactic:
simp [replaceVertex, hw]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Nat/Simproc.lean
theorem add_sub_add_ge (a c : Nat) {b d : Nat} (h : b ≥ d) : a + b - (c + d) = a + (b - d) - c

Proof state:
a c b d : Nat
h : b ≥ d
⊢ a + b - (c + d) = a + (b - d) - c

Tactic:
rw [Nat.add_comm c d, Nat.sub_add_eq, Nat.add_sub_assoc h a]

Result:
no goals
-- Mathlib/Algebra/Ring/Parity.lean
lemma iterate_bit0 (hf : Involutive f) (n : ℕ) : f^[2 * n] = id

Proof state:
α : Type u_4
f : α → α
hf : Involutive f
n : ℕ
⊢ f^[2 * n] = id

Tactic:
rw [iterate_mul, involutive_iff_iter_2_eq_id.1 hf, iterate_id]

Result:
no goals
-- Mathlib/Order/Nucleus.lean
lemma map_himp_apply (n : Nucleus X) (x y : X) : n (x ⇨ n y) = x ⇨ n y :=
  le_antisymm (map_himp_le.trans_eq <| by rw [n.idempotent]) n.le_apply

Proof state:
X : Type u_1
inst✝ : Frame X
n : Nucleus X
x y : X
⊢ x ⇨ n (n y) = x ⇨ n y

Tactic:
rw [n.idempotent]

Result:
no goals
-- Mathlib/Analysis/RCLike/Inner.lean
lemma wInner_one_eq_inner (f g : ι → 𝕜) :
    ⟪f, g⟫_[𝕜, 1] = inner ((WithLp.equiv 2 _).symm f) ((WithLp.equiv 2 _).symm g)

Proof state:
ι : Type u_1
𝕜 : Type u_3
inst✝¹ : Fintype ι
inst✝ : RCLike 𝕜
f g : ι → 𝕜
⊢ wInner 1 f g = inner ((WithLp.equiv 2 (ι → 𝕜)).symm f) ((WithLp.equiv 2 (ι → 𝕜)).symm g)

Tactic:
simp [wInner]

Result:
no goals
-- Mathlib/Algebra/Ring/Periodic.lean
theorem _root_.Finset.periodic_prod [Add α] [CommMonoid β] {ι : Type*} {f : ι → α → β}
    (s : Finset ι) (hs : ∀ i ∈ s, Periodic (f i) c) : Periodic (∏ i ∈ s, f i) c :=
  s.prod_to_list f ▸ (s.toList.map f).periodic_prod (by simpa [-Periodic] )

Proof state:
α : Type u_1
β : Type u_2
c : α
inst✝¹ : Add α
inst✝ : CommMonoid β
ι : Type u_4
f : ι → α → β
s : Finset ι
hs : ∀ i ∈ s, Periodic (f i) c
⊢ ∀ f_1 ∈ List.map f s.toList, Periodic f_1 c

Tactic:
simpa [-Periodic]

Result:
no goals
-- Mathlib/Tactic/CategoryTheory/Monoidal/Normalize.lean
theorem evalWhiskerRightAux_cons {f g h i j : C} {η : g ⟶ h} {ηs : i ⟶ j}
    {ηs' : i ⊗ f ⟶ j ⊗ f} {η₁ : g ⊗ (i ⊗ f) ⟶ h ⊗ (j ⊗ f)}
    {η₂ : g ⊗ (i ⊗ f) ⟶ (h ⊗ j) ⊗ f} {η₃ : (g ⊗ i) ⊗ f ⟶ (h ⊗ j) ⊗ f}
    (e_ηs' : ηs ▷ f = ηs') (e_η₁ : ((Iso.refl _).hom ≫ η ≫ (Iso.refl _).hom) ⊗ ηs' = η₁)
    (e_η₂ : η₁ ≫ (α_ _ _ _).inv = η₂) (e_η₃ : (α_ _ _ _).hom ≫ η₂ = η₃) :
    (η ⊗ ηs) ▷ f = η₃

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : MonoidalCategory C
f g h i j : C
η : g ⟶ h
ηs : i ⟶ j
ηs' : i ⊗ f ⟶ j ⊗ f
η₁ : g ⊗ i ⊗ f ⟶ h ⊗ j ⊗ f
η₂ : g ⊗ i ⊗ f ⟶ (h ⊗ j) ⊗ f
η₃ : (g ⊗ i) ⊗ f ⟶ (h ⊗ j) ⊗ f
e_ηs' : ηs ▷ f = ηs'
e_η₁ : (Iso.refl g).hom ≫ η ≫ (Iso.refl h).hom ⊗ ηs' = η₁
e_η₂ : η₁ ≫ (α_ h j f).inv = η₂
e_η₃ : (α_ g i f).hom ≫ η₂ = η₃
⊢ (η ⊗ ηs) ▷ f = η₃

Tactic:
simp [← e_ηs', ← e_η₁, ← e_η₂, ← e_η₃, MonoidalCategory.tensorHom_def]

Result:
no goals
-- Mathlib/Probability/Distributions/Uniform.lean
theorem mem_support_ofMultiset_iff (a : α) : a ∈ (ofMultiset s hs).support ↔ a ∈ s.toFinset

Proof state:
α : Type u_1
s : Multiset α
hs : s ≠ 0
a : α
⊢ a ∈ (ofMultiset s hs).support ↔ a ∈ s.toFinset

Tactic:
simp

Result:
no goals
-- Mathlib/Probability/Independence/Basic.lean
theorem IndepFun.ae_eq {mβ : MeasurableSpace β} {mβ' : MeasurableSpace β'}
    {f' : Ω → β} {g' : Ω → β'} (hfg : IndepFun f g μ)
    (hf : f =ᵐ[μ] f') (hg : g =ᵐ[μ] g') : IndepFun f' g' μ

Proof state:
Ω : Type u_1
β : Type u_6
β' : Type u_7
_mΩ : MeasurableSpace Ω
μ : Measure Ω
f : Ω → β
g : Ω → β'
mβ : MeasurableSpace β
mβ' : MeasurableSpace β'
f' : Ω → β
g' : Ω → β'
hfg : IndepFun f g μ
hf : f =ᶠ[ae μ] f'
hg : g =ᶠ[ae μ] g'
⊢ IndepFun f' g' μ

Tactic:
refine Kernel.IndepFun.ae_eq hfg ?_ ?_ <;>
  simp only [ae_dirac_eq, Filter.eventually_pure, Kernel.const_apply]

Result:
case refine_1
Ω : Type u_1
β : Type u_6
β' : Type u_7
_mΩ : MeasurableSpace Ω
μ : Measure Ω
f : Ω → β
g : Ω → β'
mβ : MeasurableSpace β
mβ' : MeasurableSpace β'
f' : Ω → β
g' : Ω → β'
hfg : IndepFun f g μ
hf : f =ᶠ[ae μ] f'
hg : g =ᶠ[ae μ] g'
⊢ f =ᶠ[ae μ] f'

case refine_2
Ω : Type u_1
β : Type u_6
β' : Type u_7
_mΩ : MeasurableSpace Ω
μ : Measure Ω
f : Ω → β
g : Ω → β'
mβ : MeasurableSpace β
mβ' : MeasurableSpace β'
f' : Ω → β
g' : Ω → β'
hfg : IndepFun f g μ
hf : f =ᶠ[ae μ] f'
hg : g =ᶠ[ae μ] g'
⊢ g =ᶠ[ae μ] g'

Proof state:
case refine_1
Ω : Type u_1
β : Type u_6
β' : Type u_7
_mΩ : MeasurableSpace Ω
μ : Measure Ω
f : Ω → β
g : Ω → β'
mβ : MeasurableSpace β
mβ' : MeasurableSpace β'
f' : Ω → β
g' : Ω → β'
hfg : IndepFun f g μ
hf : f =ᶠ[ae μ] f'
hg : g =ᶠ[ae μ] g'
⊢ f =ᶠ[ae μ] f'

case refine_2
Ω : Type u_1
β : Type u_6
β' : Type u_7
_mΩ : MeasurableSpace Ω
μ : Measure Ω
f : Ω → β
g : Ω → β'
mβ : MeasurableSpace β
mβ' : MeasurableSpace β'
f' : Ω → β
g' : Ω → β'
hfg : IndepFun f g μ
hf : f =ᶠ[ae μ] f'
hg : g =ᶠ[ae μ] g'
⊢ g =ᶠ[ae μ] g'

Tactic:
exacts [hf, hg]

Result:
no goals
-- Mathlib/Data/List/Rotate.lean
theorem IsRotated.refl (l : List α) : l ~r l :=
  ⟨0, by simp⟩

Proof state:
α : Type u
l : List α
⊢ l.rotate 0 = l

Tactic:
simp

Result:
no goals
-- Mathlib/Data/Nat/Init.lean
protected lemma sub_lt_iff_lt_add (hba : b ≤ a) : a - b < c ↔ a < b + c

Proof state:
a b c : ℕ
hba : b ≤ a
⊢ a - b < c ↔ a < b + c

Tactic:
omega

Result:
no goals
-- Mathlib/NumberTheory/Padics/Hensel.lean
theorem tendsto_zero_of_norm_tendsto_zero : Tendsto (fun i => F.eval (ncs i)) atTop (𝓝 0) :=
  tendsto_iff_norm_sub_tendsto_zero.2 (by simpa using hnorm)

Proof state:
p : ℕ
inst✝ : Fact (Nat.Prime p)
ncs : CauSeq ℤ_[p] norm
F : Polynomial ℤ_[p]
hnorm : Tendsto (fun i => ‖Polynomial.eval (↑ncs i) F‖) atTop (𝓝 0)
⊢ Tendsto (fun e => ‖Polynomial.eval (↑ncs e) F - 0‖) atTop (𝓝 0)

Tactic:
simpa using hnorm

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Trigonometric/Basic.lean
theorem cos_sub_pi_div_two (x : ℝ) : cos (x - π / 2) = sin x

Proof state:
x : ℝ
⊢ cos (x - π / 2) = sin x

Tactic:
simp [sub_eq_add_neg, cos_add]

Result:
no goals
-- Mathlib/Data/Stream/Init.lean
theorem mem_of_mem_even (a : α) (s : Stream' α) : a ∈ even s → a ∈ s := fun ⟨n, h⟩ =>
  Exists.intro (2 * n) (by rw [h, get_even])

Proof state:
α : Type u
a : α
s : Stream' α
x✝ : a ∈ s.even
n : ℕ
h : (fun b => a = b) (s.even.get n)
⊢ (fun b => a = b) (s.get (2 * n))

Tactic:
rw [h, get_even]

Result:
no goals
-- Mathlib/Algebra/Field/Subfield/Basic.lean
theorem coe_sSup_of_directedOn {S : Set (Subfield K)} (Sne : S.Nonempty)
    (hS : DirectedOn (· ≤ ·) S) : (↑(sSup S) : Set K) = ⋃ s ∈ S, ↑s :=
  Set.ext fun x => by simp [mem_sSup_of_directedOn Sne hS]

Proof state:
K : Type u
inst✝ : DivisionRing K
S : Set (Subfield K)
Sne : S.Nonempty
hS : DirectedOn (fun x1 x2 => x1 ≤ x2) S
x : K
⊢ x ∈ ↑(sSup S) ↔ x ∈ ⋃ s ∈ S, ↑s

Tactic:
simp [mem_sSup_of_directedOn Sne hS]

Result:
no goals
-- Mathlib/Data/Real/EReal.lean
@[simp]
lemma preimage_coe_Ioo_bot_top : Real.toEReal ⁻¹' Ioo ⊥ ⊤ = univ

Proof state:
⊢ Real.toEReal ⁻¹' (Ioi ⊥ ∩ Iio ⊤) = univ

Tactic:
simp

Result:
no goals

Proof state:
⊢ Real.toEReal ⁻¹' Ioo ⊥ ⊤ = univ

Tactic:
rw [← Ioi_inter_Iio]

Result:
⊢ Real.toEReal ⁻¹' (Ioi ⊥ ∩ Iio ⊤) = univ
-- Mathlib/Algebra/Algebra/Spectrum.lean
theorem star_mem_resolventSet_iff {r : R} {a : A} :
    star r ∈ resolventSet R a ↔ r ∈ resolventSet R (star a)

Proof state:
R : Type u
A : Type v
inst✝⁵ : CommSemiring R
inst✝⁴ : Ring A
inst✝³ : Algebra R A
inst✝² : InvolutiveStar R
inst✝¹ : StarRing A
inst✝ : StarModule R A
r : R
a : A
⊢ star r ∈ resolventSet R a ↔ r ∈ resolventSet R (star a)

Tactic:
refine ⟨fun h => ?_, fun h => ?_⟩ <;>
  simpa only [mem_resolventSet_iff, Algebra.algebraMap_eq_smul_one, star_sub, star_smul,
    star_star, star_one] using IsUnit.star h

Result:
no goals
-- Mathlib/Logic/Unique.lean
theorem subsingleton_unique' : ∀ h₁ h₂ : Unique α, h₁ = h₂
  | ⟨⟨x⟩, h⟩, ⟨⟨y⟩, _⟩ => by congr; rw [h x, h y]

Proof state:
case e_toInhabited.e_default
α : Sort u_1
x : α
h : ∀ (a : α), a = default
y : α
uniq✝ : ∀ (a : α), a = default
⊢ x = y

Tactic:
rw [h x, h y]

Result:
no goals

Proof state:
α : Sort u_1
x : α
h : ∀ (a : α), a = default
y : α
uniq✝ : ∀ (a : α), a = default
⊢ { default := x, uniq := h } = { default := y, uniq := uniq✝ }

Tactic:
congr

Result:
case e_toInhabited.e_default
α : Sort u_1
x : α
h : ∀ (a : α), a = default
y : α
uniq✝ : ∀ (a : α), a = default
⊢ x = y
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Nat/Lemmas.lean
theorem dvd_of_pow_dvd {p k m : Nat} (hk : 1 ≤ k) (hpk : p ^ k ∣ m) : p ∣ m

Proof state:
p k m : Nat
hk : 1 ≤ k
hpk : p ^ k ∣ m
⊢ p ^ 1 ∣ m

Tactic:
exact pow_dvd_of_le_of_pow_dvd hk hpk

Result:
no goals

Proof state:
p k m : Nat
hk : 1 ≤ k
hpk : p ^ k ∣ m
⊢ p ∣ m

Tactic:
rw [← Nat.pow_one p]

Result:
p k m : Nat
hk : 1 ≤ k
hpk : p ^ k ∣ m
⊢ p ^ 1 ∣ m
-- Mathlib/Algebra/Colimit/Ring.lean
theorem inv_mul_cancel {p : Ring.DirectLimit G f} (hp : p ≠ 0) : inv G f p * p = 1

Proof state:
ι : Type u_1
inst✝³ : Preorder ι
G : ι → Type u_2
inst✝² : Nonempty ι
inst✝¹ : IsDirected ι fun x1 x2 => x1 ≤ x2
inst✝ : (i : ι) → Field (G i)
f : (i j : ι) → i ≤ j → G i → G j
p : Ring.DirectLimit G f
hp : p ≠ 0
⊢ inv G f p * p = 1

Tactic:
rw [_root_.mul_comm, DirectLimit.mul_inv_cancel G f hp]

Result:
no goals
-- Mathlib/Algebra/MonoidAlgebra/Defs.lean
theorem single_one_mul_apply [MulOneClass G] (f : MonoidAlgebra k G) (r : k) (x : G) :
    (single (1 : G) r * f) x = r * f x :=
  f.single_mul_apply_aux fun a ha => by rw [one_mul]

Proof state:
k : Type u₁
G : Type u₂
inst✝¹ : Semiring k
inst✝ : MulOneClass G
f : MonoidAlgebra k G
r : k
x a : G
ha : a ∈ f.support
⊢ 1 * a = x ↔ a = x

Tactic:
rw [one_mul]

Result:
no goals
-- Mathlib/Data/Finset/Pi.lean
@[simp]
lemma pi_eq_empty : s.pi t = ∅ ↔ ∃ a ∈ s, t a = ∅

Proof state:
α : Type u_1
β : α → Type u
s : Finset α
t : (a : α) → Finset (β a)
inst✝ : DecidableEq α
⊢ s.pi t = ∅ ↔ ∃ a ∈ s, t a = ∅

Tactic:
simp [← not_nonempty_iff_eq_empty]

Result:
no goals
-- Mathlib/Data/Seq/Seq.lean
theorem not_mem_nil (a : α) : a ∉ @nil α := fun ⟨_, (h : some a = none)⟩ => by injection h

Proof state:
α : Type u
a : α
x✝ : a ∈ nil
w✝ : ℕ
h : some a = none
⊢ False

Tactic:
injection h

Result:
no goals
-- Mathlib/SetTheory/Cardinal/Free.lean
theorem mk_freeAbelianGroup [Nonempty α] : #(FreeAbelianGroup α) = max #α ℵ₀

Proof state:
α : Type u
inst✝ : Nonempty α
⊢ #(FreeAbelianGroup α) = #α ⊔ ℵ₀

Tactic:
rw [Cardinal.mk_congr (FreeAbelianGroup.equivFinsupp α).toEquiv]

Result:
α : Type u
inst✝ : Nonempty α
⊢ #(α →₀ ℤ) = #α ⊔ ℵ₀

Proof state:
α : Type u
inst✝ : Nonempty α
⊢ #(α →₀ ℤ) = #α ⊔ ℵ₀

Tactic:
simp

Result:
no goals
-- Mathlib/Analysis/Calculus/FormalMultilinearSeries.lean
theorem order_eq_zero_iff' : p.order = 0 ↔ p = 0 ∨ p 0 ≠ 0

Proof state:
𝕜 : Type u
E : Type v
F : Type w
inst✝¹⁰ : Semiring 𝕜
inst✝⁹ : AddCommMonoid E
inst✝⁸ : Module 𝕜 E
inst✝⁷ : TopologicalSpace E
inst✝⁶ : ContinuousAdd E
inst✝⁵ : ContinuousConstSMul 𝕜 E
inst✝⁴ : AddCommMonoid F
inst✝³ : Module 𝕜 F
inst✝² : TopologicalSpace F
inst✝¹ : ContinuousAdd F
inst✝ : ContinuousConstSMul 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
⊢ p.order = 0 ↔ p = 0 ∨ p 0 ≠ 0

Tactic:
simpa [order, Nat.sInf_eq_zero, FormalMultilinearSeries.ext_iff, eq_empty_iff_forall_not_mem]
  using or_comm

Result:
no goals
-- Mathlib/MeasureTheory/Integral/Periodic.lean
theorem tendsto_atBot_intervalIntegral_of_pos'
    (h_int : IntervalIntegrable g MeasureSpace.volume 0 T) (h₀ : ∀ x, 0 < g x) (hT : 0 < T) :
    Tendsto (fun t => ∫ x in (0)..t, g x) atBot atBot

Proof state:
T : ℝ
g : ℝ → ℝ
hg : Periodic g T
h_int : IntervalIntegrable g volume 0 T
h₀ : ∀ (x : ℝ), 0 < g x
hT : 0 < T
⊢ Tendsto (fun t => ∫ (x : ℝ) in 0 ..t, g x) atBot atBot

Tactic:
exact hg.tendsto_atBot_intervalIntegral_of_pos (intervalIntegral_pos_of_pos h_int h₀ hT) hT

Result:
no goals
-- Mathlib/Data/Set/Lattice.lean
theorem union_distrib_iInter₂_left (s : Set α) (t : ∀ i, κ i → Set α) :
    (s ∪ ⋂ (i) (j), t i j) = ⋂ (i) (j), s ∪ t i j

Proof state:
α : Type u_1
ι : Sort u_5
κ : ι → Sort u_8
s : Set α
t : (i : ι) → κ i → Set α
⊢ s ∪ ⋂ i, ⋂ j, t i j = ⋂ i, ⋂ j, s ∪ t i j

Tactic:
simp_rw [union_distrib_iInter_left]

Result:
no goals
-- Mathlib/Data/List/Map2.lean
theorem nil_zipWith (f : α → β → γ) (l : List β) : zipWith f [] l = []

Proof state:
α : Type u
β : Type v
γ : Type w
f : α → β → γ
l : List β
⊢ zipWith f [] l = []

Tactic:
cases l <;> rfl

Result:
no goals
-- Mathlib/Analysis/Asymptotics/SuperpolynomialDecay.lean
theorem superpolynomialDecay_param_mul_iff (hk : Tendsto k l atTop) :
    SuperpolynomialDecay l k (k * f) ↔ SuperpolynomialDecay l k f :=
  ⟨fun h =>
    (h.inv_param_mul hk).congr'
      ((hk.eventually_ne_atTop 0).mono fun x hx => by simp [← mul_assoc, inv_mul_cancel₀ hx]),
    fun h => h.param_mul⟩

Proof state:
α : Type u_1
β : Type u_2
l : Filter α
k f : α → β
inst✝² : TopologicalSpace β
inst✝¹ : LinearOrderedField β
inst✝ : OrderTopology β
hk : Tendsto k l atTop
h : SuperpolynomialDecay l k (k * f)
x : α
hx : k x ≠ 0
⊢ (k⁻¹ * (k * f)) x = f x

Tactic:
simp [← mul_assoc, inv_mul_cancel₀ hx]

Result:
no goals
-- Mathlib/Computability/Reduce.lean
theorem toNat_manyOneEquiv {p : Set α} : ManyOneEquiv (toNat p) p

Proof state:
α : Type u
inst✝¹ : Primcodable α
inst✝ : Inhabited α
p : Set α
⊢ ManyOneEquiv (toNat p) p

Tactic:
simp [ManyOneEquiv]

Result:
no goals
-- Mathlib/Data/Fin/Tuple/Finset.lean
lemma map_consEquiv_filter_piFinset (P : (∀ i, α (succ i)) → Prop) [DecidablePred P] :
    {r ∈ piFinset S | P (tail r)}.map (consEquiv α).symm.toEmbedding =
      S 0 ×ˢ {r ∈ piFinset (tail S) | P r}

Proof state:
case h
n : ℕ
α : Fin (n + 1) → Type u_1
S : (i : Fin (n + 1)) → Finset (α i)
P : ((i : Fin n) → α i.succ) → Prop
inst✝ : DecidablePred P
a✝ : α 0 × ((i : Fin n) → α i.succ)
⊢ a✝ ∈ map (consEquiv α).symm.toEmbedding (filter (fun r => P fun i => r i.succ) (piFinset S)) ↔
    a✝ ∈ S 0 ×ˢ filter (fun r => P r) (piFinset fun i => S i.succ)

Tactic:
simp [Fin.forall_iff_succ, and_assoc]

Result:
no goals

Proof state:
n : ℕ
α : Fin (n + 1) → Type u_1
S : (i : Fin (n + 1)) → Finset (α i)
P : ((i : Fin n) → α i.succ) → Prop
inst✝ : DecidablePred P
⊢ map (consEquiv α).symm.toEmbedding (filter (fun r => P (tail r)) (piFinset S)) =
    S 0 ×ˢ filter (fun r => P r) (piFinset (tail S))

Tactic:
unfold tail

Result:
n : ℕ
α : Fin (n + 1) → Type u_1
S : (i : Fin (n + 1)) → Finset (α i)
P : ((i : Fin n) → α i.succ) → Prop
inst✝ : DecidablePred P
⊢ map (consEquiv α).symm.toEmbedding (filter (fun r => P fun i => r i.succ) (piFinset S)) =
    S 0 ×ˢ filter (fun r => P r) (piFinset fun i => S i.succ)

Proof state:
n : ℕ
α : Fin (n + 1) → Type u_1
S : (i : Fin (n + 1)) → Finset (α i)
P : ((i : Fin n) → α i.succ) → Prop
inst✝ : DecidablePred P
⊢ map (consEquiv α).symm.toEmbedding (filter (fun r => P fun i => r i.succ) (piFinset S)) =
    S 0 ×ˢ filter (fun r => P r) (piFinset fun i => S i.succ)

Tactic:
ext

Result:
case h
n : ℕ
α : Fin (n + 1) → Type u_1
S : (i : Fin (n + 1)) → Finset (α i)
P : ((i : Fin n) → α i.succ) → Prop
inst✝ : DecidablePred P
a✝ : α 0 × ((i : Fin n) → α i.succ)
⊢ a✝ ∈ map (consEquiv α).symm.toEmbedding (filter (fun r => P fun i => r i.succ) (piFinset S)) ↔
    a✝ ∈ S 0 ×ˢ filter (fun r => P r) (piFinset fun i => S i.succ)
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Attach.lean
theorem _root_.List.attachWith_toArray {l : List α} {P : α → Prop} {H : ∀ x ∈ l.toArray, P x} :
    l.toArray.attachWith P H = (l.attachWith P (by simpa using H)).toArray

Proof state:
α : Type ?u.401
l : List α
P : α → Prop
H : ∀ (x : α), x ∈ l.toArray → P x
⊢ ∀ (x : α), x ∈ l → P x

Tactic:
simpa using H

Result:
no goals

Proof state:
α : Type u_1
l : List α
P : α → Prop
H : ∀ (x : α), x ∈ l.toArray → P x
⊢ l.toArray.attachWith P H = (l.attachWith P ⋯).toArray

Tactic:
simp [attachWith]

Result:
no goals
-- Mathlib/Analysis/Calculus/IteratedDeriv/Defs.lean
theorem iteratedDerivWithin_succ' {x : 𝕜} :
    iteratedDerivWithin (n + 1) f s x = (iteratedDerivWithin n (derivWithin f s) s) x

Proof state:
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
n : ℕ
f : 𝕜 → F
s : Set 𝕜
x : 𝕜
⊢ (fun g => derivWithin g s)^[n + 1] f x = (fun g => derivWithin g s)^[n] (derivWithin f s) x

Tactic:
rfl

Result:
no goals

Proof state:
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
n : ℕ
f : 𝕜 → F
s : Set 𝕜
x : 𝕜
⊢ iteratedDerivWithin (n + 1) f s x = iteratedDerivWithin n (derivWithin f s) s x

Tactic:
rw [iteratedDerivWithin_eq_iterate, iteratedDerivWithin_eq_iterate]

Result:
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
n : ℕ
f : 𝕜 → F
s : Set 𝕜
x : 𝕜
⊢ (fun g => derivWithin g s)^[n + 1] f x = (fun g => derivWithin g s)^[n] (derivWithin f s) x
-- Mathlib/LinearAlgebra/Matrix/SesquilinearForm.lean
theorem Matrix.toLinearMap₂_compl₁₂ (M : Matrix n m R) (P : Matrix n n' R) (Q : Matrix m m' R) :
    (Matrix.toLinearMap₂ b₁ b₂ M).compl₁₂ (toLin b₁' b₁ P) (toLin b₂' b₂ Q) =
      Matrix.toLinearMap₂ b₁' b₂' (Pᵀ * M * Q) :=
  (LinearMap.toMatrix₂ b₁' b₂').injective
    (by
      simp only [LinearMap.toMatrix₂_compl₁₂ b₁ b₂, LinearMap.toMatrix₂_toLinearMap₂,
        toMatrix_toLin])

Proof state:
R : Type u_1
M₁ : Type u_6
M₂ : Type u_7
M₁' : Type u_8
M₂' : Type u_9
n : Type u_11
m : Type u_12
n' : Type u_13
m' : Type u_14
inst✝¹⁶ : CommSemiring R
inst✝¹⁵ : AddCommMonoid M₁
inst✝¹⁴ : Module R M₁
inst✝¹³ : AddCommMonoid M₂
inst✝¹² : Module R M₂
inst✝¹¹ : DecidableEq n
inst✝¹⁰ : Fintype n
inst✝⁹ : DecidableEq m
inst✝⁸ : Fintype m
b₁ : Basis n R M₁
b₂ : Basis m R M₂
inst✝⁷ : AddCommMonoid M₁'
inst✝⁶ : Module R M₁'
inst✝⁵ : AddCommMonoid M₂'
inst✝⁴ : Module R M₂'
b₁' : Basis n' R M₁'
b₂' : Basis m' R M₂'
inst✝³ : Fintype n'
inst✝² : Fintype m'
inst✝¹ : DecidableEq n'
inst✝ : DecidableEq m'
M : Matrix n m R
P : Matrix n n' R
Q : Matrix m m' R
⊢ (toMatrix₂ b₁' b₂') (((toLinearMap₂ b₁ b₂) M).compl₁₂ ((toLin b₁' b₁) P) ((toLin b₂' b₂) Q)) =
    (toMatrix₂ b₁' b₂') ((toLinearMap₂ b₁' b₂') (Pᵀ * M * Q))

Tactic:
simp only [LinearMap.toMatrix₂_compl₁₂ b₁ b₂, LinearMap.toMatrix₂_toLinearMap₂,
  toMatrix_toLin]

Result:
no goals
-- Mathlib/CategoryTheory/Limits/Shapes/PiProd.lean
lemma hasBinaryProduct_of_products : HasBinaryProduct (∏ᶜ (fun (i : {x : I // P x}) ↦ X i.val))
    (∏ᶜ (fun (i : {x : I // ¬ P x}) ↦ X i.val))

Proof state:
C : Type u_1
I : Type u_2
inst✝³ : Category.{u_3, u_1} C
X : I → C
P : I → Prop
inst✝² : HasProduct X
inst✝¹ : HasProduct fun i => X ↑i
inst✝ : HasProduct fun i => X ↑i
⊢ HasBinaryProduct (∏ᶜ fun i => X ↑i) (∏ᶜ fun i => X ↑i)

Tactic:
exact ⟨Pi.binaryFanOfProp X P, Pi.binaryFanOfPropIsLimit X P⟩

Result:
no goals

Proof state:
C : Type u_1
I : Type u_2
inst✝³ : Category.{u_3, u_1} C
X : I → C
P : I → Prop
inst✝² : HasProduct X
inst✝¹ : HasProduct fun i => X ↑i
inst✝ : HasProduct fun i => X ↑i
⊢ HasBinaryProduct (∏ᶜ fun i => X ↑i) (∏ᶜ fun i => X ↑i)

Tactic:
classical exact ⟨Pi.binaryFanOfProp X P, Pi.binaryFanOfPropIsLimit X P⟩

Result:
no goals
-- Mathlib/Data/List/Zip.lean
theorem revzip_map_snd (l : List α) : (revzip l).map Prod.snd = l.reverse

Proof state:
α : Type u
l : List α
⊢ map Prod.snd l.revzip = l.reverse

Tactic:
rw [← unzip_snd, unzip_revzip]

Result:
no goals