harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Data/Nat/Totient.lean
theorem sum_totient (n : ℕ) : n.divisors.sum φ = n

Proof state:
case inl

⊢ (divisors 0).sum φ = 0

Tactic:
simp

Result:
no goals

Proof state:
case inr
n : ℕ
hn : n > 0
⊢ n.divisors.sum φ = n

Tactic:
rw [← sum_div_divisors n φ]

Result:
case inr
n : ℕ
hn : n > 0
⊢ ∑ d ∈ n.divisors, φ (n / d) = n

Proof state:
n : ℕ
⊢ n.divisors.sum φ = n

Tactic:
rcases n.eq_zero_or_pos with (rfl | hn)

Result:
case inl

⊢ (divisors 0).sum φ = 0

case inr
n : ℕ
hn : n > 0
⊢ n.divisors.sum φ = n

Proof state:
n : ℕ
hn : n > 0
x : ℕ
x✝ : x ∈ range n
⊢ n.gcd x ∣ n

Tactic:
apply gcd_dvd_left

Result:
no goals

Proof state:
n : ℕ
hn : n > 0
⊢ n = ∑ d ∈ n.divisors, #(filter (fun k => n.gcd k = d) (range n))

Tactic:
nth_rw 1 [← card_range n]

Result:
n : ℕ
hn : n > 0
⊢ #(range n) = ∑ d ∈ n.divisors, #(filter (fun k => n.gcd k = d) (range n))

Proof state:
case inr
n : ℕ
hn : n > 0
this : n = ∑ d ∈ n.divisors, #(filter (fun k => n.gcd k = d) (range n))
⊢ ∑ d ∈ n.divisors, φ (n / d) = ∑ d ∈ n.divisors, #(filter (fun k => n.gcd k = d) (range n))

Tactic:
exact sum_congr rfl fun x hx => totient_div_of_dvd (dvd_of_mem_divisors hx)

Result:
no goals

Proof state:
case inr
n : ℕ
hn : n > 0
⊢ ∑ d ∈ n.divisors, φ (n / d) = n

Tactic:
have : n = ∑ d ∈ n.divisors, #{k ∈ range n | n.gcd k = d} := by
  nth_rw 1 [← card_range n]
  refine card_eq_sum_card_fiberwise fun x _ => mem_divisors.2 ⟨?_, hn.ne'⟩
  apply gcd_dvd_left

Result:
case inr
n : ℕ
hn : n > 0
this : n = ∑ d ∈ n.divisors, #(filter (fun k => n.gcd k = d) (range n))
⊢ ∑ d ∈ n.divisors, φ (n / d) = n

Proof state:
n : ℕ
hn : n > 0
⊢ #(range n) = ∑ d ∈ n.divisors, #(filter (fun k => n.gcd k = d) (range n))

Tactic:
refine card_eq_sum_card_fiberwise fun x _ => mem_divisors.2 ⟨?_, hn.ne'⟩

Result:
n : ℕ
hn : n > 0
x : ℕ
x✝ : x ∈ range n
⊢ n.gcd x ∣ n

Proof state:
case inr
n : ℕ
hn : n > 0
this : n = ∑ d ∈ n.divisors, #(filter (fun k => n.gcd k = d) (range n))
⊢ ∑ d ∈ n.divisors, φ (n / d) = n

Tactic:
nth_rw 3 [this]

Result:
case inr
n : ℕ
hn : n > 0
this : n = ∑ d ∈ n.divisors, #(filter (fun k => n.gcd k = d) (range n))
⊢ ∑ d ∈ n.divisors, φ (n / d) = ∑ d ∈ n.divisors, #(filter (fun k => n.gcd k = d) (range n))
-- Mathlib/Probability/Independence/Conditional.lean
lemma condIndepSet_iff (s t : Set Ω) (hs : MeasurableSet s) (ht : MeasurableSet t)
    (μ : Measure Ω) [IsFiniteMeasure μ] :
    CondIndepSet m' hm' s t μ ↔ (μ⟦s ∩ t | m'⟧) =ᵐ[μ] (μ⟦s | m'⟧) * (μ⟦t | m'⟧)

Proof state:
Ω : Type u_1
m' mΩ : MeasurableSpace Ω
inst✝¹ : StandardBorelSpace Ω
hm' : m' ≤ mΩ
s t : Set Ω
hs : MeasurableSet s
ht : MeasurableSet t
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
⊢ CondIndepSet m' hm' s t μ ↔
    μ[(s ∩ t).indicator fun ω => 1|m'] =ᶠ[ae μ] μ[s.indicator fun ω => 1|m'] * μ[t.indicator fun ω => 1|m']

Tactic:
rw [condIndepSet_iff_condIndepSets_singleton _ _ hs ht μ, condIndepSets_singleton_iff _ _ hs ht]

Result:
no goals
-- Mathlib/Order/RelIso/Set.lean
theorem range_eq (e : r ≃r s) : Set.range e = Set.univ

Proof state:
α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
e : r ≃r s
⊢ Set.range ⇑e = Set.univ

Tactic:
simp

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Complex/Arg.lean
theorem arg_inv (x : ℂ) : arg x⁻¹ = if arg x = π then π else -arg x

Proof state:
x : ℂ
⊢ (↑(normSq x)⁻¹ * (starRingEnd ℂ) x).arg = ((starRingEnd ℂ) x).arg

Tactic:
by_cases hx : x = 0

Result:
case pos
x : ℂ
hx : x = 0
⊢ (↑(normSq x)⁻¹ * (starRingEnd ℂ) x).arg = ((starRingEnd ℂ) x).arg

case neg
x : ℂ
hx : ¬x = 0
⊢ (↑(normSq x)⁻¹ * (starRingEnd ℂ) x).arg = ((starRingEnd ℂ) x).arg

Proof state:
case pos
x : ℂ
hx : x = 0
⊢ (↑(normSq x)⁻¹ * (starRingEnd ℂ) x).arg = ((starRingEnd ℂ) x).arg

Tactic:
simp [hx]

Result:
no goals

Proof state:
x : ℂ
⊢ x⁻¹.arg = if x.arg = π then π else -x.arg

Tactic:
rw [← arg_conj, inv_def, mul_comm]

Result:
x : ℂ
⊢ (↑(normSq x)⁻¹ * (starRingEnd ℂ) x).arg = ((starRingEnd ℂ) x).arg

Proof state:
case neg
x : ℂ
hx : ¬x = 0
⊢ (↑(normSq x)⁻¹ * (starRingEnd ℂ) x).arg = ((starRingEnd ℂ) x).arg

Tactic:
exact arg_real_mul (conj x) (by simp [hx])

Result:
no goals

Proof state:
x : ℂ
hx : ¬x = 0
⊢ 0 < (normSq x)⁻¹

Tactic:
simp [hx]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Int/Order.lean
theorem add_lt_of_lt_sub_right {a b c : Int} (h : a < c - b) : a + b < c

Proof state:
a b c : Int
h : a < c - b
⊢ a + b < c

Tactic:
have h := Int.add_lt_add_right h b

Result:
a b c : Int
h✝ : a < c - b
h : a + b < c - b + b
⊢ a + b < c

Proof state:
a b c : Int
h✝ : a < c - b
h : a + b < c - b + b
⊢ a + b < c

Tactic:
rwa [Int.sub_add_cancel] at h

Result:
no goals
-- Mathlib/Data/Fintype/Basic.lean
theorem Fin.univ_succAbove (n : ℕ) (p : Fin (n + 1)) :
    (univ : Finset (Fin (n + 1))) = Finset.cons p (univ.map <| Fin.succAboveEmb p) (by simp)

Proof state:
n : ℕ
p : Fin (n + 1)
⊢ univ = Finset.cons p (map p.succAboveEmb univ) ⋯

Tactic:
simp [map_eq_image]

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
n : ℕ
p : Fin (n + 1)
⊢ p ∉ map p.succAboveEmb univ

Tactic:
simp

Result:
no goals
-- Mathlib/Geometry/Manifold/IsManifold/ExtChartAt.lean
theorem nhdsWithin_extChartAt_target_eq_of_mem {x : M} {z : E} (hz : z ∈ (extChartAt I x).target) :
    𝓝[(extChartAt I x).target] z = 𝓝[range I] z

Proof state:
𝕜 : Type u_1
E : Type u_2
M : Type u_3
H : Type u_4
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
inst✝² : TopologicalSpace H
inst✝¹ : TopologicalSpace M
I : ModelWithCorners 𝕜 E H
inst✝ : ChartedSpace H M
x : M
z : E
hz : z ∈ (extChartAt I x).target
⊢ 𝓝[(extChartAt I x).target] ↑(extChartAt I x) (↑(extChartAt I x).symm z) =
    𝓝[range ↑I] ↑(extChartAt I x) (↑(extChartAt I x).symm z)

Tactic:
exact nhdsWithin_extChartAt_target_eq' ((extChartAt I x).map_target hz)

Result:
no goals

Proof state:
𝕜 : Type u_1
E : Type u_2
M : Type u_3
H : Type u_4
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
inst✝² : TopologicalSpace H
inst✝¹ : TopologicalSpace M
I : ModelWithCorners 𝕜 E H
inst✝ : ChartedSpace H M
x : M
z : E
hz : z ∈ (extChartAt I x).target
⊢ 𝓝[(extChartAt I x).target] z = 𝓝[range ↑I] z

Tactic:
rw [← PartialEquiv.right_inv (extChartAt I x) hz]

Result:
𝕜 : Type u_1
E : Type u_2
M : Type u_3
H : Type u_4
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
inst✝² : TopologicalSpace H
inst✝¹ : TopologicalSpace M
I : ModelWithCorners 𝕜 E H
inst✝ : ChartedSpace H M
x : M
z : E
hz : z ∈ (extChartAt I x).target
⊢ 𝓝[(extChartAt I x).target] ↑(extChartAt I x) (↑(extChartAt I x).symm z) =
    𝓝[range ↑I] ↑(extChartAt I x) (↑(extChartAt I x).symm z)
-- Mathlib/MeasureTheory/Integral/Average.lean
theorem integral_sub_average (μ : Measure α) [IsFiniteMeasure μ] (f : α → E) :
    ∫ x, f x - ⨍ a, f a ∂μ ∂μ = 0

Proof state:
case h.e'_6
α : Type u_1
E : Type u_2
m0 : MeasurableSpace α
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : CompleteSpace E
μ : Measure α
inst✝ : IsFiniteMeasure μ
f : α → E
hf : ¬Integrable f μ
h : Integrable (fun x => f x - ⨍ (a : α), f a ∂μ) μ
⊢ f = (fun x => f x - ⨍ (a : α), f a ∂μ) + fun x => ⨍ (a : α), f a ∂μ

Tactic:
exact (sub_add_cancel _ _).symm

Result:
no goals

Proof state:
case neg
α : Type u_1
E : Type u_2
m0 : MeasurableSpace α
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : CompleteSpace E
μ : Measure α
inst✝ : IsFiniteMeasure μ
f : α → E
hf : ¬Integrable f μ
h : Integrable (fun x => f x - ⨍ (a : α), f a ∂μ) μ
⊢ Integrable f μ

Tactic:
convert h.add (integrable_const (⨍ a, f a ∂μ))

Result:
case h.e'_6
α : Type u_1
E : Type u_2
m0 : MeasurableSpace α
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : CompleteSpace E
μ : Measure α
inst✝ : IsFiniteMeasure μ
f : α → E
hf : ¬Integrable f μ
h : Integrable (fun x => f x - ⨍ (a : α), f a ∂μ) μ
⊢ f = (fun x => f x - ⨍ (a : α), f a ∂μ) + fun x => ⨍ (a : α), f a ∂μ

Proof state:
case neg
α : Type u_1
E : Type u_2
m0 : MeasurableSpace α
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : CompleteSpace E
μ : Measure α
inst✝ : IsFiniteMeasure μ
f : α → E
hf : ¬Integrable f μ
⊢ ∫ (x : α), f x - ⨍ (a : α), f a ∂μ ∂μ = 0

Tactic:
refine integral_undef fun h => hf ?_

Result:
case neg
α : Type u_1
E : Type u_2
m0 : MeasurableSpace α
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : CompleteSpace E
μ : Measure α
inst✝ : IsFiniteMeasure μ
f : α → E
hf : ¬Integrable f μ
h : Integrable (fun x => f x - ⨍ (a : α), f a ∂μ) μ
⊢ Integrable f μ

Proof state:
case pos
α : Type u_1
E : Type u_2
m0 : MeasurableSpace α
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : CompleteSpace E
μ : Measure α
inst✝ : IsFiniteMeasure μ
f : α → E
hf : Integrable f μ
⊢ ∫ (x : α), f x - ⨍ (a : α), f a ∂μ ∂μ = 0

Tactic:
rw [integral_sub hf (integrable_const _), integral_average, sub_self]

Result:
no goals

Proof state:
α : Type u_1
E : Type u_2
m0 : MeasurableSpace α
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : CompleteSpace E
μ : Measure α
inst✝ : IsFiniteMeasure μ
f : α → E
⊢ ∫ (x : α), f x - ⨍ (a : α), f a ∂μ ∂μ = 0

Tactic:
by_cases hf : Integrable f μ

Result:
case pos
α : Type u_1
E : Type u_2
m0 : MeasurableSpace α
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : CompleteSpace E
μ : Measure α
inst✝ : IsFiniteMeasure μ
f : α → E
hf : Integrable f μ
⊢ ∫ (x : α), f x - ⨍ (a : α), f a ∂μ ∂μ = 0

case neg
α : Type u_1
E : Type u_2
m0 : MeasurableSpace α
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : CompleteSpace E
μ : Measure α
inst✝ : IsFiniteMeasure μ
f : α → E
hf : ¬Integrable f μ
⊢ ∫ (x : α), f x - ⨍ (a : α), f a ∂μ ∂μ = 0
-- Mathlib/Analysis/MellinTransform.lean
theorem hasMellin_sub {f g : ℝ → E} {s : ℂ} (hf : MellinConvergent f s)
    (hg : MellinConvergent g s) : HasMellin (fun t => f t - g t) s (mellin f s - mellin g s) :=
  ⟨by simpa only [MellinConvergent, smul_sub] using hf.sub hg, by
    simpa only [mellin, smul_sub] using integral_sub hf hg⟩

Proof state:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f g : ℝ → E
s : ℂ
hf : MellinConvergent f s
hg : MellinConvergent g s
⊢ MellinConvergent (fun t => f t - g t) s

Tactic:
simpa only [MellinConvergent, smul_sub] using hf.sub hg

Result:
no goals

Proof state:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f g : ℝ → E
s : ℂ
hf : MellinConvergent f s
hg : MellinConvergent g s
⊢ mellin (fun t => f t - g t) s = mellin f s - mellin g s

Tactic:
simpa only [mellin, smul_sub] using integral_sub hf hg

Result:
no goals
-- Mathlib/AlgebraicGeometry/EllipticCurve/Projective.lean
lemma equation_iff (P : Fin 3 → R) : W'.Equation P ↔
    P y ^ 2 * P z + W'.a₁ * P x * P y * P z + W'.a₃ * P y * P z ^ 2
      - (P x ^ 3 + W'.a₂ * P x ^ 2 * P z + W'.a₄ * P x * P z ^ 2 + W'.a₆ * P z ^ 3) = 0

Proof state:
R : Type r
inst✝ : CommRing R
W' : Projective R
P : Fin 3 → R
⊢ W'.Equation P ↔
    P y ^ 2 * P z + W'.a₁ * P x * P y * P z + W'.a₃ * P y * P z ^ 2 -
        (P x ^ 3 + W'.a₂ * P x ^ 2 * P z + W'.a₄ * P x * P z ^ 2 + W'.a₆ * P z ^ 3) =
      0

Tactic:
rw [Equation, eval_polynomial, sub_eq_zero]

Result:
no goals
-- Mathlib/CategoryTheory/Limits/Shapes/Multiequalizer.lean
theorem ι_sigmaπ (b) : Sigma.ι I.right b ≫ sigmaπ I = π I b

Proof state:
C : Type u
inst✝³ : Category.{v, u} C
J : MultispanShape
I : MultispanIndex J C
inst✝² : HasMulticoequalizer I
inst✝¹ : HasCoproduct I.left
inst✝ : HasCoproduct I.right
b : J.R
⊢ Sigma.ι I.right b ≫ coequalizer.π I.fstSigmaMap I.sndSigmaMap =
    (Multicofork.ofSigmaCofork I (colimit.cocone (parallelPair I.fstSigmaMap I.sndSigmaMap))).π b

Tactic:
rfl

Result:
no goals

Proof state:
C : Type u
inst✝³ : Category.{v, u} C
J : MultispanShape
I : MultispanIndex J C
inst✝² : HasMulticoequalizer I
inst✝¹ : HasCoproduct I.left
inst✝ : HasCoproduct I.right
b : J.R
⊢ Sigma.ι I.right b ≫ coequalizer.π I.fstSigmaMap I.sndSigmaMap =
    π I b ≫
      (colimit.isoColimitCocone
          {
            cocone :=
              I.multicoforkEquivSigmaCofork.inverse.obj (colimit.cocone (parallelPair I.fstSigmaMap I.sndSigmaMap)),
            isColimit :=
              IsColimit.ofPreservesCoconeInitial I.multicoforkEquivSigmaCofork.inverse
                (colimit.isColimit (parallelPair I.fstSigmaMap I.sndSigmaMap)) }).hom

Tactic:
simp only [MultispanIndex.multicoforkEquivSigmaCofork_inverse,
  MultispanIndex.ofSigmaCoforkFunctor_obj, colimit.isoColimitCocone_ι_hom,
  Multicofork.ofSigmaCofork_pt, colimit.cocone_x, Multicofork.π_eq_app_right]

Result:
C : Type u
inst✝³ : Category.{v, u} C
J : MultispanShape
I : MultispanIndex J C
inst✝² : HasMulticoequalizer I
inst✝¹ : HasCoproduct I.left
inst✝ : HasCoproduct I.right
b : J.R
⊢ Sigma.ι I.right b ≫ coequalizer.π I.fstSigmaMap I.sndSigmaMap =
    (Multicofork.ofSigmaCofork I (colimit.cocone (parallelPair I.fstSigmaMap I.sndSigmaMap))).π b

Proof state:
C : Type u
inst✝³ : Category.{v, u} C
J : MultispanShape
I : MultispanIndex J C
inst✝² : HasMulticoequalizer I
inst✝¹ : HasCoproduct I.left
inst✝ : HasCoproduct I.right
b : J.R
⊢ Sigma.ι I.right b ≫ sigmaπ I = π I b

Tactic:
rw [sigmaπ, ← Category.assoc, Iso.comp_inv_eq, isoCoequalizer]

Result:
C : Type u
inst✝³ : Category.{v, u} C
J : MultispanShape
I : MultispanIndex J C
inst✝² : HasMulticoequalizer I
inst✝¹ : HasCoproduct I.left
inst✝ : HasCoproduct I.right
b : J.R
⊢ Sigma.ι I.right b ≫ coequalizer.π I.fstSigmaMap I.sndSigmaMap =
    π I b ≫
      (colimit.isoColimitCocone
          {
            cocone :=
              I.multicoforkEquivSigmaCofork.inverse.obj (colimit.cocone (parallelPair I.fstSigmaMap I.sndSigmaMap)),
            isColimit :=
              IsColimit.ofPreservesCoconeInitial I.multicoforkEquivSigmaCofork.inverse
                (colimit.isColimit (parallelPair I.fstSigmaMap I.sndSigmaMap)) }).hom
-- Mathlib/Data/TypeVec.lean
theorem fst_diag {α : TypeVec n} : TypeVec.prod.fst ⊚ (prod.diag : α ⟹ _) = id

Proof state:
case h.fs
n n✝ : ℕ
a✝ : Fin2 n✝
i_ih : ∀ {α : TypeVec.{u_1} n✝}, (prod.fst ⊚ prod.diag) a✝ = id a✝
α : TypeVec.{u_1} (n✝ + 1)
⊢ (prod.fst ⊚ prod.diag) a✝.fs = id a✝.fs

Tactic:
apply i_ih

Result:
no goals

Proof state:
case h
n : ℕ
α : TypeVec.{u_1} n
i : Fin2 n
⊢ (prod.fst ⊚ prod.diag) i = id i

Tactic:
induction i with
| fz => rfl
| fs _ i_ih => apply i_ih

Result:
no goals

Proof state:
n : ℕ
α : TypeVec.{u_1} n
⊢ prod.fst ⊚ prod.diag = id

Tactic:
funext i

Result:
case h
n : ℕ
α : TypeVec.{u_1} n
i : Fin2 n
⊢ (prod.fst ⊚ prod.diag) i = id i

Proof state:
case h.fz
n n✝ : ℕ
α : TypeVec.{u_1} (n✝ + 1)
⊢ (prod.fst ⊚ prod.diag) Fin2.fz = id Fin2.fz

Tactic:
rfl

Result:
no goals
-- Mathlib/Algebra/Order/BigOperators/Group/Finset.lean
theorem exists_one_lt_of_prod_one_of_exists_ne_one' (f : ι → M) (h₁ : ∏ i ∈ s, f i = 1)
    (h₂ : ∃ i ∈ s, f i ≠ 1) : ∃ i ∈ s, 1 < f i

Proof state:
ι : Type u_1
M : Type u_4
inst✝ : LinearOrderedCancelCommMonoid M
s : Finset ι
f : ι → M
h₂ : ∃ i ∈ s, f i ≠ 1
h₁ : ∀ i ∈ s, f i ≤ 1
⊢ ∏ i ∈ s, f i ≠ 1

Tactic:
obtain ⟨i, m, i_ne⟩ : ∃ i ∈ s, f i ≠ 1 := h₂

Result:
case intro.intro
ι : Type u_1
M : Type u_4
inst✝ : LinearOrderedCancelCommMonoid M
s : Finset ι
f : ι → M
h₁ : ∀ i ∈ s, f i ≤ 1
i : ι
m : i ∈ s
i_ne : f i ≠ 1
⊢ ∏ i ∈ s, f i ≠ 1

Proof state:
ι : Type u_1
M : Type u_4
inst✝ : LinearOrderedCancelCommMonoid M
s : Finset ι
f : ι → M
h₁ : ∏ i ∈ s, f i = 1
h₂ : ∃ i ∈ s, f i ≠ 1
⊢ ∃ i ∈ s, 1 < f i

Tactic:
contrapose! h₁

Result:
ι : Type u_1
M : Type u_4
inst✝ : LinearOrderedCancelCommMonoid M
s : Finset ι
f : ι → M
h₂ : ∃ i ∈ s, f i ≠ 1
h₁ : ∀ i ∈ s, f i ≤ 1
⊢ ∏ i ∈ s, f i ≠ 1

Proof state:
case intro.intro
ι : Type u_1
M : Type u_4
inst✝ : LinearOrderedCancelCommMonoid M
s : Finset ι
f : ι → M
h₁ : ∀ i ∈ s, f i ≤ 1
i : ι
m : i ∈ s
i_ne : f i ≠ 1
⊢ ∏ i ∈ s, f i ≠ 1

Tactic:
apply ne_of_lt

Result:
case intro.intro.h
ι : Type u_1
M : Type u_4
inst✝ : LinearOrderedCancelCommMonoid M
s : Finset ι
f : ι → M
h₁ : ∀ i ∈ s, f i ≤ 1
i : ι
m : i ∈ s
i_ne : f i ≠ 1
⊢ ∏ i ∈ s, f i < 1

Proof state:
case intro.intro.h
ι : Type u_1
M : Type u_4
inst✝ : LinearOrderedCancelCommMonoid M
s : Finset ι
f : ι → M
h₁ : ∀ i ∈ s, f i ≤ 1
i : ι
m : i ∈ s
i_ne : f i ≠ 1
⊢ ∏ i ∈ s, f i < 1

Tactic:
calc
  ∏ j ∈ s, f j < ∏ j ∈ s, 1 := prod_lt_prod' h₁ ⟨i, m, (h₁ i m).lt_of_ne i_ne⟩
  _ = 1 := prod_const_one

Result:
no goals
-- Mathlib/NumberTheory/LSeries/RiemannZeta.lean
lemma HurwitzZeta.cosZeta_zero : cosZeta 0 = riemannZeta

Proof state:
⊢ cosZeta 0 = riemannZeta

Tactic:
simp_rw [cosZeta, riemannZeta, hurwitzZetaEven, if_true, completedHurwitzZetaEven_zero,
  completedCosZeta_zero]

Result:
no goals
-- Mathlib/Analysis/NormedSpace/OperatorNorm/Bilinear.lean
theorem norm_precompR_le (L : E →L[𝕜] Fₗ →L[𝕜] Gₗ) : ‖precompR Eₗ L‖ ≤ ‖L‖ :=
  calc
    ‖precompR Eₗ L‖ ≤ ‖compL 𝕜 Eₗ Fₗ Gₗ‖ * ‖L‖ := opNorm_comp_le _ _
    _ ≤ 1 * ‖L‖ := mul_le_mul_of_nonneg_right (norm_compL_le _ _ _ _) (norm_nonneg L)
    _ = ‖L‖

Proof state:
𝕜 : Type u_1
E : Type u_4
Fₗ : Type u_7
Gₗ : Type u_9
inst✝⁶ : SeminormedAddCommGroup E
inst✝⁵ : SeminormedAddCommGroup Fₗ
inst✝⁴ : SeminormedAddCommGroup Gₗ
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedSpace 𝕜 Fₗ
inst✝ : NormedSpace 𝕜 Gₗ
L : E →L[𝕜] Fₗ →L[𝕜] Gₗ
⊢ 1 * ‖L‖ = ‖L‖

Tactic:
rw [one_mul]

Result:
no goals
-- Mathlib/RingTheory/HahnSeries/Multiplication.lean
theorem order_C {r : R} : order (C r : HahnSeries Γ R) = 0

Proof state:
case pos
Γ : Type u_1
R : Type u_3
inst✝¹ : OrderedCancelAddCommMonoid Γ
inst✝ : NonAssocSemiring R
r : R
h : r = 0
⊢ (C r).order = 0

Tactic:
rw [h, C_zero, order_zero]

Result:
no goals

Proof state:
case neg
Γ : Type u_1
R : Type u_3
inst✝¹ : OrderedCancelAddCommMonoid Γ
inst✝ : NonAssocSemiring R
r : R
h : ¬r = 0
⊢ (C r).order = 0

Tactic:
exact order_single h

Result:
no goals

Proof state:
Γ : Type u_1
R : Type u_3
inst✝¹ : OrderedCancelAddCommMonoid Γ
inst✝ : NonAssocSemiring R
r : R
⊢ (C r).order = 0

Tactic:
by_cases h : r = 0

Result:
case pos
Γ : Type u_1
R : Type u_3
inst✝¹ : OrderedCancelAddCommMonoid Γ
inst✝ : NonAssocSemiring R
r : R
h : r = 0
⊢ (C r).order = 0

case neg
Γ : Type u_1
R : Type u_3
inst✝¹ : OrderedCancelAddCommMonoid Γ
inst✝ : NonAssocSemiring R
r : R
h : ¬r = 0
⊢ (C r).order = 0
-- Mathlib/Data/Nat/Lattice.lean
theorem iSup_lt_succ (u : ℕ → α) (n : ℕ) : ⨆ k < n + 1, u k = (⨆ k < n, u k) ⊔ u n

Proof state:
α : Type u_1
inst✝ : CompleteLattice α
u : ℕ → α
n : ℕ
⊢ ⨆ k, ⨆ (_ : k < n + 1), u k = (⨆ k, ⨆ (_ : k < n), u k) ⊔ u n

Tactic:
simp_rw [Nat.lt_add_one_iff, biSup_le_eq_sup]

Result:
no goals
-- Mathlib/CategoryTheory/Bicategory/Basic.lean
theorem associator_naturality_middle (f : a ⟶ b) {g g' : b ⟶ c} (η : g ⟶ g') (h : c ⟶ d) :
    (f ◁ η) ▷ h ≫ (α_ f g' h).hom = (α_ f g h).hom ≫ f ◁ η ▷ h

Proof state:
B : Type u
inst✝ : Bicategory B
a b c d : B
f : a ⟶ b
g g' : b ⟶ c
η : g ⟶ g'
h : c ⟶ d
⊢ (f ◁ η) ▷ h ≫ (α_ f g' h).hom = (α_ f g h).hom ≫ f ◁ η ▷ h

Tactic:
simp

Result:
no goals
-- Mathlib/Data/List/FinRange.lean
theorem Equiv.Perm.map_finRange_perm {n : ℕ} (σ : Equiv.Perm (Fin n)) :
    map σ (finRange n) ~ finRange n

Proof state:
n : ℕ
σ : Perm (Fin n)
⊢ ∀ (a : Fin n), a ∈ map (⇑σ) (finRange n) ↔ a ∈ finRange n

Tactic:
simpa [mem_map, mem_finRange] using σ.surjective

Result:
no goals

Proof state:
n : ℕ
σ : Perm (Fin n)
⊢ map (⇑σ) (finRange n) ~ finRange n

Tactic:
rw [perm_ext_iff_of_nodup ((nodup_finRange n).map σ.injective) <| nodup_finRange n]

Result:
n : ℕ
σ : Perm (Fin n)
⊢ ∀ (a : Fin n), a ∈ map (⇑σ) (finRange n) ↔ a ∈ finRange n
-- Mathlib/ModelTheory/Equivalence.lean
lemma sup_not_iff_top :
    φ ⊔ ∼φ ⇔[T] ⊤ := fun M v xs => by
  simp only [realize_iff, realize_sup, realize_not, realize_top, iff_true, or_not]

Proof state:
L : Language
T : L.Theory
α : Type w
n : ℕ
φ : L.BoundedFormula α n
M : T.ModelType
v : α → ↑M
xs : Fin n → ↑M
⊢ (φ ⊔ ∼φ ⇔ ⊤).Realize v xs

Tactic:
simp only [realize_iff, realize_sup, realize_not, realize_top, iff_true, or_not]

Result:
no goals
-- Mathlib/Order/KrullDimension.lean
/--
The Krull dimension is the supremum of the elements' heights.

If `α` is `Nonempty`, then `krullDim_eq_iSup_height_of_nonempty`, with the coercion from
`ℕ∞` to `WithBot ℕ∞` outside the supremum, can be more convenient.
-/
lemma krullDim_eq_iSup_height : krullDim α = ⨆ (a : α), ↑(height a)

Proof state:
α : Type u_1
inst✝ : Preorder α
⊢ krullDim α = ⨆ a, ↑(height a)

Tactic:
cases isEmpty_or_nonempty α with
| inl h => rw [krullDim_eq_bot, ciSup_of_empty]
| inr h => rw [krullDim_eq_iSup_height_of_nonempty, WithBot.coe_iSup (OrderTop.bddAbove _)]

Result:
no goals

Proof state:
case inr
α : Type u_1
inst✝ : Preorder α
h : Nonempty α
⊢ krullDim α = ⨆ a, ↑(height a)

Tactic:
rw [krullDim_eq_iSup_height_of_nonempty, WithBot.coe_iSup (OrderTop.bddAbove _)]

Result:
no goals

Proof state:
case inl
α : Type u_1
inst✝ : Preorder α
h : IsEmpty α
⊢ krullDim α = ⨆ a, ↑(height a)

Tactic:
rw [krullDim_eq_bot, ciSup_of_empty]

Result:
no goals
-- Mathlib/Data/Set/Subset.lean
lemma preimage_val_sInter_eq_sInter : A ↓∩ (⋂₀ S) = ⋂₀ ((A ↓∩ ·) '' S)

Proof state:
α : Type u_2
A : Set α
S : Set (Set α)
⊢ A ↓∩ ⋂₀ S = ⋂₀ ((fun x => A ↓∩ x) '' S)

Tactic:
simp only [preimage_sInter, sInter_image]

Result:
no goals
-- Mathlib/MeasureTheory/OuterMeasure/Caratheodory.lean
theorem measure_inter_union (h : s₁ ∩ s₂ ⊆ ∅) (h₁ : IsCaratheodory m s₁) {t : Set α} :
    m (t ∩ (s₁ ∪ s₂)) = m (t ∩ s₁) + m (t ∩ s₂)

Proof state:
α : Type u
m : OuterMeasure α
s₁ s₂ : Set α
h : s₁ ∩ s₂ ⊆ ∅
h₁ : m.IsCaratheodory s₁
t : Set α
⊢ m (t ∩ (s₁ ∪ s₂)) = m (t ∩ s₁) + m (t ∩ s₂)

Tactic:
rw [h₁, Set.inter_assoc, Set.union_inter_cancel_left, inter_diff_assoc, union_diff_cancel_left h]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Lemmas.lean
theorem mem_flatMap {f : α → Vector β m} {b} {l : Vector α n} : b ∈ l.flatMap f ↔ ∃ a, a ∈ l ∧ b ∈ f a

Proof state:
α : Type u_1
β : Type u_2
m n : Nat
f : α → Vector β m
b : β
l : Vector α n
⊢ b ∈ l.flatMap f ↔ ∃ a, a ∈ l ∧ b ∈ f a

Tactic:
simp [flatMap_def, mem_flatten]

Result:
α : Type u_1
β : Type u_2
m n : Nat
f : α → Vector β m
b : β
l : Vector α n
⊢ (∃ l_1, (∃ a, a ∈ l ∧ f a = l_1) ∧ b ∈ l_1) ↔ ∃ a, a ∈ l ∧ b ∈ f a

Proof state:
α : Type u_1
β : Type u_2
m n : Nat
f : α → Vector β m
b : β
l : Vector α n
⊢ (∃ l_1, (∃ a, a ∈ l ∧ f a = l_1) ∧ b ∈ l_1) ↔ ∃ a, a ∈ l ∧ b ∈ f a

Tactic:
exact ⟨fun ⟨_, ⟨a, h₁, rfl⟩, h₂⟩ => ⟨a, h₁, h₂⟩, fun ⟨a, h₁, h₂⟩ => ⟨_, ⟨a, h₁, rfl⟩, h₂⟩⟩

Result:
no goals
-- Mathlib/RingTheory/Extension.lean
@[simp]
lemma Hom.toAlgHom_id : Hom.toAlgHom (.id P) = AlgHom.id _ _

Proof state:
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
P : Extension R S
⊢ (Hom.id P).toAlgHom = AlgHom.id R P.Ring

Tactic:
ext1

Result:
case H
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
P : Extension R S
x✝ : P.Ring
⊢ (Hom.id P).toAlgHom x✝ = (AlgHom.id R P.Ring) x✝

Proof state:
case H
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
P : Extension R S
x✝ : P.Ring
⊢ (Hom.id P).toAlgHom x✝ = (AlgHom.id R P.Ring) x✝

Tactic:
simp

Result:
no goals
-- Mathlib/Combinatorics/SetFamily/Shadow.lean
/-- `s ∈ ∂ 𝒜` iff `s` is exactly one element less than something from `𝒜`.

See also `Finset.mem_shadow_iff_exists_sdiff`. -/
lemma mem_shadow_iff_exists_mem_card_add_one : t ∈ ∂ 𝒜 ↔ ∃ s ∈ 𝒜, t ⊆ s ∧ #s = #t + 1

Proof state:
α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
t✝ t : Finset α
x✝ : t ∈ 𝒜
hst : t✝ ⊆ t
⊢ #(t \ t✝) = 1 ↔ #t = #t✝ + 1

Tactic:
rw [card_sdiff hst, tsub_eq_iff_eq_add_of_le, add_comm]

Result:
α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
t✝ t : Finset α
x✝ : t ∈ 𝒜
hst : t✝ ⊆ t
⊢ #t✝ ≤ #t

Proof state:
α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
t✝ t : Finset α
x✝ : t ∈ 𝒜
hst : t✝ ⊆ t
⊢ #t✝ ≤ #t

Tactic:
exact card_mono hst

Result:
no goals

Proof state:
α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
t : Finset α
⊢ t ∈ ∂ 𝒜 ↔ ∃ s ∈ 𝒜, t ⊆ s ∧ #s = #t + 1

Tactic:
refine mem_shadow_iff_exists_sdiff.trans <| exists_congr fun t ↦ and_congr_right fun _ ↦
  and_congr_right fun hst ↦ ?_

Result:
α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
t✝ t : Finset α
x✝ : t ∈ 𝒜
hst : t✝ ⊆ t
⊢ #(t \ t✝) = 1 ↔ #t = #t✝ + 1