harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Probability/Kernel/Disintegration/Integral.lean
lemma lintegral_condKernel_mem {s : Set (β × Ω)} (hs : MeasurableSet s) :
    ∫⁻ x, ρ.condKernel x {y | (x, y) ∈ s} ∂ρ.fst = ρ s

Proof state:
β : Type u_1
Ω : Type u_2
mβ : MeasurableSpace β
inst✝³ : MeasurableSpace Ω
inst✝² : StandardBorelSpace Ω
inst✝¹ : Nonempty Ω
ρ : Measure (β × Ω)
inst✝ : IsFiniteMeasure ρ
s : Set (β × Ω)
hs : MeasurableSet s
⊢ ∫⁻ (x : β), (ρ.condKernel x) {y | (x, y) ∈ s} ∂ρ.fst = ∫⁻ (a : β), (ρ.condKernel a) (Prod.mk a ⁻¹' s) ∂ρ.fst

Tactic:
rfl

Result:
no goals

Proof state:
β : Type u_1
Ω : Type u_2
mβ : MeasurableSpace β
inst✝³ : MeasurableSpace Ω
inst✝² : StandardBorelSpace Ω
inst✝¹ : Nonempty Ω
ρ : Measure (β × Ω)
inst✝ : IsFiniteMeasure ρ
s : Set (β × Ω)
hs : MeasurableSet s
⊢ ∫⁻ (x : β), (ρ.condKernel x) {y | (x, y) ∈ s} ∂ρ.fst = (ρ.fst ⊗ₘ ρ.condKernel) s

Tactic:
simp_rw [compProd_apply hs]

Result:
β : Type u_1
Ω : Type u_2
mβ : MeasurableSpace β
inst✝³ : MeasurableSpace Ω
inst✝² : StandardBorelSpace Ω
inst✝¹ : Nonempty Ω
ρ : Measure (β × Ω)
inst✝ : IsFiniteMeasure ρ
s : Set (β × Ω)
hs : MeasurableSet s
⊢ ∫⁻ (x : β), (ρ.condKernel x) {y | (x, y) ∈ s} ∂ρ.fst = ∫⁻ (a : β), (ρ.condKernel a) (Prod.mk a ⁻¹' s) ∂ρ.fst

Proof state:
β : Type u_1
Ω : Type u_2
mβ : MeasurableSpace β
inst✝³ : MeasurableSpace Ω
inst✝² : StandardBorelSpace Ω
inst✝¹ : Nonempty Ω
ρ : Measure (β × Ω)
inst✝ : IsFiniteMeasure ρ
s : Set (β × Ω)
hs : MeasurableSet s
⊢ ∫⁻ (x : β), (ρ.condKernel x) {y | (x, y) ∈ s} ∂ρ.fst = ρ s

Tactic:
conv_rhs => rw [← ρ.disintegrate ρ.condKernel]

Result:
β : Type u_1
Ω : Type u_2
mβ : MeasurableSpace β
inst✝³ : MeasurableSpace Ω
inst✝² : StandardBorelSpace Ω
inst✝¹ : Nonempty Ω
ρ : Measure (β × Ω)
inst✝ : IsFiniteMeasure ρ
s : Set (β × Ω)
hs : MeasurableSet s
⊢ ∫⁻ (x : β), (ρ.condKernel x) {y | (x, y) ∈ s} ∂ρ.fst = (ρ.fst ⊗ₘ ρ.condKernel) s
-- Mathlib/Algebra/Ring/Subsemiring/Basic.lean
theorem mem_sSup_of_directedOn {S : Set (Subsemiring R)} (Sne : S.Nonempty)
    (hS : DirectedOn (· ≤ ·) S) {x : R} : x ∈ sSup S ↔ ∃ s ∈ S, x ∈ s

Proof state:
R : Type u
inst✝ : NonAssocSemiring R
S : Set (Subsemiring R)
Sne : S.Nonempty
hS : DirectedOn (fun x1 x2 => x1 ≤ x2) S
x : R
this : Nonempty ↑S
⊢ x ∈ sSup S ↔ ∃ s ∈ S, x ∈ s

Tactic:
simp only [sSup_eq_iSup', mem_iSup_of_directed hS.directed_val, SetCoe.exists, Subtype.coe_mk,
  exists_prop]

Result:
no goals

Proof state:
R : Type u
inst✝ : NonAssocSemiring R
S : Set (Subsemiring R)
Sne : S.Nonempty
hS : DirectedOn (fun x1 x2 => x1 ≤ x2) S
x : R
⊢ x ∈ sSup S ↔ ∃ s ∈ S, x ∈ s

Tactic:
haveI : Nonempty S := Sne.to_subtype

Result:
R : Type u
inst✝ : NonAssocSemiring R
S : Set (Subsemiring R)
Sne : S.Nonempty
hS : DirectedOn (fun x1 x2 => x1 ≤ x2) S
x : R
this : Nonempty ↑S
⊢ x ∈ sSup S ↔ ∃ s ∈ S, x ∈ s
-- Mathlib/Order/Interval/Finset/Basic.lean
theorem Icc_subset_Iic_self : Icc a b ⊆ Iic b

Proof state:
α : Type u_2
a b : α
inst✝² : Preorder α
inst✝¹ : LocallyFiniteOrderBot α
inst✝ : LocallyFiniteOrder α
⊢ Icc a b ⊆ Iic b

Tactic:
simpa [← coe_subset] using Set.Icc_subset_Iic_self

Result:
no goals
-- Mathlib/CategoryTheory/Monoidal/Category.lean
theorem comp_whiskerRight {W X Y : C} (f : W ⟶ X) (g : X ⟶ Y) (Z : C) :
    (f ≫ g) ▷ Z = f ▷ Z ≫ g ▷ Z

Proof state:
C : Type u
𝒞 : Category.{v, u} C
inst✝ : MonoidalCategory C
W X Y : C
f : W ⟶ X
g : X ⟶ Y
Z : C
⊢ (f ≫ g) ▷ Z = f ▷ Z ≫ g ▷ Z

Tactic:
simp only [← tensorHom_id, ← tensor_comp, id_comp]

Result:
no goals
-- Mathlib/Data/PFun.lean
theorem mem_dom (f : α →. β) (x : α) : x ∈ Dom f ↔ ∃ y, y ∈ f x

Proof state:
α : Type u_1
β : Type u_2
f : α →. β
x : α
⊢ x ∈ f.Dom ↔ ∃ y, y ∈ f x

Tactic:
simp [Dom, Part.dom_iff_mem]

Result:
no goals
-- Mathlib/RingTheory/Valuation/Basic.lean
theorem map_sub (x y : R) : v (x - y) ≤ max (v x) (v y) :=
  calc
    v (x - y) = v (x + -y)

Proof state:
R : Type u_3
Γ₀ : Type u_4
inst✝¹ : Ring R
inst✝ : LinearOrderedCommMonoidWithZero Γ₀
v : Valuation R Γ₀
x y : R
⊢ v (x - y) = v (x + -y)

Tactic:
rw [sub_eq_add_neg]

Result:
no goals

Proof state:
R : Type u_3
Γ₀ : Type u_4
inst✝¹ : Ring R
inst✝ : LinearOrderedCommMonoidWithZero Γ₀
v : Valuation R Γ₀
x y : R
⊢ v x ⊔ v (-y) = v x ⊔ v y

Tactic:
rw [map_neg]

Result:
no goals
-- Mathlib/Algebra/BigOperators/Group/Finset/Basic.lean
theorem prod_sumElim (s : Finset α) (t : Finset γ) (f : α → β) (g : γ → β) :
    ∏ x ∈ s.disjSum t, Sum.elim f g x = (∏ x ∈ s, f x) * ∏ x ∈ t, g x

Proof state:
α : Type u_3
β : Type u_4
γ : Type u_5
inst✝ : CommMonoid β
s : Finset α
t : Finset γ
f : α → β
g : γ → β
⊢ ∏ x ∈ s.disjSum t, Sum.elim f g x = (∏ x ∈ s, f x) * ∏ x ∈ t, g x

Tactic:
simp

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/RawLemmas.lean
theorem get!_of_isEmpty [EquivBEq α] [LawfulHashable α] [Inhabited β] (h : m.1.WF) {a : α} :
    m.1.isEmpty = true → get! m a = default

Proof state:
α : Type u
inst✝⁴ : BEq α
inst✝³ : Hashable α
β : Type v
m : Raw₀ α fun x => β
inst✝² : EquivBEq α
inst✝¹ : LawfulHashable α
inst✝ : Inhabited β
h : m.val.WF
a : α
⊢ (toListModel m.val.buckets).isEmpty = true → getValue! a (toListModel m.val.buckets) = default

Tactic:
empty

Result:
no goals

Proof state:
α : Type u
inst✝⁴ : BEq α
inst✝³ : Hashable α
β : Type v
m : Raw₀ α fun x => β
inst✝² : EquivBEq α
inst✝¹ : LawfulHashable α
inst✝ : Inhabited β
h : m.val.WF
a : α
⊢ m.val.isEmpty = true → get! m a = default

Tactic:
simp_to_model

Result:
α : Type u
inst✝⁴ : BEq α
inst✝³ : Hashable α
β : Type v
m : Raw₀ α fun x => β
inst✝² : EquivBEq α
inst✝¹ : LawfulHashable α
inst✝ : Inhabited β
h : m.val.WF
a : α
⊢ (toListModel m.val.buckets).isEmpty = true → getValue! a (toListModel m.val.buckets) = default
-- Mathlib/Order/UpperLower/Basic.lean
theorem compl_iInf₂ (f : ∀ i, κ i → LowerSet α) :
    (⨅ (i) (j), f i j).compl = ⨅ (i) (j), (f i j).compl

Proof state:
α : Type u_1
ι : Sort u_4
κ : ι → Sort u_5
inst✝ : LE α
f : (i : ι) → κ i → LowerSet α
⊢ (⨅ i, ⨅ j, f i j).compl = ⨅ i, ⨅ j, (f i j).compl

Tactic:
simp_rw [LowerSet.compl_iInf]

Result:
no goals
-- Mathlib/Analysis/Calculus/Conformal/InnerProduct.lean
theorem conformalAt_iff' {f : E → F} {x : E} : ConformalAt f x ↔
    ∃ c : ℝ, 0 < c ∧ ∀ u v : E, ⟪fderiv ℝ f x u, fderiv ℝ f x v⟫ = c * ⟪u, v⟫

Proof state:
E : Type u_1
F : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace ℝ E
inst✝ : InnerProductSpace ℝ F
f : E → F
x : E
⊢ ConformalAt f x ↔ ∃ c, 0 < c ∧ ∀ (u v : E), inner ((fderiv ℝ f x) u) ((fderiv ℝ f x) v) = c * inner u v

Tactic:
rw [conformalAt_iff_isConformalMap_fderiv, isConformalMap_iff]

Result:
no goals
-- Mathlib/NumberTheory/SmoothNumbers.lean
lemma mem_smoothNumbersUpTo {N k n : ℕ} :
    n ∈ smoothNumbersUpTo N k ↔ n ≤ N ∧ n ∈ smoothNumbers k

Proof state:
N k n : ℕ
⊢ n ∈ N.smoothNumbersUpTo k ↔ n ≤ N ∧ n ∈ k.smoothNumbers

Tactic:
simp [smoothNumbersUpTo, lt_succ]

Result:
no goals
-- Mathlib/Data/Complex/Trigonometric.lean
theorem sin_sub : sin (x - y) = sin x * cos y - cos x * sin y

Proof state:
x y : ℂ
⊢ sin (x - y) = sin x * cos y - cos x * sin y

Tactic:
simp [sub_eq_add_neg, sin_add, sin_neg, cos_neg]

Result:
no goals
-- Mathlib/Order/Closure.lean
theorem closure_sup_closure_right (x y : α) : c (x ⊔ c y) = c (x ⊔ y)

Proof state:
α : Type u_1
inst✝ : SemilatticeSup α
c : ClosureOperator α
x y : α
⊢ c (x ⊔ c y) = c (x ⊔ y)

Tactic:
rw [sup_comm, closure_sup_closure_left, sup_comm (a := x)]

Result:
no goals
-- Mathlib/MeasureTheory/Integral/BoundedContinuousFunction.lean
lemma apply_le_nndist_zero {X : Type*} [TopologicalSpace X] (f : X →ᵇ ℝ≥0) (x : X) :
    f x ≤ nndist 0 f

Proof state:
case h.e'_3
X : Type u_1
inst✝ : TopologicalSpace X
f : X →ᵇ ℝ≥0
x : X
⊢ f x = nndist (0 x) (f x)

Tactic:
simp only [coe_zero, Pi.zero_apply, NNReal.nndist_zero_eq_val]

Result:
no goals

Proof state:
X : Type u_1
inst✝ : TopologicalSpace X
f : X →ᵇ ℝ≥0
x : X
⊢ f x ≤ nndist 0 f

Tactic:
convert nndist_coe_le_nndist x

Result:
case h.e'_3
X : Type u_1
inst✝ : TopologicalSpace X
f : X →ᵇ ℝ≥0
x : X
⊢ f x = nndist (0 x) (f x)
-- Mathlib/Logic/IsEmpty.lean
theorem isEmpty_ulift {α} : IsEmpty (ULift α) ↔ IsEmpty α

Proof state:
α : Type u_4
⊢ IsEmpty (ULift.{u_5, u_4} α) ↔ IsEmpty α

Tactic:
simp only [← not_nonempty_iff, nonempty_ulift]

Result:
no goals
-- Mathlib/Algebra/BigOperators/Group/Finset/Basic.lean
theorem card_biUnion [DecidableEq β] {s : Finset α} {t : α → Finset β}
    (h : ∀ x ∈ s, ∀ y ∈ s, x ≠ y → Disjoint (t x) (t y)) : #(s.biUnion t) = ∑ u ∈ s, #(t u)

Proof state:
α : Type u_3
β : Type u_4
inst✝ : DecidableEq β
s : Finset α
t : α → Finset β
h : ∀ x ∈ s, ∀ y ∈ s, x ≠ y → Disjoint (t x) (t y)
⊢ #(s.biUnion t) = ∑ u ∈ s, #(t u)

Tactic:
simpa using sum_biUnion h (β := ℕ) (f := 1)

Result:
no goals
-- Mathlib/Data/Int/Log.lean
theorem log_one_left (r : R) : log 1 r = 0

Proof state:
case neg
R : Type u_1
inst✝¹ : LinearOrderedSemifield R
inst✝ : FloorSemiring R
r : R
hr : ¬1 ≤ r
⊢ log 1 r = 0

Tactic:
simp only [log, Nat.log_one_left, Nat.cast_zero, Nat.clog_one_left, neg_zero, ite_self]

Result:
no goals

Proof state:
R : Type u_1
inst✝¹ : LinearOrderedSemifield R
inst✝ : FloorSemiring R
r : R
⊢ log 1 r = 0

Tactic:
by_cases hr : 1 ≤ r

Result:
case pos
R : Type u_1
inst✝¹ : LinearOrderedSemifield R
inst✝ : FloorSemiring R
r : R
hr : 1 ≤ r
⊢ log 1 r = 0

case neg
R : Type u_1
inst✝¹ : LinearOrderedSemifield R
inst✝ : FloorSemiring R
r : R
hr : ¬1 ≤ r
⊢ log 1 r = 0

Proof state:
case pos
R : Type u_1
inst✝¹ : LinearOrderedSemifield R
inst✝ : FloorSemiring R
r : R
hr : 1 ≤ r
⊢ log 1 r = 0

Tactic:
simp_all only [log, ↓reduceIte, Nat.log_one_left, Nat.cast_zero]

Result:
no goals
-- Mathlib/Data/Set/Function.lean
theorem piecewise_preimage (f g : α → β) (t) : s.piecewise f g ⁻¹' t = s.ite (f ⁻¹' t) (g ⁻¹' t) :=
  ext fun x => by by_cases x ∈ s <;> simp [*, Set.ite]

Proof state:
α : Type u_1
β : Type u_2
s : Set α
inst✝ : (j : α) → Decidable (j ∈ s)
f g : α → β
t : Set β
x : α
⊢ x ∈ s.piecewise f g ⁻¹' t ↔ x ∈ s.ite (f ⁻¹' t) (g ⁻¹' t)

Tactic:
by_cases x ∈ s <;> simp [*, Set.ite]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Lemmas.lean
theorem all_eq {l : List α} : l.all p = decide (∀ x, x ∈ l → p x)

Proof state:
α : Type u_1
p : α → Bool
l : List α
⊢ l.all p = decide (∀ (x : α), x ∈ l → p x = true)

Tactic:
induction l <;> simp [*]

Result:
no goals
-- Mathlib/Algebra/Ring/Parity.lean
lemma even_or_odd' (n : ℕ) : ∃ k, n = 2 * k ∨ n = 2 * k + 1

Proof state:
n : ℕ
⊢ ∃ k, n = 2 * k ∨ n = 2 * k + 1

Tactic:
simpa only [← two_mul, exists_or, Odd, Even] using even_or_odd n

Result:
no goals
-- Mathlib/LinearAlgebra/Quotient/Basic.lean
theorem factor_comp_apply (H1 : p ≤ p') (H2 : p' ≤ p'') (x : M ⧸ p) :
    factor H2 (factor H1 x) = factor (H1.trans H2) x

Proof state:
R : Type u_1
M : Type u_2
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
p p' p'' : Submodule R M
H1 : p ≤ p'
H2 : p' ≤ p''
x : M ⧸ p
⊢ (factor H2) ((factor H1) x) = (factor ⋯) x

Tactic:
rw [← comp_apply]

Result:
R : Type u_1
M : Type u_2
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
p p' p'' : Submodule R M
H1 : p ≤ p'
H2 : p' ≤ p''
x : M ⧸ p
⊢ (factor H2 ∘ₗ factor H1) x = (factor ⋯) x

Proof state:
R : Type u_1
M : Type u_2
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
p p' p'' : Submodule R M
H1 : p ≤ p'
H2 : p' ≤ p''
x : M ⧸ p
⊢ (factor H2 ∘ₗ factor H1) x = (factor ⋯) x

Tactic:
simp

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Count.lean
theorem countP_eq_zero {p} : countP p l = 0 ↔ ∀ a ∈ l, ¬p a

Proof state:
case mk
α✝ : Type u_1
n✝ : Nat
p : α✝ → Bool
toArray✝ : Array α✝
size_toArray✝ : toArray✝.size = n✝
⊢ countP p { toArray := toArray✝, size_toArray := size_toArray✝ } = 0 ↔
    ∀ (a : α✝), a ∈ { toArray := toArray✝, size_toArray := size_toArray✝ } → ¬p a = true

Tactic:
simp

Result:
no goals

Proof state:
α✝ : Type u_1
n✝ : Nat
l : Vector α✝ n✝
p : α✝ → Bool
⊢ countP p l = 0 ↔ ∀ (a : α✝), a ∈ l → ¬p a = true

Tactic:
cases l

Result:
case mk
α✝ : Type u_1
n✝ : Nat
p : α✝ → Bool
toArray✝ : Array α✝
size_toArray✝ : toArray✝.size = n✝
⊢ countP p { toArray := toArray✝, size_toArray := size_toArray✝ } = 0 ↔
    ∀ (a : α✝), a ∈ { toArray := toArray✝, size_toArray := size_toArray✝ } → ¬p a = true
-- Mathlib/Data/Finset/Lattice/Prod.lean
theorem sup_product_right (s : Finset β) (t : Finset γ) (f : β × γ → α) :
    (s ×ˢ t).sup f = t.sup fun i' => s.sup fun i => f ⟨i, i'⟩

Proof state:
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝¹ : SemilatticeSup α
inst✝ : OrderBot α
s : Finset β
t : Finset γ
f : β × γ → α
⊢ (s ×ˢ t).sup f = t.sup fun i' => s.sup fun i => f (i, i')

Tactic:
rw [sup_product_left, Finset.sup_comm]

Result:
no goals
-- Mathlib/Algebra/Polynomial/Laurent.lean
theorem degree_C_le (a : R) : (C a).degree ≤ 0 :=
  (le_of_eq (by rw [T_zero, mul_one])).trans (degree_C_mul_T_le 0 a)

Proof state:
R : Type u_1
inst✝ : Semiring R
a : R
⊢ (C a).degree = (C a * T 0).degree

Tactic:
rw [T_zero, mul_one]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem singleton_eq_append_iff {a b : Array α} {x : α} :
    #[x] = a ++ b ↔ (a = #[] ∧ b = #[x]) ∨ (a = #[x] ∧ b = #[])

Proof state:
α : Type u_1
a b : Array α
x : α
⊢ #[x] = a ++ b ↔ a = #[] ∧ b = #[x] ∨ a = #[x] ∧ b = #[]

Tactic:
rw [eq_comm, append_eq_singleton_iff]

Result:
no goals
-- Mathlib/NumberTheory/Zsqrtd/Basic.lean
theorem sqLe_smul {c d x y : ℕ} (n : ℕ) (xy : SqLe x c y d) : SqLe (n * x) c (n * y) d

Proof state:
c d x y n : ℕ
xy : SqLe x c y d
⊢ SqLe (n * x) c (n * y) d

Tactic:
simpa [SqLe, mul_left_comm, mul_assoc] using Nat.mul_le_mul_left (n * n) xy

Result:
no goals
-- Mathlib/Geometry/Euclidean/Angle/Oriented/Rotation.lean
theorem linearEquiv_det_rotation (θ : Real.Angle) :
    LinearEquiv.det (o.rotation θ).toLinearEquiv = 1 :=
  Units.ext <| by
    -- Porting note: Lean can't see through `LinearEquiv.coe_det` and needed the rewrite
    -- in mathlib3 this was just `units.ext <| o.det_rotation θ`
    simpa only [LinearEquiv.coe_det, Units.val_one] using o.det_rotation θ

Proof state:
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
θ : Real.Angle
⊢ ↑(LinearEquiv.det (o.rotation θ).toLinearEquiv) = ↑1

Tactic:
simpa only [LinearEquiv.coe_det, Units.val_one] using o.det_rotation θ

Result:
no goals
-- Mathlib/RingTheory/FinitePresentation.lean
theorem of_surjective (f : A →+* B) (hf : Surjective f) (hker : f.ker.FG) :
    f.FinitePresentation

Proof state:
A : Type u_1
B : Type u_2
inst✝¹ : CommRing A
inst✝ : CommRing B
f : A →+* B
hf : Surjective ⇑f
hker : (ker f).FG
⊢ (f.comp (RingHom.id A)).FinitePresentation

Tactic:
exact (id A).comp_surjective hf hker

Result:
no goals

Proof state:
A : Type u_1
B : Type u_2
inst✝¹ : CommRing A
inst✝ : CommRing B
f : A →+* B
hf : Surjective ⇑f
hker : (ker f).FG
⊢ f.FinitePresentation

Tactic:
rw [← f.comp_id]

Result:
A : Type u_1
B : Type u_2
inst✝¹ : CommRing A
inst✝ : CommRing B
f : A →+* B
hf : Surjective ⇑f
hker : (ker f).FG
⊢ (f.comp (RingHom.id A)).FinitePresentation
-- Mathlib/RingTheory/PowerSeries/WellKnown.lean
theorem constantCoeff_exp : constantCoeff A (exp A) = 1

Proof state:
A : Type u_1
inst✝¹ : Ring A
inst✝ : Algebra ℚ A
⊢ (algebraMap ℚ A) (1 / ↑0!) = 1

Tactic:
simp

Result:
no goals

Proof state:
A : Type u_1
inst✝¹ : Ring A
inst✝ : Algebra ℚ A
⊢ (constantCoeff A) (exp A) = 1

Tactic:
rw [← coeff_zero_eq_constantCoeff_apply, coeff_exp]

Result:
A : Type u_1
inst✝¹ : Ring A
inst✝ : Algebra ℚ A
⊢ (algebraMap ℚ A) (1 / ↑0!) = 1
-- Mathlib/Analysis/Normed/Group/Hom.lean
theorem ker_zero : (0 : NormedAddGroupHom V₁ V₂).ker = ⊤

Proof state:
V₁ : Type u_3
V₂ : Type u_4
inst✝¹ : SeminormedAddCommGroup V₁
inst✝ : SeminormedAddCommGroup V₂
⊢ ker 0 = ⊤

Tactic:
ext

Result:
case h
V₁ : Type u_3
V₂ : Type u_4
inst✝¹ : SeminormedAddCommGroup V₁
inst✝ : SeminormedAddCommGroup V₂
x✝ : V₁
⊢ x✝ ∈ ker 0 ↔ x✝ ∈ ⊤

Proof state:
case h
V₁ : Type u_3
V₂ : Type u_4
inst✝¹ : SeminormedAddCommGroup V₁
inst✝ : SeminormedAddCommGroup V₂
x✝ : V₁
⊢ x✝ ∈ ker 0 ↔ x✝ ∈ ⊤

Tactic:
simp [mem_ker]

Result:
no goals
-- Mathlib/FieldTheory/KummerExtension.lean
lemma adjoinRootXPowSubCEquiv_symm_eq_root :
    (adjoinRootXPowSubCEquiv hζ H hα).symm α = root _

Proof state:
case a
K : Type u
inst✝³ : Field K
n : ℕ
hζ : (primitiveRoots n K).Nonempty
a : K
H : Irreducible (X ^ n - C a)
L : Type u_1
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : IsSplittingField K L (X ^ n - C a)
α : L
hα : α ^ n = (algebraMap K L) a
⊢ (adjoinRootXPowSubCEquiv hζ H hα) ((adjoinRootXPowSubCEquiv hζ H hα).symm α) =
    (adjoinRootXPowSubCEquiv hζ H hα) (root (X ^ n - C a))

Tactic:
rw [(adjoinRootXPowSubCEquiv hζ H hα).apply_symm_apply, adjoinRootXPowSubCEquiv_root]

Result:
no goals

Proof state:
K : Type u
inst✝³ : Field K
n : ℕ
hζ : (primitiveRoots n K).Nonempty
a : K
H : Irreducible (X ^ n - C a)
L : Type u_1
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : IsSplittingField K L (X ^ n - C a)
α : L
hα : α ^ n = (algebraMap K L) a
⊢ (adjoinRootXPowSubCEquiv hζ H hα).symm α = root (X ^ n - C a)

Tactic:
apply (adjoinRootXPowSubCEquiv hζ H hα).injective

Result:
case a
K : Type u
inst✝³ : Field K
n : ℕ
hζ : (primitiveRoots n K).Nonempty
a : K
H : Irreducible (X ^ n - C a)
L : Type u_1
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : IsSplittingField K L (X ^ n - C a)
α : L
hα : α ^ n = (algebraMap K L) a
⊢ (adjoinRootXPowSubCEquiv hζ H hα) ((adjoinRootXPowSubCEquiv hζ H hα).symm α) =
    (adjoinRootXPowSubCEquiv hζ H hα) (root (X ^ n - C a))
-- Mathlib/Data/ZMod/Basic.lean
theorem val_eq_one : ∀ {n : ℕ} (_ : 1 < n) (a : ZMod n), a.val = 1 ↔ a = 1
  | 0, hn, _
  | 1, hn, _ => by simp at hn
  | n + 2, _, _ => by simp only [val, ZMod, Fin.ext_iff, Fin.val_one]

Proof state:
hn : 1 < 1
x✝ : ZMod 1
⊢ x✝.val = 1 ↔ x✝ = 1

Tactic:
simp at hn

Result:
no goals

Proof state:
n : ℕ
x✝¹ : 1 < n + 2
x✝ : ZMod (n + 2)
⊢ x✝.val = 1 ↔ x✝ = 1

Tactic:
simp only [val, ZMod, Fin.ext_iff, Fin.val_one]

Result:
no goals
-- Mathlib/Data/ZMod/Basic.lean
theorem val_pos {n : ℕ} {a : ZMod n} : 0 < a.val ↔ a ≠ 0

Proof state:
n : ℕ
a : ZMod n
⊢ 0 < a.val ↔ a ≠ 0

Tactic:
simp [pos_iff_ne_zero]

Result:
no goals
-- Mathlib/Data/Set/Function.lean
theorem mapsTo_empty_iff : MapsTo f s ∅ ↔ s = ∅

Proof state:
α : Type u_1
β : Type u_2
s : Set α
f : α → β
⊢ MapsTo f s ∅ ↔ s = ∅

Tactic:
simp [mapsTo', subset_empty_iff]

Result:
no goals
-- Mathlib/Order/Filter/AtTopBot/Basic.lean
theorem frequently_high_scores [LinearOrder β] [NoMaxOrder β] {u : ℕ → β}
    (hu : Tendsto u atTop atTop) : ∃ᶠ n in atTop, ∀ k < n, u k < u n

Proof state:
β : Type u_4
inst✝¹ : LinearOrder β
inst✝ : NoMaxOrder β
u : ℕ → β
hu : Tendsto u atTop atTop
⊢ ∃ᶠ (n : ℕ) in atTop, ∀ k < n, u k < u n

Tactic:
simpa [frequently_atTop] using high_scores hu

Result:
no goals
-- Mathlib/Geometry/Manifold/IsManifold/ExtChartAt.lean
theorem writtenInExtChartAt_extChartAt_symm {x : M} {y : E} (h : y ∈ (extChartAt I x).target) :
    writtenInExtChartAt 𝓘(𝕜, E) I (extChartAt I x x) (extChartAt I x).symm y = y

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
y : E
h : y ∈ (extChartAt I x).target
⊢ writtenInExtChartAt 𝓘(𝕜, E) I (↑(extChartAt I x) x) (↑(extChartAt I x).symm) y = y

Tactic:
simp_all only [mfld_simps]

Result:
no goals
-- Mathlib/LinearAlgebra/Eigenspace/Basic.lean
@[deprecated mapsTo_iSup_genEigenspace_of_comm (since := "2024-10-23")]
lemma mapsTo_iSup_genEigenspace_of_comm {f g : End R M} (h : Commute f g) (μ : R) :
    MapsTo g ↑(⨆ k : ℕ, f.genEigenspace μ k) ↑(⨆ k : ℕ, f.genEigenspace μ k)

Proof state:
R : Type v
M : Type w
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f g : End R M
h : Commute f g
μ : R
⊢ MapsTo ⇑g ↑(f.maxGenEigenspace μ) ↑(f.maxGenEigenspace μ)

Tactic:
apply mapsTo_maxGenEigenspace_of_comm h

Result:
no goals

Proof state:
R : Type v
M : Type w
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f g : End R M
h : Commute f g
μ : R
⊢ MapsTo ⇑g ↑(⨆ k, (f.genEigenspace μ) ↑k) ↑(⨆ k, (f.genEigenspace μ) ↑k)

Tactic:
rw [iSup_genEigenspace_eq]

Result:
R : Type v
M : Type w
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f g : End R M
h : Commute f g
μ : R
⊢ MapsTo ⇑g ↑(f.maxGenEigenspace μ) ↑(f.maxGenEigenspace μ)
-- Mathlib/Algebra/BigOperators/Expect.lean
lemma expect_comm (s : Finset ι) (t : Finset κ) (f : ι → κ → M) :
    𝔼 i ∈ s, 𝔼 j ∈ t, f i j = 𝔼 j ∈ t, 𝔼 i ∈ s, f i j

Proof state:
ι : Type u_1
κ : Type u_2
M : Type u_3
inst✝¹ : AddCommMonoid M
inst✝ : Module ℚ≥0 M
s : Finset ι
t : Finset κ
f : ι → κ → M
⊢ 𝔼 i ∈ s, 𝔼 j ∈ t, f i j = 𝔼 j ∈ t, 𝔼 i ∈ s, f i j

Tactic:
rw [expect, expect, ← expect_sum_comm, ← expect_sum_comm, expect, expect, smul_comm, sum_comm]

Result:
no goals
-- Mathlib/Algebra/Group/AddChar.lean
@[simp, norm_cast] lemma coe_eq_one : ⇑ψ = 1 ↔ ψ = 0

Proof state:
A : Type u_1
M : Type u_3
inst✝¹ : AddMonoid A
inst✝ : Monoid M
ψ : AddChar A M
⊢ ⇑ψ = 1 ↔ ψ = 0

Tactic:
rw [← coe_zero, DFunLike.coe_fn_eq]

Result:
no goals
-- Mathlib/Algebra/Polynomial/Coeff.lean
theorem coeff_X_mul (p : R[X]) (n : ℕ) : coeff (X * p) (n + 1) = coeff p n

Proof state:
R : Type u
inst✝ : Semiring R
p : R[X]
n : ℕ
⊢ (X * p).coeff (n + 1) = p.coeff n

Tactic:
rw [(commute_X p).eq, coeff_mul_X]

Result:
no goals
-- Mathlib/Analysis/Convex/Basic.lean
theorem Convex.linear_image (hs : Convex 𝕜 s) (f : E →ₗ[𝕜] F) : Convex 𝕜 (f '' s)

Proof state:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : OrderedSemiring 𝕜
inst✝³ : AddCommMonoid E
inst✝² : AddCommMonoid F
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 F
s : Set E
hs : Convex 𝕜 s
f : E →ₗ[𝕜] F
⊢ Convex 𝕜 (⇑f '' s)

Tactic:
rintro _ ⟨x, hx, rfl⟩ _ ⟨y, hy, rfl⟩ a b ha hb hab

Result:
case intro.intro.intro.intro
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : OrderedSemiring 𝕜
inst✝³ : AddCommMonoid E
inst✝² : AddCommMonoid F
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 F
s : Set E
hs : Convex 𝕜 s
f : E →ₗ[𝕜] F
x : E
hx : x ∈ s
y : E
hy : y ∈ s
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
⊢ a • f x + b • f y ∈ ⇑f '' s

Proof state:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : OrderedSemiring 𝕜
inst✝³ : AddCommMonoid E
inst✝² : AddCommMonoid F
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 F
s : Set E
hs : Convex 𝕜 s
f : E →ₗ[𝕜] F
x : E
hx : x ∈ s
y : E
hy : y ∈ s
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
⊢ f (a • x + b • y) = a • f x + b • f y

Tactic:
rw [f.map_add, f.map_smul, f.map_smul]

Result:
no goals

Proof state:
case intro.intro.intro.intro
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : OrderedSemiring 𝕜
inst✝³ : AddCommMonoid E
inst✝² : AddCommMonoid F
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 F
s : Set E
hs : Convex 𝕜 s
f : E →ₗ[𝕜] F
x : E
hx : x ∈ s
y : E
hy : y ∈ s
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
⊢ a • f x + b • f y ∈ ⇑f '' s

Tactic:
exact ⟨a • x + b • y, hs hx hy ha hb hab, by rw [f.map_add, f.map_smul, f.map_smul]⟩

Result:
no goals
-- Mathlib/Topology/Algebra/Module/Cardinality.lean
theorem continuum_le_cardinal_of_isOpen
    {E : Type*} (𝕜 : Type*) [NontriviallyNormedField 𝕜] [CompleteSpace 𝕜] [AddCommGroup E]
    [Module 𝕜 E] [Nontrivial E] [TopologicalSpace E] [ContinuousAdd E] [ContinuousSMul 𝕜 E]
    {s : Set E} (hs : IsOpen s) (h's : s.Nonempty) : 𝔠 ≤ #s

Proof state:
E : Type u_1
𝕜 : Type u_2
inst✝⁷ : NontriviallyNormedField 𝕜
inst✝⁶ : CompleteSpace 𝕜
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module 𝕜 E
inst✝³ : Nontrivial E
inst✝² : TopologicalSpace E
inst✝¹ : ContinuousAdd E
inst✝ : ContinuousSMul 𝕜 E
s : Set E
hs : IsOpen s
h's : s.Nonempty
⊢ 𝔠 ≤ #↑s

Tactic:
simpa [cardinal_eq_of_isOpen 𝕜 hs h's] using continuum_le_cardinal_of_module 𝕜 E

Result:
no goals
-- Mathlib/Analysis/Calculus/FDeriv/Measurable.lean
theorem measurableSet_of_differentiableWithinAt_Ioi :
    MeasurableSet { x | DifferentiableWithinAt ℝ f (Ioi x) x }

Proof state:
F : Type u_1
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
f : ℝ → F
inst✝ : CompleteSpace F
⊢ MeasurableSet {x | DifferentiableWithinAt ℝ f (Ioi x) x}

Tactic:
simpa [differentiableWithinAt_Ioi_iff_Ici] using measurableSet_of_differentiableWithinAt_Ici f

Result:
no goals