harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Algebra/GeomSum.lean
theorem geom_sum_pos_iff [LinearOrderedRing α] (hn : n ≠ 0) :
    (0 < ∑ i ∈ range n, x ^ i) ↔ Odd n ∨ 0 < x + 1

Proof state:
case refine_2.inl
α : Type u
n : ℕ
x : α
inst✝ : LinearOrderedRing α
hn✝ : n ≠ 0
hn : Odd n
⊢ 0 < ∑ i ∈ range n, x ^ i

Tactic:
exact hn.geom_sum_pos

Result:
no goals

Proof state:
case refine_2.inr
α : Type u
n : ℕ
x : α
inst✝ : LinearOrderedRing α
hn : n ≠ 0
hx' : 0 < x + 1
⊢ 0 < ∑ i ∈ range n, x ^ i

Tactic:
exact geom_sum_pos' hx' hn

Result:
no goals

Proof state:
case refine_2
α : Type u
n : ℕ
x : α
inst✝ : LinearOrderedRing α
hn : n ≠ 0
⊢ Odd n ∨ 0 < x + 1 → 0 < ∑ i ∈ range n, x ^ i

Tactic:
rintro (hn | hx')

Result:
case refine_2.inl
α : Type u
n : ℕ
x : α
inst✝ : LinearOrderedRing α
hn✝ : n ≠ 0
hn : Odd n
⊢ 0 < ∑ i ∈ range n, x ^ i

case refine_2.inr
α : Type u
n : ℕ
x : α
inst✝ : LinearOrderedRing α
hn : n ≠ 0
hx' : 0 < x + 1
⊢ 0 < ∑ i ∈ range n, x ^ i

Proof state:
case refine_1
α : Type u
n : ℕ
x : α
inst✝ : LinearOrderedRing α
hn : n ≠ 0
h : 0 < ∑ i ∈ range n, x ^ i
⊢ Odd n ∨ 0 < x + 1

Tactic:
rw [or_iff_not_imp_left, ← not_le, Nat.not_odd_iff_even]

Result:
case refine_1
α : Type u
n : ℕ
x : α
inst✝ : LinearOrderedRing α
hn : n ≠ 0
h : 0 < ∑ i ∈ range n, x ^ i
⊢ Even n → ¬x + 1 ≤ 0

Proof state:
case refine_1
α : Type u
n : ℕ
x : α
inst✝ : LinearOrderedRing α
hn✝ : n ≠ 0
h : 0 < ∑ i ∈ range n, x ^ i
hn : Even n
hx : x + 1 ≤ 0
⊢ ∑ i ∈ range n, x ^ i ≤ 0

Tactic:
simpa [if_pos hn] using geom_sum_alternating_of_le_neg_one hx n

Result:
no goals

Proof state:
α : Type u
n : ℕ
x : α
inst✝ : LinearOrderedRing α
hn : n ≠ 0
⊢ 0 < ∑ i ∈ range n, x ^ i ↔ Odd n ∨ 0 < x + 1

Tactic:
refine ⟨fun h => ?_, ?_⟩

Result:
case refine_1
α : Type u
n : ℕ
x : α
inst✝ : LinearOrderedRing α
hn : n ≠ 0
h : 0 < ∑ i ∈ range n, x ^ i
⊢ Odd n ∨ 0 < x + 1

case refine_2
α : Type u
n : ℕ
x : α
inst✝ : LinearOrderedRing α
hn : n ≠ 0
⊢ Odd n ∨ 0 < x + 1 → 0 < ∑ i ∈ range n, x ^ i

Proof state:
case refine_1
α : Type u
n : ℕ
x : α
inst✝ : LinearOrderedRing α
hn : n ≠ 0
h : 0 < ∑ i ∈ range n, x ^ i
⊢ Even n → ¬x + 1 ≤ 0

Tactic:
refine fun hn hx => h.not_le ?_

Result:
case refine_1
α : Type u
n : ℕ
x : α
inst✝ : LinearOrderedRing α
hn✝ : n ≠ 0
h : 0 < ∑ i ∈ range n, x ^ i
hn : Even n
hx : x + 1 ≤ 0
⊢ ∑ i ∈ range n, x ^ i ≤ 0
-- Mathlib/Data/List/NatAntidiagonal.lean
theorem length_antidiagonal (n : ℕ) : (antidiagonal n).length = n + 1

Proof state:
n : ℕ
⊢ (antidiagonal n).length = n + 1

Tactic:
rw [antidiagonal, length_map, length_range]

Result:
no goals
-- Mathlib/CategoryTheory/Preadditive/LeftExact.lean
/-- A functor between preadditive categories preserves all equalizers if it preserves all kernels.
-/
lemma preservesEqualizers_of_preservesKernels
    [∀ {X Y} (f : X ⟶ Y), PreservesLimit (parallelPair f 0) F] :
    PreservesLimitsOfShape WalkingParallelPair F where
  preservesLimit {K}

Proof state:
C : Type u₁
inst✝⁶ : Category.{v₁, u₁} C
inst✝⁵ : Preadditive C
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
inst✝³ : Preadditive D
F : C ⥤ D
inst✝² : F.PreservesZeroMorphisms
inst✝¹ : HasBinaryBiproducts C
inst✝ : ∀ {X Y : C} (f : X ⟶ Y), PreservesLimit (parallelPair f 0) F
K : WalkingParallelPair ⥤ C
⊢ PreservesLimit K F

Tactic:
letI := preservesEqualizer_of_preservesKernels F (K.map WalkingParallelPairHom.left)
    (K.map WalkingParallelPairHom.right)

Result:
C : Type u₁
inst✝⁶ : Category.{v₁, u₁} C
inst✝⁵ : Preadditive C
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
inst✝³ : Preadditive D
F : C ⥤ D
inst✝² : F.PreservesZeroMorphisms
inst✝¹ : HasBinaryBiproducts C
inst✝ : ∀ {X Y : C} (f : X ⟶ Y), PreservesLimit (parallelPair f 0) F
K : WalkingParallelPair ⥤ C
this : PreservesLimit (parallelPair (K.map WalkingParallelPairHom.left) (K.map WalkingParallelPairHom.right)) F :=
  preservesEqualizer_of_preservesKernels F (K.map WalkingParallelPairHom.left) (K.map WalkingParallelPairHom.right)
⊢ PreservesLimit K F

Proof state:
C : Type u₁
inst✝⁶ : Category.{v₁, u₁} C
inst✝⁵ : Preadditive C
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
inst✝³ : Preadditive D
F : C ⥤ D
inst✝² : F.PreservesZeroMorphisms
inst✝¹ : HasBinaryBiproducts C
inst✝ : ∀ {X Y : C} (f : X ⟶ Y), PreservesLimit (parallelPair f 0) F
K : WalkingParallelPair ⥤ C
this : PreservesLimit (parallelPair (K.map WalkingParallelPairHom.left) (K.map WalkingParallelPairHom.right)) F :=
  preservesEqualizer_of_preservesKernels F (K.map WalkingParallelPairHom.left) (K.map WalkingParallelPairHom.right)
⊢ PreservesLimit K F

Tactic:
apply preservesLimit_of_iso_diagram F (diagramIsoParallelPair K).symm

Result:
no goals
-- Mathlib/Topology/Order/Monotone.lean
theorem Monotone.map_iSup_of_continuousAt {ι : Sort*} {f : α → β} {g : ι → α}
    (Cf : ContinuousAt f (iSup g)) (Mf : Monotone f) (fbot : f ⊥ = ⊥) :
    f (⨆ i, g i) = ⨆ i, f (g i)

Proof state:
α : Type u_1
β : Type u_2
inst✝⁵ : CompleteLinearOrder α
inst✝⁴ : TopologicalSpace α
inst✝³ : OrderTopology α
inst✝² : CompleteLinearOrder β
inst✝¹ : TopologicalSpace β
inst✝ : OrderClosedTopology β
ι : Sort u_3
f : α → β
g : ι → α
Cf : ContinuousAt f (iSup g)
Mf : Monotone f
fbot : f ⊥ = ⊥
⊢ f (⨆ i, g i) = ⨆ i, f (g i)

Tactic:
rw [iSup, Mf.map_sSup_of_continuousAt Cf fbot, ← range_comp, iSup, comp_def]

Result:
no goals
-- Mathlib/MeasureTheory/Measure/Lebesgue/Basic.lean
theorem volume_emetric_closedBall (a : ℝ) (r : ℝ≥0∞) : volume (EMetric.closedBall a r) = 2 * r

Proof state:
a : ℝ
r : ℝ≥0∞
⊢ volume (EMetric.closedBall a r) = 2 * r

Tactic:
rcases eq_or_ne r ∞ with (rfl | hr)

Result:
case inl
a : ℝ
⊢ volume (EMetric.closedBall a ⊤) = 2 * ⊤

case inr
a : ℝ
r : ℝ≥0∞
hr : r ≠ ⊤
⊢ volume (EMetric.closedBall a r) = 2 * r

Proof state:
case inl
a : ℝ
⊢ volume (EMetric.closedBall a ⊤) = 2 * ⊤

Tactic:
rw [EMetric.closedBall_top, volume_univ, two_mul, _root_.top_add]

Result:
no goals

Proof state:
case inr
a : ℝ
r : ℝ≥0∞
hr : r ≠ ⊤
⊢ volume (EMetric.closedBall a r) = 2 * r

Tactic:
lift r to ℝ≥0 using hr

Result:
case inr.intro
a : ℝ
r : ℝ≥0
⊢ volume (EMetric.closedBall a ↑r) = 2 * ↑r

Proof state:
case inr.intro
a : ℝ
r : ℝ≥0
⊢ volume (EMetric.closedBall a ↑r) = 2 * ↑r

Tactic:
rw [Metric.emetric_closedBall_nnreal, volume_closedBall, two_mul, ← NNReal.coe_add,
  ENNReal.ofReal_coe_nnreal, ENNReal.coe_add, two_mul]

Result:
no goals
-- Mathlib/Algebra/Homology/ShortComplex/RightHomology.lean
@[reassoc]
lemma rightHomologyι_descOpcycles_π_eq_zero_of_boundary (x : S.X₃ ⟶ A) (hx : k = S.g ≫ x) :
    S.rightHomologyι ≫ S.descOpcycles k (by rw [hx, S.zero_assoc, zero_comp]) = 0 :=
  RightHomologyData.ι_descQ_eq_zero_of_boundary _ k x hx

Proof state:
C : Type u_1
inst✝² : Category.{?u.258415, u_1} C
inst✝¹ : HasZeroMorphisms C
S S₁ S₂ S₃ : ShortComplex C
h : S.RightHomologyData
A : C
k : S.X₂ ⟶ A
hk : S.f ≫ k = 0
inst✝ : S.HasRightHomology
x : S.X₃ ⟶ A
hx : k = S.g ≫ x
⊢ S.f ≫ k = 0

Tactic:
rw [hx, S.zero_assoc, zero_comp]

Result:
no goals
-- Mathlib/Order/DirectedInverseSystem.lean
theorem globalEquiv_naturality ⦃i j⦄ (h : i ≤ j) (x : F j) :
    letI e := globalEquiv equivSucc equivLim
    e i (f h x) = piLTProj h (e j x)

Proof state:
ι : Type u_6
F : ι → Type u_7
X : ι → Type u_8
inst✝³ : LinearOrder ι
f : ⦃i j : ι⦄ → i ≤ j → F j → F i
inst✝² : WellFoundedLT ι
inst✝¹ : SuccOrder ι
inst✝ : InverseSystem f
equivSucc : (i : ι) → ¬IsMax i → { e // ∀ (x : F i⁺), (e x).1 = f ⋯ x }
equivLim : (i : ι) → IsSuccPrelimit i → { e // ∀ (x : F i) (l : ↑(Iio i)), ↑(e x) l = f ⋯ x }
i j : ι
h : i ≤ j
x : F j
⊢ globalEquiv equivSucc equivLim i = (InverseSystem.globalEquivAux equivSucc equivLim j).equiv ⟨i, h⟩

Tactic:
exact pEquivOn_apply_eq ((isLowerSet_Iic _).inter <| isLowerSet_Iic _)

Result:
no goals

Proof state:
ι : Type u_6
F : ι → Type u_7
X : ι → Type u_8
inst✝³ : LinearOrder ι
f : ⦃i j : ι⦄ → i ≤ j → F j → F i
inst✝² : WellFoundedLT ι
inst✝¹ : SuccOrder ι
inst✝ : InverseSystem f
equivSucc : (i : ι) → ¬IsMax i → { e // ∀ (x : F i⁺), (e x).1 = f ⋯ x }
equivLim : (i : ι) → IsSuccPrelimit i → { e // ∀ (x : F i) (l : ↑(Iio i)), ↑(e x) l = f ⋯ x }
i j : ι
h : i ≤ j
x : F j
⊢ (globalEquiv equivSucc equivLim i) (f h x) = piLTProj h ((globalEquiv equivSucc equivLim j) x)

Tactic:
refine (DFunLike.congr_fun ?_ _).trans ((globalEquivAux equivSucc equivLim j).nat le_rfl h h x)

Result:
ι : Type u_6
F : ι → Type u_7
X : ι → Type u_8
inst✝³ : LinearOrder ι
f : ⦃i j : ι⦄ → i ≤ j → F j → F i
inst✝² : WellFoundedLT ι
inst✝¹ : SuccOrder ι
inst✝ : InverseSystem f
equivSucc : (i : ι) → ¬IsMax i → { e // ∀ (x : F i⁺), (e x).1 = f ⋯ x }
equivLim : (i : ι) → IsSuccPrelimit i → { e // ∀ (x : F i) (l : ↑(Iio i)), ↑(e x) l = f ⋯ x }
i j : ι
h : i ≤ j
x : F j
⊢ globalEquiv equivSucc equivLim i = (InverseSystem.globalEquivAux equivSucc equivLim j).equiv ⟨i, h⟩
-- Mathlib/.lake/packages/batteries/Batteries/Data/Nat/Lemmas.lean
theorem recDiagAux_zero_right {motive : Nat → Nat → Sort _}
    (zero_left : ∀ n, motive 0 n) (zero_right : ∀ m, motive m 0)
    (succ_succ : ∀ m n, motive m n → motive (m+1) (n+1)) (m)
    (h : zero_left 0 = zero_right 0

Proof state:
case zero
motive : Nat → Nat → Sort u_1
zero_left : (n : Nat) → motive 0 n
zero_right : (m : Nat) → motive m 0
succ_succ : (m n : Nat) → motive m n → motive (m + 1) (n + 1)
h : autoParam (zero_left 0 = zero_right 0) _auto✝
⊢ Nat.recDiagAux zero_left zero_right succ_succ 0 0 = zero_right 0

case succ
motive : Nat → Nat → Sort u_1
zero_left : (n : Nat) → motive 0 n
zero_right : (m : Nat) → motive m 0
succ_succ : (m n : Nat) → motive m n → motive (m + 1) (n + 1)
h : autoParam (zero_left 0 = zero_right 0) _auto✝
n✝ : Nat
⊢ Nat.recDiagAux zero_left zero_right succ_succ (n✝ + 1) 0 = zero_right (n✝ + 1)

Tactic:
exact h

Result:
case succ
motive : Nat → Nat → Sort u_1
zero_left : (n : Nat) → motive 0 n
zero_right : (m : Nat) → motive m 0
succ_succ : (m n : Nat) → motive m n → motive (m + 1) (n + 1)
h : autoParam (zero_left 0 = zero_right 0) _auto✝
n✝ : Nat
⊢ Nat.recDiagAux zero_left zero_right succ_succ (n✝ + 1) 0 = zero_right (n✝ + 1)

Proof state:
motive : Nat → Nat → Sort u_1
zero_left : (n : Nat) → motive 0 n
zero_right : (m : Nat) → motive m 0
succ_succ : (m n : Nat) → motive m n → motive (m + 1) (n + 1)
m : Nat
h : autoParam (zero_left 0 = zero_right 0) _auto✝
⊢ Nat.recDiagAux zero_left zero_right succ_succ m 0 = zero_right m

Tactic:
cases m

Result:
case zero
motive : Nat → Nat → Sort u_1
zero_left : (n : Nat) → motive 0 n
zero_right : (m : Nat) → motive m 0
succ_succ : (m n : Nat) → motive m n → motive (m + 1) (n + 1)
h : autoParam (zero_left 0 = zero_right 0) _auto✝
⊢ Nat.recDiagAux zero_left zero_right succ_succ 0 0 = zero_right 0

case succ
motive : Nat → Nat → Sort u_1
zero_left : (n : Nat) → motive 0 n
zero_right : (m : Nat) → motive m 0
succ_succ : (m n : Nat) → motive m n → motive (m + 1) (n + 1)
h : autoParam (zero_left 0 = zero_right 0) _auto✝
n✝ : Nat
⊢ Nat.recDiagAux zero_left zero_right succ_succ (n✝ + 1) 0 = zero_right (n✝ + 1)

Proof state:
case succ
motive : Nat → Nat → Sort u_1
zero_left : (n : Nat) → motive 0 n
zero_right : (m : Nat) → motive m 0
succ_succ : (m n : Nat) → motive m n → motive (m + 1) (n + 1)
h : autoParam (zero_left 0 = zero_right 0) _auto✝
n✝ : Nat
⊢ Nat.recDiagAux zero_left zero_right succ_succ (n✝ + 1) 0 = zero_right (n✝ + 1)

Tactic:
rfl

Result:
no goals
-- Mathlib/Algebra/Order/GroupWithZero/Unbundled/Lemmas.lean
lemma mulLeft₀_symm (a : G₀) (ha : 0 < a) : (mulLeft₀ a ha).symm = mulLeft₀ a⁻¹ (inv_pos.2 ha)

Proof state:
case h.h
G₀ : Type u_1
inst✝⁴ : GroupWithZero G₀
inst✝³ : PartialOrder G₀
inst✝² : PosMulMono G₀
inst✝¹ : PosMulReflectLE G₀
inst✝ : ZeroLEOneClass G₀
a : G₀
ha : 0 < a
x✝ : G₀
⊢ (mulLeft₀ a ha).symm x✝ = (mulLeft₀ a⁻¹ ⋯) x✝

Tactic:
rfl

Result:
no goals

Proof state:
G₀ : Type u_1
inst✝⁴ : GroupWithZero G₀
inst✝³ : PartialOrder G₀
inst✝² : PosMulMono G₀
inst✝¹ : PosMulReflectLE G₀
inst✝ : ZeroLEOneClass G₀
a : G₀
ha : 0 < a
⊢ (mulLeft₀ a ha).symm = mulLeft₀ a⁻¹ ⋯

Tactic:
ext

Result:
case h.h
G₀ : Type u_1
inst✝⁴ : GroupWithZero G₀
inst✝³ : PartialOrder G₀
inst✝² : PosMulMono G₀
inst✝¹ : PosMulReflectLE G₀
inst✝ : ZeroLEOneClass G₀
a : G₀
ha : 0 < a
x✝ : G₀
⊢ (mulLeft₀ a ha).symm x✝ = (mulLeft₀ a⁻¹ ⋯) x✝
-- Mathlib/Probability/Independence/Basic.lean
lemma IndepSet_iff (s t : Set Ω) (μ : Measure Ω) :
    IndepSet s t μ ↔ ∀ t1 t2, MeasurableSet[generateFrom {s}] t1
      → MeasurableSet[generateFrom {t}] t2 → μ (t1 ∩ t2) = μ t1 * μ t2

Proof state:
Ω : Type u_1
x✝ : MeasurableSpace Ω
s t : Set Ω
μ : Measure Ω
⊢ IndepSet s t μ ↔ ∀ (t1 t2 : Set Ω), MeasurableSet t1 → MeasurableSet t2 → μ (t1 ∩ t2) = μ t1 * μ t2

Tactic:
simp only [IndepSet_iff_Indep, Indep_iff]

Result:
no goals
-- Mathlib/Algebra/BigOperators/Group/Finset/Basic.lean
@[to_additive]
lemma mulIndicator_biUnion (s : Finset ι) (t : ι → Set κ) {f : κ → β}
    (hs : (s : Set ι).PairwiseDisjoint t) :
    mulIndicator (⋃ i ∈ s, t i) f = fun a ↦ ∏ i ∈ s, mulIndicator (t i) f a

Proof state:
case cons.h
ι : Type u_1
β : Type u_4
inst✝ : CommMonoid β
κ : Type u_7
t : ι → Set κ
f : κ → β
i : ι
s : Finset ι
hi : i ∉ s
ih : (↑s).PairwiseDisjoint t → (⋃ i ∈ s, t i).mulIndicator f = fun a => ∏ i ∈ s, (t i).mulIndicator f a
hs : (↑(cons i s hi)).PairwiseDisjoint t
j : κ
⊢ (⋃ i_1 ∈ cons i s hi, t i_1).mulIndicator f j = ∏ i ∈ cons i s hi, (t i).mulIndicator f j

Tactic:
rw [coe_cons, Set.pairwiseDisjoint_insert_of_not_mem (Finset.mem_coe.not.2 hi)] at hs

Result:
case cons.h
ι : Type u_1
β : Type u_4
inst✝ : CommMonoid β
κ : Type u_7
t : ι → Set κ
f : κ → β
i : ι
s : Finset ι
hi : i ∉ s
ih : (↑s).PairwiseDisjoint t → (⋃ i ∈ s, t i).mulIndicator f = fun a => ∏ i ∈ s, (t i).mulIndicator f a
hs : (↑s).PairwiseDisjoint t ∧ ∀ j ∈ ↑s, Disjoint (t i) (t j)
j : κ
⊢ (⋃ i_1 ∈ cons i s hi, t i_1).mulIndicator f j = ∏ i ∈ cons i s hi, (t i).mulIndicator f j

Proof state:
case cons.h
ι : Type u_1
β : Type u_4
inst✝ : CommMonoid β
κ : Type u_7
t : ι → Set κ
f : κ → β
i : ι
s : Finset ι
hi : i ∉ s
ih : (↑s).PairwiseDisjoint t → (⋃ i ∈ s, t i).mulIndicator f = fun a => ∏ i ∈ s, (t i).mulIndicator f a
hs : (↑s).PairwiseDisjoint t ∧ ∀ j ∈ ↑s, Disjoint (t i) (t j)
j : κ
⊢ (⋃ i_1 ∈ cons i s hi, t i_1).mulIndicator f j = ∏ i ∈ cons i s hi, (t i).mulIndicator f j

Tactic:
rw [prod_cons, cons_eq_insert, set_biUnion_insert, mulIndicator_union_of_not_mem_inter, ih hs.1]

Result:
case cons.h.h
ι : Type u_1
β : Type u_4
inst✝ : CommMonoid β
κ : Type u_7
t : ι → Set κ
f : κ → β
i : ι
s : Finset ι
hi : i ∉ s
ih : (↑s).PairwiseDisjoint t → (⋃ i ∈ s, t i).mulIndicator f = fun a => ∏ i ∈ s, (t i).mulIndicator f a
hs : (↑s).PairwiseDisjoint t ∧ ∀ j ∈ ↑s, Disjoint (t i) (t j)
j : κ
⊢ j ∉ t i ∩ ⋃ x ∈ s, t x

Proof state:
case empty
ι : Type u_1
β : Type u_4
inst✝ : CommMonoid β
κ : Type u_7
t : ι → Set κ
f : κ → β
hs : (↑∅).PairwiseDisjoint t
⊢ (⋃ i ∈ ∅, t i).mulIndicator f = fun a => ∏ i ∈ ∅, (t i).mulIndicator f a

Tactic:
simp

Result:
no goals

Proof state:
case cons
ι : Type u_1
β : Type u_4
inst✝ : CommMonoid β
κ : Type u_7
t : ι → Set κ
f : κ → β
i : ι
s : Finset ι
hi : i ∉ s
ih : (↑s).PairwiseDisjoint t → (⋃ i ∈ s, t i).mulIndicator f = fun a => ∏ i ∈ s, (t i).mulIndicator f a
hs : (↑(cons i s hi)).PairwiseDisjoint t
⊢ (⋃ i_1 ∈ cons i s hi, t i_1).mulIndicator f = fun a => ∏ i ∈ cons i s hi, (t i).mulIndicator f a

Tactic:
ext j

Result:
case cons.h
ι : Type u_1
β : Type u_4
inst✝ : CommMonoid β
κ : Type u_7
t : ι → Set κ
f : κ → β
i : ι
s : Finset ι
hi : i ∉ s
ih : (↑s).PairwiseDisjoint t → (⋃ i ∈ s, t i).mulIndicator f = fun a => ∏ i ∈ s, (t i).mulIndicator f a
hs : (↑(cons i s hi)).PairwiseDisjoint t
j : κ
⊢ (⋃ i_1 ∈ cons i s hi, t i_1).mulIndicator f j = ∏ i ∈ cons i s hi, (t i).mulIndicator f j
-- Mathlib/Algebra/Ring/Parity.lean
lemma Even.neg_one_pow (h : Even n) : (-1 : α) ^ n = 1

Proof state:
α : Type u_2
inst✝¹ : Monoid α
inst✝ : HasDistribNeg α
n : ℕ
h : Even n
⊢ (-1) ^ n = 1

Tactic:
rw [h.neg_pow, one_pow]

Result:
no goals
-- Mathlib/Algebra/GCDMonoid/Basic.lean
theorem lcm_eq_zero_iff [GCDMonoid α] (a b : α) : lcm a b = 0 ↔ a = 0 ∨ b = 0 :=
  Iff.intro
    (fun h : lcm a b = 0 => by
      have : Associated (a * b) 0 := (gcd_mul_lcm a b).symm.trans <| by rw [h, mul_zero]
      rwa [← mul_eq_zero, ← associated_zero_iff_eq_zero])
    (by rintro (rfl | rfl) <;> [apply lcm_zero_left; apply lcm_zero_right])

Proof state:
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : GCDMonoid α
a b : α
⊢ a = 0 ∨ b = 0 → lcm a b = 0

Tactic:
rintro (rfl | rfl) <;> [apply lcm_zero_left; apply lcm_zero_right]

Result:
no goals

Proof state:
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : GCDMonoid α
a b : α
h : lcm a b = 0
⊢ a = 0 ∨ b = 0

Tactic:
have : Associated (a * b) 0 := (gcd_mul_lcm a b).symm.trans <| by rw [h, mul_zero]

Result:
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : GCDMonoid α
a b : α
h : lcm a b = 0
this : Associated (a * b) 0
⊢ a = 0 ∨ b = 0

Proof state:
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : GCDMonoid α
a b : α
h : lcm a b = 0
⊢ Associated (gcd a b * lcm a b) 0

Tactic:
rw [h, mul_zero]

Result:
no goals

Proof state:
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : GCDMonoid α
a b : α
h : lcm a b = 0
this : Associated (a * b) 0
⊢ a = 0 ∨ b = 0

Tactic:
rwa [← mul_eq_zero, ← associated_zero_iff_eq_zero]

Result:
no goals
-- Mathlib/Data/Num/Lemmas.lean
theorem add_to_nat : ∀ m n, ((m + n : PosNum) : ℕ) = m + n
  | 1, b => by rw [one_add b, succ_to_nat, add_comm, cast_one]
  | a, 1 => by rw [add_one a, succ_to_nat, cast_one]
  | bit0 a, bit0 b => (congr_arg (fun n ↦ n + n) (add_to_nat a b)).trans <| add_add_add_comm _ _ _ _
  | bit0 a, bit1 b =>
    (congr_arg (fun n ↦ (n + n) + 1) (add_to_nat a b)).trans <|
      show (a + b + (a + b) + 1 : ℕ) = a + a + (b + b + 1) by simp [add_left_comm]
  | bit1 a, bit0 b =>
    (congr_arg (fun n ↦ (n + n) + 1) (add_to_nat a b)).trans <|
      show (a + b + (a + b) + 1 : ℕ) = a + a + 1 + (b + b) by simp [add_comm, add_left_comm]
  | bit1 a, bit1 b =>
    show (succ (a + b) + succ (a + b) : ℕ) = a + a + 1 + (b + b + 1) by
      rw [succ_to_nat, add_to_nat a b]; simp [add_left_comm]

Proof state:
a b : PosNum
⊢ ↑a + ↑b + 1 + (↑a + ↑b + 1) = ↑a + ↑a + 1 + (↑b + ↑b + 1)

Tactic:
simp [add_left_comm]

Result:
no goals

Proof state:
a b : PosNum
⊢ ↑(a + b).succ + ↑(a + b).succ = ↑a + ↑a + 1 + (↑b + ↑b + 1)

Tactic:
rw [succ_to_nat, add_to_nat a b]

Result:
a b : PosNum
⊢ ↑a + ↑b + 1 + (↑a + ↑b + 1) = ↑a + ↑a + 1 + (↑b + ↑b + 1)

Proof state:
a b : PosNum
⊢ ↑a + ↑b + (↑a + ↑b) + 1 = ↑a + ↑a + (↑b + ↑b + 1)

Tactic:
simp [add_left_comm]

Result:
no goals

Proof state:
b : PosNum
⊢ ↑(1 + b) = ↑1 + ↑b

Tactic:
rw [one_add b, succ_to_nat, add_comm, cast_one]

Result:
no goals

Proof state:
a : PosNum
⊢ ↑(a + 1) = ↑a + ↑1

Tactic:
rw [add_one a, succ_to_nat, cast_one]

Result:
no goals

Proof state:
a b : PosNum
⊢ ↑a + ↑b + (↑a + ↑b) + 1 = ↑a + ↑a + 1 + (↑b + ↑b)

Tactic:
simp [add_comm, add_left_comm]

Result:
no goals
-- Mathlib/NumberTheory/LSeries/Nonvanishing.lean
/-- The logarithms of the Euler factors of a Dirichlet L-series form a summable sequence. -/
lemma summable_neg_log_one_sub_mul_prime_cpow {s : ℂ} (hs : 1 < s.re) :
    Summable fun p : Nat.Primes ↦ -log (1 - χ p * (p : ℂ) ^ (-s))

Proof state:
N : ℕ
χ : DirichletCharacter ℂ N
s : ℂ
hs : 1 < s.re
p : Nat.Primes
⊢ ‖χ ↑↑p * ↑↑p ^ (-s)‖ ≤ ↑↑p ^ (-s).re

Tactic:
simpa only [norm_mul, norm_natCast_cpow_of_re_ne_zero _ <| re_neg_ne_zero_of_one_lt_re hs]
  using mul_le_of_le_one_left (by positivity) (χ.norm_le_one _)

Result:
no goals

Proof state:
N : ℕ
χ : DirichletCharacter ℂ N
s : ℂ
hs : 1 < s.re
this : ∀ (p : Nat.Primes), ‖χ ↑↑p * ↑↑p ^ (-s)‖ ≤ ↑↑p ^ (-s).re
⊢ Summable fun p => -log (1 - χ ↑↑p * ↑↑p ^ (-s))

Tactic:
refine (Nat.Primes.summable_rpow.mpr ?_).of_nonneg_of_le (fun _ ↦ norm_nonneg _) this
  |>.of_norm.clog_one_sub.neg

Result:
N : ℕ
χ : DirichletCharacter ℂ N
s : ℂ
hs : 1 < s.re
this : ∀ (p : Nat.Primes), ‖χ ↑↑p * ↑↑p ^ (-s)‖ ≤ ↑↑p ^ (-s).re
⊢ (-s).re < -1

Proof state:
N : ℕ
χ : DirichletCharacter ℂ N
s : ℂ
hs : 1 < s.re
⊢ Summable fun p => -log (1 - χ ↑↑p * ↑↑p ^ (-s))

Tactic:
have (p : Nat.Primes) : ‖χ p * (p : ℂ) ^ (-s)‖ ≤ (p : ℝ) ^ (-s).re := by
  simpa only [norm_mul, norm_natCast_cpow_of_re_ne_zero _ <| re_neg_ne_zero_of_one_lt_re hs]
    using mul_le_of_le_one_left (by positivity) (χ.norm_le_one _)

Result:
N : ℕ
χ : DirichletCharacter ℂ N
s : ℂ
hs : 1 < s.re
this : ∀ (p : Nat.Primes), ‖χ ↑↑p * ↑↑p ^ (-s)‖ ≤ ↑↑p ^ (-s).re
⊢ Summable fun p => -log (1 - χ ↑↑p * ↑↑p ^ (-s))

Proof state:
N : ℕ
χ : DirichletCharacter ℂ N
s : ℂ
hs : 1 < s.re
this : ∀ (p : Nat.Primes), ‖χ ↑↑p * ↑↑p ^ (-s)‖ ≤ ↑↑p ^ (-s).re
⊢ (-s).re < -1

Tactic:
simp only [neg_re, neg_lt_neg_iff, hs]

Result:
no goals

Proof state:
N : ℕ
χ : DirichletCharacter ℂ N
s : ℂ
hs : 1 < s.re
p : Nat.Primes
⊢ 0 ≤ ↑↑p ^ (-s).re

Tactic:
positivity

Result:
no goals
-- Mathlib/Topology/Category/Profinite/Nobeling.lean
theorem continuous_swapTrue : Continuous (SwapTrue o : (I → Bool) → I → Bool)

Proof state:
I : Type u
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
o : Ordinal.{u}
⊢ Continuous (SwapTrue o)

Tactic:
dsimp (config := { unfoldPartialApp := true }) [SwapTrue]

Result:
I : Type u
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
o : Ordinal.{u}
⊢ Continuous fun f i => if ord I i = o then true else f i

Proof state:
case h.hg
I : Type u
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
o : Ordinal.{u}
i : I
⊢ Continuous (ite (ord I i = o) true)

Tactic:
apply continuous_bot

Result:
no goals

Proof state:
case h
I : Type u
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
o : Ordinal.{u}
⊢ ∀ (i : I), Continuous fun a => if ord I i = o then true else a i

Tactic:
intro i

Result:
case h
I : Type u
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
o : Ordinal.{u}
i : I
⊢ Continuous fun a => if ord I i = o then true else a i

Proof state:
case h.hf
I : Type u
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
o : Ordinal.{u}
i : I
⊢ Continuous fun x => x i

Tactic:
apply continuous_apply

Result:
no goals

Proof state:
I : Type u
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
o : Ordinal.{u}
⊢ Continuous fun f i => if ord I i = o then true else f i

Tactic:
apply continuous_pi

Result:
case h
I : Type u
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
o : Ordinal.{u}
⊢ ∀ (i : I), Continuous fun a => if ord I i = o then true else a i

Proof state:
case h
I : Type u
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
o : Ordinal.{u}
i : I
⊢ Continuous fun a => if ord I i = o then true else a i

Tactic:
apply Continuous.comp'

Result:
case h.hg
I : Type u
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
o : Ordinal.{u}
i : I
⊢ Continuous (ite (ord I i = o) true)

case h.hf
I : Type u
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
o : Ordinal.{u}
i : I
⊢ Continuous fun x => x i
-- Mathlib/Data/Real/ConjExponents.lean
theorem conj_eq : q = p / (p - 1)

Proof state:
p q : ℝ
h : p.IsConjExponent q
this : p⁻¹ + q⁻¹ = 1
⊢ q = p / (p - 1)

Tactic:
rw [← eq_sub_iff_add_eq', inv_eq_iff_eq_inv] at this

Result:
p q : ℝ
h : p.IsConjExponent q
this : q = (1 - p⁻¹)⁻¹
⊢ q = p / (p - 1)

Proof state:
p q : ℝ
h : p.IsConjExponent q
this : q = (1 - p⁻¹)⁻¹
⊢ q = p / (p - 1)

Tactic:
field_simp [this, h.ne_zero]

Result:
no goals

Proof state:
p q : ℝ
h : p.IsConjExponent q
⊢ q = p / (p - 1)

Tactic:
have := h.inv_add_inv_conj

Result:
p q : ℝ
h : p.IsConjExponent q
this : p⁻¹ + q⁻¹ = 1
⊢ q = p / (p - 1)
-- Mathlib/FieldTheory/Laurent.lean
theorem laurent_X : laurent r X = X + C r

Proof state:
R : Type u
inst✝¹ : CommRing R
r : R
inst✝ : IsDomain R
⊢ (laurent r) X = X + C r

Tactic:
rw [← algebraMap_X, laurent_algebraMap, taylor_X, _root_.map_add, algebraMap_C]

Result:
no goals
-- Mathlib/Analysis/Convex/Between.lean
theorem mem_vsub_const_affineSegment {x y z : P} (p : P) :
    z -ᵥ p ∈ affineSegment R (x -ᵥ p) (y -ᵥ p) ↔ z ∈ affineSegment R x y

Proof state:
R : Type u_1
V : Type u_2
P : Type u_4
inst✝³ : OrderedRing R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
x y z p : P
⊢ z -ᵥ p ∈ affineSegment R (x -ᵥ p) (y -ᵥ p) ↔ z ∈ affineSegment R x y

Tactic:
rw [← affineSegment_vsub_const_image, (vsub_left_injective p).mem_set_image]

Result:
no goals