harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Nat/Compare.lean
theorem compare_def_le (a b : Nat) :
    compare a b = if a ≤ b then if b ≤ a then .eq else .lt else .gt

Proof state:
a b : Nat
hge : ¬a < b
hgt : b < a
⊢ Ordering.gt = if a ≤ b then if b ≤ a then Ordering.eq else Ordering.lt else Ordering.gt

Tactic:
simp [Nat.le_of_lt hgt, Nat.not_le.2 hgt]

Result:
no goals

Proof state:
case isTrue
a b : Nat
hge : ¬a < b
h✝ : b < a
⊢ Ordering.gt = if a ≤ b then if b ≤ a then Ordering.eq else Ordering.lt else Ordering.gt

Tactic:
next hgt => simp [Nat.le_of_lt hgt, Nat.not_le.2 hgt]

Result:
no goals

Proof state:
a b : Nat
hge : ¬a < b
hle : ¬b < a
⊢ Ordering.eq = if a ≤ b then if b ≤ a then Ordering.eq else Ordering.lt else Ordering.gt

Tactic:
simp [Nat.not_lt.1 hge, Nat.not_lt.1 hle]

Result:
no goals

Proof state:
a b : Nat
hge : ¬a < b
⊢ (if b < a then Ordering.gt else Ordering.eq) =
    if a ≤ b then if b ≤ a then Ordering.eq else Ordering.lt else Ordering.gt

Tactic:
split

Result:
case isTrue
a b : Nat
hge : ¬a < b
h✝ : b < a
⊢ Ordering.gt = if a ≤ b then if b ≤ a then Ordering.eq else Ordering.lt else Ordering.gt

case isFalse
a b : Nat
hge : ¬a < b
h✝ : ¬b < a
⊢ Ordering.eq = if a ≤ b then if b ≤ a then Ordering.eq else Ordering.lt else Ordering.gt

Proof state:
a b : Nat
hlt : a < b
⊢ Ordering.lt = if a ≤ b then if b ≤ a then Ordering.eq else Ordering.lt else Ordering.gt

Tactic:
simp [Nat.le_of_lt hlt, Nat.not_le.2 hlt]

Result:
no goals

Proof state:
a b : Nat
⊢ (if a < b then Ordering.lt else if b < a then Ordering.gt else Ordering.eq) =
    if a ≤ b then if b ≤ a then Ordering.eq else Ordering.lt else Ordering.gt

Tactic:
split

Result:
case isTrue
a b : Nat
h✝ : a < b
⊢ Ordering.lt = if a ≤ b then if b ≤ a then Ordering.eq else Ordering.lt else Ordering.gt

case isFalse
a b : Nat
h✝ : ¬a < b
⊢ (if b < a then Ordering.gt else Ordering.eq) =
    if a ≤ b then if b ≤ a then Ordering.eq else Ordering.lt else Ordering.gt

Proof state:
case isFalse
a b : Nat
hge : ¬a < b
h✝ : ¬b < a
⊢ Ordering.eq = if a ≤ b then if b ≤ a then Ordering.eq else Ordering.lt else Ordering.gt

Tactic:
next hle => simp [Nat.not_lt.1 hge, Nat.not_lt.1 hle]

Result:
no goals

Proof state:
a b : Nat
⊢ compare a b = if a ≤ b then if b ≤ a then Ordering.eq else Ordering.lt else Ordering.gt

Tactic:
rw [compare_def_lt]

Result:
a b : Nat
⊢ (if a < b then Ordering.lt else if b < a then Ordering.gt else Ordering.eq) =
    if a ≤ b then if b ≤ a then Ordering.eq else Ordering.lt else Ordering.gt

Proof state:
case isTrue
a b : Nat
h✝ : a < b
⊢ Ordering.lt = if a ≤ b then if b ≤ a then Ordering.eq else Ordering.lt else Ordering.gt

Tactic:
next hlt => simp [Nat.le_of_lt hlt, Nat.not_le.2 hlt]

Result:
no goals
-- Mathlib/Topology/PartitionOfUnity.lean
theorem finite_tsupport : {i | x₀ ∈ tsupport (ρ i)}.Finite

Proof state:
ι : Type u
X : Type v
inst✝ : TopologicalSpace X
s : Set X
ρ : PartitionOfUnity ι X s
x₀ : X
⊢ {i | x₀ ∈ tsupport ⇑(ρ i)}.Finite

Tactic:
rcases ρ.locallyFinite x₀ with ⟨t, t_in, ht⟩

Result:
case intro.intro
ι : Type u
X : Type v
inst✝ : TopologicalSpace X
s : Set X
ρ : PartitionOfUnity ι X s
x₀ : X
t : Set X
t_in : t ∈ 𝓝 x₀
ht : {i | ((fun i => support ⇑(ρ i)) i ∩ t).Nonempty}.Finite
⊢ {i | x₀ ∈ tsupport ⇑(ρ i)}.Finite

Proof state:
case intro.intro
ι : Type u
X : Type v
inst✝ : TopologicalSpace X
s : Set X
ρ : PartitionOfUnity ι X s
x₀ : X
t : Set X
t_in : t ∈ 𝓝 x₀
ht : {i | ((fun i => support ⇑(ρ i)) i ∩ t).Nonempty}.Finite
⊢ {i | x₀ ∈ tsupport ⇑(ρ i)}.Finite

Tactic:
apply ht.subset

Result:
case intro.intro
ι : Type u
X : Type v
inst✝ : TopologicalSpace X
s : Set X
ρ : PartitionOfUnity ι X s
x₀ : X
t : Set X
t_in : t ∈ 𝓝 x₀
ht : {i | ((fun i => support ⇑(ρ i)) i ∩ t).Nonempty}.Finite
⊢ {i | x₀ ∈ tsupport ⇑(ρ i)} ⊆ {i | ((fun i => support ⇑(ρ i)) i ∩ t).Nonempty}

Proof state:
case intro.intro
ι : Type u
X : Type v
inst✝ : TopologicalSpace X
s : Set X
ρ : PartitionOfUnity ι X s
x₀ : X
t : Set X
t_in : t ∈ 𝓝 x₀
ht : {i | ((fun i => support ⇑(ρ i)) i ∩ t).Nonempty}.Finite
⊢ {i | x₀ ∈ tsupport ⇑(ρ i)} ⊆ {i | ((fun i => support ⇑(ρ i)) i ∩ t).Nonempty}

Tactic:
rintro i hi

Result:
case intro.intro
ι : Type u
X : Type v
inst✝ : TopologicalSpace X
s : Set X
ρ : PartitionOfUnity ι X s
x₀ : X
t : Set X
t_in : t ∈ 𝓝 x₀
ht : {i | ((fun i => support ⇑(ρ i)) i ∩ t).Nonempty}.Finite
i : ι
hi : i ∈ {i | x₀ ∈ tsupport ⇑(ρ i)}
⊢ i ∈ {i | ((fun i => support ⇑(ρ i)) i ∩ t).Nonempty}

Proof state:
case intro.intro
ι : Type u
X : Type v
inst✝ : TopologicalSpace X
s : Set X
ρ : PartitionOfUnity ι X s
x₀ : X
t : Set X
t_in : t ∈ 𝓝 x₀
ht : {i | ((fun i => support ⇑(ρ i)) i ∩ t).Nonempty}.Finite
i : ι
hi : i ∈ {i | x₀ ∈ tsupport ⇑(ρ i)}
⊢ i ∈ {i | (t ∩ support ⇑(ρ i)).Nonempty}

Tactic:
exact mem_closure_iff_nhds.mp hi t t_in

Result:
no goals

Proof state:
case intro.intro
ι : Type u
X : Type v
inst✝ : TopologicalSpace X
s : Set X
ρ : PartitionOfUnity ι X s
x₀ : X
t : Set X
t_in : t ∈ 𝓝 x₀
ht : {i | ((fun i => support ⇑(ρ i)) i ∩ t).Nonempty}.Finite
i : ι
hi : i ∈ {i | x₀ ∈ tsupport ⇑(ρ i)}
⊢ i ∈ {i | ((fun i => support ⇑(ρ i)) i ∩ t).Nonempty}

Tactic:
simp only [inter_comm]

Result:
case intro.intro
ι : Type u
X : Type v
inst✝ : TopologicalSpace X
s : Set X
ρ : PartitionOfUnity ι X s
x₀ : X
t : Set X
t_in : t ∈ 𝓝 x₀
ht : {i | ((fun i => support ⇑(ρ i)) i ∩ t).Nonempty}.Finite
i : ι
hi : i ∈ {i | x₀ ∈ tsupport ⇑(ρ i)}
⊢ i ∈ {i | (t ∩ support ⇑(ρ i)).Nonempty}
-- Mathlib/Algebra/Order/Ring/Basic.lean
lemma add_sq_le : (a + b) ^ 2 ≤ 2 * (a ^ 2 + b ^ 2)

Proof state:
R : Type u_3
inst✝¹ : LinearOrderedSemiring R
a b : R
inst✝ : ExistsAddOfLE R
⊢ (a + b) ^ 2 = a ^ 2 + b ^ 2 + (a * b + b * a)

Tactic:
simp_rw [pow_succ', pow_zero, mul_one, add_mul, mul_add, add_comm (b * a), add_add_add_comm]

Result:
no goals

Proof state:
case inr
R : Type u_3
inst✝¹ : LinearOrderedSemiring R
a b : R
inst✝ : ExistsAddOfLE R
h✝ : b ≤ a
⊢ a * b + b * a ≤ a * a + b * b

Tactic:
exact mul_add_mul_le_mul_add_mul' ‹_› ‹_›

Result:
no goals

Proof state:
case inl
R : Type u_3
inst✝¹ : LinearOrderedSemiring R
a b : R
inst✝ : ExistsAddOfLE R
h✝ : a ≤ b
⊢ a * b + b * a ≤ a * a + b * b

Tactic:
exact mul_add_mul_le_mul_add_mul ‹_› ‹_›

Result:
no goals

Proof state:
R : Type u_3
inst✝¹ : LinearOrderedSemiring R
a b : R
inst✝ : ExistsAddOfLE R
⊢ (a + b) ^ 2 ≤ 2 * (a ^ 2 + b ^ 2)

Tactic:
calc
  (a + b) ^ 2 = a ^ 2 + b ^ 2 + (a * b + b * a) := by
      simp_rw [pow_succ', pow_zero, mul_one, add_mul, mul_add, add_comm (b * a), add_add_add_comm]
  _ ≤ a ^ 2 + b ^ 2 + (a * a + b * b) := add_le_add_left ?_ _
  _ = _ := by simp_rw [pow_succ', pow_zero, mul_one, two_mul]

Result:
R : Type u_3
inst✝¹ : LinearOrderedSemiring R
a b : R
inst✝ : ExistsAddOfLE R
⊢ a * b + b * a ≤ a * a + b * b

Proof state:
R : Type u_3
inst✝¹ : LinearOrderedSemiring R
a b : R
inst✝ : ExistsAddOfLE R
⊢ a * b + b * a ≤ a * a + b * b

Tactic:
cases le_total a b

Result:
case inl
R : Type u_3
inst✝¹ : LinearOrderedSemiring R
a b : R
inst✝ : ExistsAddOfLE R
h✝ : a ≤ b
⊢ a * b + b * a ≤ a * a + b * b

case inr
R : Type u_3
inst✝¹ : LinearOrderedSemiring R
a b : R
inst✝ : ExistsAddOfLE R
h✝ : b ≤ a
⊢ a * b + b * a ≤ a * a + b * b

Proof state:
R : Type u_3
inst✝¹ : LinearOrderedSemiring R
a b : R
inst✝ : ExistsAddOfLE R
⊢ a ^ 2 + b ^ 2 + (a * a + b * b) = 2 * (a ^ 2 + b ^ 2)

Tactic:
simp_rw [pow_succ', pow_zero, mul_one, two_mul]

Result:
no goals
-- Mathlib/Order/Fin/Basic.lean
/-- While in many cases `Fin.castOrderIso` is better than `Equiv.cast`/`cast`, sometimes we want to
apply a generic lemma about `cast`. -/
lemma castOrderIso_toEquiv (h : n = m) : (castOrderIso h).toEquiv = Equiv.cast (h ▸ rfl)

Proof state:
m n : ℕ
h : n = m
⊢ (castOrderIso h).toEquiv = Equiv.cast ⋯

Tactic:
subst h

Result:
n : ℕ
⊢ (castOrderIso ⋯).toEquiv = Equiv.cast ⋯

Proof state:
n : ℕ
⊢ (castOrderIso ⋯).toEquiv = Equiv.cast ⋯

Tactic:
rfl

Result:
no goals
-- Mathlib/NumberTheory/LSeries/RiemannZeta.lean
theorem tendsto_sub_mul_tsum_nat_cpow :
    Tendsto (fun s : ℂ ↦ (s - 1) * ∑' (n : ℕ), 1 / (n : ℂ) ^ s) (𝓝[{s | 1 < re s}] 1) (𝓝 1)

Proof state:
case refine_1

⊢ {s | 1 < s.re} ⊆ {1}ᶜ

Tactic:
simp only [subset_compl_singleton_iff, mem_setOf_eq, one_re, not_lt, le_refl]

Result:
no goals

Proof state:
⊢ Tendsto (fun s => (s - 1) * ∑' (n : ℕ), 1 / ↑n ^ s) (𝓝[{s | 1 < s.re}] 1) (𝓝 1)

Tactic:
refine (tendsto_nhdsWithin_mono_left ?_ riemannZeta_residue_one).congr' ?_

Result:
case refine_1

⊢ {s | 1 < s.re} ⊆ {1}ᶜ

case refine_2

⊢ (fun s => (s - 1) * riemannZeta s) =ᶠ[𝓝[{s | 1 < s.re}] 1] fun s => (s - 1) * ∑' (n : ℕ), 1 / ↑n ^ s

Proof state:
case refine_2

⊢ (fun s => (s - 1) * riemannZeta s) =ᶠ[𝓝[{s | 1 < s.re}] 1] fun s => (s - 1) * ∑' (n : ℕ), 1 / ↑n ^ s

Tactic:
filter_upwards [eventually_mem_nhdsWithin] with s hs using
  congr_arg _ <| zeta_eq_tsum_one_div_nat_cpow hs

Result:
no goals
-- Mathlib/Order/BooleanGenerators.lean
lemma eq_atoms_of_sSup_eq_top (hS : BooleanGenerators S) (h : sSup S = ⊤) :
    S = {a : α | IsAtom a}

Proof state:
case a
α : Type u_1
inst✝¹ : CompleteLattice α
S : Set α
inst✝ : IsCompactlyGenerated α
hS : BooleanGenerators S
h : sSup S = ⊤
a : α
ha : a ∈ {a | IsAtom a}
⊢ a ∈ S

Tactic:
obtain ⟨T, hT, rfl⟩ := hS.atomistic a (le_top.trans h.ge)

Result:
case a.intro.intro
α : Type u_1
inst✝¹ : CompleteLattice α
S : Set α
inst✝ : IsCompactlyGenerated α
hS : BooleanGenerators S
h : sSup S = ⊤
T : Set α
hT : T ⊆ S
ha : sSup T ∈ {a | IsAtom a}
⊢ sSup T ∈ S

Proof state:
α : Type u_1
inst✝¹ : CompleteLattice α
S : Set α
inst✝ : IsCompactlyGenerated α
hS : BooleanGenerators S
h : sSup S = ⊤
⊢ S = {a | IsAtom a}

Tactic:
apply le_antisymm

Result:
case a
α : Type u_1
inst✝¹ : CompleteLattice α
S : Set α
inst✝ : IsCompactlyGenerated α
hS : BooleanGenerators S
h : sSup S = ⊤
⊢ S ≤ {a | IsAtom a}

case a
α : Type u_1
inst✝¹ : CompleteLattice α
S : Set α
inst✝ : IsCompactlyGenerated α
hS : BooleanGenerators S
h : sSup S = ⊤
⊢ {a | IsAtom a} ≤ S

Proof state:
case a
α : Type u_1
inst✝¹ : CompleteLattice α
S : Set α
inst✝ : IsCompactlyGenerated α
hS : BooleanGenerators S
h : sSup S = ⊤
⊢ {a | IsAtom a} ≤ S

Tactic:
intro a ha

Result:
case a
α : Type u_1
inst✝¹ : CompleteLattice α
S : Set α
inst✝ : IsCompactlyGenerated α
hS : BooleanGenerators S
h : sSup S = ⊤
a : α
ha : a ∈ {a | IsAtom a}
⊢ a ∈ S

Proof state:
case a.intro.intro
α : Type u_1
inst✝¹ : CompleteLattice α
S : Set α
inst✝ : IsCompactlyGenerated α
hS : BooleanGenerators S
h : sSup S = ⊤
T : Set α
hT : T ⊆ S
ha : sSup T ∈ {a | IsAtom a}
⊢ sSup T ∈ S

Tactic:
exact hS.mem_of_isAtom_of_le_sSup_atoms _ ha (sSup_le_sSup hT)

Result:
no goals

Proof state:
case a
α : Type u_1
inst✝¹ : CompleteLattice α
S : Set α
inst✝ : IsCompactlyGenerated α
hS : BooleanGenerators S
h : sSup S = ⊤
⊢ S ≤ {a | IsAtom a}

Tactic:
exact hS.isAtom

Result:
no goals
-- Mathlib/Order/Filter/AtTopBot/Basic.lean
theorem tendsto_comp_val_Ici_atTop [Preorder α] [IsDirected α (· ≤ ·)]
    {a : α} {f : α → β} {l : Filter β} :
    Tendsto (fun x : Ici a => f x) atTop l ↔ Tendsto f atTop l

Proof state:
α : Type u_3
β : Type u_4
inst✝¹ : Preorder α
inst✝ : IsDirected α fun x1 x2 => x1 ≤ x2
a : α
f : α → β
l : Filter β
⊢ Tendsto (fun x => f ↑x) atTop l ↔ Tendsto f atTop l

Tactic:
rw [← map_val_Ici_atTop a, tendsto_map'_iff, Function.comp_def]

Result:
no goals
-- Mathlib/LinearAlgebra/TensorProduct/Graded/External.lean
theorem gradedComm_gradedMul (x y : DirectSum _ 𝒜 ⊗[R] DirectSum _ ℬ) :
    gradedComm R 𝒜 ℬ (gradedMul R 𝒜 ℬ x y)
      = gradedMul R ℬ 𝒜 (gradedComm R 𝒜 ℬ x) (gradedComm R 𝒜 ℬ y)

Proof state:
case a.H.h.H.h.a.H.h.H.h.e_a
R : Type u_1
ι : Type u_2
inst✝¹¹ : CommSemiring ι
inst✝¹⁰ : Module ι (Additive ℤˣ)
inst✝⁹ : DecidableEq ι
𝒜 : ι → Type u_3
ℬ : ι → Type u_4
inst✝⁸ : CommRing R
inst✝⁷ : (i : ι) → AddCommGroup (𝒜 i)
inst✝⁶ : (i : ι) → AddCommGroup (ℬ i)
inst✝⁵ : (i : ι) → Module R (𝒜 i)
inst✝⁴ : (i : ι) → Module R (ℬ i)
inst✝³ : DirectSum.GRing 𝒜
inst✝² : DirectSum.GRing ℬ
inst✝¹ : DirectSum.GAlgebra R 𝒜
inst✝ : DirectSum.GAlgebra R ℬ
x y : DirectSum ι 𝒜 ⊗[R] DirectSum ι ℬ
i₁ : ι
a₁ : 𝒜 i₁
j₁ : ι
b₁ : ℬ j₁
i₂ : ι
a₂ : 𝒜 i₂
j₂ : ι
b₂ : ℬ j₂
⊢ (-1) ^ (j₁ * i₂ + (j₁ * i₁ + j₂ * i₁ + (j₁ * i₂ + j₂ * i₂))) = (-1) ^ (j₂ * i₂ + (j₁ * i₁ + j₂ * i₁))

Tactic:
abel_nf

Result:
case a.H.h.H.h.a.H.h.H.h.e_a
R : Type u_1
ι : Type u_2
inst✝¹¹ : CommSemiring ι
inst✝¹⁰ : Module ι (Additive ℤˣ)
inst✝⁹ : DecidableEq ι
𝒜 : ι → Type u_3
ℬ : ι → Type u_4
inst✝⁸ : CommRing R
inst✝⁷ : (i : ι) → AddCommGroup (𝒜 i)
inst✝⁶ : (i : ι) → AddCommGroup (ℬ i)
inst✝⁵ : (i : ι) → Module R (𝒜 i)
inst✝⁴ : (i : ι) → Module R (ℬ i)
inst✝³ : DirectSum.GRing 𝒜
inst✝² : DirectSum.GRing ℬ
inst✝¹ : DirectSum.GAlgebra R 𝒜
inst✝ : DirectSum.GAlgebra R ℬ
x y : DirectSum ι 𝒜 ⊗[R] DirectSum ι ℬ
i₁ : ι
a₁ : 𝒜 i₁
j₁ : ι
b₁ : ℬ j₁
i₂ : ι
a₂ : 𝒜 i₂
j₂ : ι
b₂ : ℬ j₂
⊢ (-1) ^ (2 • (j₁ * i₂) + (j₁ * i₁ + (j₂ * i₁ + j₂ * i₂))) = (-1) ^ (j₁ * i₁ + (j₂ * i₁ + j₂ * i₂))

Proof state:
R : Type u_1
ι : Type u_2
inst✝¹¹ : CommSemiring ι
inst✝¹⁰ : Module ι (Additive ℤˣ)
inst✝⁹ : DecidableEq ι
𝒜 : ι → Type u_3
ℬ : ι → Type u_4
inst✝⁸ : CommRing R
inst✝⁷ : (i : ι) → AddCommGroup (𝒜 i)
inst✝⁶ : (i : ι) → AddCommGroup (ℬ i)
inst✝⁵ : (i : ι) → Module R (𝒜 i)
inst✝⁴ : (i : ι) → Module R (ℬ i)
inst✝³ : DirectSum.GRing 𝒜
inst✝² : DirectSum.GRing ℬ
inst✝¹ : DirectSum.GAlgebra R 𝒜
inst✝ : DirectSum.GAlgebra R ℬ
x y : DirectSum ι 𝒜 ⊗[R] DirectSum ι ℬ
⊢ (gradedComm R 𝒜 ℬ) (((gradedMul R 𝒜 ℬ) x) y) = ((gradedMul R ℬ 𝒜) ((gradedComm R 𝒜 ℬ) x)) ((gradedComm R 𝒜 ℬ) y)

Tactic:
suffices (gradedMul R 𝒜 ℬ).compr₂ (gradedComm R 𝒜 ℬ).toLinearMap
    = (gradedMul R ℬ 𝒜 ∘ₗ (gradedComm R 𝒜 ℬ).toLinearMap).compl₂
      (gradedComm R 𝒜 ℬ).toLinearMap from
  LinearMap.congr_fun₂ this x y

Result:
R : Type u_1
ι : Type u_2
inst✝¹¹ : CommSemiring ι
inst✝¹⁰ : Module ι (Additive ℤˣ)
inst✝⁹ : DecidableEq ι
𝒜 : ι → Type u_3
ℬ : ι → Type u_4
inst✝⁸ : CommRing R
inst✝⁷ : (i : ι) → AddCommGroup (𝒜 i)
inst✝⁶ : (i : ι) → AddCommGroup (ℬ i)
inst✝⁵ : (i : ι) → Module R (𝒜 i)
inst✝⁴ : (i : ι) → Module R (ℬ i)
inst✝³ : DirectSum.GRing 𝒜
inst✝² : DirectSum.GRing ℬ
inst✝¹ : DirectSum.GAlgebra R 𝒜
inst✝ : DirectSum.GAlgebra R ℬ
x y : DirectSum ι 𝒜 ⊗[R] DirectSum ι ℬ
⊢ (gradedMul R 𝒜 ℬ).compr₂ ↑(gradedComm R 𝒜 ℬ) = (gradedMul R ℬ 𝒜 ∘ₗ ↑(gradedComm R 𝒜 ℬ)).compl₂ ↑(gradedComm R 𝒜 ℬ)
-- Mathlib/LinearAlgebra/TensorProduct/Basic.lean
theorem rTensor_zpow (f : M ≃ₗ[R] M) (n : ℤ) : f.rTensor N ^ n = (f ^ n).rTensor N

Proof state:
R : Type u_1
inst✝⁴ : CommSemiring R
M : Type u_5
N : Type u_6
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid N
inst✝¹ : Module R M
inst✝ : Module R N
f : M ≃ₗ[R] M
n : ℤ
⊢ rTensor N f ^ n = rTensor N (f ^ n)

Tactic:
simpa only [one_zpow] using TensorProduct.congr_zpow f (1 : N ≃ₗ[R] N) n

Result:
no goals
-- Mathlib/Algebra/Module/DedekindDomain.lean
theorem isInternal_prime_power_torsion_of_is_torsion_by_ideal [DecidableEq (Ideal R)]
    {I : Ideal R} (hI : I ≠ ⊥) (hM : Module.IsTorsionBySet R M I) :
    DirectSum.IsInternal fun p : (factors I).toFinset =>
      torsionBySet R M (p ^ (factors I).count ↑p : Ideal R)

Proof state:
R : Type u
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
M : Type v
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : IsDedekindDomain R
inst✝ : DecidableEq (Ideal R)
I : Ideal R
hI : I ≠ ⊥
hM : Module.IsTorsionBySet R M ↑I
P : Multiset (Ideal R) := factors I
⊢ DirectSum.IsInternal fun p => torsionBySet R M ↑(↑p ^ Multiset.count (↑p) (factors I))

Tactic:
have prime_of_mem := fun p (hp : p ∈ P.toFinset) =>
  prime_of_factor p (Multiset.mem_toFinset.mp hp)

Result:
R : Type u
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
M : Type v
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : IsDedekindDomain R
inst✝ : DecidableEq (Ideal R)
I : Ideal R
hI : I ≠ ⊥
hM : Module.IsTorsionBySet R M ↑I
P : Multiset (Ideal R) := factors I
prime_of_mem : ∀ p ∈ P.toFinset, Prime p
⊢ DirectSum.IsInternal fun p => torsionBySet R M ↑(↑p ^ Multiset.count (↑p) (factors I))

Proof state:
R : Type u
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
M : Type v
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : IsDedekindDomain R
inst✝ : DecidableEq (Ideal R)
I : Ideal R
hI : I ≠ ⊥
hM : Module.IsTorsionBySet R M ↑I
P : Multiset (Ideal R) := factors I
prime_of_mem : ∀ p ∈ P.toFinset, Prime p
p : Ideal R
hp : p ∈ ↑(factors I).toFinset
q : Ideal R
hq : q ∈ ↑(factors I).toFinset
pq : p ≠ q
⊢ p ^ (Multiset.count p (normalizedFactors (q ^ Multiset.count q P)) ⊓ Multiset.count p P) = ⊤

Tactic:
suffices (normalizedFactors _).count p = 0 by rw [this, zero_min, pow_zero, Ideal.one_eq_top]

Result:
R : Type u
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
M : Type v
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : IsDedekindDomain R
inst✝ : DecidableEq (Ideal R)
I : Ideal R
hI : I ≠ ⊥
hM : Module.IsTorsionBySet R M ↑I
P : Multiset (Ideal R) := factors I
prime_of_mem : ∀ p ∈ P.toFinset, Prime p
p : Ideal R
hp : p ∈ ↑(factors I).toFinset
q : Ideal R
hq : q ∈ ↑(factors I).toFinset
pq : p ≠ q
⊢ Multiset.count p (normalizedFactors (q ^ Multiset.count q P)) = 0
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Nat/Lemmas.lean
theorem shiftLeft_succ : ∀(m n), m <<< (n + 1) = 2 * (m <<< n)
| _, 0 => rfl
| _, k + 1 => by
  rw [shiftLeft_succ_inside _ (k+1)]
  rw [shiftLeft_succ _ k, shiftLeft_succ_inside]

Proof state:
x✝ k : Nat
⊢ (2 * x✝) <<< (k + 1) = 2 * x✝ <<< (k + 1)

Tactic:
rw [shiftLeft_succ _ k, shiftLeft_succ_inside]

Result:
no goals

Proof state:
x✝ k : Nat
⊢ x✝ <<< (k + 1 + 1) = 2 * x✝ <<< (k + 1)

Tactic:
rw [shiftLeft_succ_inside _ (k+1)]

Result:
x✝ k : Nat
⊢ (2 * x✝) <<< (k + 1) = 2 * x✝ <<< (k + 1)
-- Mathlib/LinearAlgebra/Finsupp/Supported.lean
theorem disjoint_supported_supported {s t : Set α} (h : Disjoint s t) :
    Disjoint (supported M R s) (supported M R t) :=
  disjoint_iff.2 <| by rw [← supported_inter, disjoint_iff_inter_eq_empty.1 h, supported_empty]

Proof state:
α : Type u_1
M : Type u_2
R : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s t : Set α
h : Disjoint s t
⊢ supported M R s ⊓ supported M R t = ⊥

Tactic:
rw [← supported_inter, disjoint_iff_inter_eq_empty.1 h, supported_empty]

Result:
no goals
-- Mathlib/GroupTheory/Index.lean
@[to_additive (attr := simp)]
lemma index_prod (H : Subgroup G) (K : Subgroup G') : (H.prod K).index = H.index * K.index

Proof state:
G : Type u_1
G' : Type u_2
inst✝¹ : Group G
inst✝ : Group G'
H : Subgroup G
K : Subgroup G'
x y : G × G'
⊢ (QuotientGroup.leftRel (H.prod K)) x y ↔ ((QuotientGroup.leftRel H).prod (QuotientGroup.leftRel K)) x y

Tactic:
rw [QuotientGroup.leftRel_prod]

Result:
no goals

Proof state:
G : Type u_1
G' : Type u_2
inst✝¹ : Group G
inst✝ : Group G'
H : Subgroup G
K : Subgroup G'
⊢ Nat.card ((G × G') ⧸ H.prod K) = Nat.card ((G ⧸ H) × G' ⧸ K)

Tactic:
refine Nat.card_congr
  ((Quotient.congrRight (fun x y ↦ ?_)).trans (Setoid.prodQuotientEquiv _ _).symm)

Result:
G : Type u_1
G' : Type u_2
inst✝¹ : Group G
inst✝ : Group G'
H : Subgroup G
K : Subgroup G'
x y : G × G'
⊢ (QuotientGroup.leftRel (H.prod K)) x y ↔ ((QuotientGroup.leftRel H).prod (QuotientGroup.leftRel K)) x y

Proof state:
G : Type u_1
G' : Type u_2
inst✝¹ : Group G
inst✝ : Group G'
H : Subgroup G
K : Subgroup G'
⊢ (H.prod K).index = H.index * K.index

Tactic:
simp_rw [index, ← Nat.card_prod]

Result:
G : Type u_1
G' : Type u_2
inst✝¹ : Group G
inst✝ : Group G'
H : Subgroup G
K : Subgroup G'
⊢ Nat.card ((G × G') ⧸ H.prod K) = Nat.card ((G ⧸ H) × G' ⧸ K)
-- Mathlib/Data/Matroid/Closure.lean
lemma Indep.isBasis_closure (hI : M.Indep I) : M.IsBasis I (M.closure I)

Proof state:
α : Type u_2
M : Matroid α
I : Set α
hI : M.Indep I
⊢ M.IsBasis I (M.closure I)

Tactic:
rw [hI.closure_eq_setOf_isBasis_insert]

Result:
α : Type u_2
M : Matroid α
I : Set α
hI : M.Indep I
⊢ M.IsBasis I {x | M.IsBasis I (insert x I)}

Proof state:
α : Type u_2
M : Matroid α
I : Set α
hI : M.Indep I
⊢ M.IsBasis I {x | M.IsBasis I (insert x I)}

Tactic:
exact hI.isBasis_setOf_insert_isBasis

Result:
no goals
-- Mathlib/Topology/Order/OrderClosed.lean
theorem PredOrder.nhdsGT_eq_nhdsNE [PredOrder α] (a : α) : 𝓝[>] a = 𝓝[≠] a

Proof state:
α : Type u
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : ClosedIicTopology α
inst✝ : PredOrder α
a : α
⊢ 𝓝[>] a = 𝓝[≠] a

Tactic:
rw [← nhdsLT_sup_nhdsGT, PredOrder.nhdsLT, bot_sup_eq]

Result:
no goals
-- Mathlib/MeasureTheory/Measure/WithDensity.lean
lemma withDensity_inv_same₀ {μ : Measure α} {f : α → ℝ≥0∞}
    (hf : AEMeasurable f μ) (hf_ne_zero : ∀ᵐ x ∂μ, f x ≠ 0) (hf_ne_top : ∀ᵐ x ∂μ, f x ≠ ∞) :
    (μ.withDensity f).withDensity (fun x ↦ (f x)⁻¹) = μ

Proof state:
case h
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : AEMeasurable f μ
hf_ne_zero✝ : ∀ᵐ (x : α) ∂μ, f x ≠ 0
hf_ne_top✝ : ∀ᵐ (x : α) ∂μ, f x ≠ ⊤
x : α
hf_ne_zero : f x ≠ 0
hf_ne_top : f x ≠ ⊤
⊢ f x * (f x)⁻¹ = 1 x

Tactic:
rw [ENNReal.mul_inv_cancel hf_ne_zero hf_ne_top, Pi.one_apply]

Result:
no goals

Proof state:
case h
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : AEMeasurable f μ
hf_ne_zero✝ : ∀ᵐ (x : α) ∂μ, f x ≠ 0
hf_ne_top✝ : ∀ᵐ (x : α) ∂μ, f x ≠ ⊤
x : α
hf_ne_zero : f x ≠ 0
hf_ne_top : f x ≠ ⊤
⊢ (f * fun x => (f x)⁻¹) x = 1 x

Tactic:
simp only [Pi.mul_apply]

Result:
case h
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : AEMeasurable f μ
hf_ne_zero✝ : ∀ᵐ (x : α) ∂μ, f x ≠ 0
hf_ne_top✝ : ∀ᵐ (x : α) ∂μ, f x ≠ ⊤
x : α
hf_ne_zero : f x ≠ 0
hf_ne_top : f x ≠ ⊤
⊢ f x * (f x)⁻¹ = 1 x

Proof state:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : AEMeasurable f μ
hf_ne_zero : ∀ᵐ (x : α) ∂μ, f x ≠ 0
hf_ne_top : ∀ᵐ (x : α) ∂μ, f x ≠ ⊤
⊢ (f * fun x => (f x)⁻¹) =ᶠ[ae μ] 1

Tactic:
filter_upwards [hf_ne_zero, hf_ne_top] with x hf_ne_zero hf_ne_top

Result:
case h
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : AEMeasurable f μ
hf_ne_zero✝ : ∀ᵐ (x : α) ∂μ, f x ≠ 0
hf_ne_top✝ : ∀ᵐ (x : α) ∂μ, f x ≠ ⊤
x : α
hf_ne_zero : f x ≠ 0
hf_ne_top : f x ≠ ⊤
⊢ (f * fun x => (f x)⁻¹) x = 1 x

Proof state:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : AEMeasurable f μ
hf_ne_zero : ∀ᵐ (x : α) ∂μ, f x ≠ 0
hf_ne_top : ∀ᵐ (x : α) ∂μ, f x ≠ ⊤
⊢ ((μ.withDensity f).withDensity fun x => (f x)⁻¹) = μ

Tactic:
rw [← withDensity_mul₀ hf hf.inv]

Result:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : AEMeasurable f μ
hf_ne_zero : ∀ᵐ (x : α) ∂μ, f x ≠ 0
hf_ne_top : ∀ᵐ (x : α) ∂μ, f x ≠ ⊤
⊢ μ.withDensity (f * fun x => (f x)⁻¹) = μ

Proof state:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : AEMeasurable f μ
hf_ne_zero : ∀ᵐ (x : α) ∂μ, f x ≠ 0
hf_ne_top : ∀ᵐ (x : α) ∂μ, f x ≠ ⊤
⊢ μ.withDensity (f * fun x => (f x)⁻¹) = μ

Tactic:
suffices (f * fun x ↦ (f x)⁻¹) =ᵐ[μ] 1 by
  rw [withDensity_congr_ae this, withDensity_one]

Result:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : AEMeasurable f μ
hf_ne_zero : ∀ᵐ (x : α) ∂μ, f x ≠ 0
hf_ne_top : ∀ᵐ (x : α) ∂μ, f x ≠ ⊤
⊢ (f * fun x => (f x)⁻¹) =ᶠ[ae μ] 1

Proof state:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : AEMeasurable f μ
hf_ne_zero : ∀ᵐ (x : α) ∂μ, f x ≠ 0
hf_ne_top : ∀ᵐ (x : α) ∂μ, f x ≠ ⊤
this : (f * fun x => (f x)⁻¹) =ᶠ[ae μ] 1
⊢ μ.withDensity (f * fun x => (f x)⁻¹) = μ

Tactic:
rw [withDensity_congr_ae this, withDensity_one]

Result:
no goals
-- Mathlib/Algebra/Order/Monoid/Unbundled/Basic.lean
theorem one_lt_of_lt_mul_right [MulLeftReflectLT α] {a b : α} (h : a < a * b) :
    1 < b :=
  lt_of_mul_lt_mul_left' (a := a) <| by simpa only [mul_one]

Proof state:
α : Type u_1
inst✝² : MulOneClass α
inst✝¹ : LT α
inst✝ : MulLeftReflectLT α
a b : α
h : a < a * b
⊢ a * 1 < a * b

Tactic:
simpa only [mul_one]

Result:
no goals
-- Mathlib/Data/Sym/Basic.lean
theorem eq_replicate_iff : s = replicate n a ↔ ∀ b ∈ s, b = a

Proof state:
α : Type u_1
n : ℕ
s : Sym α n
a : α
⊢ ((↑s).card = n ∧ ∀ b ∈ ↑s, b = a) ↔ ∀ b ∈ s, b = a

Tactic:
exact and_iff_right s.2

Result:
no goals

Proof state:
α : Type u_1
n : ℕ
s : Sym α n
a : α
⊢ s = replicate n a ↔ ∀ b ∈ s, b = a

Tactic:
erw [Subtype.ext_iff, Multiset.eq_replicate]

Result:
α : Type u_1
n : ℕ
s : Sym α n
a : α
⊢ ((↑s).card = n ∧ ∀ b ∈ ↑s, b = a) ↔ ∀ b ∈ s, b = a