harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Geometry/Manifold/IsManifold/ExtChartAt.lean
lemma extend_image_target_mem_nhds {x : M} (hx : x ∈ f.source) :
    I '' f.target ∈ 𝓝[range I] (f.extend I) x

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
f : PartialHomeomorph M H
I : ModelWithCorners 𝕜 E H
x : M
hx : x ∈ f.source
⊢ ↑f ⁻¹' f.target ∈ 𝓝 x

Tactic:
exact (f.continuousAt hx).preimage_mem_nhds (f.open_target.mem_nhds (f.map_source hx))

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
f : PartialHomeomorph M H
I : ModelWithCorners 𝕜 E H
x : M
hx : x ∈ f.source
⊢ ↑I '' f.target ∈ 𝓝[range ↑I] ↑(f.extend I) x

Tactic:
rw [← f.map_extend_nhds hx, Filter.mem_map,
  f.extend_coe, Set.preimage_comp, I.preimage_image f.target]

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
f : PartialHomeomorph M H
I : ModelWithCorners 𝕜 E H
x : M
hx : x ∈ f.source
⊢ ↑f ⁻¹' f.target ∈ 𝓝 x
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem push_ne_self {a : α} {xs : Array α} : xs.push a ≠ xs

Proof state:
case mk
α : Type u_1
a : α
toList✝ : List α
⊢ { toList := toList✝ }.push a ≠ { toList := toList✝ }

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
a : α
xs : Array α
⊢ xs.push a ≠ xs

Tactic:
cases xs

Result:
case mk
α : Type u_1
a : α
toList✝ : List α
⊢ { toList := toList✝ }.push a ≠ { toList := toList✝ }
-- Mathlib/ModelTheory/Satisfiability.lean
theorem models_toFormula_iff {φ : L.BoundedFormula α n} : T ⊨ᵇ φ.toFormula ↔ T ⊨ᵇ φ

Proof state:
case refine_1
L : Language
T : L.Theory
α : Type w
n : ℕ
φ : L.BoundedFormula α n
h : T ⊨ᵇ φ.toFormula
M : T.ModelType
v : α → ↑M
xs : Fin n → ↑M
h' : φ.Realize v xs
⊢ φ.Realize v xs

Tactic:
exact h'

Result:
no goals

Proof state:
case refine_2
L : Language
T : L.Theory
α : Type w
n : ℕ
φ : L.BoundedFormula α n
⊢ T ⊨ᵇ φ → T ⊨ᵇ φ.toFormula

Tactic:
simp only [models_formula_iff, BoundedFormula.realize_toFormula]

Result:
case refine_2
L : Language
T : L.Theory
α : Type w
n : ℕ
φ : L.BoundedFormula α n
⊢ T ⊨ᵇ φ → ∀ (M : T.ModelType) (v : α ⊕ Fin n → ↑M), φ.Realize (v ∘ Sum.inl) (v ∘ Sum.inr)

Proof state:
case refine_1
L : Language
T : L.Theory
α : Type w
n : ℕ
φ : L.BoundedFormula α n
h : T ⊨ᵇ φ.toFormula
M : T.ModelType
v : α → ↑M
xs : Fin n → ↑M
⊢ φ.Realize v xs

Tactic:
have h' : φ.toFormula.Realize (Sum.elim v xs) := h.realize_formula M

Result:
case refine_1
L : Language
T : L.Theory
α : Type w
n : ℕ
φ : L.BoundedFormula α n
h : T ⊨ᵇ φ.toFormula
M : T.ModelType
v : α → ↑M
xs : Fin n → ↑M
h' : φ.toFormula.Realize (Sum.elim v xs)
⊢ φ.Realize v xs

Proof state:
case refine_2
L : Language
T : L.Theory
α : Type w
n : ℕ
φ : L.BoundedFormula α n
⊢ T ⊨ᵇ φ → ∀ (M : T.ModelType) (v : α ⊕ Fin n → ↑M), φ.Realize (v ∘ Sum.inl) (v ∘ Sum.inr)

Tactic:
exact fun h M v => h M _ _

Result:
no goals

Proof state:
case refine_1
L : Language
T : L.Theory
α : Type w
n : ℕ
φ : L.BoundedFormula α n
h : T ⊨ᵇ φ.toFormula
M : T.ModelType
v : α → ↑M
xs : Fin n → ↑M
h' : φ.toFormula.Realize (Sum.elim v xs)
⊢ φ.Realize v xs

Tactic:
simp only [BoundedFormula.realize_toFormula, Sum.elim_comp_inl, Sum.elim_comp_inr] at h'

Result:
case refine_1
L : Language
T : L.Theory
α : Type w
n : ℕ
φ : L.BoundedFormula α n
h : T ⊨ᵇ φ.toFormula
M : T.ModelType
v : α → ↑M
xs : Fin n → ↑M
h' : φ.Realize v xs
⊢ φ.Realize v xs

Proof state:
L : Language
T : L.Theory
α : Type w
n : ℕ
φ : L.BoundedFormula α n
⊢ T ⊨ᵇ φ.toFormula ↔ T ⊨ᵇ φ

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

Result:
case refine_1
L : Language
T : L.Theory
α : Type w
n : ℕ
φ : L.BoundedFormula α n
h : T ⊨ᵇ φ.toFormula
M : T.ModelType
v : α → ↑M
xs : Fin n → ↑M
⊢ φ.Realize v xs

case refine_2
L : Language
T : L.Theory
α : Type w
n : ℕ
φ : L.BoundedFormula α n
⊢ T ⊨ᵇ φ → T ⊨ᵇ φ.toFormula
-- Mathlib/MeasureTheory/SetAlgebra.lean
theorem biInter_mem {ι : Type*} (h𝒜 : IsSetAlgebra 𝒜) {s : ι → Set α} (S : Finset ι)
    (hs : ∀ i ∈ S, s i ∈ 𝒜) : ⋂ i ∈ S, s i ∈ 𝒜

Proof state:
case neg
α : Type u_1
𝒜 : Set (Set α)
ι : Type u_2
h𝒜 : IsSetAlgebra 𝒜
s : ι → Set α
S : Finset ι
hs : ∀ i ∈ S, s i ∈ 𝒜
h : S.Nonempty
⊢ ⋂ i ∈ S, s i ∈ 𝒜

Tactic:
exact h𝒜.isSetRing.biInter_mem S h hs

Result:
no goals

Proof state:
case pos
α : Type u_1
𝒜 : Set (Set α)
ι : Type u_2
h𝒜 : IsSetAlgebra 𝒜
s : ι → Set α
S : Finset ι
hs : ∀ i ∈ S, s i ∈ 𝒜
h : S = ∅
⊢ univ ∈ 𝒜

Tactic:
exact h𝒜.univ_mem

Result:
no goals

Proof state:
case pos
α : Type u_1
𝒜 : Set (Set α)
ι : Type u_2
h𝒜 : IsSetAlgebra 𝒜
s : ι → Set α
S : Finset ι
hs : ∀ i ∈ S, s i ∈ 𝒜
h : S = ∅
⊢ ⋂ i ∈ S, s i ∈ 𝒜

Tactic:
rw [h, ← Finset.set_biInter_coe, Finset.coe_empty, biInter_empty]

Result:
case pos
α : Type u_1
𝒜 : Set (Set α)
ι : Type u_2
h𝒜 : IsSetAlgebra 𝒜
s : ι → Set α
S : Finset ι
hs : ∀ i ∈ S, s i ∈ 𝒜
h : S = ∅
⊢ univ ∈ 𝒜

Proof state:
case neg
α : Type u_1
𝒜 : Set (Set α)
ι : Type u_2
h𝒜 : IsSetAlgebra 𝒜
s : ι → Set α
S : Finset ι
hs : ∀ i ∈ S, s i ∈ 𝒜
h : ¬S = ∅
⊢ ⋂ i ∈ S, s i ∈ 𝒜

Tactic:
rw [← ne_eq, ← Finset.nonempty_iff_ne_empty] at h

Result:
case neg
α : Type u_1
𝒜 : Set (Set α)
ι : Type u_2
h𝒜 : IsSetAlgebra 𝒜
s : ι → Set α
S : Finset ι
hs : ∀ i ∈ S, s i ∈ 𝒜
h : S.Nonempty
⊢ ⋂ i ∈ S, s i ∈ 𝒜

Proof state:
α : Type u_1
𝒜 : Set (Set α)
ι : Type u_2
h𝒜 : IsSetAlgebra 𝒜
s : ι → Set α
S : Finset ι
hs : ∀ i ∈ S, s i ∈ 𝒜
⊢ ⋂ i ∈ S, s i ∈ 𝒜

Tactic:
by_cases h : S = ∅

Result:
case pos
α : Type u_1
𝒜 : Set (Set α)
ι : Type u_2
h𝒜 : IsSetAlgebra 𝒜
s : ι → Set α
S : Finset ι
hs : ∀ i ∈ S, s i ∈ 𝒜
h : S = ∅
⊢ ⋂ i ∈ S, s i ∈ 𝒜

case neg
α : Type u_1
𝒜 : Set (Set α)
ι : Type u_2
h𝒜 : IsSetAlgebra 𝒜
s : ι → Set α
S : Finset ι
hs : ∀ i ∈ S, s i ∈ 𝒜
h : ¬S = ∅
⊢ ⋂ i ∈ S, s i ∈ 𝒜
-- Mathlib/Algebra/Polynomial/Lifts.lean
theorem lifts_iff_coeff_lifts (p : S[X]) : p ∈ lifts f ↔ ∀ n : ℕ, p.coeff n ∈ Set.range f

Proof state:
R : Type u
inst✝¹ : Semiring R
S : Type v
inst✝ : Semiring S
f : R →+* S
p : S[X]
⊢ p ∈ lifts f ↔ ∀ (n : ℕ), p.coeff n ∈ Set.range ⇑f

Tactic:
rw [lifts_iff_ringHom_rangeS, mem_map_rangeS f]

Result:
R : Type u
inst✝¹ : Semiring R
S : Type v
inst✝ : Semiring S
f : R →+* S
p : S[X]
⊢ (∀ (n : ℕ), p.coeff n ∈ f.rangeS) ↔ ∀ (n : ℕ), p.coeff n ∈ Set.range ⇑f

Proof state:
R : Type u
inst✝¹ : Semiring R
S : Type v
inst✝ : Semiring S
f : R →+* S
p : S[X]
⊢ (∀ (n : ℕ), p.coeff n ∈ f.rangeS) ↔ ∀ (n : ℕ), p.coeff n ∈ Set.range ⇑f

Tactic:
rfl

Result:
no goals
-- Mathlib/Algebra/Homology/Double.lean
@[simp, reassoc]
lemma mkHomFromDouble_f₀ :
    (mkHomFromDouble hi₀₁ h φ₀ φ₁ comm hφ).f i₀ =
      (doubleXIso₀ f hi₀₁).hom ≫ φ₀

Proof state:
C : Type u_1
inst✝² : Category.{u_3, u_1} C
inst✝¹ : HasZeroMorphisms C
inst✝ : HasZeroObject C
X₀ X₁ : C
f : X₀ ⟶ X₁
ι : Type u_2
c : ComplexShape ι
i₀ i₁ : ι
hi₀₁ : c.Rel i₀ i₁
h : i₀ ≠ i₁
K : HomologicalComplex C c
φ₀ : X₀ ⟶ K.X i₀
φ₁ : X₁ ⟶ K.X i₁
comm : φ₀ ≫ K.d i₀ i₁ = f ≫ φ₁
hφ : ∀ (k : ι), c.Rel i₁ k → φ₁ ≫ K.d i₁ k = 0
⊢ (if i₀ = i₀ then 𝟙 ((double f hi₀₁).X i₀) ≫ (doubleXIso₀ f hi₀₁).hom ≫ φ₀ ≫ 𝟙 (K.X i₀)
    else if hk₁ : i₀ = i₁ then eqToHom ⋯ ≫ (doubleXIso₁ f hi₀₁ h).hom ≫ φ₁ ≫ eqToHom ⋯ else 0) =
    (doubleXIso₀ f hi₀₁).hom ≫ φ₀

Tactic:
rw [if_pos rfl, id_comp, comp_id]

Result:
no goals

Proof state:
C : Type u_1
inst✝² : Category.{u_3, u_1} C
inst✝¹ : HasZeroMorphisms C
inst✝ : HasZeroObject C
X₀ X₁ : C
f : X₀ ⟶ X₁
ι : Type u_2
c : ComplexShape ι
i₀ i₁ : ι
hi₀₁ : c.Rel i₀ i₁
h : i₀ ≠ i₁
K : HomologicalComplex C c
φ₀ : X₀ ⟶ K.X i₀
φ₁ : X₁ ⟶ K.X i₁
comm : φ₀ ≫ K.d i₀ i₁ = f ≫ φ₁
hφ : ∀ (k : ι), c.Rel i₁ k → φ₁ ≫ K.d i₁ k = 0
⊢ (mkHomFromDouble hi₀₁ h φ₀ φ₁ comm hφ).f i₀ = (doubleXIso₀ f hi₀₁).hom ≫ φ₀

Tactic:
dsimp [mkHomFromDouble]

Result:
C : Type u_1
inst✝² : Category.{u_3, u_1} C
inst✝¹ : HasZeroMorphisms C
inst✝ : HasZeroObject C
X₀ X₁ : C
f : X₀ ⟶ X₁
ι : Type u_2
c : ComplexShape ι
i₀ i₁ : ι
hi₀₁ : c.Rel i₀ i₁
h : i₀ ≠ i₁
K : HomologicalComplex C c
φ₀ : X₀ ⟶ K.X i₀
φ₁ : X₁ ⟶ K.X i₁
comm : φ₀ ≫ K.d i₀ i₁ = f ≫ φ₁
hφ : ∀ (k : ι), c.Rel i₁ k → φ₁ ≫ K.d i₁ k = 0
⊢ (if i₀ = i₀ then 𝟙 ((double f hi₀₁).X i₀) ≫ (doubleXIso₀ f hi₀₁).hom ≫ φ₀ ≫ 𝟙 (K.X i₀)
    else if hk₁ : i₀ = i₁ then eqToHom ⋯ ≫ (doubleXIso₁ f hi₀₁ h).hom ≫ φ₁ ≫ eqToHom ⋯ else 0) =
    (doubleXIso₀ f hi₀₁).hom ≫ φ₀
-- Mathlib/Algebra/Order/Floor.lean
lemma div_two_lt_floor (ha : 1 ≤ a) : a / 2 < ⌊a⌋

Proof state:
case refine_3
k : Type u_4
inst✝¹ : LinearOrderedField k
inst✝ : FloorRing k
a : k
ha : 1 ≤ a
⊢ 1 ≤ a

Tactic:
assumption

Result:
no goals

Proof state:
k : Type u_4
inst✝¹ : LinearOrderedField k
inst✝ : FloorRing k
a : k
ha : 1 ≤ a
⊢ 2⁻¹ * a < ↑⌊a⌋

Tactic:
refine mul_lt_floor ?_ ?_ ?_ <;> norm_num

Result:
case refine_3
k : Type u_4
inst✝¹ : LinearOrderedField k
inst✝ : FloorRing k
a : k
ha : 1 ≤ a
⊢ 1 ≤ a

Proof state:
k : Type u_4
inst✝¹ : LinearOrderedField k
inst✝ : FloorRing k
a : k
ha : 1 ≤ a
⊢ a / 2 < ↑⌊a⌋

Tactic:
rw [div_eq_inv_mul]

Result:
k : Type u_4
inst✝¹ : LinearOrderedField k
inst✝ : FloorRing k
a : k
ha : 1 ≤ a
⊢ 2⁻¹ * a < ↑⌊a⌋
-- Mathlib/RingTheory/Flat/FaithfullyFlat/Basic.lean
lemma lTensor_reflects_triviality
    [FaithfullyFlat R M] (N : Type*) [AddCommGroup N] [Module R N]
    [Subsingleton (M ⊗[R] N)] :
    Subsingleton N

Proof state:
R : Type u
M : Type v
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : FaithfullyFlat R M
N : Type u_1
inst✝² : AddCommGroup N
inst✝¹ : Module R N
inst✝ : Subsingleton (M ⊗[R] N)
⊢ Subsingleton N

Tactic:
haveI : Subsingleton (N ⊗[R] M) := (TensorProduct.comm R N M).toEquiv.injective.subsingleton

Result:
R : Type u
M : Type v
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : FaithfullyFlat R M
N : Type u_1
inst✝² : AddCommGroup N
inst✝¹ : Module R N
inst✝ : Subsingleton (M ⊗[R] N)
this : Subsingleton (N ⊗[R] M)
⊢ Subsingleton N

Proof state:
R : Type u
M : Type v
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : FaithfullyFlat R M
N : Type u_1
inst✝² : AddCommGroup N
inst✝¹ : Module R N
inst✝ : Subsingleton (M ⊗[R] N)
this : Subsingleton (N ⊗[R] M)
⊢ Subsingleton N

Tactic:
apply rTensor_reflects_triviality R M

Result:
no goals
-- Mathlib/Data/Set/Prod.lean
theorem prod_eq_iff_eq (ht : t.Nonempty) : s ×ˢ t = s₁ ×ˢ t ↔ s = s₁

Proof state:
α : Type u_1
β : Type u_2
s s₁ : Set α
t : Set β
ht : t.Nonempty
⊢ s ×ˢ t = s₁ ×ˢ t ↔ s = s₁

Tactic:
simp_rw [prod_eq_prod_iff, ht.ne_empty, and_true, or_iff_left_iff_imp, or_false]

Result:
α : Type u_1
β : Type u_2
s s₁ : Set α
t : Set β
ht : t.Nonempty
⊢ s = ∅ ∧ s₁ = ∅ → s = s₁

Proof state:
case intro
α : Type u_1
β : Type u_2
t : Set β
ht : t.Nonempty
⊢ ∅ = ∅

Tactic:
rfl

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
s s₁ : Set α
t : Set β
ht : t.Nonempty
⊢ s = ∅ ∧ s₁ = ∅ → s = s₁

Tactic:
rintro ⟨rfl, rfl⟩

Result:
case intro
α : Type u_1
β : Type u_2
t : Set β
ht : t.Nonempty
⊢ ∅ = ∅
-- Mathlib/AlgebraicGeometry/IdealSheaf.lean
@[reassoc (attr := simp)]
lemma glueDataT_fst (U V : X.affineOpens) :
    I.glueDataT U V ≫ pullback.fst _ _ ≫ glueDataObjι _ _ =
      pullback.snd _ _ ≫ X.homOfLE inf_le_right

Proof state:
X : Scheme
I : X.IdealSheafData
U V : ↑X.affineOpens
⊢ Hom.liftQuotient (pullback.snd (I.glueDataObjι U) (X.homOfLE ⋯) ≫ X.homOfLE ⋯ ≫ (IsAffineOpen.isoSpec ⋯).hom)
        (I.ideal V) ⋯ ≫
      Spec.map (CommRingCat.ofHom (Ideal.Quotient.mk (I.ideal V))) ≫ (IsAffineOpen.isoSpec ⋯).inv =
    pullback.snd (I.glueDataObjι U) (X.homOfLE ⋯) ≫ X.homOfLE ⋯

Tactic:
rw [Scheme.Hom.liftQuotient_comp_assoc, Category.assoc, Category.assoc, Iso.hom_inv_id,
  Category.comp_id]

Result:
no goals

Proof state:
X : Scheme
I : X.IdealSheafData
U V : ↑X.affineOpens
⊢ I.glueDataT U V ≫ pullback.fst (I.glueDataObjι V) (X.homOfLE ⋯) ≫ I.glueDataObjι V =
    pullback.snd (I.glueDataObjι U) (X.homOfLE ⋯) ≫ X.homOfLE ⋯

Tactic:
refine (pullback.lift_fst_assoc _ _ _ _).trans ?_

Result:
X : Scheme
I : X.IdealSheafData
U V : ↑X.affineOpens
⊢ Hom.liftQuotient (pullback.snd (I.glueDataObjι U) (X.homOfLE ⋯) ≫ X.homOfLE ⋯ ≫ (IsAffineOpen.isoSpec ⋯).hom)
        (I.ideal V) ⋯ ≫
      I.glueDataObjι V =
    pullback.snd (I.glueDataObjι U) (X.homOfLE ⋯) ≫ X.homOfLE ⋯

Proof state:
X : Scheme
I : X.IdealSheafData
U V : ↑X.affineOpens
⊢ Hom.liftQuotient (pullback.snd (I.glueDataObjι U) (X.homOfLE ⋯) ≫ X.homOfLE ⋯ ≫ (IsAffineOpen.isoSpec ⋯).hom)
        (I.ideal V) ⋯ ≫
      I.glueDataObjι V =
    pullback.snd (I.glueDataObjι U) (X.homOfLE ⋯) ≫ X.homOfLE ⋯

Tactic:
conv_lhs => enter [2]; rw [glueDataObjι]

Result:
X : Scheme
I : X.IdealSheafData
U V : ↑X.affineOpens
⊢ Hom.liftQuotient (pullback.snd (I.glueDataObjι U) (X.homOfLE ⋯) ≫ X.homOfLE ⋯ ≫ (IsAffineOpen.isoSpec ⋯).hom)
        (I.ideal V) ⋯ ≫
      Spec.map (CommRingCat.ofHom (Ideal.Quotient.mk (I.ideal V))) ≫ (IsAffineOpen.isoSpec ⋯).inv =
    pullback.snd (I.glueDataObjι U) (X.homOfLE ⋯) ≫ X.homOfLE ⋯
-- Mathlib/Algebra/BigOperators/Associated.lean
theorem Finset.prod_primes_dvd [CancelCommMonoidWithZero α] [Subsingleton αˣ] {s : Finset α} (n : α)
    (h : ∀ a ∈ s, Prime a) (div : ∀ a ∈ s, a ∣ n) : (∏ p ∈ s, p) ∣ n

Proof state:
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : Subsingleton αˣ
s : Finset α
n : α
h : ∀ a ∈ s, Prime a
div : ∀ a ∈ s, a ∣ n
⊢ ∏ p ∈ s, p ∣ n

Tactic:
classical
  exact
    Multiset.prod_primes_dvd n (by simpa only [Multiset.map_id', Finset.mem_def] using h)
      (by simpa only [Multiset.map_id', Finset.mem_def] using div)
      (by
        simp only [Multiset.map_id', associated_eq_eq, Multiset.countP_eq_card_filter,
          ← s.val.count_eq_card_filter_eq, ← Multiset.nodup_iff_count_le_one, s.nodup])

Result:
no goals

Proof state:
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : Subsingleton αˣ
s : Finset α
n : α
h : ∀ a ∈ s, Prime a
div : ∀ a ∈ s, a ∣ n
⊢ ∀ (a : α), Multiset.countP (Associated a) (Multiset.map (fun p => p) s.val) ≤ 1

Tactic:
simp only [Multiset.map_id', associated_eq_eq, Multiset.countP_eq_card_filter,
  ← s.val.count_eq_card_filter_eq, ← Multiset.nodup_iff_count_le_one, s.nodup]

Result:
no goals

Proof state:
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : Subsingleton αˣ
s : Finset α
n : α
h : ∀ a ∈ s, Prime a
div : ∀ a ∈ s, a ∣ n
⊢ ∀ a ∈ Multiset.map (fun p => p) s.val, Prime a

Tactic:
simpa only [Multiset.map_id', Finset.mem_def] using h

Result:
no goals

Proof state:
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : Subsingleton αˣ
s : Finset α
n : α
h : ∀ a ∈ s, Prime a
div : ∀ a ∈ s, a ∣ n
⊢ ∀ a ∈ Multiset.map (fun p => p) s.val, a ∣ n

Tactic:
simpa only [Multiset.map_id', Finset.mem_def] using div

Result:
no goals

Proof state:
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : Subsingleton αˣ
s : Finset α
n : α
h : ∀ a ∈ s, Prime a
div : ∀ a ∈ s, a ∣ n
⊢ ∏ p ∈ s, p ∣ n

Tactic:
exact
  Multiset.prod_primes_dvd n (by simpa only [Multiset.map_id', Finset.mem_def] using h)
    (by simpa only [Multiset.map_id', Finset.mem_def] using div)
    (by
      simp only [Multiset.map_id', associated_eq_eq, Multiset.countP_eq_card_filter,
        ← s.val.count_eq_card_filter_eq, ← Multiset.nodup_iff_count_le_one, s.nodup])

Result:
no goals
-- Mathlib/GroupTheory/Coset/Defs.lean
theorem leftRel_apply {x y : α} : leftRel s x y ↔ x⁻¹ * y ∈ s :=
  calc
    (∃ a : s.op, y * MulOpposite.unop a = x) ↔ ∃ a : s, y * a = x :=
      s.equivOp.symm.exists_congr_left
    _ ↔ ∃ a : s, x⁻¹ * y = a⁻¹

Proof state:
α : Type u_1
inst✝ : Group α
s : Subgroup α
x y : α
⊢ (∃ a, x⁻¹ * y = ↑a⁻¹) ↔ x⁻¹ * y ∈ s

Tactic:
simp [exists_inv_mem_iff_exists_mem]

Result:
no goals

Proof state:
α : Type u_1
inst✝ : Group α
s : Subgroup α
x y : α
⊢ (∃ a, y * ↑a = x) ↔ ∃ a, x⁻¹ * y = ↑a⁻¹

Tactic:
simp only [inv_mul_eq_iff_eq_mul, Subgroup.coe_inv, eq_mul_inv_iff_mul_eq]

Result:
no goals
-- Mathlib/Probability/Moments/Basic.lean
theorem mgf_const_add (α : ℝ) : mgf (fun ω => α + X ω) μ t = exp (t * α) * mgf X μ t

Proof state:
case e_f.h
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t α : ℝ
x : Ω
⊢ (fun ω => rexp (t * (α + X ω))) x = rexp (t * α) * rexp (t * X x)

Tactic:
dsimp

Result:
case e_f.h
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t α : ℝ
x : Ω
⊢ rexp (t * (α + X x)) = rexp (t * α) * rexp (t * X x)

Proof state:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t α : ℝ
⊢ ∫ (x : Ω), (fun ω => rexp (t * (α + X ω))) x ∂μ = ∫ (a : Ω), rexp (t * α) * rexp (t * X a) ∂μ

Tactic:
congr with x

Result:
case e_f.h
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t α : ℝ
x : Ω
⊢ (fun ω => rexp (t * (α + X ω))) x = rexp (t * α) * rexp (t * X x)

Proof state:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t α : ℝ
⊢ mgf (fun ω => α + X ω) μ t = rexp (t * α) * mgf X μ t

Tactic:
rw [mgf, mgf, ← integral_mul_left]

Result:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t α : ℝ
⊢ ∫ (x : Ω), (fun ω => rexp (t * (α + X ω))) x ∂μ = ∫ (a : Ω), rexp (t * α) * rexp (t * X a) ∂μ

Proof state:
case e_f.h
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t α : ℝ
x : Ω
⊢ rexp (t * (α + X x)) = rexp (t * α) * rexp (t * X x)

Tactic:
rw [mul_add, exp_add]

Result:
no goals
-- Mathlib/Algebra/Lie/Submodule.lean
theorem iSupIndep_iff_toSubmodule {ι : Type*} {N : ι → LieSubmodule R L M} :
    iSupIndep N ↔ iSupIndep fun i ↦ (N i : Submodule R M)

Proof state:
R : Type u
L : Type v
M : Type w
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : LieRingModule L M
ι : Type u_1
N : ι → LieSubmodule R L M
⊢ iSupIndep N ↔ iSupIndep fun i => ↑(N i)

Tactic:
simp [iSupIndep_def, disjoint_iff_toSubmodule]

Result:
no goals
-- Mathlib/Topology/Instances/ENNReal/Lemmas.lean
lemma le_liminf_mul {α : Type*} {f : Filter α} {u v : α → ℝ≥0∞} :
    liminf u f * liminf v f ≤ liminf (u * v) f

Proof state:
α : Type u_5
f : Filter α
u v : α → ℝ≥0∞
⊢ liminf u f * liminf v f ≤ liminf (u * v) f

Tactic:
refine mul_le_of_forall_lt fun a a_u b b_v ↦ (le_liminf_iff).2 fun c c_ab ↦ ?_

Result:
α : Type u_5
f : Filter α
u v : α → ℝ≥0∞
a : ℝ≥0∞
a_u : a < liminf u f
b : ℝ≥0∞
b_v : b < liminf v f
c : ℝ≥0∞
c_ab : c < a * b
⊢ ∀ᶠ (a : α) in f, c < (u * v) a

Proof state:
case h
α : Type u_5
f : Filter α
u v : α → ℝ≥0∞
a : ℝ≥0∞
a_u : a < liminf u f
b : ℝ≥0∞
b_v : b < liminf v f
c : ℝ≥0∞
c_ab : c < a * b
x : α
a_x : a < u x
b_x : b < v x
⊢ c < (u * v) x

Tactic:
exact c_ab.trans (mul_lt_mul a_x b_x)

Result:
no goals

Proof state:
α : Type u_5
f : Filter α
u v : α → ℝ≥0∞
a : ℝ≥0∞
a_u : a < liminf u f
b : ℝ≥0∞
b_v : b < liminf v f
c : ℝ≥0∞
c_ab : c < a * b
⊢ ∀ᶠ (a : α) in f, c < (u * v) a

Tactic:
filter_upwards [eventually_lt_of_lt_liminf a_u, eventually_lt_of_lt_liminf b_v] with x a_x b_x

Result:
case h
α : Type u_5
f : Filter α
u v : α → ℝ≥0∞
a : ℝ≥0∞
a_u : a < liminf u f
b : ℝ≥0∞
b_v : b < liminf v f
c : ℝ≥0∞
c_ab : c < a * b
x : α
a_x : a < u x
b_x : b < v x
⊢ c < (u * v) x
-- Mathlib/CategoryTheory/Generator/Preadditive.lean
theorem Preadditive.isSeparator_iff (G : C) :
    IsSeparator G ↔ ∀ ⦃X Y : C⦄ (f : X ⟶ Y), (∀ h : G ⟶ X, h ≫ f = 0) → f = 0 :=
  ⟨fun hG X Y f hf => hG.def _ _ (by simpa only [Limits.comp_zero] using hf), fun hG =>
    (isSeparator_def _).2 fun X Y f g hfg =>
      sub_eq_zero.1 <| hG _ (by simpa only [Preadditive.comp_sub, sub_eq_zero] using hfg)⟩

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
G : C
hG : ∀ ⦃X Y : C⦄ (f : X ⟶ Y), (∀ (h : G ⟶ X), h ≫ f = 0) → f = 0
X Y : C
f g : X ⟶ Y
hfg : ∀ (h : G ⟶ X), h ≫ f = h ≫ g
⊢ ∀ (h : G ⟶ X), h ≫ (f - g) = 0

Tactic:
simpa only [Preadditive.comp_sub, sub_eq_zero] using hfg

Result:
no goals

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
G : C
hG : IsSeparator G
X Y : C
f : X ⟶ Y
hf : ∀ (h : G ⟶ X), h ≫ f = 0
⊢ ∀ (h : G ⟶ X), h ≫ f = h ≫ 0

Tactic:
simpa only [Limits.comp_zero] using hf

Result:
no goals
-- Mathlib/LinearAlgebra/Finsupp/LinearCombination.lean
theorem linearCombination_single_index (c : M) (a : α) (f : α →₀ R) [DecidableEq α] :
    linearCombination R (Pi.single a c) f = f a • c

Proof state:
α : Type u_1
M : Type u_2
R : Type u_5
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
c : M
a : α
f : α →₀ R
inst✝ : DecidableEq α
x✝ : f a = 0
⊢ 0 • Pi.single a c a = 0

Tactic:
simp only [single_eq_same, zero_smul]

Result:
no goals

Proof state:
α : Type u_1
M : Type u_2
R : Type u_5
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
c : M
a : α
f : α →₀ R
inst✝ : DecidableEq α
⊢ (linearCombination R (Pi.single a c)) f = f a • c

Tactic:
rw [linearCombination_apply, sum_eq_single a, Pi.single_eq_same]

Result:
case h₀
α : Type u_1
M : Type u_2
R : Type u_5
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
c : M
a : α
f : α →₀ R
inst✝ : DecidableEq α
⊢ ∀ (b : α), f b ≠ 0 → b ≠ a → f b • Pi.single a c b = 0

case h₁
α : Type u_1
M : Type u_2
R : Type u_5
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
c : M
a : α
f : α →₀ R
inst✝ : DecidableEq α
⊢ f a = 0 → 0 • Pi.single a c a = 0

Proof state:
case h₀
α : Type u_1
M : Type u_2
R : Type u_5
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
c : M
a : α
f : α →₀ R
inst✝ : DecidableEq α
⊢ ∀ (b : α), f b ≠ 0 → b ≠ a → f b • Pi.single a c b = 0

Tactic:
exact fun i _ hi ↦ by rw [Pi.single_eq_of_ne hi, smul_zero]

Result:
no goals

Proof state:
α : Type u_1
M : Type u_2
R : Type u_5
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
c : M
a : α
f : α →₀ R
inst✝ : DecidableEq α
i : α
x✝ : f i ≠ 0
hi : i ≠ a
⊢ f i • Pi.single a c i = 0

Tactic:
rw [Pi.single_eq_of_ne hi, smul_zero]

Result:
no goals

Proof state:
case h₁
α : Type u_1
M : Type u_2
R : Type u_5
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
c : M
a : α
f : α →₀ R
inst✝ : DecidableEq α
⊢ f a = 0 → 0 • Pi.single a c a = 0

Tactic:
exact fun _ ↦ by simp only [single_eq_same, zero_smul]

Result:
no goals
-- Mathlib/Algebra/CharP/Defs.lean
@[simp] lemma ringExpChar.eq_one [CharZero R] : ringExpChar R = 1

Proof state:
R : Type u_1
inst✝¹ : NonAssocSemiring R
inst✝ : CharZero R
⊢ ringExpChar R = 1

Tactic:
rw [ringExpChar, ringChar.eq_zero, max_eq_right (Nat.zero_le _)]

Result:
no goals
-- Mathlib/Algebra/Group/Basic.lean
theorem inv_mul_eq_iff_eq_mul : a⁻¹ * b = c ↔ b = a * c :=
  ⟨fun h ↦ by rw [← h, mul_inv_cancel_left], fun h ↦ by rw [h, inv_mul_cancel_left]⟩

Proof state:
G : Type u_3
inst✝ : Group G
a b c : G
h : a⁻¹ * b = c
⊢ b = a * c

Tactic:
rw [← h, mul_inv_cancel_left]

Result:
no goals

Proof state:
G : Type u_3
inst✝ : Group G
a b c : G
h : b = a * c
⊢ a⁻¹ * b = c

Tactic:
rw [h, inv_mul_cancel_left]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Complex/Circle.lean
@[simp] lemma toCircle_zero : toCircle (0 : AddCircle T) = 1

Proof state:
T : ℝ
⊢ toCircle 0 = 1

Tactic:
rw [← QuotientAddGroup.mk_zero, toCircle_apply_mk, mul_zero, Circle.exp_zero]

Result:
no goals