harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Algebra/Ring/Subsemiring/Defs.lean
@[aesop safe apply (rule_sets := [SetLike])]
lemma ofNat_mem [AddSubmonoidWithOneClass S R] (s : S) (n : ℕ) [n.AtLeastTwo] :
    ofNat(n) ∈ s

Proof state:
S : Type u_1
R : Type u_2
inst✝³ : AddMonoidWithOne R
inst✝² : SetLike S R
inst✝¹ : AddSubmonoidWithOneClass S R
s : S
n : ℕ
inst✝ : n.AtLeastTwo
⊢ ↑(OfNat.ofNat n) ∈ s

Tactic:
exact natCast_mem s n

Result:
no goals

Proof state:
S : Type u_1
R : Type u_2
inst✝³ : AddMonoidWithOne R
inst✝² : SetLike S R
inst✝¹ : AddSubmonoidWithOneClass S R
s : S
n : ℕ
inst✝ : n.AtLeastTwo
⊢ OfNat.ofNat n ∈ s

Tactic:
rw [← Nat.cast_ofNat]

Result:
S : Type u_1
R : Type u_2
inst✝³ : AddMonoidWithOne R
inst✝² : SetLike S R
inst✝¹ : AddSubmonoidWithOneClass S R
s : S
n : ℕ
inst✝ : n.AtLeastTwo
⊢ ↑(OfNat.ofNat n) ∈ s
-- Mathlib/Combinatorics/SimpleGraph/Walk.lean
theorem darts_append {u v w : V} (p : G.Walk u v) (p' : G.Walk v w) :
    (p.append p').darts = p.darts ++ p'.darts

Proof state:
V : Type u
G : SimpleGraph V
u v w : V
p : G.Walk u v
p' : G.Walk v w
⊢ (p.append p').darts = p.darts ++ p'.darts

Tactic:
induction p <;> simp [*]

Result:
no goals
-- Mathlib/Algebra/Group/Submonoid/Operations.lean
theorem map_comap_eq_self {f : F} {S : Submonoid N} (h : S ≤ MonoidHom.mrange f) :
    (S.comap f).map f = S

Proof state:
M : Type u_1
N : Type u_2
inst✝² : MulOneClass M
inst✝¹ : MulOneClass N
F : Type u_4
inst✝ : FunLike F M N
mc : MonoidHomClass F M N
f : F
S : Submonoid N
h : S ≤ MonoidHom.mrange f
⊢ map f (comap f S) = S

Tactic:
simpa only [inf_of_le_left h] using map_comap_eq f S

Result:
no goals
-- Mathlib/Algebra/Order/Monovary.lean
/-- Two functions monovary iff the rearrangement inequality holds. -/
lemma monovary_iff_smul_rearrangement :
    Monovary f g ↔ ∀ i j, f i • g j + f j • g i ≤ f i • g i + f j • g j :=
  monovaryOn_univ.symm.trans <| monovaryOn_iff_smul_rearrangement.trans <| by
    simp only [Set.mem_univ, forall_true_left]

Proof state:
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝³ : LinearOrderedRing α
inst✝² : LinearOrderedAddCommGroup β
inst✝¹ : Module α β
inst✝ : OrderedSMul α β
f : ι → α
g : ι → β
⊢ (∀ ⦃i : ι⦄, i ∈ Set.univ → ∀ ⦃j : ι⦄, j ∈ Set.univ → f i • g j + f j • g i ≤ f i • g i + f j • g j) ↔
    ∀ (i j : ι), f i • g j + f j • g i ≤ f i • g i + f j • g j

Tactic:
simp only [Set.mem_univ, forall_true_left]

Result:
no goals
-- Mathlib/Data/Finset/Card.lean
theorem one_lt_card_iff_nontrivial : 1 < #s ↔ s.Nontrivial

Proof state:
α : Type u_1
s : Finset α
⊢ 1 < #s ↔ s.Nontrivial

Tactic:
rw [← not_iff_not, not_lt, Finset.Nontrivial, ← Set.nontrivial_coe_sort,
  not_nontrivial_iff_subsingleton, card_le_one_iff_subsingleton_coe, coe_sort_coe]

Result:
no goals
-- Mathlib/RingTheory/Ideal/Maps.lean
theorem annihilator_iSup (ι : Sort w) (f : ι → Submodule R M) :
    annihilator (⨆ i, f i) = ⨅ i, annihilator (f i) :=
  le_antisymm (le_iInf fun _ => annihilator_mono <| le_iSup _ _) fun r H =>
    mem_annihilator.2 fun n hn ↦ iSup_induction f (C := (r • · = 0)) hn
      (fun i ↦ mem_annihilator.1 <| (mem_iInf _).mp H i) (smul_zero _)
      fun m₁ m₂ h₁ h₂ ↦ by simp_rw [smul_add, h₁, h₂, add_zero]

Proof state:
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
ι : Sort w
f : ι → Submodule R M
r : R
H : r ∈ ⨅ i, (f i).annihilator
n : M
hn : n ∈ ⨆ i, f i
m₁ m₂ : M
h₁ : (fun x => r • x = 0) m₁
h₂ : (fun x => r • x = 0) m₂
⊢ (fun x => r • x = 0) (m₁ + m₂)

Tactic:
simp_rw [smul_add, h₁, h₂, add_zero]

Result:
no goals
-- Mathlib/Tactic/PNatToNat.lean
@[pnat_to_nat_coe]
lemma coe_inj (m n : PNat) : m = n ↔ (m : ℕ) = (n : ℕ)

Proof state:
m n : ℕ+
⊢ m = n ↔ ↑m = ↑n

Tactic:
simp

Result:
no goals
-- Mathlib/Analysis/Calculus/LineDeriv/Basic.lean
theorem HasLineDerivWithinAt.congr_mono (h : HasLineDerivWithinAt 𝕜 f f' s x v) (ht : EqOn f₁ f t)
    (hx : f₁ x = f x) (h₁ : t ⊆ s) : HasLineDerivWithinAt 𝕜 f₁ f' t x v :=
  HasDerivWithinAt.congr_mono h (fun _ hy ↦ ht hy) (by simpa using hx) (preimage_mono h₁)

Proof state:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
F : Type u_2
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
E : Type u_3
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
f f₁ : E → F
f' : F
s t : Set E
x v : E
h : HasLineDerivWithinAt 𝕜 f f' s x v
ht : EqOn f₁ f t
hx : f₁ x = f x
h₁ : t ⊆ s
⊢ f₁ (x + 0 • v) = f (x + 0 • v)

Tactic:
simpa using hx

Result:
no goals
-- Mathlib/MeasureTheory/Measure/GiryMonad.lean
theorem join_eq_bind (μ : Measure (Measure α)) : join μ = bind μ id

Proof state:
α : Type u_1
mα : MeasurableSpace α
μ : Measure (Measure α)
⊢ μ.join = μ.bind id

Tactic:
rw [bind, map_id]

Result:
no goals
-- Mathlib/InformationTheory/Hamming.lean
theorem hammingDist_triangle_left (x y z : ∀ i, β i) :
    hammingDist x y ≤ hammingDist z x + hammingDist z y

Proof state:
ι : Type u_2
β : ι → Type u_3
inst✝¹ : Fintype ι
inst✝ : (i : ι) → DecidableEq (β i)
x y z : (i : ι) → β i
⊢ hammingDist x y ≤ hammingDist z x + hammingDist z y

Tactic:
rw [hammingDist_comm z]

Result:
ι : Type u_2
β : ι → Type u_3
inst✝¹ : Fintype ι
inst✝ : (i : ι) → DecidableEq (β i)
x y z : (i : ι) → β i
⊢ hammingDist x y ≤ hammingDist x z + hammingDist z y

Proof state:
ι : Type u_2
β : ι → Type u_3
inst✝¹ : Fintype ι
inst✝ : (i : ι) → DecidableEq (β i)
x y z : (i : ι) → β i
⊢ hammingDist x y ≤ hammingDist x z + hammingDist z y

Tactic:
exact hammingDist_triangle _ _ _

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Lemmas.lean
theorem getLast?_isSome : l.getLast?.isSome ↔ l ≠ []

Proof state:
α✝ : Type u_1
l : List α✝
⊢ l.getLast?.isSome = true ↔ l ≠ []

Tactic:
rw [getLast?_eq_head?_reverse, head?_isSome]

Result:
α✝ : Type u_1
l : List α✝
⊢ l.reverse ≠ [] ↔ l ≠ []

Proof state:
α✝ : Type u_1
l : List α✝
⊢ l.reverse ≠ [] ↔ l ≠ []

Tactic:
simp

Result:
no goals
-- Mathlib/Algebra/Order/CompleteField.lean
theorem inducedMap_add (x y : α) :
    inducedMap α β (x + y) = inducedMap α β x + inducedMap α β y

Proof state:
α : Type u_2
β : Type u_3
inst✝² : LinearOrderedField α
inst✝¹ : ConditionallyCompleteLinearOrderedField β
inst✝ : Archimedean α
x y : α
⊢ inducedMap α β (x + y) = inducedMap α β x + inducedMap α β y

Tactic:
rw [inducedMap, cutMap_add]

Result:
α : Type u_2
β : Type u_3
inst✝² : LinearOrderedField α
inst✝¹ : ConditionallyCompleteLinearOrderedField β
inst✝ : Archimedean α
x y : α
⊢ sSup (cutMap β x + cutMap β y) = inducedMap α β x + inducedMap α β y

Proof state:
α : Type u_2
β : Type u_3
inst✝² : LinearOrderedField α
inst✝¹ : ConditionallyCompleteLinearOrderedField β
inst✝ : Archimedean α
x y : α
⊢ sSup (cutMap β x + cutMap β y) = inducedMap α β x + inducedMap α β y

Tactic:
exact csSup_add (cutMap_nonempty β x) (cutMap_bddAbove β x) (cutMap_nonempty β y)
  (cutMap_bddAbove β y)

Result:
no goals
-- Mathlib/Data/Set/Function.lean
theorem surjective_iff_surjOn_univ : Surjective f ↔ SurjOn f univ univ

Proof state:
α : Type u_1
β : Type u_2
f : α → β
⊢ Surjective f ↔ SurjOn f univ univ

Tactic:
simp [Surjective, SurjOn, subset_def]

Result:
no goals
-- Mathlib/RingTheory/KrullDimension/Basic.lean
lemma Ring.krullDimLE_one_iff : Ring.KrullDimLE 1 R ↔
    ∀ I : Ideal R, I.IsPrime → I ∈ minimalPrimes R ∨ I.IsMaximal

Proof state:
R : Type u_1
inst✝ : CommSemiring R
⊢ (∀ (a : Ideal R) (b : a.IsPrime),
      ((PrimeSpectrum.equivSubtype R).symm ⟨a, b⟩).asIdeal ∈ minimalPrimes R ∨
        ((PrimeSpectrum.equivSubtype R).symm ⟨a, b⟩).asIdeal.IsMaximal) ↔
    ∀ (I : Ideal R), I.IsPrime → I ∈ minimalPrimes R ∨ I.IsMaximal

Tactic:
rfl

Result:
no goals

Proof state:
R : Type u_1
inst✝ : CommSemiring R
⊢ KrullDimLE 1 R ↔ ∀ (I : Ideal R), I.IsPrime → I ∈ minimalPrimes R ∨ I.IsMaximal

Tactic:
simp_rw [Ring.KrullDimLE, Order.krullDimLE_iff, Nat.cast_one,
  Order.krullDim_le_one_iff, (PrimeSpectrum.equivSubtype R).forall_congr_left,
  Subtype.forall, PrimeSpectrum.isMax_iff, PrimeSpectrum.isMin_iff]

Result:
R : Type u_1
inst✝ : CommSemiring R
⊢ (∀ (a : Ideal R) (b : a.IsPrime),
      ((PrimeSpectrum.equivSubtype R).symm ⟨a, b⟩).asIdeal ∈ minimalPrimes R ∨
        ((PrimeSpectrum.equivSubtype R).symm ⟨a, b⟩).asIdeal.IsMaximal) ↔
    ∀ (I : Ideal R), I.IsPrime → I ∈ minimalPrimes R ∨ I.IsMaximal
-- Mathlib/NumberTheory/NumberField/FinitePlaces.lean
theorem FinitePlace.norm_eq_one_iff_not_mem (x : 𝓞 (WithVal (v.valuation K))) :
    ‖embedding v x‖ = 1 ↔ x ∉ v.asIdeal

Proof state:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
v : HeightOneSpectrum (𝓞 K)
x : 𝓞 (WithVal (valuation K v))
⊢ v.intValuationDef x = 1 ↔ 1 ≤ v.intValuationDef x

Tactic:
exact (intValuation_le_one v x).ge_iff_eq.symm

Result:
no goals

Proof state:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
v : HeightOneSpectrum (𝓞 K)
x : 𝓞 (WithVal (valuation K v))
⊢ ‖(embedding v) ↑x‖ = 1 ↔ x ∉ v.asIdeal

Tactic:
rw [norm_def_int, NNReal.coe_eq_one, toNNReal_eq_one_iff (v.intValuationDef x)
  (absNorm_ne_zero v) (one_lt_absNorm_nnreal v).ne', ← dvd_span_singleton,
  ← intValuation_lt_one_iff_dvd, not_lt]

Result:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
v : HeightOneSpectrum (𝓞 K)
x : 𝓞 (WithVal (valuation K v))
⊢ v.intValuationDef x = 1 ↔ 1 ≤ v.intValuationDef x
-- Mathlib/Combinatorics/Young/YoungDiagram.lean
theorem le_of_transpose_le {μ ν : YoungDiagram} (h_le : μ.transpose ≤ ν) :
    μ ≤ ν.transpose := fun c hc => by
  simp only [mem_cells, mem_transpose]
  apply h_le
  simpa

Proof state:
μ ν : YoungDiagram
h_le : μ.transpose ≤ ν
c : ℕ × ℕ
hc : c ∈ μ.cells
⊢ c ∈ ν.transpose.cells

Tactic:
simp only [mem_cells, mem_transpose]

Result:
μ ν : YoungDiagram
h_le : μ.transpose ≤ ν
c : ℕ × ℕ
hc : c ∈ μ.cells
⊢ c.swap ∈ ν

Proof state:
case a
μ ν : YoungDiagram
h_le : μ.transpose ≤ ν
c : ℕ × ℕ
hc : c ∈ μ.cells
⊢ c.swap ∈ μ.transpose.cells

Tactic:
simpa

Result:
no goals

Proof state:
μ ν : YoungDiagram
h_le : μ.transpose ≤ ν
c : ℕ × ℕ
hc : c ∈ μ.cells
⊢ c.swap ∈ ν

Tactic:
apply h_le

Result:
case a
μ ν : YoungDiagram
h_le : μ.transpose ≤ ν
c : ℕ × ℕ
hc : c ∈ μ.cells
⊢ c.swap ∈ μ.transpose.cells
-- Mathlib/Analysis/Convex/AmpleSet.lean
theorem union {s t : Set F} (hs : AmpleSet s) (ht : AmpleSet t) : AmpleSet (s ∪ t)

Proof state:
F : Type u_1
inst✝² : AddCommGroup F
inst✝¹ : Module ℝ F
inst✝ : TopologicalSpace F
s t : Set F
hs : AmpleSet s
ht : AmpleSet t
x : F
hx : x ∈ s ∪ t
⊢ (convexHull ℝ) (connectedComponentIn (s ∪ t) x) = univ

Tactic:
rcases hx with (h | h) <;>
[have hx := hs x h; have hx := ht x h] <;>
rw [← Set.univ_subset_iff, ← hx] <;>
apply convexHull_mono <;>
apply connectedComponentIn_mono <;>
[apply subset_union_left; apply subset_union_right]

Result:
no goals

Proof state:
F : Type u_1
inst✝² : AddCommGroup F
inst✝¹ : Module ℝ F
inst✝ : TopologicalSpace F
s t : Set F
hs : AmpleSet s
ht : AmpleSet t
⊢ AmpleSet (s ∪ t)

Tactic:
intro x hx

Result:
F : Type u_1
inst✝² : AddCommGroup F
inst✝¹ : Module ℝ F
inst✝ : TopologicalSpace F
s t : Set F
hs : AmpleSet s
ht : AmpleSet t
x : F
hx : x ∈ s ∪ t
⊢ (convexHull ℝ) (connectedComponentIn (s ∪ t) x) = univ
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Attach.lean
theorem unattach_filter {p : α → Prop} {l : Array { x // p x }}
    {f : { x // p x } → Bool} {g : α → Bool} (hf : ∀ x h, f ⟨x, h⟩ = g x) :
    (l.filter f).unattach = l.unattach.filter g

Proof state:
α : Type u_1
p : α → Prop
l : Array { x // p x }
f : { x // p x } → Bool
g : α → Bool
hf : ∀ (x : α) (h : p x), f ⟨x, h⟩ = g x
⊢ (filter f l).unattach = filter g l.unattach

Tactic:
cases l

Result:
case mk
α : Type u_1
p : α → Prop
f : { x // p x } → Bool
g : α → Bool
hf : ∀ (x : α) (h : p x), f ⟨x, h⟩ = g x
toList✝ : List { x // p x }
⊢ (filter f { toList := toList✝ }).unattach = filter g { toList := toList✝ }.unattach

Proof state:
case mk
α : Type u_1
p : α → Prop
f : { x // p x } → Bool
g : α → Bool
hf : ∀ (x : α) (h : p x), f ⟨x, h⟩ = g x
toList✝ : List { x // p x }
⊢ (filter f { toList := toList✝ }).unattach = filter g { toList := toList✝ }.unattach

Tactic:
simp [hf]

Result:
no goals
-- Mathlib/LinearAlgebra/LinearIndependent/Defs.lean
theorem LinearIndependent.injective [Nontrivial R] (hv : LinearIndependent R v) : Injective v

Proof state:
ι : Type u'
R : Type u_2
M : Type u_4
v : ι → M
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Nontrivial R
hv : LinearIndependent R v
⊢ Injective v

Tactic:
simpa [comp_def]
  using Injective.comp hv (Finsupp.single_left_injective one_ne_zero)

Result:
no goals
-- Mathlib/Order/Interval/Set/Basic.lean
theorem Ioc_diff_Ioi : Ioc a b \ Ioi c = Ioc a (min b c) :=
  ext <| by simp +contextual [iff_def]

Proof state:
α : Type u_1
inst✝ : LinearOrder α
a b c : α
⊢ ∀ (x : α), x ∈ Ioc a b \ Ioi c ↔ x ∈ Ioc a (b ⊓ c)

Tactic:
simp +contextual [iff_def]

Result:
no goals
-- Mathlib/Data/Fintype/Powerset.lean
theorem Fintype.card_finset_len [Fintype α] (k : ℕ) :
    Fintype.card { s : Finset α // #s = k } = Nat.choose (Fintype.card α) k

Proof state:
α : Type u_1
inst✝ : Fintype α
k : ℕ
⊢ card { s // #s = k } = (card α).choose k

Tactic:
simp [Fintype.subtype_card, Finset.card_univ]

Result:
no goals
-- Mathlib/Topology/UniformSpace/Pi.lean
lemma Pi.uniformSpace_comap_precomp' (φ : ι' → ι) :
    UniformSpace.comap (fun g i' ↦ g (φ i')) (Pi.uniformSpace (fun i' ↦ α (φ i'))) =
    ⨅ i', UniformSpace.comap (eval (φ i')) (U (φ i'))

Proof state:
ι : Type u_1
ι' : Type u_2
α : ι → Type u
U : (i : ι) → UniformSpace (α i)
φ : ι' → ι
⊢ UniformSpace.comap (fun g i' => g (φ i')) (uniformSpace fun i' => α (φ i')) =
    ⨅ i', UniformSpace.comap (eval (φ i')) (U (φ i'))

Tactic:
simp [Pi.uniformSpace_eq, UniformSpace.comap_iInf, ← UniformSpace.comap_comap, comp_def]

Result:
no goals
-- Mathlib/RingTheory/AdjoinRoot.lean
theorem minpoly_powerBasis_gen (hf : f ≠ 0) :
    minpoly K (powerBasis hf).gen = f * C f.leadingCoeff⁻¹

Proof state:
K : Type w
inst✝ : Field K
f : K[X]
hf : f ≠ 0
⊢ minpoly K (powerBasis hf).gen = f * C f.leadingCoeff⁻¹

Tactic:
rw [powerBasis_gen, minpoly_root hf]

Result:
no goals
-- Mathlib/Data/Int/Init.lean
lemma pred_neg_pred (a : ℤ) : pred (-pred a) = -a

Proof state:
a : ℤ
⊢ (-a.pred).pred = -a

Tactic:
rw [neg_pred, pred_succ]

Result:
no goals
-- Mathlib/Order/Monotone/MonovaryOrder.lean
lemma monovary_iff_exists_antitone :
    Monovary f g ↔ ∃ (_ : LinearOrder ι), Antitone f ∧ Antitone g

Proof state:
ι : Type u_1
α : Type u_3
β : Type u_4
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : ι → α
g : ι → β
⊢ Monovary f g ↔ ∃ x, Antitone f ∧ Antitone g

Tactic:
simp [← monovaryOn_univ, monovaryOn_iff_exists_antitoneOn]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Trigonometric/Basic.lean
theorem sqrtTwoAddSeries_zero : sqrtTwoAddSeries x 0 = x

Proof state:
x : ℝ
⊢ x.sqrtTwoAddSeries 0 = x

Tactic:
simp

Result:
no goals
-- Mathlib/Topology/MetricSpace/Pseudo/Defs.lean
theorem closedBall_diff_ball : closedBall x ε \ ball x ε = sphere x ε

Proof state:
α : Type u
inst✝ : PseudoMetricSpace α
x : α
ε : ℝ
⊢ closedBall x ε \ ball x ε = sphere x ε

Tactic:
rw [← ball_union_sphere, Set.union_diff_cancel_left sphere_disjoint_ball.symm.le_bot]

Result:
no goals
-- Mathlib/Data/Finsupp/Fin.lean
theorem tail_update_zero : tail (update t 0 y) = tail t

Proof state:
n : ℕ
M : Type u_1
inst✝ : Zero M
y : M
t : Fin (n + 1) →₀ M
⊢ (t.update 0 y).tail = t.tail

Tactic:
simp [tail]

Result:
no goals
-- Mathlib/MeasureTheory/Integral/Prod.lean
theorem measurableSet_integrable [SFinite ν] ⦃f : α → β → E⦄
    (hf : StronglyMeasurable (uncurry f)) : MeasurableSet {x | Integrable (f x) ν}

Proof state:
α : Type u_1
β : Type u_2
E : Type u_3
inst✝³ : MeasurableSpace α
inst✝² : MeasurableSpace β
ν : Measure β
inst✝¹ : NormedAddCommGroup E
inst✝ : SFinite ν
f : α → β → E
hf : StronglyMeasurable (uncurry f)
⊢ MeasurableSet {x | HasFiniteIntegral (f x) ν}

Tactic:
exact measurableSet_lt (Measurable.lintegral_prod_right hf.enorm) measurable_const

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
E : Type u_3
inst✝³ : MeasurableSpace α
inst✝² : MeasurableSpace β
ν : Measure β
inst✝¹ : NormedAddCommGroup E
inst✝ : SFinite ν
f : α → β → E
hf : StronglyMeasurable (uncurry f)
⊢ MeasurableSet {x | Integrable (f x) ν}

Tactic:
simp_rw [Integrable, hf.of_uncurry_left.aestronglyMeasurable, true_and]

Result:
α : Type u_1
β : Type u_2
E : Type u_3
inst✝³ : MeasurableSpace α
inst✝² : MeasurableSpace β
ν : Measure β
inst✝¹ : NormedAddCommGroup E
inst✝ : SFinite ν
f : α → β → E
hf : StronglyMeasurable (uncurry f)
⊢ MeasurableSet {x | HasFiniteIntegral (f x) ν}
-- Mathlib/Algebra/CubicDiscriminant.lean
theorem degree_of_c_eq_zero (ha : P.a = 0) (hb : P.b = 0) (hc : P.c = 0) : P.toPoly.degree ≤ 0

Proof state:
R : Type u_1
P : Cubic R
inst✝ : Semiring R
ha : P.a = 0
hb : P.b = 0
hc : P.c = 0
⊢ P.toPoly.degree ≤ 0

Tactic:
simpa only [of_c_eq_zero ha hb hc] using degree_C_le

Result:
no goals
-- Mathlib/Tactic/CategoryTheory/Monoidal/Normalize.lean
theorem evalWhiskerRight_comp {f f' g h : C}
    {η : f ⟶ f'} {η₁ : f ⊗ g ⟶ f' ⊗ g} {η₂ : (f ⊗ g) ⊗ h ⟶ (f' ⊗ g) ⊗ h}
    {η₃ : (f ⊗ g) ⊗ h ⟶ f' ⊗ (g ⊗ h)} {η₄ : f ⊗ (g ⊗ h) ⟶ f' ⊗ (g ⊗ h)}
    (e_η₁ : η ▷ g = η₁) (e_η₂ : η₁ ▷ h = η₂)
    (e_η₃ : η₂ ≫ (α_ _ _ _).hom = η₃) (e_η₄ : (α_ _ _ _).inv ≫ η₃ = η₄) :
    η ▷ (g ⊗ h) = η₄

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : MonoidalCategory C
f f' g h : C
η : f ⟶ f'
η₁ : f ⊗ g ⟶ f' ⊗ g
η₂ : (f ⊗ g) ⊗ h ⟶ (f' ⊗ g) ⊗ h
η₃ : (f ⊗ g) ⊗ h ⟶ f' ⊗ g ⊗ h
η₄ : f ⊗ g ⊗ h ⟶ f' ⊗ g ⊗ h
e_η₁ : η ▷ g = η₁
e_η₂ : η₁ ▷ h = η₂
e_η₃ : η₂ ≫ (α_ f' g h).hom = η₃
e_η₄ : (α_ f g h).inv ≫ η₃ = η₄
⊢ η ▷ (g ⊗ h) = η₄

Tactic:
simp [e_η₁, e_η₂, e_η₃, e_η₄]

Result:
no goals
-- Mathlib/.lake/packages/batteries/Batteries/Data/RBMap/Lemmas.lean
theorem foldr_eq_foldr_toList {t : RBNode α} : t.foldr f init = t.toList.foldr f init

Proof state:
α : Type u_1
α✝ : Type u_2
f : α → α✝ → α✝
init : α✝
t : RBNode α
⊢ foldr f t init = List.foldr f init t.toList

Tactic:
induction t generalizing init <;> simp [*]

Result:
no goals
-- Mathlib/Topology/MetricSpace/HausdorffDimension.lean
theorem dimH_image_le_of_locally_lipschitzOn [SecondCountableTopology X] {f : X → Y} {s : Set X}
    (hf : ∀ x ∈ s, ∃ C : ℝ≥0, ∃ t ∈ 𝓝[s] x, LipschitzOnWith C f t) : dimH (f '' s) ≤ dimH s

Proof state:
X : Type u_2
Y : Type u_3
inst✝² : EMetricSpace X
inst✝¹ : EMetricSpace Y
inst✝ : SecondCountableTopology X
f : X → Y
s : Set X
hf : ∀ x ∈ s, ∃ C, ∃ t ∈ 𝓝[s] x, LipschitzOnWith C f t
⊢ dimH (f '' s) ≤ dimH s

Tactic:
have : ∀ x ∈ s, ∃ C : ℝ≥0, ∃ t ∈ 𝓝[s] x, HolderOnWith C 1 f t := by
  simpa only [holderOnWith_one] using hf

Result:
X : Type u_2
Y : Type u_3
inst✝² : EMetricSpace X
inst✝¹ : EMetricSpace Y
inst✝ : SecondCountableTopology X
f : X → Y
s : Set X
hf : ∀ x ∈ s, ∃ C, ∃ t ∈ 𝓝[s] x, LipschitzOnWith C f t
this : ∀ x ∈ s, ∃ C, ∃ t ∈ 𝓝[s] x, HolderOnWith C 1 f t
⊢ dimH (f '' s) ≤ dimH s

Proof state:
X : Type u_2
Y : Type u_3
inst✝² : EMetricSpace X
inst✝¹ : EMetricSpace Y
inst✝ : SecondCountableTopology X
f : X → Y
s : Set X
hf : ∀ x ∈ s, ∃ C, ∃ t ∈ 𝓝[s] x, LipschitzOnWith C f t
this : ∀ x ∈ s, ∃ C, ∃ t ∈ 𝓝[s] x, HolderOnWith C 1 f t
⊢ dimH (f '' s) ≤ dimH s

Tactic:
simpa only [ENNReal.coe_one, div_one] using dimH_image_le_of_locally_holder_on zero_lt_one this

Result:
no goals

Proof state:
X : Type u_2
Y : Type u_3
inst✝² : EMetricSpace X
inst✝¹ : EMetricSpace Y
inst✝ : SecondCountableTopology X
f : X → Y
s : Set X
hf : ∀ x ∈ s, ∃ C, ∃ t ∈ 𝓝[s] x, LipschitzOnWith C f t
⊢ ∀ x ∈ s, ∃ C, ∃ t ∈ 𝓝[s] x, HolderOnWith C 1 f t

Tactic:
simpa only [holderOnWith_one] using hf

Result:
no goals
-- Mathlib/Data/DFinsupp/Order.lean
theorem single_le_iff {f : Π₀ i, α i} {i : ι} {a : α i} :
    single i a ≤ f ↔ a ≤ f i

Proof state:
ι : Type u_1
α : ι → Type u_2
inst✝³ : (i : ι) → AddCommMonoid (α i)
inst✝² : (i : ι) → PartialOrder (α i)
inst✝¹ : ∀ (i : ι), CanonicallyOrderedAdd (α i)
inst✝ : DecidableEq ι
f : Π₀ (i : ι), α i
i : ι
a : α i
⊢ single i a ≤ f ↔ a ≤ f i

Tactic:
exact (le_iff' support_single_subset).trans <| by simp

Result:
no goals

Proof state:
ι : Type u_1
α : ι → Type u_2
inst✝³ : (i : ι) → AddCommMonoid (α i)
inst✝² : (i : ι) → PartialOrder (α i)
inst✝¹ : ∀ (i : ι), CanonicallyOrderedAdd (α i)
inst✝ : DecidableEq ι
f : Π₀ (i : ι), α i
i : ι
a : α i
⊢ (∀ i_1 ∈ {i}, (single i a) i_1 ≤ f i_1) ↔ a ≤ f i

Tactic:
simp

Result:
no goals

Proof state:
ι : Type u_1
α : ι → Type u_2
inst✝³ : (i : ι) → AddCommMonoid (α i)
inst✝² : (i : ι) → PartialOrder (α i)
inst✝¹ : ∀ (i : ι), CanonicallyOrderedAdd (α i)
inst✝ : DecidableEq ι
f : Π₀ (i : ι), α i
i : ι
a : α i
⊢ single i a ≤ f ↔ a ≤ f i

Tactic:
classical exact (le_iff' support_single_subset).trans <| by simp

Result:
no goals
-- Mathlib/Data/Nat/Init.lean
lemma one_mod_eq_one : ∀ {n : ℕ}, 1 % n = 1 ↔ n ≠ 1
  | 0 | 1 | n + 2 => by simp

Proof state:
n : ℕ
⊢ 1 % (n + 2) = 1 ↔ n + 2 ≠ 1

Tactic:
simp

Result:
no goals
-- Mathlib/Data/Nat/Init.lean
lemma pred_sub (n m : ℕ) : pred n - m = pred (n - m)

Proof state:
n m : ℕ
⊢ n.pred - m = (n - m).pred

Tactic:
rw [← Nat.sub_one, Nat.sub_sub, one_add, sub_succ]

Result:
no goals
-- Mathlib/Algebra/Lie/Derivation/Killing.lean
/-- The restriction of the Killing form of a finite-dimensional Killing Lie algebra to the range of
the adjoint action is nondegenerate. -/
lemma killingForm_restrict_range_ad_nondegenerate :
    ((killingForm R 𝔻).restrict 𝕀).Nondegenerate

Proof state:
R : Type u_1
L : Type u_2
inst✝⁴ : Field R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
inst✝¹ : Module.Finite R L
inst✝ : LieAlgebra.IsKilling R L
⊢ ((killingForm R (LieDerivation R L L)).restrict (ad R L).range.toSubmodule).Nondegenerate

Tactic:
convert LieAlgebra.IsKilling.killingForm_nondegenerate R 𝕀

Result:
case h.e'_6.h.h.h
R : Type u_1
L : Type u_2
inst✝⁴ : Field R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
inst✝¹ : Module.Finite R L
inst✝ : LieAlgebra.IsKilling R L
e_2✝ : ↥(ad R L).range.toSubmodule = ↥(ad R L).range
he✝¹ : (ad R L).range.addCommMonoid = AddCommGroup.toAddCommMonoid
he✝ : (ad R L).range.module = LieAlgebra.toModule
⊢ (killingForm R (LieDerivation R L L)).restrict (ad R L).range.toSubmodule = killingForm R ↥(ad R L).range

Proof state:
case h.e'_6.h.h.h
R : Type u_1
L : Type u_2
inst✝⁴ : Field R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
inst✝¹ : Module.Finite R L
inst✝ : LieAlgebra.IsKilling R L
e_2✝ : ↥(ad R L).range.toSubmodule = ↥(ad R L).range
he✝¹ : (ad R L).range.addCommMonoid = AddCommGroup.toAddCommMonoid
he✝ : (ad R L).range.module = LieAlgebra.toModule
⊢ (killingForm R (LieDerivation R L L)).restrict (ad R L).range.toSubmodule = killingForm R ↥(ad R L).range

Tactic:
exact killingForm_restrict_range_ad R L

Result:
no goals
-- Mathlib/Computability/MyhillNerode.lean
theorem IsRegular.of_finite_range_leftQuotient (h : Set.Finite (Set.range L.leftQuotient)) :
    L.IsRegular :=
  Language.isRegular_iff.mpr ⟨_, h.fintype, L.toDFA, by simp⟩

Proof state:
α : Type u
L : Language α
h : (Set.range L.leftQuotient).Finite
⊢ L.toDFA.accepts = L

Tactic:
simp

Result:
no goals
-- Mathlib/RingTheory/WittVector/InitTail.lean
theorem init_mul (x y : 𝕎 R) (n : ℕ) : init n (x * y) = init n (init n x * init n y)

Proof state:
p : ℕ
R : Type u_1
inst✝¹ : CommRing R
inst✝ : Fact (Nat.Prime p)
x y : 𝕎 R
n : ℕ
⊢ init n (x * y) = init n (init n x * init n y)

Tactic:
init_ring using wittMul_vars

Result:
no goals
-- Mathlib/Data/ENNReal/Inv.lean
/-- Very general version for distributivity of division over an infimum.

See `ENNReal.iInf_div_of_ne` for the special case assuming `a ≠ 0` and `a ≠ ∞`, and
`ENNReal.iInf_div` for the special case assuming `Nonempty ι`. -/
lemma iInf_div' (hinfty : a = 0 → ⨅ i, f i = 0 → ∃ i, f i = 0) (h₀ : a = ∞ → Nonempty ι) :
    (⨅ i, f i) / a = ⨅ i, f i / a := iInf_mul' (by simpa) (by simpa)

Proof state:
ι : Sort u_1
f : ι → ℝ≥0∞
a : ℝ≥0∞
hinfty : a = 0 → ⨅ i, f i = 0 → ∃ i, f i = 0
h₀ : a = ⊤ → Nonempty ι
⊢ a⁻¹ = 0 → Nonempty ι

Tactic:
simpa

Result:
no goals

Proof state:
ι : Sort u_1
f : ι → ℝ≥0∞
a : ℝ≥0∞
hinfty : a = 0 → ⨅ i, f i = 0 → ∃ i, f i = 0
h₀ : a = ⊤ → Nonempty ι
⊢ a⁻¹ = ⊤ → ⨅ i, f i = 0 → ∃ i, f i = 0

Tactic:
simpa

Result:
no goals