harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/AlgebraicTopology/SimplicialSet/Nerve.lean
theorem δ₁_mk₂_eq : (nerve C).δ 1 (ComposableArrows.mk₂ f g) = ComposableArrows.mk₁ (f ≫ g) :=
  ComposableArrows.ext₁ rfl rfl (by simp; rfl)

Proof state:
C : Type u_1
inst✝ : Category.{u_2, u_1} C
X₀ X₁ X₂ : C
f : X₀ ⟶ X₁
g : X₁ ⟶ X₂
⊢ ComposableArrows.hom (SimplicialObject.δ (nerve C) 1 (ComposableArrows.mk₂ f g)) =
    eqToHom ⋯ ≫ (ComposableArrows.mk₁ (f ≫ g)).hom ≫ eqToHom ⋯

Tactic:
simp

Result:
C : Type u_1
inst✝ : Category.{u_2, u_1} C
X₀ X₁ X₂ : C
f : X₀ ⟶ X₁
g : X₁ ⟶ X₂
⊢ ComposableArrows.hom (SimplicialObject.δ (nerve C) 1 ((ComposableArrows.mk₁ g).precomp f)) = f ≫ g

Proof state:
C : Type u_1
inst✝ : Category.{u_2, u_1} C
X₀ X₁ X₂ : C
f : X₀ ⟶ X₁
g : X₁ ⟶ X₂
⊢ ComposableArrows.hom (SimplicialObject.δ (nerve C) 1 ((ComposableArrows.mk₁ g).precomp f)) = f ≫ g

Tactic:
rfl

Result:
no goals
-- Mathlib/Data/Nat/Cast/Defs.lean
theorem one_add_one_eq_two [AddMonoidWithOne R] : 1 + 1 = (2 : R)

Proof state:
R : Type u_1
inst✝ : AddMonoidWithOne R
⊢ 1 + 1 = 2

Tactic:
rw [← Nat.cast_one, ← Nat.cast_add]

Result:
R : Type u_1
inst✝ : AddMonoidWithOne R
⊢ ↑(1 + 1) = 2

Proof state:
R : Type u_1
inst✝ : AddMonoidWithOne R
⊢ ↑(1 + 1) = 2

Tactic:
apply congrArg

Result:
case h
R : Type u_1
inst✝ : AddMonoidWithOne R
⊢ 1 + 1 = 2

Proof state:
case h
R : Type u_1
inst✝ : AddMonoidWithOne R
⊢ 1 + 1 = 2

Tactic:
decide

Result:
no goals
-- Mathlib/Data/Part.lean
theorem some_union_some [Union α] (a b : α) : some a ∪ some b = some (a ∪ b)

Proof state:
α : Type u_1
inst✝ : Union α
a b : α
⊢ some a ∪ some b = some (a ∪ b)

Tactic:
simp [union_def]

Result:
no goals
-- Mathlib/Analysis/PSeries.lean
theorem summable_condensed_iff_of_nonneg {f : ℕ → ℝ} (h_nonneg : ∀ n, 0 ≤ f n)
    (h_mono : ∀ ⦃m n⦄, 0 < m → m ≤ n → f n ≤ f m) :
    (Summable fun k : ℕ => (2 : ℝ) ^ k * f (2 ^ k)) ↔ Summable f

Proof state:
f : ℕ → ℝ
h_nonneg : ∀ (n : ℕ), 0 ≤ f n
h_mono : ∀ ⦃m n : ℕ⦄, 0 < m → m ≤ n → f n ≤ f m
h_succ_diff : SuccDiffBounded 2 fun x => 2 ^ x
⊢ (Summable fun k => 2 ^ k * f (2 ^ k)) ↔ Summable f

Tactic:
convert summable_schlomilch_iff_of_nonneg h_nonneg h_mono (pow_pos zero_lt_two)
  (pow_right_strictMono₀ one_lt_two) two_ne_zero h_succ_diff

Result:
case h.e'_1.h.e'_5.h.h.e'_5
f : ℕ → ℝ
h_nonneg : ∀ (n : ℕ), 0 ≤ f n
h_mono : ∀ ⦃m n : ℕ⦄, 0 < m → m ≤ n → f n ≤ f m
h_succ_diff : SuccDiffBounded 2 fun x => 2 ^ x
x✝ : ℕ
⊢ 2 ^ x✝ = ↑(2 ^ (x✝ + 1)) - ↑(2 ^ x✝)

Proof state:
f : ℕ → ℝ
h_nonneg : ∀ (n : ℕ), 0 ≤ f n
h_mono : ∀ ⦃m n : ℕ⦄, 0 < m → m ≤ n → f n ≤ f m
n : ℕ
⊢ (fun x => 2 ^ x) (n + 2) - (fun x => 2 ^ x) (n + 1) ≤ 2 • ((fun x => 2 ^ x) (n + 1) - (fun x => 2 ^ x) n)

Tactic:
simp [pow_succ, mul_two, two_mul]

Result:
no goals

Proof state:
f : ℕ → ℝ
h_nonneg : ∀ (n : ℕ), 0 ≤ f n
h_mono : ∀ ⦃m n : ℕ⦄, 0 < m → m ≤ n → f n ≤ f m
⊢ SuccDiffBounded 2 fun x => 2 ^ x

Tactic:
intro n

Result:
f : ℕ → ℝ
h_nonneg : ∀ (n : ℕ), 0 ≤ f n
h_mono : ∀ ⦃m n : ℕ⦄, 0 < m → m ≤ n → f n ≤ f m
n : ℕ
⊢ (fun x => 2 ^ x) (n + 2) - (fun x => 2 ^ x) (n + 1) ≤ 2 • ((fun x => 2 ^ x) (n + 1) - (fun x => 2 ^ x) n)

Proof state:
case h.e'_1.h.e'_5.h.h.e'_5
f : ℕ → ℝ
h_nonneg : ∀ (n : ℕ), 0 ≤ f n
h_mono : ∀ ⦃m n : ℕ⦄, 0 < m → m ≤ n → f n ≤ f m
h_succ_diff : SuccDiffBounded 2 fun x => 2 ^ x
x✝ : ℕ
⊢ 2 ^ x✝ = ↑(2 ^ (x✝ + 1)) - ↑(2 ^ x✝)

Tactic:
simp [pow_succ, mul_two, two_mul]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem getLsbD_sshiftRight' {x y : BitVec w} {i : Nat} :
    getLsbD (x.sshiftRight' y) i =
      (!decide (w ≤ i) && if y.toNat + i < w then x.getLsbD (y.toNat + i) else x.msb)

Proof state:
w : Nat
x y : BitVec w
i : Nat
⊢ (x.sshiftRight' y).getLsbD i = (!decide (w ≤ i) && if y.toNat + i < w then x.getLsbD (y.toNat + i) else x.msb)

Tactic:
simp only [BitVec.sshiftRight', BitVec.getLsbD_sshiftRight]

Result:
no goals
-- Mathlib/SetTheory/Ordinal/Arithmetic.lean
theorem IsNormal.limit_lt {f} (H : IsNormal f) {o} (h : IsLimit o) {a} :
    a < f o ↔ ∃ b < o, a < f b :=
  not_iff_not.1 <| by simpa only [exists_prop, not_exists, not_and, not_lt] using H.2 _ h a

Proof state:
f : Ordinal.{u_4} → Ordinal.{u_5}
H : IsNormal f
o : Ordinal.{u_4}
h : o.IsLimit
a : Ordinal.{u_5}
⊢ ¬a < f o ↔ ¬∃ b < o, a < f b

Tactic:
simpa only [exists_prop, not_exists, not_and, not_lt] using H.2 _ h a

Result:
no goals
-- Mathlib/Algebra/Ring/Int/Parity.lean
@[deprecated not_even_iff_odd (since := "2024-08-21")]
lemma odd_iff_not_even : Odd n ↔ ¬Even n

Proof state:
n : ℤ
⊢ Odd n ↔ ¬Even n

Tactic:
rw [not_even_iff, odd_iff]

Result:
no goals
-- Mathlib/RingTheory/AlgebraicIndependent/TranscendenceBasis.lean
theorem AlgebraicIndependent.isTranscendenceBasis_iff {ι : Type w} {R : Type u} [CommRing R]
    [Nontrivial R] {A : Type v} [CommRing A] [Algebra R A] {x : ι → A}
    (i : AlgebraicIndependent R x) :
    IsTranscendenceBasis R x ↔
      ∀ (κ : Type v) (w : κ → A) (_ : AlgebraicIndependent R w) (j : ι → κ) (_ : w ∘ j = x),
        Surjective j

Proof state:
case mpr
ι : Type w
R : Type u
inst✝³ : CommRing R
inst✝² : Nontrivial R
A : Type v
inst✝¹ : CommRing A
inst✝ : Algebra R A
x : ι → A
i : AlgebraicIndependent R x
⊢ (∀ (κ : Type v) (w : κ → A), AlgebraicIndependent R w → ∀ (j : ι → κ), w ∘ j = x → Surjective j) →
    IsTranscendenceBasis R x

Tactic:
intro p

Result:
case mpr
ι : Type w
R : Type u
inst✝³ : CommRing R
inst✝² : Nontrivial R
A : Type v
inst✝¹ : CommRing A
inst✝ : Algebra R A
x : ι → A
i : AlgebraicIndependent R x
p : ∀ (κ : Type v) (w : κ → A), AlgebraicIndependent R w → ∀ (j : ι → κ), w ∘ j = x → Surjective j
⊢ IsTranscendenceBasis R x

Proof state:
ι : Type w
R : Type u
inst✝³ : CommRing R
inst✝² : Nontrivial R
A : Type v
inst✝¹ : CommRing A
inst✝ : Algebra R A
x : ι → A
i : AlgebraicIndependent R x
⊢ IsTranscendenceBasis R x ↔
    ∀ (κ : Type v) (w : κ → A), AlgebraicIndependent R w → ∀ (j : ι → κ), w ∘ j = x → Surjective j

Tactic:
fconstructor

Result:
case mp
ι : Type w
R : Type u
inst✝³ : CommRing R
inst✝² : Nontrivial R
A : Type v
inst✝¹ : CommRing A
inst✝ : Algebra R A
x : ι → A
i : AlgebraicIndependent R x
⊢ IsTranscendenceBasis R x →
    ∀ (κ : Type v) (w : κ → A), AlgebraicIndependent R w → ∀ (j : ι → κ), w ∘ j = x → Surjective j

case mpr
ι : Type w
R : Type u
inst✝³ : CommRing R
inst✝² : Nontrivial R
A : Type v
inst✝¹ : CommRing A
inst✝ : Algebra R A
x : ι → A
i : AlgebraicIndependent R x
⊢ (∀ (κ : Type v) (w : κ → A), AlgebraicIndependent R w → ∀ (j : ι → κ), w ∘ j = x → Surjective j) →
    IsTranscendenceBasis R x

Proof state:
case h
ι : Type w
R : Type u
inst✝³ : CommRing R
inst✝² : Nontrivial R
A : Type v
inst✝¹ : CommRing A
inst✝ : Algebra R A
x : ι → A
i : AlgebraicIndependent R x
p : ∀ (κ : Type v) (w : κ → A), AlgebraicIndependent R w → ∀ (j : ι → κ), w ∘ j = x → Surjective j
w : Set A
i' : AlgebraicIndependent R Subtype.val
h : range x ≤ w
x✝ : ι
⊢ (Subtype.val ∘ fun i => ⟨x i, ⋯⟩) x✝ = x x✝

Tactic:
simp

Result:
no goals

Proof state:
case mp
ι : Type w
R : Type u
inst✝³ : CommRing R
inst✝² : Nontrivial R
A : Type v
inst✝¹ : CommRing A
inst✝ : Algebra R A
x : ι → A
i : AlgebraicIndependent R x
⊢ IsTranscendenceBasis R x →
    ∀ (κ : Type v) (w : κ → A), AlgebraicIndependent R w → ∀ (j : ι → κ), w ∘ j = x → Surjective j

Tactic:
rintro p κ w i' j rfl

Result:
case mp
ι : Type w
R : Type u
inst✝³ : CommRing R
inst✝² : Nontrivial R
A : Type v
inst✝¹ : CommRing A
inst✝ : Algebra R A
κ : Type v
w : κ → A
i' : AlgebraicIndependent R w
j : ι → κ
i : AlgebraicIndependent R (w ∘ j)
p : IsTranscendenceBasis R (w ∘ j)
⊢ Surjective j
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lex/Lemmas.lean
theorem lex_toList [BEq α] (lt : α → α → Bool) (l₁ l₂ : Array α) :
    l₁.toList.lex l₂.toList lt = l₁.lex l₂ lt

Proof state:
α : Type u_1
inst✝ : BEq α
lt : α → α → Bool
l₁ l₂ : Array α
⊢ l₁.toList.lex l₂.toList lt = l₁.lex l₂ lt

Tactic:
cases l₁ <;> cases l₂ <;> simp

Result:
no goals
-- Mathlib/CategoryTheory/Limits/Lattice.lean
theorem prod_eq_inf [SemilatticeInf α] [OrderTop α] (x y : α) : Limits.prod x y = x ⊓ y :=
  calc
    Limits.prod x y = limit (pair x y) := rfl
    _ = Finset.univ.inf (pair x y).obj

Proof state:
α : Type u
inst✝¹ : SemilatticeInf α
inst✝ : OrderTop α
x y : α
⊢ x ⊓ (y ⊓ ⊤) = x ⊓ y

Tactic:
rw [inf_top_eq]

Result:
no goals

Proof state:
α : Type u
inst✝¹ : SemilatticeInf α
inst✝ : OrderTop α
x y : α
⊢ limit (pair x y) = Finset.univ.inf (pair x y).obj

Tactic:
rw [finite_limit_eq_finset_univ_inf (pair.{u} x y)]

Result:
no goals
-- Mathlib/Algebra/Order/GroupWithZero/Unbundled.lean
@[simp] lemma zpow_le_one_iff_right₀ (ha : 1 < a) : a ^ n ≤ 1 ↔ n ≤ 0

Proof state:
G₀ : Type u_2
inst✝⁴ : GroupWithZero G₀
inst✝³ : PartialOrder G₀
inst✝² : ZeroLEOneClass G₀
inst✝¹ : PosMulReflectLT G₀
a : G₀
inst✝ : PosMulStrictMono G₀
n : ℤ
ha : 1 < a
⊢ a ^ n ≤ 1 ↔ n ≤ 0

Tactic:
simp [← zpow_le_zpow_iff_right₀ ha]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/SimpLemmas.lean
theorem letFun_congr {α : Sort u} {β : Sort v}  {a a' : α} {f f' : α → β} (h₁ : a = a') (h₂ : ∀ x, f x = f' x)
    : @letFun α (fun _ => β) a f = @letFun α (fun _ => β) a' f'

Proof state:
α : Sort u
β : Sort v
a a' : α
f f' : α → β
h₁ : a = a'
h₂ : ∀ (x : α), f x = f' x
⊢ letFun a f = letFun a' f'

Tactic:
rw [h₁, funext h₂]

Result:
no goals
-- Mathlib/MeasureTheory/Decomposition/Exhaustion.lean
lemma sigmaFinite_of_measure_compl_sigmaFiniteSet_eq_zero (h : μ μ.sigmaFiniteSetᶜ = 0) :
    SigmaFinite μ

Proof state:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
h : μ μ.sigmaFiniteSetᶜ = 0
⊢ SigmaFinite (μ.restrict μ.sigmaFiniteSet)

Tactic:
infer_instance

Result:
no goals

Proof state:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
h : μ μ.sigmaFiniteSetᶜ = 0
⊢ SigmaFinite μ

Tactic:
rw [← Measure.restrict_add_restrict_compl (μ := μ) (measurableSet_sigmaFiniteSet (μ := μ)),
  Measure.restrict_eq_zero.mpr h, add_zero]

Result:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
h : μ μ.sigmaFiniteSetᶜ = 0
⊢ SigmaFinite (μ.restrict μ.sigmaFiniteSet)
-- Mathlib/Order/CompactlyGenerated/Basic.lean
theorem sSup_compact_eq_top : sSup { a : α | CompleteLattice.IsCompactElement a } = ⊤

Proof state:
α : Type u_2
inst✝¹ : CompleteLattice α
inst✝ : IsCompactlyGenerated α
⊢ sSup {a | CompleteLattice.IsCompactElement a} = ⊤

Tactic:
refine Eq.trans (congr rfl (Set.ext fun x => ?_)) (sSup_compact_le_eq ⊤)

Result:
α : Type u_2
inst✝¹ : CompleteLattice α
inst✝ : IsCompactlyGenerated α
x : α
⊢ x ∈ {a | CompleteLattice.IsCompactElement a} ↔ x ∈ {c | CompleteLattice.IsCompactElement c ∧ c ≤ ⊤}

Proof state:
α : Type u_2
inst✝¹ : CompleteLattice α
inst✝ : IsCompactlyGenerated α
x : α
⊢ x ∈ {a | CompleteLattice.IsCompactElement a} ↔ x ∈ {c | CompleteLattice.IsCompactElement c ∧ c ≤ ⊤}

Tactic:
exact (and_iff_left le_top).symm

Result:
no goals
-- Mathlib/GroupTheory/GroupAction/ConjAct.lean
theorem orbit_eq_carrier_conjClasses (g : G) :
    orbit (ConjAct G) g = (ConjClasses.mk g).carrier

Proof state:
case h
G : Type u_3
inst✝ : Group G
g h : G
⊢ h ∈ orbit (ConjAct G) g ↔ h ∈ (ConjClasses.mk g).carrier

Tactic:
rw [ConjClasses.mem_carrier_iff_mk_eq, ConjClasses.mk_eq_mk_iff_isConj, mem_orbit_conjAct]

Result:
no goals

Proof state:
G : Type u_3
inst✝ : Group G
g : G
⊢ orbit (ConjAct G) g = (ConjClasses.mk g).carrier

Tactic:
ext h

Result:
case h
G : Type u_3
inst✝ : Group G
g h : G
⊢ h ∈ orbit (ConjAct G) g ↔ h ∈ (ConjClasses.mk g).carrier
-- Mathlib/Topology/Algebra/Affine.lean
theorem homothety_continuous (x : F) (t : R) : Continuous <| homothety x t

Proof state:
R : Type u_1
F : Type u_3
inst✝⁵ : AddCommGroup F
inst✝⁴ : TopologicalSpace F
inst✝³ : IsTopologicalAddGroup F
inst✝² : CommRing R
inst✝¹ : Module R F
inst✝ : ContinuousConstSMul R F
x : F
t : R
this : ⇑(homothety x t) = fun y => t • (y - x) + x
⊢ Continuous ⇑(homothety x t)

Tactic:
rw [this]

Result:
R : Type u_1
F : Type u_3
inst✝⁵ : AddCommGroup F
inst✝⁴ : TopologicalSpace F
inst✝³ : IsTopologicalAddGroup F
inst✝² : CommRing R
inst✝¹ : Module R F
inst✝ : ContinuousConstSMul R F
x : F
t : R
this : ⇑(homothety x t) = fun y => t • (y - x) + x
⊢ Continuous fun y => t • (y - x) + x

Proof state:
R : Type u_1
F : Type u_3
inst✝⁵ : AddCommGroup F
inst✝⁴ : TopologicalSpace F
inst✝³ : IsTopologicalAddGroup F
inst✝² : CommRing R
inst✝¹ : Module R F
inst✝ : ContinuousConstSMul R F
x : F
t : R
⊢ ⇑(homothety x t) = fun y => t • (y - x) + x

Tactic:
ext y

Result:
case h
R : Type u_1
F : Type u_3
inst✝⁵ : AddCommGroup F
inst✝⁴ : TopologicalSpace F
inst✝³ : IsTopologicalAddGroup F
inst✝² : CommRing R
inst✝¹ : Module R F
inst✝ : ContinuousConstSMul R F
x : F
t : R
y : F
⊢ (homothety x t) y = t • (y - x) + x

Proof state:
case h
R : Type u_1
F : Type u_3
inst✝⁵ : AddCommGroup F
inst✝⁴ : TopologicalSpace F
inst✝³ : IsTopologicalAddGroup F
inst✝² : CommRing R
inst✝¹ : Module R F
inst✝ : ContinuousConstSMul R F
x : F
t : R
y : F
⊢ (homothety x t) y = t • (y - x) + x

Tactic:
simp [homothety_apply]

Result:
no goals

Proof state:
R : Type u_1
F : Type u_3
inst✝⁵ : AddCommGroup F
inst✝⁴ : TopologicalSpace F
inst✝³ : IsTopologicalAddGroup F
inst✝² : CommRing R
inst✝¹ : Module R F
inst✝ : ContinuousConstSMul R F
x : F
t : R
this : ⇑(homothety x t) = fun y => t • (y - x) + x
⊢ Continuous fun y => t • (y - x) + x

Tactic:
exact ((continuous_id.sub continuous_const).const_smul _).add continuous_const

Result:
no goals

Proof state:
R : Type u_1
F : Type u_3
inst✝⁵ : AddCommGroup F
inst✝⁴ : TopologicalSpace F
inst✝³ : IsTopologicalAddGroup F
inst✝² : CommRing R
inst✝¹ : Module R F
inst✝ : ContinuousConstSMul R F
x : F
t : R
⊢ Continuous ⇑(homothety x t)

Tactic:
suffices ⇑(homothety x t) = fun y => t • (y - x) + x by
  rw [this]
  exact ((continuous_id.sub continuous_const).const_smul _).add continuous_const

Result:
R : Type u_1
F : Type u_3
inst✝⁵ : AddCommGroup F
inst✝⁴ : TopologicalSpace F
inst✝³ : IsTopologicalAddGroup F
inst✝² : CommRing R
inst✝¹ : Module R F
inst✝ : ContinuousConstSMul R F
x : F
t : R
⊢ ⇑(homothety x t) = fun y => t • (y - x) + x
-- Mathlib/Analysis/SpecialFunctions/MulExpNegMulSq.lean
theorem dist_mulExpNegMulSq_le_two_mul_sqrt (hε : 0 < ε) (x y : ℝ) :
    dist (mulExpNegMulSq ε x) (mulExpNegMulSq ε y) ≤ 2 * (sqrt ε)⁻¹

Proof state:
ε : ℝ
hε : 0 < ε
x y : ℝ
⊢ dist (ε.mulExpNegMulSq x) (ε.mulExpNegMulSq y) ≤ 2 * (√ε)⁻¹

Tactic:
apply le_trans (dist_triangle (mulExpNegMulSq ε x) 0 (mulExpNegMulSq ε y))

Result:
ε : ℝ
hε : 0 < ε
x y : ℝ
⊢ dist (ε.mulExpNegMulSq x) 0 + dist 0 (ε.mulExpNegMulSq y) ≤ 2 * (√ε)⁻¹

Proof state:
ε : ℝ
hε : 0 < ε
x y : ℝ
⊢ |ε.mulExpNegMulSq x| + |ε.mulExpNegMulSq y| ≤ (√ε)⁻¹ + (√ε)⁻¹

Tactic:
exact add_le_add (abs_mulExpNegMulSq_le hε) (abs_mulExpNegMulSq_le hε)

Result:
no goals

Proof state:
ε : ℝ
hε : 0 < ε
x y : ℝ
⊢ dist (ε.mulExpNegMulSq x) 0 + dist 0 (ε.mulExpNegMulSq y) ≤ 2 * (√ε)⁻¹

Tactic:
simp only [dist_zero_right, norm_eq_abs, dist_zero_left, two_mul]

Result:
ε : ℝ
hε : 0 < ε
x y : ℝ
⊢ |ε.mulExpNegMulSq x| + |ε.mulExpNegMulSq y| ≤ (√ε)⁻¹ + (√ε)⁻¹
-- Mathlib/Analysis/Convex/Basic.lean
lemma stdSimplex_unique [Nonempty ι] [Subsingleton ι] : stdSimplex 𝕜 ι = {fun _ ↦ 1}

Proof state:
case intro
𝕜 : Type u_1
ι : Type u_5
inst✝³ : OrderedSemiring 𝕜
inst✝² : Fintype ι
inst✝¹ : Nonempty ι
inst✝ : Subsingleton ι
val✝ : Unique ι
⊢ ∀ x ∈ stdSimplex 𝕜 ι, x = fun x => 1

Tactic:
rintro f ⟨-, hf⟩

Result:
case intro.intro
𝕜 : Type u_1
ι : Type u_5
inst✝³ : OrderedSemiring 𝕜
inst✝² : Fintype ι
inst✝¹ : Nonempty ι
inst✝ : Subsingleton ι
val✝ : Unique ι
f : ι → 𝕜
hf : ∑ x : ι, f x = 1
⊢ f = fun x => 1

Proof state:
case intro.intro
𝕜 : Type u_1
ι : Type u_5
inst✝³ : OrderedSemiring 𝕜
inst✝² : Fintype ι
inst✝¹ : Nonempty ι
inst✝ : Subsingleton ι
val✝ : Unique ι
f : ι → 𝕜
hf : ∑ x : ι, f x = 1
⊢ f = fun x => 1

Tactic:
rw [Fintype.sum_unique] at hf

Result:
case intro.intro
𝕜 : Type u_1
ι : Type u_5
inst✝³ : OrderedSemiring 𝕜
inst✝² : Fintype ι
inst✝¹ : Nonempty ι
inst✝ : Subsingleton ι
val✝ : Unique ι
f : ι → 𝕜
hf : f default = 1
⊢ f = fun x => 1

Proof state:
𝕜 : Type u_1
ι : Type u_5
inst✝³ : OrderedSemiring 𝕜
inst✝² : Fintype ι
inst✝¹ : Nonempty ι
inst✝ : Subsingleton ι
⊢ stdSimplex 𝕜 ι = {fun x => 1}

Tactic:
cases nonempty_unique ι

Result:
case intro
𝕜 : Type u_1
ι : Type u_5
inst✝³ : OrderedSemiring 𝕜
inst✝² : Fintype ι
inst✝¹ : Nonempty ι
inst✝ : Subsingleton ι
val✝ : Unique ι
⊢ stdSimplex 𝕜 ι = {fun x => 1}

Proof state:
case intro.intro
𝕜 : Type u_1
ι : Type u_5
inst✝³ : OrderedSemiring 𝕜
inst✝² : Fintype ι
inst✝¹ : Nonempty ι
inst✝ : Subsingleton ι
val✝ : Unique ι
f : ι → 𝕜
hf : f default = 1
⊢ f = fun x => 1

Tactic:
exact funext (Unique.forall_iff.2 hf)

Result:
no goals

Proof state:
case intro
𝕜 : Type u_1
ι : Type u_5
inst✝³ : OrderedSemiring 𝕜
inst✝² : Fintype ι
inst✝¹ : Nonempty ι
inst✝ : Subsingleton ι
val✝ : Unique ι
⊢ stdSimplex 𝕜 ι = {fun x => 1}

Tactic:
refine eq_singleton_iff_unique_mem.2 ⟨⟨fun _ ↦ zero_le_one, Fintype.sum_unique _⟩, ?_⟩

Result:
case intro
𝕜 : Type u_1
ι : Type u_5
inst✝³ : OrderedSemiring 𝕜
inst✝² : Fintype ι
inst✝¹ : Nonempty ι
inst✝ : Subsingleton ι
val✝ : Unique ι
⊢ ∀ x ∈ stdSimplex 𝕜 ι, x = fun x => 1
-- Mathlib/Analysis/Convex/Strict.lean
theorem StrictConvex.smul_mem_of_zero_mem (hs : StrictConvex 𝕜 s) (zero_mem : (0 : E) ∈ s)
    (hx : x ∈ s) (hx₀ : x ≠ 0) {t : 𝕜} (ht₀ : 0 < t) (ht₁ : t < 1) : t • x ∈ interior s

Proof state:
𝕜 : Type u_1
E : Type u_3
inst✝³ : OrderedRing 𝕜
inst✝² : TopologicalSpace E
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s : Set E
x : E
hs : StrictConvex 𝕜 s
zero_mem : 0 ∈ s
hx : x ∈ s
hx₀ : x ≠ 0
t : 𝕜
ht₀ : 0 < t
ht₁ : t < 1
⊢ t • x ∈ interior s

Tactic:
simpa using hs.add_smul_mem zero_mem (by simpa using hx) hx₀ ht₀ ht₁

Result:
no goals

Proof state:
𝕜 : Type u_1
E : Type u_3
inst✝³ : OrderedRing 𝕜
inst✝² : TopologicalSpace E
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s : Set E
x : E
hs : StrictConvex 𝕜 s
zero_mem : 0 ∈ s
hx : x ∈ s
hx₀ : x ≠ 0
t : 𝕜
ht₀ : 0 < t
ht₁ : t < 1
⊢ 0 + x ∈ s

Tactic:
simpa using hx

Result:
no goals
-- Mathlib/FieldTheory/KummerExtension.lean
theorem X_pow_sub_C_splits_of_isPrimitiveRoot
    {n : ℕ} {ζ : K} (hζ : IsPrimitiveRoot ζ n) {α a : K} (e : α ^ n = a) :
    (X ^ n - C a).Splits (RingHom.id _)

Proof state:
case inr
K : Type u
inst✝ : Field K
n : ℕ
ζ : K
hζ : IsPrimitiveRoot ζ n
α a : K
e : α ^ n = a
hn : n > 0
⊢ Splits (RingHom.id K) (X ^ n - C a)

Tactic:
rw [splits_iff_card_roots, ← nthRoots, hζ.card_nthRoots, natDegree_X_pow_sub_C, if_pos ⟨α, e⟩]

Result:
no goals

Proof state:
case inl
K : Type u
inst✝ : Field K
n : ℕ
ζ : K
hζ : IsPrimitiveRoot ζ n
α a : K
e : α ^ n = a
hn : n = 0
⊢ Splits (RingHom.id K) (X ^ n - C a)

Tactic:
rw [hn, pow_zero, ← C.map_one, ← map_sub]

Result:
case inl
K : Type u
inst✝ : Field K
n : ℕ
ζ : K
hζ : IsPrimitiveRoot ζ n
α a : K
e : α ^ n = a
hn : n = 0
⊢ Splits (RingHom.id K) (C (1 - a))

Proof state:
K : Type u
inst✝ : Field K
n : ℕ
ζ : K
hζ : IsPrimitiveRoot ζ n
α a : K
e : α ^ n = a
⊢ Splits (RingHom.id K) (X ^ n - C a)

Tactic:
cases n.eq_zero_or_pos with
| inl hn =>
  rw [hn, pow_zero, ← C.map_one, ← map_sub]
  exact splits_C _ _
| inr hn =>
  rw [splits_iff_card_roots, ← nthRoots, hζ.card_nthRoots, natDegree_X_pow_sub_C, if_pos ⟨α, e⟩]

Result:
no goals

Proof state:
case inl
K : Type u
inst✝ : Field K
n : ℕ
ζ : K
hζ : IsPrimitiveRoot ζ n
α a : K
e : α ^ n = a
hn : n = 0
⊢ Splits (RingHom.id K) (C (1 - a))

Tactic:
exact splits_C _ _

Result:
no goals
-- Mathlib/Algebra/BigOperators/Expect.lean
/-- Reorder an average.

The difference with `Finset.expect_bij` is that the bijection is specified with an inverse, rather
than as a surjective injection.

The difference with `Finset.expect_nbij'` is that the bijection and its inverse are allowed to use
membership of the domains of the averages, rather than being non-dependent functions. -/
lemma expect_bij' (i : ∀ a ∈ s, κ) (j : ∀ a ∈ t, ι) (hi : ∀ a ha, i a ha ∈ t)
    (hj : ∀ a ha, j a ha ∈ s) (left_inv : ∀ a ha, j (i a ha) (hi a ha) = a)
    (right_inv : ∀ a ha, i (j a ha) (hj a ha) = a) (h : ∀ a ha, f a = g (i a ha)) :
    𝔼 i ∈ s, f i = 𝔼 i ∈ t, g i

Proof state:
ι : Type u_1
κ : Type u_2
M : Type u_3
inst✝¹ : AddCommMonoid M
inst✝ : Module ℚ≥0 M
s : Finset ι
f : ι → M
t : Finset κ
g : κ → M
i : (a : ι) → a ∈ s → κ
j : (a : κ) → a ∈ t → ι
hi : ∀ (a : ι) (ha : a ∈ s), i a ha ∈ t
hj : ∀ (a : κ) (ha : a ∈ t), j a ha ∈ s
left_inv : ∀ (a : ι) (ha : a ∈ s), j (i a ha) ⋯ = a
right_inv : ∀ (a : κ) (ha : a ∈ t), i (j a ha) ⋯ = a
h : ∀ (a : ι) (ha : a ∈ s), f a = g (i a ha)
⊢ 𝔼 i ∈ s, f i = 𝔼 i ∈ t, g i

Tactic:
simp_rw [expect, card_bij' i j hi hj left_inv right_inv, sum_bij' i j hi hj left_inv right_inv h]

Result:
no goals
-- Mathlib/Data/Nat/Init.lean
protected lemma mul_div_cancel_left' (Hd : a ∣ b) : a * (b / a) = b

Proof state:
a b : ℕ
Hd : a ∣ b
⊢ a * (b / a) = b

Tactic:
rw [Nat.mul_comm, Nat.div_mul_cancel Hd]

Result:
no goals
-- Mathlib/Algebra/BigOperators/Group/Finset/Basic.lean
theorem card_eq_sum_card_fiberwise [DecidableEq β] {f : α → β} {s : Finset α} {t : Finset β}
    (H : ∀ x ∈ s, f x ∈ t) : #s = ∑ b ∈ t, #{a ∈ s | f a = b}

Proof state:
α : Type u_3
β : Type u_4
inst✝ : DecidableEq β
f : α → β
s : Finset α
t : Finset β
H : ∀ x ∈ s, f x ∈ t
⊢ #s = ∑ b ∈ t, #(filter (fun a => f a = b) s)

Tactic:
simp only [card_eq_sum_ones, sum_fiberwise_of_maps_to H]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Lemmas.lean
theorem get?_eq_getElem? (l : List α) (i : Nat) : l.get? i = l[i]?

Proof state:
case isFalse
α : Type u_1
l : List α
i : Nat
h✝ : ¬i < l.length
⊢ l.get? i = none

Tactic:
exact (get?_eq_none_iff.2 <| Nat.not_lt.1 ‹_›)

Result:
no goals

Proof state:
case isTrue
α : Type u_1
l : List α
i : Nat
h✝ : i < l.length
⊢ l.get? i = some l[i]

Tactic:
exact (get?_eq_get ‹_›)

Result:
no goals

Proof state:
α : Type u_1
l : List α
i : Nat
⊢ l.get? i = if h : i < l.length then some l[i] else none

Tactic:
split

Result:
case isTrue
α : Type u_1
l : List α
i : Nat
h✝ : i < l.length
⊢ l.get? i = some l[i]

case isFalse
α : Type u_1
l : List α
i : Nat
h✝ : ¬i < l.length
⊢ l.get? i = none

Proof state:
α : Type u_1
l : List α
i : Nat
⊢ l.get? i = l[i]?

Tactic:
simp only [getElem?_def]

Result:
α : Type u_1
l : List α
i : Nat
⊢ l.get? i = if h : i < l.length then some l[i] else none
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Nat/TakeDrop.lean
theorem getLast?_drop {l : List α} : (l.drop n).getLast? = if l.length ≤ n then none else l.getLast?

Proof state:
case isTrue
α : Type u_1
n : Nat
l : List α
h✝ : l.length ≤ n
⊢ l[n + (l.length - n - 1)]? = none

Tactic:
rw [getElem?_eq_none (by omega)]

Result:
no goals

Proof state:
case isFalse.e_a
α : Type u_1
n : Nat
l : List α
h✝ : ¬l.length ≤ n
⊢ n + (l.length - n - 1) = l.length - 1

Tactic:
omega

Result:
no goals

Proof state:
α : Type u_1
n : Nat
l : List α
h✝ : l.length ≤ n
⊢ l.length ≤ n + (l.length - n - 1)

Tactic:
omega

Result:
no goals

Proof state:
case isFalse
α : Type u_1
n : Nat
l : List α
h✝ : ¬l.length ≤ n
⊢ l[n + (l.length - n - 1)]? = l[l.length - 1]?

Tactic:
congr

Result:
case isFalse.e_a
α : Type u_1
n : Nat
l : List α
h✝ : ¬l.length ≤ n
⊢ n + (l.length - n - 1) = l.length - 1

Proof state:
case isFalse
α : Type u_1
n : Nat
l : List α
h✝ : ¬l.length ≤ n
⊢ l[n + (l.length - n - 1)]? = l.getLast?

Tactic:
rw [getLast?_eq_getElem?]

Result:
case isFalse
α : Type u_1
n : Nat
l : List α
h✝ : ¬l.length ≤ n
⊢ l[n + (l.length - n - 1)]? = l[l.length - 1]?

Proof state:
α : Type u_1
n : Nat
l : List α
⊢ (drop n l).getLast? = if l.length ≤ n then none else l.getLast?

Tactic:
rw [getLast?_eq_getElem?, getElem?_drop]

Result:
α : Type u_1
n : Nat
l : List α
⊢ l[n + ((drop n l).length - 1)]? = if l.length ≤ n then none else l.getLast?

Proof state:
α : Type u_1
n : Nat
l : List α
⊢ l[n + ((drop n l).length - 1)]? = if l.length ≤ n then none else l.getLast?

Tactic:
rw [length_drop]

Result:
α : Type u_1
n : Nat
l : List α
⊢ l[n + (l.length - n - 1)]? = if l.length ≤ n then none else l.getLast?

Proof state:
α : Type u_1
n : Nat
l : List α
⊢ l[n + (l.length - n - 1)]? = if l.length ≤ n then none else l.getLast?

Tactic:
split

Result:
case isTrue
α : Type u_1
n : Nat
l : List α
h✝ : l.length ≤ n
⊢ l[n + (l.length - n - 1)]? = none

case isFalse
α : Type u_1
n : Nat
l : List α
h✝ : ¬l.length ≤ n
⊢ l[n + (l.length - n - 1)]? = l.getLast?