harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Algebra/Group/Basic.lean
/-- If `x ^ n = 1`, then `x ^ m` is the same as `x ^ (m % n)` -/
@[to_additive nsmul_eq_mod_nsmul "If `n • x = 0`, then `m • x` is the same as `(m % n) • x`"]
lemma pow_eq_pow_mod (m : ℕ) (ha : a ^ n = 1) : a ^ m = a ^ (m % n)

Proof state:
M : Type u_4
inst✝ : Monoid M
a : M
n m : ℕ
ha : a ^ n = 1
⊢ a ^ m = a ^ (m % n)

Tactic:
calc
  a ^ m = a ^ (m % n + n * (m / n)) := by rw [Nat.mod_add_div]
  _ = a ^ (m % n) := by simp [pow_add, pow_mul, ha]

Result:
no goals

Proof state:
M : Type u_4
inst✝ : Monoid M
a : M
n m : ℕ
ha : a ^ n = 1
⊢ a ^ (m % n + n * (m / n)) = a ^ (m % n)

Tactic:
simp [pow_add, pow_mul, ha]

Result:
no goals

Proof state:
M : Type u_4
inst✝ : Monoid M
a : M
n m : ℕ
ha : a ^ n = 1
⊢ a ^ m = a ^ (m % n + n * (m / n))

Tactic:
rw [Nat.mod_add_div]

Result:
no goals
-- Mathlib/Data/Seq/WSeq.lean
theorem toList_ofList (l : List α) : l ∈ toList (ofList l)

Proof state:
α : Type u
l : List α
⊢ l ∈ (↑l).toList

Tactic:
induction' l with a l IH

Result:
case nil
α : Type u
⊢ [] ∈ (↑[]).toList

case cons
α : Type u
a : α
l : List α
IH : l ∈ (↑l).toList
⊢ a :: l ∈ (↑(a :: l)).toList

Proof state:
case cons
α : Type u
a : α
l : List α
IH : l ∈ (↑l).toList
⊢ a :: l ∈ (↑(a :: l)).toList

Tactic:
simpa [ret_mem] using think_mem (Computation.mem_map _ IH)

Result:
no goals

Proof state:
case nil
α : Type u
⊢ [] ∈ (↑[]).toList

Tactic:
simp [ret_mem]

Result:
no goals
-- Mathlib/Topology/Algebra/InfiniteSum/Group.lean
theorem HasProd.hasProd_compl_iff {s : Set β} (hf : HasProd (f ∘ (↑) : s → α) a₁) :
    HasProd (f ∘ (↑) : ↑sᶜ → α) a₂ ↔ HasProd f (a₁ * a₂)

Proof state:
α : Type u_1
β : Type u_2
inst✝² : CommGroup α
inst✝¹ : TopologicalSpace α
inst✝ : IsTopologicalGroup α
f : β → α
a₁ a₂ : α
s : Set β
hf : HasProd (s.mulIndicator f) a₁
h : HasProd f (a₁ * a₂)
⊢ HasProd (sᶜ.mulIndicator f) a₂

Tactic:
rw [Set.mulIndicator_compl]

Result:
α : Type u_1
β : Type u_2
inst✝² : CommGroup α
inst✝¹ : TopologicalSpace α
inst✝ : IsTopologicalGroup α
f : β → α
a₁ a₂ : α
s : Set β
hf : HasProd (s.mulIndicator f) a₁
h : HasProd f (a₁ * a₂)
⊢ HasProd (f * (s.mulIndicator f)⁻¹) a₂

Proof state:
α : Type u_1
β : Type u_2
inst✝² : CommGroup α
inst✝¹ : TopologicalSpace α
inst✝ : IsTopologicalGroup α
f : β → α
a₁ a₂ : α
s : Set β
hf : HasProd (s.mulIndicator f) a₁
h : HasProd f (a₁ * a₂)
⊢ HasProd (f * (s.mulIndicator f)⁻¹) a₂

Tactic:
simpa only [div_eq_mul_inv, mul_inv_cancel_comm] using h.div hf

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
inst✝² : CommGroup α
inst✝¹ : TopologicalSpace α
inst✝ : IsTopologicalGroup α
f : β → α
a₁ a₂ : α
s : Set β
hf : HasProd (f ∘ Subtype.val) a₁
⊢ HasProd (f ∘ Subtype.val) a₂ ↔ HasProd f (a₁ * a₂)

Tactic:
refine ⟨fun h ↦ hf.mul_compl h, fun h ↦ ?_⟩

Result:
α : Type u_1
β : Type u_2
inst✝² : CommGroup α
inst✝¹ : TopologicalSpace α
inst✝ : IsTopologicalGroup α
f : β → α
a₁ a₂ : α
s : Set β
hf : HasProd (f ∘ Subtype.val) a₁
h : HasProd f (a₁ * a₂)
⊢ HasProd (f ∘ Subtype.val) a₂

Proof state:
α : Type u_1
β : Type u_2
inst✝² : CommGroup α
inst✝¹ : TopologicalSpace α
inst✝ : IsTopologicalGroup α
f : β → α
a₁ a₂ : α
s : Set β
hf : HasProd (f ∘ Subtype.val) a₁
h : HasProd f (a₁ * a₂)
⊢ HasProd (f ∘ Subtype.val) a₂

Tactic:
rw [hasProd_subtype_iff_mulIndicator] at hf ⊢

Result:
α : Type u_1
β : Type u_2
inst✝² : CommGroup α
inst✝¹ : TopologicalSpace α
inst✝ : IsTopologicalGroup α
f : β → α
a₁ a₂ : α
s : Set β
hf : HasProd (s.mulIndicator f) a₁
h : HasProd f (a₁ * a₂)
⊢ HasProd (sᶜ.mulIndicator f) a₂
-- Mathlib/Combinatorics/SimpleGraph/Path.lean
theorem iso_image_comp_eq_map_iff_eq_comp {C : G.ConnectedComponent} :
    G'.connectedComponentMk (φ v) = C.map ↑(↑φ : G ↪g G') ↔ G.connectedComponentMk v = C

Proof state:
V : Type u
V' : Type v
G : SimpleGraph V
G' : SimpleGraph V'
φ : G ≃g G'
v : V
C : G.ConnectedComponent
u : V
⊢ G'.connectedComponentMk (φ v) = map (RelIso.toRelEmbedding φ).toRelHom (G.connectedComponentMk u) ↔
    G.connectedComponentMk v = G.connectedComponentMk u

Tactic:
simp only [Iso.reachable_iff, ConnectedComponent.map_mk, RelEmbedding.coe_toRelHom,
  RelIso.coe_toRelEmbedding, ConnectedComponent.eq]

Result:
no goals

Proof state:
V : Type u
V' : Type v
G : SimpleGraph V
G' : SimpleGraph V'
φ : G ≃g G'
v : V
C : G.ConnectedComponent
⊢ G'.connectedComponentMk (φ v) = map (RelIso.toRelEmbedding φ).toRelHom C ↔ G.connectedComponentMk v = C

Tactic:
refine C.ind fun u => ?_

Result:
V : Type u
V' : Type v
G : SimpleGraph V
G' : SimpleGraph V'
φ : G ≃g G'
v : V
C : G.ConnectedComponent
u : V
⊢ G'.connectedComponentMk (φ v) = map (RelIso.toRelEmbedding φ).toRelHom (G.connectedComponentMk u) ↔
    G.connectedComponentMk v = G.connectedComponentMk u
-- Mathlib/NumberTheory/EllipticDivisibilitySequence.lean
@[simp]
lemma preNormEDS_four : preNormEDS b c d 4 = d

Proof state:
R : Type u
inst✝ : CommRing R
b c d : R
⊢ preNormEDS b c d 4 = d

Tactic:
erw [preNormEDS_ofNat, preNormEDS'_four]

Result:
no goals
-- Mathlib/MeasureTheory/Measure/Lebesgue/VolumeOfBalls.lean
theorem Complex.volume_sum_rpow_lt [Nonempty ι] {p : ℝ} (hp : 1 ≤ p) (r : ℝ) :
    volume {x : ι → ℂ | (∑ i, ‖x i‖ ^ p) ^ (1 / p) < r} = (.ofReal r) ^ (2 * card ι) *
      .ofReal ((π * Real.Gamma (2 / p + 1)) ^ card ι / Real.Gamma (2 * card ι / p + 1))

Proof state:
case inl
ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : Nonempty ι
p : ℝ
hp : 1 ≤ p
r : ℝ
h₁ : ∀ (x : ι → ℂ), 0 ≤ ∑ i : ι, ‖x i‖ ^ p
h₂ : ∀ (x : ι → ℂ), 0 ≤ (∑ i : ι, ‖x i‖ ^ p) ^ (1 / p)
hr : r ≤ 0
⊢ volume {x | (∑ i : ι, ‖x i‖ ^ p) ^ (1 / p) < r} =
    ENNReal.ofReal r ^ (2 * card ι) *
      ENNReal.ofReal ((π * Real.Gamma (2 / p + 1)) ^ card ι / Real.Gamma (2 * ↑(card ι) / p + 1))

Tactic:
have : {x : ι → ℂ | (∑ i, ‖x i‖ ^ p) ^ (1 / p) < r} = ∅ := by
  ext x
  refine ⟨fun hx => ?_, fun hx => hx.elim⟩
  exact not_le.mpr (lt_of_lt_of_le (Set.mem_setOf.mp hx) hr) (h₂ x)

Result:
case inl
ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : Nonempty ι
p : ℝ
hp : 1 ≤ p
r : ℝ
h₁ : ∀ (x : ι → ℂ), 0 ≤ ∑ i : ι, ‖x i‖ ^ p
h₂ : ∀ (x : ι → ℂ), 0 ≤ (∑ i : ι, ‖x i‖ ^ p) ^ (1 / p)
hr : r ≤ 0
this : {x | (∑ i : ι, ‖x i‖ ^ p) ^ (1 / p) < r} = ∅
⊢ volume {x | (∑ i : ι, ‖x i‖ ^ p) ^ (1 / p) < r} =
    ENNReal.ofReal r ^ (2 * card ι) *
      ENNReal.ofReal ((π * Real.Gamma (2 / p + 1)) ^ card ι / Real.Gamma (2 * ↑(card ι) / p + 1))

Proof state:
ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : Nonempty ι
p : ℝ
hp : 1 ≤ p
r : ℝ
x : ι → ℂ
⊢ 0 ≤ ∑ i : ι, ‖x i‖ ^ p

Tactic:
positivity

Result:
no goals

Proof state:
case inr
ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : Nonempty ι
p : ℝ
hp : 1 ≤ p
r : ℝ
h₁ : ∀ (x : ι → ℂ), 0 ≤ ∑ i : ι, ‖x i‖ ^ p
h₂ : ∀ (x : ι → ℂ), 0 ≤ (∑ i : ι, ‖x i‖ ^ p) ^ (1 / p)
hr : 0 < r
⊢ volume {x | (∑ i : ι, ‖x i‖ ^ p) ^ (1 / p) < r} =
    ENNReal.ofReal r ^ (2 * card ι) *
      ENNReal.ofReal ((π * Real.Gamma (2 / p + 1)) ^ card ι / Real.Gamma (2 * ↑(card ι) / p + 1))

Tactic:
rw [← Complex.volume_sum_rpow_lt_one _ hp, ← ENNReal.ofReal_pow (le_of_lt hr)]

Result:
case inr
ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : Nonempty ι
p : ℝ
hp : 1 ≤ p
r : ℝ
h₁ : ∀ (x : ι → ℂ), 0 ≤ ∑ i : ι, ‖x i‖ ^ p
h₂ : ∀ (x : ι → ℂ), 0 ≤ (∑ i : ι, ‖x i‖ ^ p) ^ (1 / p)
hr : 0 < r
⊢ volume {x | (∑ i : ι, ‖x i‖ ^ p) ^ (1 / p) < r} =
    ENNReal.ofReal (r ^ (2 * card ι)) * volume {x | ∑ i : ι, ‖x i‖ ^ p < 1}
-- Mathlib/Topology/Basic.lean
theorem eventually_nhds_iff {p : X → Prop} :
    (∀ᶠ y in 𝓝 x, p y) ↔ ∃ t : Set X, (∀ y ∈ t, p y) ∧ IsOpen t ∧ x ∈ t :=
  mem_nhds_iff.trans <| by simp only [subset_def, exists_prop, mem_setOf_eq]

Proof state:
X : Type u
x : X
inst✝ : TopologicalSpace X
p : X → Prop
⊢ (∃ t ⊆ {x | (fun y => p y) x}, IsOpen t ∧ x ∈ t) ↔ ∃ t, (∀ y ∈ t, p y) ∧ IsOpen t ∧ x ∈ t

Tactic:
simp only [subset_def, exists_prop, mem_setOf_eq]

Result:
no goals
-- Mathlib/Data/Nat/PartENat.lean
theorem eq_top_iff_forall_lt (x : PartENat) : x = ⊤ ↔ ∀ n : ℕ, (n : PartENat) < x

Proof state:
case mp
n : ℕ
⊢ ↑n < ⊤

Tactic:
exact natCast_lt_top _

Result:
no goals

Proof state:
case mpr
x : PartENat
⊢ x ≠ ⊤ → ∃ n, ¬↑n < x

Tactic:
rw [ne_top_iff]

Result:
case mpr
x : PartENat
⊢ (∃ n, x = ↑n) → ∃ n, ¬↑n < x

Proof state:
case mp
x : PartENat
⊢ x = ⊤ → ∀ (n : ℕ), ↑n < x

Tactic:
rintro rfl n

Result:
case mp
n : ℕ
⊢ ↑n < ⊤

Proof state:
case mpr
x : PartENat
⊢ (∃ n, x = ↑n) → ∃ n, ¬↑n < x

Tactic:
rintro ⟨n, rfl⟩

Result:
case mpr.intro
n : ℕ
⊢ ∃ n_1, ¬↑n_1 < ↑n

Proof state:
x : PartENat
⊢ x = ⊤ ↔ ∀ (n : ℕ), ↑n < x

Tactic:
constructor

Result:
case mp
x : PartENat
⊢ x = ⊤ → ∀ (n : ℕ), ↑n < x

case mpr
x : PartENat
⊢ (∀ (n : ℕ), ↑n < x) → x = ⊤

Proof state:
case mpr
x : PartENat
⊢ (∀ (n : ℕ), ↑n < x) → x = ⊤

Tactic:
contrapose!

Result:
case mpr
x : PartENat
⊢ x ≠ ⊤ → ∃ n, ¬↑n < x

Proof state:
case mpr.intro
n : ℕ
⊢ ∃ n_1, ¬↑n_1 < ↑n

Tactic:
exact ⟨n, irrefl _⟩

Result:
no goals
-- Mathlib/Algebra/Ring/Periodic.lean
theorem Antiperiodic.sub_nsmul_eq [AddGroup α] [AddGroup β] (h : Antiperiodic f c) (n : ℕ) :
    f (x - n • c) = (-1) ^ n • f x

Proof state:
α : Type u_1
β : Type u_2
f : α → β
c x : α
inst✝¹ : AddGroup α
inst✝ : AddGroup β
h : Antiperiodic f c
n : ℕ
⊢ f (x - n • c) = (-1) ^ n • f x

Tactic:
simpa only [Int.reduceNeg, natCast_zsmul] using h.sub_zsmul_eq n

Result:
no goals
-- Mathlib/Data/Finset/Grade.lean
lemma covBy_iff_exists_erase : s ⋖ t ↔ ∃ a ∈ t, t.erase a = s

Proof state:
α : Type u_1
s t : Finset α
inst✝ : DecidableEq α
⊢ s ⋖ t ↔ ∃ a ∈ t, t.erase a = s

Tactic:
simp only [← coe_covBy_coe, Set.covBy_iff_exists_sdiff_singleton, ← coe_inj, coe_erase, mem_coe]

Result:
no goals
-- Mathlib/Analysis/Normed/Group/Basic.lean
theorem ne_one_of_nnnorm_ne_zero {a : E} : ‖a‖₊ ≠ 0 → a ≠ 1 :=
  mt <| by
    rintro rfl
    exact nnnorm_one'

Proof state:
E : Type u_5
inst✝ : SeminormedGroup E
a : E
⊢ a = 1 → ‖a‖₊ = 0

Tactic:
rintro rfl

Result:
E : Type u_5
inst✝ : SeminormedGroup E
⊢ ‖1‖₊ = 0

Proof state:
E : Type u_5
inst✝ : SeminormedGroup E
⊢ ‖1‖₊ = 0

Tactic:
exact nnnorm_one'

Result:
no goals
-- Mathlib/Data/Matroid/Rank/Finite.lean
lemma isRkFinite_ground (M : Matroid α) [RankFinite M] : M.IsRkFinite M.E

Proof state:
α : Type u_1
M : Matroid α
inst✝ : M.RankFinite
⊢ M.IsRkFinite M.E

Tactic:
rwa [isRkFinite_ground_iff_rankFinite]

Result:
no goals
-- Mathlib/Analysis/Calculus/FDeriv/Equiv.lean
lemma _root_.fderiv_continuousLinearEquiv_comp' (L : G ≃L[𝕜] G') (f : E → (F →L[𝕜] G)) :
    fderiv 𝕜 (fun x ↦ (L : G →L[𝕜] G').comp (f x)) =
      fun x ↦ (((ContinuousLinearEquiv.refl 𝕜 F).arrowCongr L)) ∘L (fderiv 𝕜 f x)

Proof state:
case h
𝕜 : Type u_1
inst✝⁸ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace 𝕜 E
F : Type u_3
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
G : Type u_4
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
G' : Type u_5
inst✝¹ : NormedAddCommGroup G'
inst✝ : NormedSpace 𝕜 G'
L : G ≃L[𝕜] G'
f : E → F →L[𝕜] G
x : E
⊢ fderiv 𝕜 (fun x => (↑L).comp (f x)) x = (↑((ContinuousLinearEquiv.refl 𝕜 F).arrowCongr L)).comp (fderiv 𝕜 f x)

Tactic:
exact fderiv_continuousLinearEquiv_comp L f x

Result:
no goals

Proof state:
𝕜 : Type u_1
inst✝⁸ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace 𝕜 E
F : Type u_3
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
G : Type u_4
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
G' : Type u_5
inst✝¹ : NormedAddCommGroup G'
inst✝ : NormedSpace 𝕜 G'
L : G ≃L[𝕜] G'
f : E → F →L[𝕜] G
⊢ (fderiv 𝕜 fun x => (↑L).comp (f x)) = fun x => (↑((ContinuousLinearEquiv.refl 𝕜 F).arrowCongr L)).comp (fderiv 𝕜 f x)

Tactic:
ext x : 1

Result:
case h
𝕜 : Type u_1
inst✝⁸ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace 𝕜 E
F : Type u_3
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
G : Type u_4
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
G' : Type u_5
inst✝¹ : NormedAddCommGroup G'
inst✝ : NormedSpace 𝕜 G'
L : G ≃L[𝕜] G'
f : E → F →L[𝕜] G
x : E
⊢ fderiv 𝕜 (fun x => (↑L).comp (f x)) x = (↑((ContinuousLinearEquiv.refl 𝕜 F).arrowCongr L)).comp (fderiv 𝕜 f x)
-- Mathlib/Order/InitialSeg.lean
theorem isLowerSet_range [Preorder α] (f : α ≤i β) : IsLowerSet (Set.range f)

Proof state:
case intro
α : Type u_1
β : Type u_2
inst✝¹ : PartialOrder β
inst✝ : Preorder α
f : (fun x1 x2 => x1 < x2) ≼i fun x1 x2 => x1 < x2
b : β
a : α
h : b ≤ f a
⊢ b ∈ Set.range ⇑f

Tactic:
exact mem_range_of_le f h

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : PartialOrder β
inst✝ : Preorder α
f : (fun x1 x2 => x1 < x2) ≼i fun x1 x2 => x1 < x2
⊢ IsLowerSet (Set.range ⇑f)

Tactic:
rintro _ b h ⟨a, rfl⟩

Result:
case intro
α : Type u_1
β : Type u_2
inst✝¹ : PartialOrder β
inst✝ : Preorder α
f : (fun x1 x2 => x1 < x2) ≼i fun x1 x2 => x1 < x2
b : β
a : α
h : b ≤ f a
⊢ b ∈ Set.range ⇑f
-- Mathlib/Geometry/RingedSpace/LocallyRingedSpace.lean
@[reassoc (attr := simp)]
lemma stalkMap_inv_hom (e : X ≅ Y) (x : X) :
    e.inv.stalkMap (e.hom.base x) ≫ e.hom.stalkMap x =
      X.presheaf.stalkSpecializes (specializes_of_eq <| by simp)

Proof state:
X✝ X Y Z : LocallyRingedSpace
f : X ⟶ Y
g : Y ⟶ Z
e : X ≅ Y
x : ↑X.toTopCat
⊢ x = (ConcreteCategory.hom e.inv.base) ((ConcreteCategory.hom e.hom.base) x)

Tactic:
simp

Result:
no goals

Proof state:
X Y : LocallyRingedSpace
e : X ≅ Y
x : ↑X.toTopCat
⊢ e.hom ≫ e.inv = 𝟙 X

Tactic:
simp

Result:
no goals

Proof state:
X Y : LocallyRingedSpace
e : X ≅ Y
x : ↑X.toTopCat
⊢ X.presheaf.stalkSpecializes ⋯ ≫ Hom.stalkMap (𝟙 X) x = X.presheaf.stalkSpecializes ⋯

Tactic:
simp

Result:
no goals

Proof state:
X Y : LocallyRingedSpace
e : X ≅ Y
x : ↑X.toTopCat
⊢ Hom.stalkMap e.inv ((ConcreteCategory.hom e.hom.base) x) ≫ Hom.stalkMap e.hom x = X.presheaf.stalkSpecializes ⋯

Tactic:
rw [← stalkMap_comp, LocallyRingedSpace.stalkMap_congr_hom (e.hom ≫ e.inv) (𝟙 _) (by simp)]

Result:
X Y : LocallyRingedSpace
e : X ≅ Y
x : ↑X.toTopCat
⊢ X.presheaf.stalkSpecializes ⋯ ≫ Hom.stalkMap (𝟙 X) x = X.presheaf.stalkSpecializes ⋯
-- Mathlib/Data/Complex/Norm.lean
@[simp] lemma nnnorm_I : ‖I‖₊ = 1

Proof state:
⊢ ‖I‖₊ = 1

Tactic:
simp [nnnorm]

Result:
no goals
-- Mathlib/Topology/Category/TopCat/Basic.lean
theorem of_homeoOfIso {X Y : TopCat.{u}} (f : X ≅ Y) : isoOfHomeo (homeoOfIso f) = f

Proof state:
case w.w
X Y : TopCat
f : X ≅ Y
x✝ : ↑X
⊢ (ConcreteCategory.hom (isoOfHomeo (homeoOfIso f)).hom) x✝ = (ConcreteCategory.hom f.hom) x✝

Tactic:
rfl

Result:
no goals

Proof state:
X Y : TopCat
f : X ≅ Y
⊢ isoOfHomeo (homeoOfIso f) = f

Tactic:
ext

Result:
case w.w
X Y : TopCat
f : X ≅ Y
x✝ : ↑X
⊢ (ConcreteCategory.hom (isoOfHomeo (homeoOfIso f)).hom) x✝ = (ConcreteCategory.hom f.hom) x✝
-- Mathlib/Analysis/BoxIntegral/UnitPartition.lean
theorem box_injective : Function.Injective (fun ν : ι → ℤ ↦ box n ν)

Proof state:
ι : Type u_1
n : ℕ
inst✝ : NeZero n
a₁✝ a₂✝ : ι → ℤ
h : a₁✝ ≠ a₂✝
⊢ box n a₁✝ ≠ box n a₂✝

Tactic:
exact Box.ne_of_disjoint_coe (disjoint.mp h)

Result:
no goals

Proof state:
ι : Type u_1
n : ℕ
inst✝ : NeZero n
⊢ Function.Injective fun ν => box n ν

Tactic:
intro _ _ h

Result:
ι : Type u_1
n : ℕ
inst✝ : NeZero n
a₁✝ a₂✝ : ι → ℤ
h : (fun ν => box n ν) a₁✝ = (fun ν => box n ν) a₂✝
⊢ a₁✝ = a₂✝

Proof state:
ι : Type u_1
n : ℕ
inst✝ : NeZero n
a₁✝ a₂✝ : ι → ℤ
h : (fun ν => box n ν) a₁✝ = (fun ν => box n ν) a₂✝
⊢ a₁✝ = a₂✝

Tactic:
contrapose! h

Result:
ι : Type u_1
n : ℕ
inst✝ : NeZero n
a₁✝ a₂✝ : ι → ℤ
h : a₁✝ ≠ a₂✝
⊢ box n a₁✝ ≠ box n a₂✝
-- Mathlib/Algebra/Homology/HomotopyCategory/Pretriangulated.lean
@[reassoc]
lemma map_comp (comm' : φ₂ ≫ b' = a' ≫ φ₃) :
    map φ₁ φ₃ (a ≫ a') (b ≫ b') (by rw [reassoc_of% comm, comm', assoc]) =
      map φ₁ φ₂ a b comm ≫ map φ₂ φ₃ a' b' comm'

Proof state:
case h
C : Type u_1
inst✝² : Category.{u_3, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasBinaryBiproducts C
K₁ L₁ K₂ L₂ K₃ L₃ : CochainComplex C ℤ
φ₁ : K₁ ⟶ L₁
φ₂ : K₂ ⟶ L₂
φ₃ : K₃ ⟶ L₃
a : K₁ ⟶ K₂
b : L₁ ⟶ L₂
comm : φ₁ ≫ b = a ≫ φ₂
a' : K₂ ⟶ K₃
b' : L₂ ⟶ L₃
comm' : φ₂ ≫ b' = a' ≫ φ₃
n : ℤ
⊢ (map φ₁ φ₃ (a ≫ a') (b ≫ b') ⋯).f n = (map φ₁ φ₂ a b comm ≫ map φ₂ φ₃ a' b' comm').f n

Tactic:
simp [ext_from_iff _ (n+1) n rfl, map]

Result:
no goals

Proof state:
C : Type u_1
D : Type u_2
inst✝⁵ : Category.{?u.80797, u_1} C
inst✝⁴ : Category.{?u.80801, u_2} D
inst✝³ : Preadditive C
inst✝² : HasBinaryBiproducts C
inst✝¹ : Preadditive D
inst✝ : HasBinaryBiproducts D
K L : CochainComplex C ℤ
φ : K ⟶ L
K₁ L₁ K₂ L₂ K₃ L₃ : CochainComplex C ℤ
φ₁ : K₁ ⟶ L₁
φ₂ : K₂ ⟶ L₂
φ₃ : K₃ ⟶ L₃
a : K₁ ⟶ K₂
b : L₁ ⟶ L₂
comm : φ₁ ≫ b = a ≫ φ₂
a' : K₂ ⟶ K₃
b' : L₂ ⟶ L₃
comm' : φ₂ ≫ b' = a' ≫ φ₃
⊢ φ₁ ≫ b ≫ b' = (a ≫ a') ≫ φ₃

Tactic:
rw [reassoc_of% comm, comm', assoc]

Result:
no goals

Proof state:
C : Type u_1
inst✝² : Category.{u_3, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasBinaryBiproducts C
K₁ L₁ K₂ L₂ K₃ L₃ : CochainComplex C ℤ
φ₁ : K₁ ⟶ L₁
φ₂ : K₂ ⟶ L₂
φ₃ : K₃ ⟶ L₃
a : K₁ ⟶ K₂
b : L₁ ⟶ L₂
comm : φ₁ ≫ b = a ≫ φ₂
a' : K₂ ⟶ K₃
b' : L₂ ⟶ L₃
comm' : φ₂ ≫ b' = a' ≫ φ₃
⊢ map φ₁ φ₃ (a ≫ a') (b ≫ b') ⋯ = map φ₁ φ₂ a b comm ≫ map φ₂ φ₃ a' b' comm'

Tactic:
ext n

Result:
case h
C : Type u_1
inst✝² : Category.{u_3, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasBinaryBiproducts C
K₁ L₁ K₂ L₂ K₃ L₃ : CochainComplex C ℤ
φ₁ : K₁ ⟶ L₁
φ₂ : K₂ ⟶ L₂
φ₃ : K₃ ⟶ L₃
a : K₁ ⟶ K₂
b : L₁ ⟶ L₂
comm : φ₁ ≫ b = a ≫ φ₂
a' : K₂ ⟶ K₃
b' : L₂ ⟶ L₃
comm' : φ₂ ≫ b' = a' ≫ φ₃
n : ℤ
⊢ (map φ₁ φ₃ (a ≫ a') (b ≫ b') ⋯).f n = (map φ₁ φ₂ a b comm ≫ map φ₂ φ₃ a' b' comm').f n
-- Mathlib/FieldTheory/Finite/Basic.lean
theorem sq_add_sq (R : Type*) [CommRing R] [IsDomain R] (p : ℕ) [NeZero p] [CharP R p] (x : ℤ) :
    ∃ a b : ℕ, ((a : R) ^ 2 + (b : R) ^ 2) = x

Proof state:
R : Type u_3
inst✝³ : CommRing R
inst✝² : IsDomain R
p : ℕ
inst✝¹ : NeZero p
inst✝ : CharP R p
x : ℤ
this : Fact (Nat.Prime p)
⊢ ∃ a b, ↑a ^ 2 + ↑b ^ 2 = ↑x

Tactic:
obtain ⟨a, b, hab⟩ := ZMod.sq_add_sq p x

Result:
case intro.intro
R : Type u_3
inst✝³ : CommRing R
inst✝² : IsDomain R
p : ℕ
inst✝¹ : NeZero p
inst✝ : CharP R p
x : ℤ
this : Fact (Nat.Prime p)
a b : ZMod p
hab : a ^ 2 + b ^ 2 = ↑x
⊢ ∃ a b, ↑a ^ 2 + ↑b ^ 2 = ↑x

Proof state:
case intro.intro
R : Type u_3
inst✝³ : CommRing R
inst✝² : IsDomain R
p : ℕ
inst✝¹ : NeZero p
inst✝ : CharP R p
x : ℤ
this : Fact (Nat.Prime p)
a b : ZMod p
hab : a ^ 2 + b ^ 2 = ↑x
⊢ ↑a.val ^ 2 + ↑b.val ^ 2 = ↑x

Tactic:
simpa using congr_arg (ZMod.castHom dvd_rfl R) hab

Result:
no goals

Proof state:
case intro.intro
R : Type u_3
inst✝³ : CommRing R
inst✝² : IsDomain R
p : ℕ
inst✝¹ : NeZero p
inst✝ : CharP R p
x : ℤ
this : Fact (Nat.Prime p)
a b : ZMod p
hab : a ^ 2 + b ^ 2 = ↑x
⊢ ∃ a b, ↑a ^ 2 + ↑b ^ 2 = ↑x

Tactic:
refine ⟨a.val, b.val, ?_⟩

Result:
case intro.intro
R : Type u_3
inst✝³ : CommRing R
inst✝² : IsDomain R
p : ℕ
inst✝¹ : NeZero p
inst✝ : CharP R p
x : ℤ
this : Fact (Nat.Prime p)
a b : ZMod p
hab : a ^ 2 + b ^ 2 = ↑x
⊢ ↑a.val ^ 2 + ↑b.val ^ 2 = ↑x

Proof state:
R : Type u_3
inst✝³ : CommRing R
inst✝² : IsDomain R
p : ℕ
inst✝¹ : NeZero p
inst✝ : CharP R p
x : ℤ
⊢ ∃ a b, ↑a ^ 2 + ↑b ^ 2 = ↑x

Tactic:
haveI := char_is_prime_of_pos R p

Result:
R : Type u_3
inst✝³ : CommRing R
inst✝² : IsDomain R
p : ℕ
inst✝¹ : NeZero p
inst✝ : CharP R p
x : ℤ
this : Fact (Nat.Prime p)
⊢ ∃ a b, ↑a ^ 2 + ↑b ^ 2 = ↑x
-- Mathlib/Data/Nat/Choose/Multinomial.lean
theorem multinomial_insert_one [DecidableEq α] (h : a ∉ s) (h₁ : f a = 1) :
    multinomial (insert a s) f = (s.sum f).succ * multinomial s f

Proof state:
α : Type u_1
s : Finset α
f : α → ℕ
a : α
inst✝ : DecidableEq α
h : a ∉ s
h₁ : f a = 1
⊢ (∑ x ∈ s, f x + 1) * (∑ x ∈ s, f x)! / (1! * ∏ x ∈ s, (f x)!) = (s.sum f).succ * ((∑ i ∈ s, f i)! / ∏ i ∈ s, (f i)!)

Tactic:
simp only [factorial, succ_eq_add_one, zero_add, mul_one, one_mul]

Result:
α : Type u_1
s : Finset α
f : α → ℕ
a : α
inst✝ : DecidableEq α
h : a ∉ s
h₁ : f a = 1
⊢ (∑ x ∈ s, f x + 1) * (∑ x ∈ s, f x)! / ∏ x ∈ s, (f x)! = (s.sum f + 1) * ((∑ x ∈ s, f x)! / ∏ x ∈ s, (f x)!)

Proof state:
α : Type u_1
s : Finset α
f : α → ℕ
a : α
inst✝ : DecidableEq α
h : a ∉ s
h₁ : f a = 1
⊢ multinomial (insert a s) f = (s.sum f).succ * multinomial s f

Tactic:
simp only [multinomial]

Result:
α : Type u_1
s : Finset α
f : α → ℕ
a : α
inst✝ : DecidableEq α
h : a ∉ s
h₁ : f a = 1
⊢ (∑ i ∈ insert a s, f i)! / ∏ i ∈ insert a s, (f i)! = (s.sum f).succ * ((∑ i ∈ s, f i)! / ∏ i ∈ s, (f i)!)

Proof state:
α : Type u_1
s : Finset α
f : α → ℕ
a : α
inst✝ : DecidableEq α
h : a ∉ s
h₁ : f a = 1
⊢ (∑ x ∈ s, f x + 1) * (∑ x ∈ s, f x)! / ∏ x ∈ s, (f x)! = (s.sum f + 1) * ((∑ x ∈ s, f x)! / ∏ x ∈ s, (f x)!)

Tactic:
rw [Nat.mul_div_assoc _ (prod_factorial_dvd_factorial_sum _ _)]

Result:
no goals

Proof state:
α : Type u_1
s : Finset α
f : α → ℕ
a : α
inst✝ : DecidableEq α
h : a ∉ s
h₁ : f a = 1
⊢ (∑ i ∈ insert a s, f i)! / ∏ i ∈ insert a s, (f i)! = (s.sum f).succ * ((∑ i ∈ s, f i)! / ∏ i ∈ s, (f i)!)

Tactic:
rw [Finset.sum_insert h, Finset.prod_insert h, h₁, add_comm, ← succ_eq_add_one, factorial_succ]

Result:
α : Type u_1
s : Finset α
f : α → ℕ
a : α
inst✝ : DecidableEq α
h : a ∉ s
h₁ : f a = 1
⊢ (∑ x ∈ s, f x + 1) * (∑ x ∈ s, f x)! / (1! * ∏ x ∈ s, (f x)!) = (s.sum f).succ * ((∑ i ∈ s, f i)! / ∏ i ∈ s, (f i)!)
-- Mathlib/Data/Ordmap/Ordset.lean
theorem all_rotateR {P l x r} : @All α P (rotateR l x r) ↔ All P l ∧ P x ∧ All P r

Proof state:
α : Type u_1
P : α → Prop
l : Ordnode α
x : α
r : Ordnode α
⊢ All P (l.rotateR x r) ↔ All P l ∧ P x ∧ All P r

Tactic:
rw [← all_dual, dual_rotateR, all_rotateL]

Result:
α : Type u_1
P : α → Prop
l : Ordnode α
x : α
r : Ordnode α
⊢ All P r.dual ∧ P x ∧ All P l.dual ↔ All P l ∧ P x ∧ All P r

Proof state:
α : Type u_1
P : α → Prop
l : Ordnode α
x : α
r : Ordnode α
⊢ All P r.dual ∧ P x ∧ All P l.dual ↔ All P l ∧ P x ∧ All P r

Tactic:
simp [all_dual, and_comm, and_left_comm, and_assoc]

Result:
no goals
-- Mathlib/Order/Filter/CardinalInter.lean
lemma cardinalInter_ofCardinalGenerate (hc : 2 < c) :
    CardinalInterFilter (cardinalGenerate g hc) c

Proof state:
α : Type u
c : Cardinal.{u}
g : Set (Set α)
hc : 2 < c
⊢ CardinalInterFilter (ofCardinalInter (CardinalGenerateSets g) hc ⋯ ⋯) c

Tactic:
apply cardinalInter_ofCardinalInter _ _ _

Result:
no goals

Proof state:
α : Type u
c : Cardinal.{u}
g : Set (Set α)
hc : 2 < c
⊢ CardinalInterFilter (cardinalGenerate g hc) c

Tactic:
delta cardinalGenerate

Result:
α : Type u
c : Cardinal.{u}
g : Set (Set α)
hc : 2 < c
⊢ CardinalInterFilter (ofCardinalInter (CardinalGenerateSets g) hc ⋯ ⋯) c
-- Mathlib/CategoryTheory/MorphismProperty/Limits.lean
lemma coproducts_le [IsStableUnderCoproducts.{w} W] :
    coproducts.{w} W ≤ W

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
W : MorphismProperty C
inst✝ : IsStableUnderCoproducts.{w, v, u} W
⊢ coproducts.{w, v, u} W ≤ W

Tactic:
intro X Y f hf

Result:
C : Type u
inst✝¹ : Category.{v, u} C
W : MorphismProperty C
inst✝ : IsStableUnderCoproducts.{w, v, u} W
X Y : C
f : X ⟶ Y
hf : coproducts.{w, v, u} W f
⊢ W f

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
W : MorphismProperty C
inst✝ : IsStableUnderCoproducts.{w, v, u} W
X Y : C
f : X ⟶ Y
hf : ∃ J, W.colimitsOfShape (Discrete J) f
⊢ W f

Tactic:
obtain ⟨J, hf⟩ := hf

Result:
case intro
C : Type u
inst✝¹ : Category.{v, u} C
W : MorphismProperty C
inst✝ : IsStableUnderCoproducts.{w, v, u} W
X Y : C
f : X ⟶ Y
J : Type w
hf : W.colimitsOfShape (Discrete J) f
⊢ W f

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
W : MorphismProperty C
inst✝ : IsStableUnderCoproducts.{w, v, u} W
X Y : C
f : X ⟶ Y
hf : coproducts.{w, v, u} W f
⊢ W f

Tactic:
rw [coproducts_iff] at hf

Result:
C : Type u
inst✝¹ : Category.{v, u} C
W : MorphismProperty C
inst✝ : IsStableUnderCoproducts.{w, v, u} W
X Y : C
f : X ⟶ Y
hf : ∃ J, W.colimitsOfShape (Discrete J) f
⊢ W f

Proof state:
case intro
C : Type u
inst✝¹ : Category.{v, u} C
W : MorphismProperty C
inst✝ : IsStableUnderCoproducts.{w, v, u} W
X Y : C
f : X ⟶ Y
J : Type w
hf : W.colimitsOfShape (Discrete J) f
⊢ W f

Tactic:
exact (isStableUnderCoproductsOfShape_of_isStableUnderCoproducts W J).colimitsOfShape_le _ hf

Result:
no goals