harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/RingTheory/RootsOfUnity/Basic.lean
theorem card_rootsOfUnity : Fintype.card (rootsOfUnity k R) ≤ k

Proof state:
R : Type u_4
k : ℕ
inst✝² : NeZero k
inst✝¹ : CommRing R
inst✝ : IsDomain R
⊢ Fintype.card ↥(rootsOfUnity k R) ≤ k

Tactic:
calc
  Fintype.card (rootsOfUnity k R) = Fintype.card { x // x ∈ nthRoots k (1 : R) } :=
    Fintype.card_congr (rootsOfUnityEquivNthRoots R k)
  _ ≤ Multiset.card (nthRoots k (1 : R)).attach := Multiset.card_le_card (Multiset.dedup_le _)
  _ = Multiset.card (nthRoots k (1 : R)) := Multiset.card_attach
  _ ≤ k := card_nthRoots k 1

Result:
no goals

Proof state:
R : Type u_4
k : ℕ
inst✝² : NeZero k
inst✝¹ : CommRing R
inst✝ : IsDomain R
⊢ Fintype.card ↥(rootsOfUnity k R) ≤ k

Tactic:
classical
calc
  Fintype.card (rootsOfUnity k R) = Fintype.card { x // x ∈ nthRoots k (1 : R) } :=
    Fintype.card_congr (rootsOfUnityEquivNthRoots R k)
  _ ≤ Multiset.card (nthRoots k (1 : R)).attach := Multiset.card_le_card (Multiset.dedup_le _)
  _ = Multiset.card (nthRoots k (1 : R)) := Multiset.card_attach
  _ ≤ k := card_nthRoots k 1

Result:
no goals
-- Mathlib/Data/Set/Function.lean
theorem preimage_invFun_of_mem [n : Nonempty α] {f : α → β} (hf : Injective f) {s : Set α}
    (h : Classical.choice n ∈ s) : invFun f ⁻¹' s = f '' s ∪ (range f)ᶜ

Proof state:
case h.inr
α : Type u_1
β : Type u_2
n : Nonempty α
f : α → β
hf : Injective f
s : Set α
h : Classical.choice n ∈ s
x : β
hx : x ∉ range f
⊢ x ∈ invFun f ⁻¹' s ↔ x ∈ f '' s ∪ (range f)ᶜ

Tactic:
simp only [mem_preimage, invFun_neg hx, h, hx, mem_union, mem_compl_iff, not_false_iff, or_true]

Result:
no goals

Proof state:
case h
α : Type u_1
β : Type u_2
n : Nonempty α
f : α → β
hf : Injective f
s : Set α
h : Classical.choice n ∈ s
x : β
⊢ x ∈ invFun f ⁻¹' s ↔ x ∈ f '' s ∪ (range f)ᶜ

Tactic:
rcases em (x ∈ range f) with (⟨a, rfl⟩ | hx)

Result:
case h.inl.intro
α : Type u_1
β : Type u_2
n : Nonempty α
f : α → β
hf : Injective f
s : Set α
h : Classical.choice n ∈ s
a : α
⊢ f a ∈ invFun f ⁻¹' s ↔ f a ∈ f '' s ∪ (range f)ᶜ

case h.inr
α : Type u_1
β : Type u_2
n : Nonempty α
f : α → β
hf : Injective f
s : Set α
h : Classical.choice n ∈ s
x : β
hx : x ∉ range f
⊢ x ∈ invFun f ⁻¹' s ↔ x ∈ f '' s ∪ (range f)ᶜ

Proof state:
α : Type u_1
β : Type u_2
n : Nonempty α
f : α → β
hf : Injective f
s : Set α
h : Classical.choice n ∈ s
⊢ invFun f ⁻¹' s = f '' s ∪ (range f)ᶜ

Tactic:
ext x

Result:
case h
α : Type u_1
β : Type u_2
n : Nonempty α
f : α → β
hf : Injective f
s : Set α
h : Classical.choice n ∈ s
x : β
⊢ x ∈ invFun f ⁻¹' s ↔ x ∈ f '' s ∪ (range f)ᶜ

Proof state:
case h.inl.intro
α : Type u_1
β : Type u_2
n : Nonempty α
f : α → β
hf : Injective f
s : Set α
h : Classical.choice n ∈ s
a : α
⊢ f a ∈ invFun f ⁻¹' s ↔ f a ∈ f '' s ∪ (range f)ᶜ

Tactic:
simp only [mem_preimage, mem_union, mem_compl_iff, mem_range_self, not_true, or_false,
  leftInverse_invFun hf _, hf.mem_set_image]

Result:
no goals
-- Mathlib/InformationTheory/KullbackLeibler/Basic.lean
lemma klDiv_eq_integral_klFun :
    klDiv μ ν = if μ ≪ ν ∧ Integrable (llr μ ν) μ
      then ENNReal.ofReal (∫ x, klFun (μ.rnDeriv ν x).toReal ∂ν)
      else ∞

Proof state:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
⊢ (if μ ≪ ν ∧ Integrable (llr μ ν) μ then ENNReal.ofReal (∫ (x : α), llr μ ν x ∂μ + (ν univ).toReal - (μ univ).toReal)
    else ⊤) =
    if μ ≪ ν ∧ Integrable (llr μ ν) μ then ENNReal.ofReal (∫ (x : α), klFun (μ.rnDeriv ν x).toReal ∂ν) else ⊤

Tactic:
exact if_ctx_congr Iff.rfl (fun h ↦ by rw [integral_klFun_rnDeriv h.1 h.2]) fun _ ↦ rfl

Result:
no goals

Proof state:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
⊢ klDiv μ ν = if μ ≪ ν ∧ Integrable (llr μ ν) μ then ENNReal.ofReal (∫ (x : α), klFun (μ.rnDeriv ν x).toReal ∂ν) else ⊤

Tactic:
rw [klDiv_def]

Result:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
⊢ (if μ ≪ ν ∧ Integrable (llr μ ν) μ then ENNReal.ofReal (∫ (x : α), llr μ ν x ∂μ + (ν univ).toReal - (μ univ).toReal)
    else ⊤) =
    if μ ≪ ν ∧ Integrable (llr μ ν) μ then ENNReal.ofReal (∫ (x : α), klFun (μ.rnDeriv ν x).toReal ∂ν) else ⊤

Proof state:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
h : μ ≪ ν ∧ Integrable (llr μ ν) μ
⊢ ENNReal.ofReal (∫ (x : α), llr μ ν x ∂μ + (ν univ).toReal - (μ univ).toReal) =
    ENNReal.ofReal (∫ (x : α), klFun (μ.rnDeriv ν x).toReal ∂ν)

Tactic:
rw [integral_klFun_rnDeriv h.1 h.2]

Result:
no goals
-- Mathlib/Algebra/Group/EvenFunction.lean
lemma Even.mul_even (hf : f.Even) (hg : g.Even) : (f * g).Even

Proof state:
α : Type u_1
inst✝¹ : Neg α
R : Type u_3
inst✝ : Mul R
f g : α → R
hf : Function.Even f
hg : Function.Even g
⊢ Function.Even (f * g)

Tactic:
intro a

Result:
α : Type u_1
inst✝¹ : Neg α
R : Type u_3
inst✝ : Mul R
f g : α → R
hf : Function.Even f
hg : Function.Even g
a : α
⊢ (f * g) (-a) = (f * g) a

Proof state:
α : Type u_1
inst✝¹ : Neg α
R : Type u_3
inst✝ : Mul R
f g : α → R
hf : Function.Even f
hg : Function.Even g
a : α
⊢ (f * g) (-a) = (f * g) a

Tactic:
simp only [Pi.mul_apply, hf a, hg a]

Result:
no goals
-- Mathlib/AlgebraicGeometry/Morphisms/Basic.lean
@[ext]
lemma ext {P Q : AffineTargetMorphismProperty}
    (H : ∀ ⦃X Y : Scheme⦄ (f : X ⟶ Y) [IsAffine Y], P f ↔ Q f) : P = Q

Proof state:
P Q : AffineTargetMorphismProperty
H : ∀ ⦃X Y : Scheme⦄ (f : X ⟶ Y) [inst : IsAffine Y], P f ↔ Q f
⊢ P = Q

Tactic:
ext

Result:
case h.h.h.h.a
P Q : AffineTargetMorphismProperty
H : ∀ ⦃X Y : Scheme⦄ (f : X ⟶ Y) [inst : IsAffine Y], P f ↔ Q f
x✝³ x✝² : Scheme
x✝¹ : x✝³ ⟶ x✝²
x✝ : IsAffine x✝²
⊢ P x✝¹ ↔ Q x✝¹

Proof state:
case h.h.h.h.a
P Q : AffineTargetMorphismProperty
H : ∀ ⦃X Y : Scheme⦄ (f : X ⟶ Y) [inst : IsAffine Y], P f ↔ Q f
x✝³ x✝² : Scheme
x✝¹ : x✝³ ⟶ x✝²
x✝ : IsAffine x✝²
⊢ P x✝¹ ↔ Q x✝¹

Tactic:
exact H _

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem getElem_append_right' (l₁ : Array α) {l₂ : Array α} {i : Nat} (hi : i < l₂.size) :
    l₂[i] = (l₁ ++ l₂)[i + l₁.size]'(by simpa [Nat.add_comm] using Nat.add_lt_add_left hi _)

Proof state:
α : Type u_1
l₁ l₂ : Array α
i : Nat
hi : i < l₂.size
⊢ l₂[i] = (l₁ ++ l₂)[i + l₁.size]

Tactic:
rw [getElem_append_right] <;> simp [*, Nat.le_add_left]

Result:
no goals

Proof state:
α : Type ?u.236703
l₁ l₂ : Array α
i : Nat
hi : i < l₂.size
⊢ i + l₁.size < (l₁ ++ l₂).size

Tactic:
simpa [Nat.add_comm] using Nat.add_lt_add_left hi _

Result:
no goals
-- Mathlib/RingTheory/UniqueFactorizationDomain/FactorSet.lean
theorem factors_one [Nontrivial α] : factors (1 : Associates α) = 0

Proof state:
case h
α : Type u_1
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : UniqueFactorizationMonoid α
inst✝ : Nontrivial α
⊢ (factors 1).prod = FactorSet.prod 0

Tactic:
rw [Associates.factors_prod]

Result:
case h
α : Type u_1
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : UniqueFactorizationMonoid α
inst✝ : Nontrivial α
⊢ 1 = FactorSet.prod 0

Proof state:
α : Type u_1
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : UniqueFactorizationMonoid α
inst✝ : Nontrivial α
⊢ factors 1 = 0

Tactic:
apply eq_of_prod_eq_prod

Result:
case h
α : Type u_1
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : UniqueFactorizationMonoid α
inst✝ : Nontrivial α
⊢ (factors 1).prod = FactorSet.prod 0

Proof state:
case h
α : Type u_1
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : UniqueFactorizationMonoid α
inst✝ : Nontrivial α
⊢ 1 = FactorSet.prod 0

Tactic:
exact Multiset.prod_zero

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem extract_size (as : Array α) : as.extract 0 as.size = as

Proof state:
case h₂.e_i
α : Type u_1
as : Array α
i✝ : Nat
hi₁✝ : i✝ < as.extract.size
hi₂✝ : i✝ < as.size
⊢ 0 + i✝ = i✝

Tactic:
rw [Nat.zero_add]

Result:
no goals

Proof state:
case h₂
α : Type u_1
as : Array α
i✝ : Nat
hi₁✝ : i✝ < as.extract.size
hi₂✝ : i✝ < as.size
⊢ as[0 + i✝] = as[i✝]

Tactic:
congr

Result:
case h₂.e_i
α : Type u_1
as : Array α
i✝ : Nat
hi₁✝ : i✝ < as.extract.size
hi₂✝ : i✝ < as.size
⊢ 0 + i✝ = i✝

Proof state:
case h₂
α : Type u_1
as : Array α
i✝ : Nat
hi₁✝ : i✝ < as.extract.size
hi₂✝ : i✝ < as.size
⊢ as.extract[i✝] = as[i✝]

Tactic:
rw [getElem_extract]

Result:
case h₂
α : Type u_1
as : Array α
i✝ : Nat
hi₁✝ : i✝ < as.extract.size
hi₂✝ : i✝ < as.size
⊢ as[0 + i✝] = as[i✝]

Proof state:
case h₂
α : Type u_1
as : Array α
⊢ ∀ (i : Nat) (hi₁ : i < as.extract.size) (hi₂ : i < as.size), as.extract[i] = as[i]

Tactic:
intros

Result:
case h₂
α : Type u_1
as : Array α
i✝ : Nat
hi₁✝ : i✝ < as.extract.size
hi₂✝ : i✝ < as.size
⊢ as.extract[i✝] = as[i✝]

Proof state:
case h₁
α : Type u_1
as : Array α
⊢ as.extract.size = as.size

Tactic:
rw [size_extract, Nat.min_self, Nat.sub_zero]

Result:
no goals

Proof state:
α : Type u_1
as : Array α
⊢ as.extract = as

Tactic:
apply ext

Result:
case h₁
α : Type u_1
as : Array α
⊢ as.extract.size = as.size

case h₂
α : Type u_1
as : Array α
⊢ ∀ (i : Nat) (hi₁ : i < as.extract.size) (hi₂ : i < as.size), as.extract[i] = as[i]
-- Mathlib/NumberTheory/LegendreSymbol/JacobiSymbol.lean
theorem sq_one' {a : ℤ} {b : ℕ} (h : a.gcd b = 1) : J(a ^ 2 | b) = 1

Proof state:
a : ℤ
b : ℕ
h : a.gcd ↑b = 1
⊢ J(a ^ 2 | b) = 1

Tactic:
rw [pow_left, sq_one h]

Result:
no goals
-- Mathlib/LinearAlgebra/AffineSpace/AffineMap.lean
theorem pi_ext_nonempty' [Nonempty ι] (h : ∀ i, f.comp (LinearMap.single _ _ i).toAffineMap =
    g.comp (LinearMap.single _ _ i).toAffineMap) : f = g

Proof state:
k : Type u_2
V2 : Type u_5
P2 : Type u_6
inst✝⁸ : Ring k
inst✝⁷ : AddCommGroup V2
inst✝⁶ : AffineSpace V2 P2
inst✝⁵ : Module k V2
ι : Type u_9
φv : ι → Type u_10
inst✝⁴ : (i : ι) → AddCommGroup (φv i)
inst✝³ : (i : ι) → Module k (φv i)
inst✝² : Finite ι
inst✝¹ : DecidableEq ι
f g : ((i : ι) → φv i) →ᵃ[k] P2
inst✝ : Nonempty ι
h : ∀ (i : ι), f.comp (LinearMap.single k φv i).toAffineMap = g.comp (LinearMap.single k φv i).toAffineMap
⊢ f = g

Tactic:
refine pi_ext_nonempty fun i x => ?_

Result:
k : Type u_2
V2 : Type u_5
P2 : Type u_6
inst✝⁸ : Ring k
inst✝⁷ : AddCommGroup V2
inst✝⁶ : AffineSpace V2 P2
inst✝⁵ : Module k V2
ι : Type u_9
φv : ι → Type u_10
inst✝⁴ : (i : ι) → AddCommGroup (φv i)
inst✝³ : (i : ι) → Module k (φv i)
inst✝² : Finite ι
inst✝¹ : DecidableEq ι
f g : ((i : ι) → φv i) →ᵃ[k] P2
inst✝ : Nonempty ι
h : ∀ (i : ι), f.comp (LinearMap.single k φv i).toAffineMap = g.comp (LinearMap.single k φv i).toAffineMap
i : ι
x : φv i
⊢ f (Pi.single i x) = g (Pi.single i x)

Proof state:
k : Type u_2
V2 : Type u_5
P2 : Type u_6
inst✝⁸ : Ring k
inst✝⁷ : AddCommGroup V2
inst✝⁶ : AffineSpace V2 P2
inst✝⁵ : Module k V2
ι : Type u_9
φv : ι → Type u_10
inst✝⁴ : (i : ι) → AddCommGroup (φv i)
inst✝³ : (i : ι) → Module k (φv i)
inst✝² : Finite ι
inst✝¹ : DecidableEq ι
f g : ((i : ι) → φv i) →ᵃ[k] P2
inst✝ : Nonempty ι
h : ∀ (i : ι), f.comp (LinearMap.single k φv i).toAffineMap = g.comp (LinearMap.single k φv i).toAffineMap
i : ι
x : φv i
⊢ f (Pi.single i x) = g (Pi.single i x)

Tactic:
convert AffineMap.congr_fun (h i) x

Result:
no goals
-- Mathlib/Algebra/Ring/Regular.lean
theorem isRegular_iff_ne_zero' [Nontrivial α] [NonUnitalNonAssocRing α] [NoZeroDivisors α]
    {k : α} : IsRegular k ↔ k ≠ 0 :=
  ⟨fun h => by
    rintro rfl
    exact not_not.mpr h.left not_isLeftRegular_zero, isRegular_of_ne_zero'⟩

Proof state:
α : Type u_1
inst✝² : Nontrivial α
inst✝¹ : NonUnitalNonAssocRing α
inst✝ : NoZeroDivisors α
k : α
h : IsRegular k
⊢ k ≠ 0

Tactic:
rintro rfl

Result:
α : Type u_1
inst✝² : Nontrivial α
inst✝¹ : NonUnitalNonAssocRing α
inst✝ : NoZeroDivisors α
h : IsRegular 0
⊢ False

Proof state:
α : Type u_1
inst✝² : Nontrivial α
inst✝¹ : NonUnitalNonAssocRing α
inst✝ : NoZeroDivisors α
h : IsRegular 0
⊢ False

Tactic:
exact not_not.mpr h.left not_isLeftRegular_zero

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Nat/BEq.lean
theorem beq_eq_decide [BEq α] (a b : List α) :
    (a == b) = if h : a.length = b.length then
      decide (∀ (i : Nat) (h' : i < a.length), a[i] == b[i]'(h ▸ h')) else false

Proof state:
α : Type u_1
inst✝ : BEq α
a b : List α
⊢ (a == b) = if h : a.length = b.length then decide (∀ (i : Nat) (h' : i < a.length), (a[i] == b[i]) = true) else false

Tactic:
simp [BEq.beq, beq_eq_isEqv, isEqv_eq_decide]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem toInt_and (x y : BitVec w) :
    BitVec.toInt (x &&& y) = Int.bmod (BitVec.toNat x &&& BitVec.toNat y) (2^w)

Proof state:
w : Nat
x y : BitVec w
⊢ (if 2 * (x.toNat &&& y.toNat) < 2 ^ w then ↑(x.toNat &&& y.toNat) else ↑(x.toNat &&& y.toNat) - ↑(2 ^ w)) =
    if x.toNat &&& y.toNat < (2 ^ w + 1) / 2 then ↑(x.toNat &&& y.toNat) else ↑(x.toNat &&& y.toNat) - ↑(2 ^ w)

Tactic:
omega

Result:
no goals

Proof state:
w : Nat
x y : BitVec w
⊢ (x &&& y).toInt = (↑(x.toNat &&& y.toNat)).bmod (2 ^ w)

Tactic:
rw_mod_cast [Int.bmod_def, BitVec.toInt, toNat_and, Nat.mod_eq_of_lt
  (Nat.and_lt_two_pow x.toNat (BitVec.isLt y))]

Result:
w : Nat
x y : BitVec w
⊢ (if 2 * (x.toNat &&& y.toNat) < 2 ^ w then ↑(x.toNat &&& y.toNat) else ↑(x.toNat &&& y.toNat) - ↑(2 ^ w)) =
    if x.toNat &&& y.toNat < (2 ^ w + 1) / 2 then ↑(x.toNat &&& y.toNat) else ↑(x.toNat &&& y.toNat) - ↑(2 ^ w)
-- Mathlib/Data/Finset/Basic.lean
theorem filter_insert (a : α) (s : Finset α) :
    filter p (insert a s) = if p a then insert a (filter p s) else filter p s

Proof state:
α : Type u_1
p : α → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidableEq α
a : α
s : Finset α
⊢ filter p (insert a s) = if p a then insert a (filter p s) else filter p s

Tactic:
ext x

Result:
case h
α : Type u_1
p : α → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidableEq α
a : α
s : Finset α
x : α
⊢ x ∈ filter p (insert a s) ↔ x ∈ if p a then insert a (filter p s) else filter p s

Proof state:
case h
α : Type u_1
p : α → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidableEq α
a : α
s : Finset α
x : α
⊢ x ∈ filter p (insert a s) ↔ x ∈ if p a then insert a (filter p s) else filter p s

Tactic:
split_ifs with h <;> by_cases h' : x = a <;> simp [h, h']

Result:
no goals
-- Mathlib/LinearAlgebra/RootSystem/Reduced.lean
@[simp]
lemma pairingIn_two_two_iff :
    P.pairingIn S i j = 2 ∧ P.pairingIn S j i = 2 ↔ i = j

Proof state:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝¹¹ : CommRing R
inst✝¹⁰ : AddCommGroup M
inst✝⁹ : Module R M
inst✝⁸ : AddCommGroup N
inst✝⁷ : Module R N
P : RootPairing ι R M N
S : Type u_5
i j : ι
inst✝⁶ : Finite ι
inst✝⁵ : CharZero R
inst✝⁴ : NoZeroSMulDivisors R M
inst✝³ : LinearOrderedCommRing S
inst✝² : Algebra S R
inst✝¹ : FaithfulSMul S R
inst✝ : P.IsValuedIn S
⊢ P.pairingIn S i j = 2 ∧ P.pairingIn S j i = 2 ↔ i = j

Tactic:
simp only [← P.pairing_two_two_iff, ← P.algebraMap_pairingIn S, ← map_ofNat (algebraMap S R),
  (algebraMap_injective S R).eq_iff]

Result:
no goals
-- Mathlib/Data/Finset/Prod.lean
/-- The product of two Finsets is nontrivial iff both are nonempty
  at least one of them is nontrivial. -/
lemma nontrivial_prod_iff : (s ×ˢ t).Nontrivial ↔
    s.Nonempty ∧ t.Nonempty ∧ (s.Nontrivial ∨ t.Nontrivial)

Proof state:
α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
⊢ 1 < #s * #t ↔ 0 < #s ∧ 0 < #t ∧ (1 < #s ∨ 1 < #t)

Tactic:
apply Nat.one_lt_mul_iff

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
⊢ (s ×ˢ t).Nontrivial ↔ s.Nonempty ∧ t.Nonempty ∧ (s.Nontrivial ∨ t.Nontrivial)

Tactic:
simp_rw [← card_pos, ← one_lt_card_iff_nontrivial, card_product]

Result:
α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
⊢ 1 < #s * #t ↔ 0 < #s ∧ 0 < #t ∧ (1 < #s ∨ 1 < #t)
-- Mathlib/NumberTheory/Padics/PadicNorm.lean
theorem sum_lt' {α : Type*} {F : α → ℚ} {t : ℚ} {s : Finset α}
    (hF : ∀ i ∈ s, padicNorm p (F i) < t) (ht : 0 < t) : padicNorm p (∑ i ∈ s, F i) < t

Proof state:
p : ℕ
hp : Fact (Nat.Prime p)
α : Type u_1
F : α → ℚ
t : ℚ
s : Finset α
hF : ∀ i ∈ s, padicNorm p (F i) < t
ht : 0 < t
⊢ padicNorm p (∑ i ∈ s, F i) < t

Tactic:
obtain rfl | hs := Finset.eq_empty_or_nonempty s

Result:
case inl
p : ℕ
hp : Fact (Nat.Prime p)
α : Type u_1
F : α → ℚ
t : ℚ
ht : 0 < t
hF : ∀ i ∈ ∅, padicNorm p (F i) < t
⊢ padicNorm p (∑ i ∈ ∅, F i) < t

case inr
p : ℕ
hp : Fact (Nat.Prime p)
α : Type u_1
F : α → ℚ
t : ℚ
s : Finset α
hF : ∀ i ∈ s, padicNorm p (F i) < t
ht : 0 < t
hs : s.Nonempty
⊢ padicNorm p (∑ i ∈ s, F i) < t

Proof state:
case inr
p : ℕ
hp : Fact (Nat.Prime p)
α : Type u_1
F : α → ℚ
t : ℚ
s : Finset α
hF : ∀ i ∈ s, padicNorm p (F i) < t
ht : 0 < t
hs : s.Nonempty
⊢ padicNorm p (∑ i ∈ s, F i) < t

Tactic:
exact sum_lt hs hF

Result:
no goals

Proof state:
case inl
p : ℕ
hp : Fact (Nat.Prime p)
α : Type u_1
F : α → ℚ
t : ℚ
ht : 0 < t
hF : ∀ i ∈ ∅, padicNorm p (F i) < t
⊢ padicNorm p (∑ i ∈ ∅, F i) < t

Tactic:
simp [ht]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Bernstein.lean
theorem lt_of_mem_S {f : C(I, ℝ)} {ε : ℝ} {h : 0 < ε} {n : ℕ} {x : I} {k : Fin (n + 1)}
    (m : k ∈ S f ε h n x) : |f k/ₙ - f x| < ε / 2

Proof state:
f : C(↑I, ℝ)
ε : ℝ
h : 0 < ε
n : ℕ
x : ↑I
k : Fin (n + 1)
m : k ∈ S f ε h n x
⊢ |f k/ₙ - f x| < ε / 2

Tactic:
apply f.dist_lt_of_dist_lt_modulus (ε / 2) (half_pos h)

Result:
f : C(↑I, ℝ)
ε : ℝ
h : 0 < ε
n : ℕ
x : ↑I
k : Fin (n + 1)
m : k ∈ S f ε h n x
⊢ dist k/ₙ x < f.modulus (ε / 2) ⋯

Proof state:
f : C(↑I, ℝ)
ε : ℝ
h : 0 < ε
n : ℕ
x : ↑I
k : Fin (n + 1)
m : k ∈ S f ε h n x
⊢ dist k/ₙ x < f.modulus (ε / 2) ⋯

Tactic:
simpa [S, (Set.mem_toFinset)] using m

Result:
no goals
-- Mathlib/LinearAlgebra/Prod.lean
theorem prod_eq_top_iff {p₁ : Submodule R M} {p₂ : Submodule R M₂} :
    p₁.prod p₂ = ⊤ ↔ p₁ = ⊤ ∧ p₂ = ⊤

Proof state:
R : Type u
M : Type v
M₂ : Type w
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R M
inst✝ : Module R M₂
p₁ : Submodule R M
p₂ : Submodule R M₂
⊢ p₁.prod p₂ = ⊤ ↔ p₁ = ⊤ ∧ p₂ = ⊤

Tactic:
simp only [eq_top_iff, le_prod_iff, ← (gc_map_comap _).le_iff_le, map_top, range_fst, range_snd]

Result:
no goals
-- Mathlib/Data/Set/Prod.lean
theorem range_piMap (f : ∀ i, α i → β i) : range (Pi.map f) = pi univ fun i ↦ range (f i)

Proof state:
ι : Type u_1
α : ι → Type u_2
β : ι → Type u_3
f : (i : ι) → α i → β i
⊢ range (Pi.map f) = univ.pi fun i => range (f i)

Tactic:
simp only [← image_univ, ← piMap_image_univ_pi, pi_univ]

Result:
no goals
-- Mathlib/LinearAlgebra/TensorProduct/RightExactness.lean
lemma lTensor.inverse_of_rightInverse_apply
    {h : P → N} (hgh : Function.RightInverse h g) (y : Q ⊗[R] N) :
    (lTensor.inverse_of_rightInverse Q hfg hgh) ((lTensor Q g) y) =
      Submodule.Quotient.mk (p := (LinearMap.range (lTensor Q f))) y

Proof state:
case h.H
R : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
inst✝⁸ : CommRing R
inst✝⁷ : AddCommGroup M
inst✝⁶ : AddCommGroup N
inst✝⁵ : AddCommGroup P
inst✝⁴ : Module R M
inst✝³ : Module R N
inst✝² : Module R P
f : M →ₗ[R] N
g : N →ₗ[R] P
Q : Type u_5
inst✝¹ : AddCommGroup Q
inst✝ : Module R Q
hfg✝ : Exact ⇑f ⇑g
hfg : ker g = range f
h : P → N
hgh : RightInverse h ⇑g
y : Q ⊗[R] N
n : Q
q : N
⊢ Submodule.Quotient.mk (n ⊗ₜ[R] h (g q)) = Submodule.Quotient.mk (n ⊗ₜ[R] q)

Tactic:
rw [Submodule.Quotient.eq, ← TensorProduct.tmul_sub]

Result:
case h.H
R : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
inst✝⁸ : CommRing R
inst✝⁷ : AddCommGroup M
inst✝⁶ : AddCommGroup N
inst✝⁵ : AddCommGroup P
inst✝⁴ : Module R M
inst✝³ : Module R N
inst✝² : Module R P
f : M →ₗ[R] N
g : N →ₗ[R] P
Q : Type u_5
inst✝¹ : AddCommGroup Q
inst✝ : Module R Q
hfg✝ : Exact ⇑f ⇑g
hfg : ker g = range f
h : P → N
hgh : RightInverse h ⇑g
y : Q ⊗[R] N
n : Q
q : N
⊢ n ⊗ₜ[R] (h (g q) - q) ∈ range (lTensor Q f)

Proof state:
case h.H.a
R : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
inst✝⁸ : CommRing R
inst✝⁷ : AddCommGroup M
inst✝⁶ : AddCommGroup N
inst✝⁵ : AddCommGroup P
inst✝⁴ : Module R M
inst✝³ : Module R N
inst✝² : Module R P
f : M →ₗ[R] N
g : N →ₗ[R] P
Q : Type u_5
inst✝¹ : AddCommGroup Q
inst✝ : Module R Q
hfg✝ : Exact ⇑f ⇑g
hfg : ker g = range f
h : P → N
hgh : RightInverse h ⇑g
y : Q ⊗[R] N
n : Q
q : N
⊢ h (g q) - q ∈ range f

Tactic:
rw [← hfg, mem_ker, map_sub, sub_eq_zero, hgh]

Result:
no goals

Proof state:
R : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
inst✝⁸ : CommRing R
inst✝⁷ : AddCommGroup M
inst✝⁶ : AddCommGroup N
inst✝⁵ : AddCommGroup P
inst✝⁴ : Module R M
inst✝³ : Module R N
inst✝² : Module R P
f : M →ₗ[R] N
g : N →ₗ[R] P
Q : Type u_5
inst✝¹ : AddCommGroup Q
inst✝ : Module R Q
hfg : Exact ⇑f ⇑g
h : P → N
hgh : RightInverse h ⇑g
y : Q ⊗[R] N
⊢ (inverse_of_rightInverse Q hfg hgh) ((lTensor Q g) y) = Submodule.Quotient.mk y

Tactic:
simp only [← LinearMap.comp_apply, ← Submodule.mkQ_apply]

Result:
R : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
inst✝⁸ : CommRing R
inst✝⁷ : AddCommGroup M
inst✝⁶ : AddCommGroup N
inst✝⁵ : AddCommGroup P
inst✝⁴ : Module R M
inst✝³ : Module R N
inst✝² : Module R P
f : M →ₗ[R] N
g : N →ₗ[R] P
Q : Type u_5
inst✝¹ : AddCommGroup Q
inst✝ : Module R Q
hfg : Exact ⇑f ⇑g
h : P → N
hgh : RightInverse h ⇑g
y : Q ⊗[R] N
⊢ (inverse_of_rightInverse Q hfg hgh ∘ₗ lTensor Q g) y = (range (lTensor Q f)).mkQ y
-- Mathlib/Combinatorics/SimpleGraph/Subgraph.lean
theorem coe_degree (G' : Subgraph G) (v : G'.verts) [Fintype (G'.coe.neighborSet v)]
    [Fintype (G'.neighborSet v)] : G'.coe.degree v = G'.degree v

Proof state:
V : Type u
G : SimpleGraph V
G' : G.Subgraph
v : ↑G'.verts
inst✝¹ : Fintype ↑(G'.coe.neighborSet v)
inst✝ : Fintype ↑(G'.neighborSet ↑v)
⊢ G'.coe.degree v = G'.degree ↑v

Tactic:
rw [← card_neighborSet_eq_degree]

Result:
V : Type u
G : SimpleGraph V
G' : G.Subgraph
v : ↑G'.verts
inst✝¹ : Fintype ↑(G'.coe.neighborSet v)
inst✝ : Fintype ↑(G'.neighborSet ↑v)
⊢ Fintype.card ↑(G'.coe.neighborSet v) = G'.degree ↑v

Proof state:
V : Type u
G : SimpleGraph V
G' : G.Subgraph
v : ↑G'.verts
inst✝¹ : Fintype ↑(G'.coe.neighborSet v)
inst✝ : Fintype ↑(G'.neighborSet ↑v)
⊢ Fintype.card ↑(G'.coe.neighborSet v) = G'.degree ↑v

Tactic:
exact Fintype.card_congr (coeNeighborSetEquiv v)

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Lemmas.lean
theorem set_append_right {s t : List α} (i : Nat) (x : α) (h : s.length ≤ i) :
    (s ++ t).set i x = s ++ t.set (i - s.length) x

Proof state:
α : Type u_1
s t : List α
i : Nat
x : α
h : s.length ≤ i
⊢ ¬i < s.length

Tactic:
simp_all

Result:
no goals

Proof state:
α : Type u_1
s t : List α
i : Nat
x : α
h : s.length ≤ i
⊢ (s ++ t).set i x = s ++ t.set (i - s.length) x

Tactic:
rw [set_append, if_neg (by simp_all)]

Result:
no goals
-- Mathlib/RingTheory/Nilpotent/Basic.lean
theorem IsNilpotent.isUnit_add_left_of_commute [Ring R] {r u : R}
    (hnil : IsNilpotent r) (hu : IsUnit u) (h_comm : Commute r u) :
    IsUnit (u + r)

Proof state:
R : Type u_1
inst✝ : Ring R
r u : R
hnil : IsNilpotent r
hu : IsUnit u
h_comm : Commute r ↑hu.unit⁻¹
⊢ IsNilpotent (r * ↑hu.unit⁻¹)

Tactic:
exact (hu.unit⁻¹.isUnit.isNilpotent_mul_unit_of_commute_iff h_comm).mpr hnil

Result:
no goals

Proof state:
R : Type u_1
inst✝ : Ring R
r u : R
hnil : IsNilpotent r
hu : IsUnit u
h_comm : Commute r ↑hu.unit⁻¹
⊢ IsUnit (1 + r * ↑hu.unit⁻¹)

Tactic:
refine IsNilpotent.isUnit_one_add ?_

Result:
R : Type u_1
inst✝ : Ring R
r u : R
hnil : IsNilpotent r
hu : IsUnit u
h_comm : Commute r ↑hu.unit⁻¹
⊢ IsNilpotent (r * ↑hu.unit⁻¹)

Proof state:
R : Type u_1
inst✝ : Ring R
r u : R
hnil : IsNilpotent r
hu : IsUnit u
h_comm : Commute r u
⊢ IsUnit (1 + r * ↑hu.unit⁻¹)

Tactic:
replace h_comm : Commute r (↑hu.unit⁻¹) := Commute.units_inv_right h_comm

Result:
R : Type u_1
inst✝ : Ring R
r u : R
hnil : IsNilpotent r
hu : IsUnit u
h_comm : Commute r ↑hu.unit⁻¹
⊢ IsUnit (1 + r * ↑hu.unit⁻¹)

Proof state:
R : Type u_1
inst✝ : Ring R
r u : R
hnil : IsNilpotent r
hu : IsUnit u
h_comm : Commute r u
⊢ IsUnit (u + r)

Tactic:
rw [← Units.isUnit_mul_units _ hu.unit⁻¹, add_mul, IsUnit.mul_val_inv]

Result:
R : Type u_1
inst✝ : Ring R
r u : R
hnil : IsNilpotent r
hu : IsUnit u
h_comm : Commute r u
⊢ IsUnit (1 + r * ↑hu.unit⁻¹)