harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Data/Set/Card.lean
theorem _root_.Function.Embedding.encard_le (e : s ↪ t) : s.encard ≤ t.encard

Proof state:
α : Type u_1
β : Type u_2
s : Set α
t : Set β
e : ↑s ↪ ↑t
⊢ ((fun a => ↑a) '' (⇑e '' univ)).encard ≤ t.encard

Tactic:
exact encard_mono (by simp)

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
s : Set α
t : Set β
e : ↑s ↪ ↑t
⊢ s.encard ≤ t.encard

Tactic:
rw [← encard_univ_coe, ← e.injective.encard_image, ← Subtype.coe_injective.encard_image]

Result:
α : Type u_1
β : Type u_2
s : Set α
t : Set β
e : ↑s ↪ ↑t
⊢ ((fun a => ↑a) '' (⇑e '' univ)).encard ≤ t.encard

Proof state:
α : Type u_1
β : Type u_2
s : Set α
t : Set β
e : ↑s ↪ ↑t
⊢ (fun a => ↑a) '' (⇑e '' univ) ≤ t

Tactic:
simp

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Bool.lean
theorem lt_iff_le_not_le : ∀ {x y : Bool}, x < y ↔ x ≤ y ∧ ¬ y ≤ x

Proof state:
⊢ ∀ {x y : Bool}, x < y ↔ x ≤ y ∧ ¬y ≤ x

Tactic:
decide

Result:
no goals
-- Mathlib/RingTheory/Support.lean
lemma Module.not_mem_support_iff' :
    p ∉ Module.support R M ↔ ∀ m : M, ∃ r ∉ p.asIdeal, r • m = 0

Proof state:
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
p : PrimeSpectrum R
⊢ p ∉ support R M ↔ ∀ (m : M), ∃ r ∉ p.asIdeal, r • m = 0

Tactic:
simp only [not_mem_support_iff, Ideal.primeCompl, LocalizedModule.subsingleton_iff,
  Submonoid.mem_mk, Subsemigroup.mem_mk, Set.mem_compl_iff, SetLike.mem_coe]

Result:
no goals
-- Mathlib/Data/Sym/Sym2.lean
theorem IsDiag.mem_range_diag {z : Sym2 α} : IsDiag z → z ∈ Set.range (@diag α)

Proof state:
case h
α : Type u_1
x : α
⊢ s(x, x) ∈ Set.range diag

Tactic:
exact ⟨_, rfl⟩

Result:
no goals

Proof state:
case h
α : Type u_1
x y : α
⊢ s(x, y).IsDiag → s(x, y) ∈ Set.range diag

Tactic:
rintro (rfl : x = y)

Result:
case h
α : Type u_1
x : α
⊢ s(x, x) ∈ Set.range diag

Proof state:
α : Type u_1
z : Sym2 α
⊢ z.IsDiag → z ∈ Set.range diag

Tactic:
induction' z with x y

Result:
case h
α : Type u_1
x y : α
⊢ s(x, y).IsDiag → s(x, y) ∈ Set.range diag
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Basic.lean
theorem replicateTR_loop_eq : ∀ n, replicateTR.loop a n acc = replicate n a ++ acc
  | 0 => rfl
  | n+1 => by rw [← replicateTR_loop_replicate_eq _ 1 n, replicate, replicate,
    replicateTR.loop, replicateTR_loop_eq n, replicateTR_loop_eq n, append_assoc]; rfl

Proof state:
α✝ : Type u_1
a : α✝
acc : List α✝
n : Nat
⊢ replicate n a ++ a :: acc = replicate n a ++ (a :: nil ++ acc)

Tactic:
rfl

Result:
no goals

Proof state:
α✝ : Type u_1
a : α✝
acc : List α✝
n : Nat
⊢ replicateTR.loop a (n + 1) acc = replicate (n + 1) a ++ acc

Tactic:
rw [← replicateTR_loop_replicate_eq _ 1 n, replicate, replicate,
replicateTR.loop, replicateTR_loop_eq n, replicateTR_loop_eq n, append_assoc]

Result:
α✝ : Type u_1
a : α✝
acc : List α✝
n : Nat
⊢ replicate n a ++ a :: acc = replicate n a ++ (a :: nil ++ acc)
-- Mathlib/Order/Interval/Finset/Fin.lean
theorem card_Iic : #(Iic b) = b + 1

Proof state:
n : ℕ
b : Fin n
⊢ #(Iic b) = ↑b + 1

Tactic:
rw [← Nat.card_Iic b, ← map_valEmbedding_Iic, card_map]

Result:
no goals
-- Mathlib/MeasureTheory/Measure/FiniteMeasureProd.lean
lemma prod_prod (s : Set α) (t : Set β) : μ.prod ν (s ×ˢ t) = μ s * ν t

Proof state:
α : Type u_1
inst✝¹ : MeasurableSpace α
β : Type u_2
inst✝ : MeasurableSpace β
μ : FiniteMeasure α
ν : FiniteMeasure β
s : Set α
t : Set β
⊢ (μ.prod ν) (s ×ˢ t) = μ s * ν t

Tactic:
simp [coeFn_def]

Result:
no goals
-- Mathlib/Algebra/Group/EvenFunction.lean
lemma Odd.mul_odd [HasDistribNeg R] (hf : f.Odd) (hg : g.Odd) : (f * g).Even

Proof state:
α : Type u_1
inst✝² : Neg α
R : Type u_3
inst✝¹ : Mul R
f g : α → R
inst✝ : HasDistribNeg R
hf : Function.Odd f
hg : Function.Odd g
⊢ Function.Even (f * g)

Tactic:
intro a

Result:
α : Type u_1
inst✝² : Neg α
R : Type u_3
inst✝¹ : Mul R
f g : α → R
inst✝ : HasDistribNeg R
hf : Function.Odd f
hg : Function.Odd g
a : α
⊢ (f * g) (-a) = (f * g) a

Proof state:
α : Type u_1
inst✝² : Neg α
R : Type u_3
inst✝¹ : Mul R
f g : α → R
inst✝ : HasDistribNeg R
hf : Function.Odd f
hg : Function.Odd g
a : α
⊢ (f * g) (-a) = (f * g) a

Tactic:
simp only [Pi.mul_apply, hf a, hg a, mul_neg, neg_mul, neg_neg]

Result:
no goals
-- Mathlib/Computability/Language.lean
theorem map_id (l : Language α) : map id l = l

Proof state:
α : Type u_1
l : Language α
⊢ (map id) l = l

Tactic:
simp [map]

Result:
no goals
-- Mathlib/NumberTheory/VonMangoldt.lean
theorem vonMangoldt_ne_zero_iff {n : ℕ} : Λ n ≠ 0 ↔ IsPrimePow n

Proof state:
case inr
n : ℕ
hn : n ≠ 1
⊢ Λ n ≠ 0 ↔ IsPrimePow n

Tactic:
exact (Real.log_pos (one_lt_cast.2 (minFac_prime hn).one_lt)).ne'.ite_ne_right_iff

Result:
no goals

Proof state:
case inl

⊢ Λ 1 ≠ 0 ↔ IsPrimePow 1

Tactic:
simp [not_isPrimePow_one]

Result:
no goals

Proof state:
n : ℕ
⊢ Λ n ≠ 0 ↔ IsPrimePow n

Tactic:
rcases eq_or_ne n 1 with (rfl | hn)

Result:
case inl

⊢ Λ 1 ≠ 0 ↔ IsPrimePow 1

case inr
n : ℕ
hn : n ≠ 1
⊢ Λ n ≠ 0 ↔ IsPrimePow n
-- Mathlib/SetTheory/Cardinal/Arithmetic.lean
theorem ciSup_mul_ciSup (g : ι' → Cardinal.{v}) :
    (⨆ i, f i) * (⨆ j, g j) = ⨆ (i) (j), f i * g j

Proof state:
ι : Type u
ι' : Type w
f : ι → Cardinal.{v}
g : ι' → Cardinal.{v}
⊢ (⨆ i, f i) * ⨆ j, g j = ⨆ i, ⨆ j, f i * g j

Tactic:
simp_rw [Cardinal.ciSup_mul f, Cardinal.mul_ciSup g]

Result:
no goals
-- Mathlib/Algebra/Order/Sub/Unbundled/Basic.lean
theorem tsub_tsub_assoc (hbc : AddLECancellable (b - c)) (h₁ : b ≤ a) (h₂ : c ≤ b) :
    a - (b - c) = a - b + c :=
  hbc.tsub_eq_of_eq_add <| by rw [add_assoc, add_tsub_cancel_of_le h₂, tsub_add_cancel_of_le h₁]

Proof state:
α : Type u_1
inst✝⁵ : AddCommSemigroup α
inst✝⁴ : PartialOrder α
inst✝³ : ExistsAddOfLE α
inst✝² : AddLeftMono α
inst✝¹ : Sub α
inst✝ : OrderedSub α
a b c : α
hbc : AddLECancellable (b - c)
h₁ : b ≤ a
h₂ : c ≤ b
⊢ a = a - b + c + (b - c)

Tactic:
rw [add_assoc, add_tsub_cancel_of_le h₂, tsub_add_cancel_of_le h₁]

Result:
no goals
-- Mathlib/Analysis/Normed/Group/Pointwise.lean
theorem div_ball : s / ball x δ = x⁻¹ • thickening δ s

Proof state:
E : Type u_1
inst✝ : SeminormedCommGroup E
δ : ℝ
s : Set E
x : E
⊢ s / ball x δ = x⁻¹ • thickening δ s

Tactic:
simp [div_eq_mul_inv]

Result:
no goals
-- Mathlib/CategoryTheory/Monoidal/Category.lean
theorem pentagon_inv_inv_hom_inv_inv :
    (α_ W X (Y ⊗ Z)).inv ≫ (α_ (W ⊗ X) Y Z).inv ≫ (α_ W X Y).hom ▷ Z =
      W ◁ (α_ X Y Z).inv ≫ (α_ W (X ⊗ Y) Z).inv :=
  eq_of_inv_eq_inv (by simp)

Proof state:
C : Type u
𝒞 : Category.{v, u} C
inst✝ : MonoidalCategory C
W X Y Z : C
⊢ inv ((α_ W X (Y ⊗ Z)).inv ≫ (α_ (W ⊗ X) Y Z).inv ≫ (α_ W X Y).hom ▷ Z) =
    inv (W ◁ (α_ X Y Z).inv ≫ (α_ W (X ⊗ Y) Z).inv)

Tactic:
simp

Result:
no goals
-- Mathlib/LinearAlgebra/LinearIndependent/Defs.lean
theorem LinearMap.linearIndepOn_iff_of_injOn (f : M →ₗ[R] M')
    (hf_inj : Set.InjOn f (span R (v '' s))) :
    LinearIndepOn R (f ∘ v) s ↔ LinearIndepOn R v s :=
  f.linearIndependent_iff_of_injOn (by rwa [← image_eq_range]) (v := fun i : s ↦ v i)

Proof state:
ι : Type u'
R : Type u_2
s : Set ι
M : Type u_4
M' : Type u_5
v : ι → M
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M'
inst✝¹ : Module R M
inst✝ : Module R M'
f : M →ₗ[R] M'
hf_inj : InjOn ⇑f ↑(span R (v '' s))
⊢ InjOn ⇑f ↑(span R (Set.range fun i => v ↑i))

Tactic:
rwa [← image_eq_range]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Int/Lemmas.lean
theorem natCast_add (a b : Nat) : ((a + b : Nat) : Int) = (a : Int) + (b : Int)

Proof state:
a b : Nat
⊢ ↑(a + b) = ↑a + ↑b

Tactic:
simp

Result:
no goals
-- Mathlib/Algebra/Module/Defs.lean
theorem neg_smul : -r • x = -(r • x) :=
  eq_neg_of_add_eq_zero_left <| by rw [← add_smul, neg_add_cancel, zero_smul]

Proof state:
R : Type u_1
M : Type u_3
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
r : R
x : M
⊢ -r • x + r • x = 0

Tactic:
rw [← add_smul, neg_add_cancel, zero_smul]

Result:
no goals
-- Mathlib/Analysis/Analytic/Constructions.lean
theorem AnalyticWithinAt.sub (hf : AnalyticWithinAt 𝕜 f s x) (hg : AnalyticWithinAt 𝕜 g s x) :
    AnalyticWithinAt 𝕜 (f - g) s x

Proof state:
𝕜 : Type u_2
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_3
F : Type u_4
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f g : E → F
s : Set E
x : E
hf : AnalyticWithinAt 𝕜 f s x
hg : AnalyticWithinAt 𝕜 g s x
⊢ AnalyticWithinAt 𝕜 (f - g) s x

Tactic:
simpa only [sub_eq_add_neg] using hf.add hg.neg

Result:
no goals
-- Mathlib/Algebra/GroupWithZero/NonZeroDivisors.lean
lemma nmem_nonZeroDivisorsLeft_iff :
    x ∉ nonZeroDivisorsLeft M₀ ↔ {y | y * x = 0 ∧ y ≠ 0}.Nonempty

Proof state:
M₀ : Type u_1
inst✝ : MonoidWithZero M₀
x : M₀
⊢ x ∉ nonZeroDivisorsLeft M₀ ↔ {y | y * x = 0 ∧ y ≠ 0}.Nonempty

Tactic:
simpa [mem_nonZeroDivisorsLeft_iff] using Set.nonempty_def.symm

Result:
no goals
-- Mathlib/Order/Filter/Map.lean
theorem map_top (f : α → β) : map f ⊤ = 𝓟 (range f)

Proof state:
α : Type u_1
β : Type u_2
f : α → β
⊢ map f ⊤ = 𝓟 (range f)

Tactic:
rw [← principal_univ, map_principal, image_univ]

Result:
no goals
-- Mathlib/CategoryTheory/ChosenFiniteProducts.lean
@[simp]
lemma lift_fst_comp_snd_comp {W X Y Z : C} (g : W ⟶ X) (g' : Y ⟶ Z) :
    lift (fst _ _ ≫ g) (snd _ _ ≫ g') = g ⊗ g'

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : ChosenFiniteProducts C
W X Y Z : C
g : W ⟶ X
g' : Y ⟶ Z
⊢ lift (fst W Y ≫ g) (snd W Y ≫ g') = g ⊗ g'

Tactic:
ext <;> simp

Result:
no goals
-- Mathlib/Analysis/Calculus/IteratedDeriv/Lemmas.lean
lemma iteratedDeriv_add (hf : ContDiffAt 𝕜 n f x) (hg : ContDiffAt 𝕜 n g x) :
    iteratedDeriv n (f + g) x = iteratedDeriv n f x + iteratedDeriv n g x

Proof state:
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
n : ℕ
x : 𝕜
f g : 𝕜 → F
hf : ContDiffAt 𝕜 (↑n) f x
hg : ContDiffAt 𝕜 (↑n) g x
⊢ iteratedDeriv n (f + g) x = iteratedDeriv n f x + iteratedDeriv n g x

Tactic:
simpa only [iteratedDerivWithin_univ] using
  iteratedDerivWithin_add (Set.mem_univ _) uniqueDiffOn_univ hf hg

Result:
no goals
-- Mathlib/RingTheory/Localization/AtPrime.lean
theorem mk'_mem_maximal_iff (x : R) (y : I.primeCompl) (h : IsLocalRing S := isLocalRing S I) :
    mk' S x y ∈ IsLocalRing.maximalIdeal S ↔ x ∈ I :=
  not_iff_not.mp <| by
    simpa only [IsLocalRing.mem_maximalIdeal, mem_nonunits_iff, Classical.not_not] using
      isUnit_mk'_iff S I x y

Proof state:
R : Type u_1
inst✝³ : CommSemiring R
S : Type u_2
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
I : Ideal R
hI : I.IsPrime
inst✝ : IsLocalization.AtPrime S I
x : R
y : ↥I.primeCompl
h : optParam (IsLocalRing S) ⋯
⊢ mk' S x y ∉ IsLocalRing.maximalIdeal S ↔ x ∉ I

Tactic:
simpa only [IsLocalRing.mem_maximalIdeal, mem_nonunits_iff, Classical.not_not] using
  isUnit_mk'_iff S I x y

Result:
no goals
-- Mathlib/CategoryTheory/Subpresheaf/Image.lean
lemma preimage_eq_top_iff (G : Subpresheaf F) (p : F' ⟶ F) :
    G.preimage p = ⊤ ↔ range p ≤ G

Proof state:
C : Type u
inst✝ : Category.{v, u} C
F F' : Cᵒᵖ ⥤ Type w
G : Subpresheaf F
p : F' ⟶ F
⊢ G.preimage p = ⊤ ↔ ⊤ ≤ G.preimage p

Tactic:
aesop

Result:
no goals

Proof state:
C : Type u
inst✝ : Category.{v, u} C
F F' : Cᵒᵖ ⥤ Type w
G : Subpresheaf F
p : F' ⟶ F
⊢ G.preimage p = ⊤ ↔ range p ≤ G

Tactic:
rw [← image_top, image_le_iff]

Result:
C : Type u
inst✝ : Category.{v, u} C
F F' : Cᵒᵖ ⥤ Type w
G : Subpresheaf F
p : F' ⟶ F
⊢ G.preimage p = ⊤ ↔ ⊤ ≤ G.preimage p
-- Mathlib/GroupTheory/Index.lean
theorem inf_relindex_right : (H ⊓ K).relindex K = H.relindex K

Proof state:
G : Type u_1
inst✝ : Group G
H K : Subgroup G
⊢ (H ⊓ K).relindex K = H.relindex K

Tactic:
rw [relindex, relindex, inf_subgroupOf_right]

Result:
no goals
-- Mathlib/LinearAlgebra/Matrix/Hermitian.lean
theorem IsHermitian.ext {A : Matrix n n α} : (∀ i j, star (A j i) = A i j) → A.IsHermitian

Proof state:
α : Type u_1
n : Type u_4
inst✝ : Star α
A : Matrix n n α
h : ∀ (i j : n), star (A j i) = A i j
⊢ A.IsHermitian

Tactic:
ext i j

Result:
case a
α : Type u_1
n : Type u_4
inst✝ : Star α
A : Matrix n n α
h : ∀ (i j : n), star (A j i) = A i j
i j : n
⊢ Aᴴ i j = A i j

Proof state:
α : Type u_1
n : Type u_4
inst✝ : Star α
A : Matrix n n α
⊢ (∀ (i j : n), star (A j i) = A i j) → A.IsHermitian

Tactic:
intro h

Result:
α : Type u_1
n : Type u_4
inst✝ : Star α
A : Matrix n n α
h : ∀ (i j : n), star (A j i) = A i j
⊢ A.IsHermitian

Proof state:
case a
α : Type u_1
n : Type u_4
inst✝ : Star α
A : Matrix n n α
h : ∀ (i j : n), star (A j i) = A i j
i j : n
⊢ Aᴴ i j = A i j

Tactic:
exact h i j

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/List/Associative.lean
theorem getValue!_insertListConst_of_contains_eq_false [BEq α] [PartialEquivBEq α] [Inhabited β]
    {l : List ((_ : α) × β)} {toInsert : List (α × β)} {k : α}
    (not_contains : (toInsert.map Prod.fst).contains k = false) :
    getValue! k (insertListConst l toInsert) = getValue! k l

Proof state:
α : Type u
β : Type v
inst✝² : BEq α
inst✝¹ : PartialEquivBEq α
inst✝ : Inhabited β
l : List ((_ : α) × β)
toInsert : List (α × β)
k : α
not_contains : (List.map Prod.fst toInsert).contains k = false
⊢ getValue! k (insertListConst l toInsert) = getValue! k l

Tactic:
simp only [getValue!_eq_getValue?]

Result:
α : Type u
β : Type v
inst✝² : BEq α
inst✝¹ : PartialEquivBEq α
inst✝ : Inhabited β
l : List ((_ : α) × β)
toInsert : List (α × β)
k : α
not_contains : (List.map Prod.fst toInsert).contains k = false
⊢ (getValue? k (insertListConst l toInsert)).get! = (getValue? k l).get!

Proof state:
α : Type u
β : Type v
inst✝² : BEq α
inst✝¹ : PartialEquivBEq α
inst✝ : Inhabited β
l : List ((_ : α) × β)
toInsert : List (α × β)
k : α
not_contains : (List.map Prod.fst toInsert).contains k = false
⊢ (getValue? k (insertListConst l toInsert)).get! = (getValue? k l).get!

Tactic:
rw [getValue?_insertListConst_of_contains_eq_false not_contains]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Lemmas.lean
theorem mkVector_eq_append_iff {l₁ : Vector α n} {l₂ : Vector α m} {a : α} :
    mkVector (n + m) a = l₁ ++ l₂ ↔ l₁ = mkVector n a ∧ l₂ = mkVector m a

Proof state:
α : Type u_1
n m : Nat
l₁ : Vector α n
l₂ : Vector α m
a : α
⊢ mkVector (n + m) a = l₁ ++ l₂ ↔ l₁ = mkVector n a ∧ l₂ = mkVector m a

Tactic:
rw [eq_comm, append_eq_mkVector_iff]

Result:
no goals
-- Mathlib/CategoryTheory/Products/Bifunctor.lean
theorem diagonal' (F : C × D ⥤ E) (X X' : C) (f : X ⟶ X') (Y Y' : D) (g : Y ⟶ Y') :
    F.map ((f, 𝟙 Y) : (X, Y) ⟶ (X', Y)) ≫ F.map ((𝟙 X', g) : (X', Y) ⟶ (X', Y')) =
      F.map ((f, g) : (X, Y) ⟶ (X', Y'))

Proof state:
C : Type u₁
D : Type u₂
E : Type u₃
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Category.{v₂, u₂} D
inst✝ : Category.{v₃, u₃} E
F : C × D ⥤ E
X X' : C
f : X ⟶ X'
Y Y' : D
g : Y ⟶ Y'
⊢ F.map (f, 𝟙 Y) ≫ F.map (𝟙 X', g) = F.map (f, g)

Tactic:
rw [← Functor.map_comp, prod_comp, Category.id_comp, Category.comp_id]

Result:
no goals
-- Mathlib/Algebra/Order/Monoid/Unbundled/Basic.lean
theorem mul_le_iff_le_one_left' [MulRightMono α]
    [MulRightReflectLE α] {a b : α} :
    a * b ≤ b ↔ a ≤ 1 :=
  Iff.trans (by rw [one_mul]) (mul_le_mul_iff_right b)

Proof state:
α : Type u_1
inst✝³ : MulOneClass α
inst✝² : LE α
inst✝¹ : MulRightMono α
inst✝ : MulRightReflectLE α
a b : α
⊢ a * b ≤ b ↔ a * b ≤ 1 * b

Tactic:
rw [one_mul]

Result:
no goals
-- Mathlib/Analysis/Calculus/ContDiff/Defs.lean
theorem contDiffOn_of_locally_contDiffOn
    (h : ∀ x ∈ s, ∃ u, IsOpen u ∧ x ∈ u ∧ ContDiffOn 𝕜 n f (s ∩ u)) : ContDiffOn 𝕜 n f s

Proof state:
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
s : Set E
f : E → F
n : WithTop ℕ∞
h : ∀ x ∈ s, ∃ u, IsOpen u ∧ x ∈ u ∧ ContDiffOn 𝕜 n f (s ∩ u)
x : E
xs : x ∈ s
u : Set E
u_open : IsOpen u
xu : x ∈ u
hu : ContDiffOn 𝕜 n f (s ∩ u)
⊢ u ∈ 𝓝 x

Tactic:
exact IsOpen.mem_nhds u_open xu

Result:
no goals

Proof state:
case intro.intro.intro
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
s : Set E
f : E → F
n : WithTop ℕ∞
h : ∀ x ∈ s, ∃ u, IsOpen u ∧ x ∈ u ∧ ContDiffOn 𝕜 n f (s ∩ u)
x : E
xs : x ∈ s
u : Set E
u_open : IsOpen u
xu : x ∈ u
hu : ContDiffOn 𝕜 n f (s ∩ u)
⊢ ContDiffWithinAt 𝕜 n f s x

Tactic:
apply (contDiffWithinAt_inter _).1 (hu x ⟨xs, xu⟩)

Result:
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
s : Set E
f : E → F
n : WithTop ℕ∞
h : ∀ x ∈ s, ∃ u, IsOpen u ∧ x ∈ u ∧ ContDiffOn 𝕜 n f (s ∩ u)
x : E
xs : x ∈ s
u : Set E
u_open : IsOpen u
xu : x ∈ u
hu : ContDiffOn 𝕜 n f (s ∩ u)
⊢ u ∈ 𝓝 x

Proof state:
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
s : Set E
f : E → F
n : WithTop ℕ∞
h : ∀ x ∈ s, ∃ u, IsOpen u ∧ x ∈ u ∧ ContDiffOn 𝕜 n f (s ∩ u)
⊢ ContDiffOn 𝕜 n f s

Tactic:
intro x xs

Result:
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
s : Set E
f : E → F
n : WithTop ℕ∞
h : ∀ x ∈ s, ∃ u, IsOpen u ∧ x ∈ u ∧ ContDiffOn 𝕜 n f (s ∩ u)
x : E
xs : x ∈ s
⊢ ContDiffWithinAt 𝕜 n f s x

Proof state:
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
s : Set E
f : E → F
n : WithTop ℕ∞
h : ∀ x ∈ s, ∃ u, IsOpen u ∧ x ∈ u ∧ ContDiffOn 𝕜 n f (s ∩ u)
x : E
xs : x ∈ s
⊢ ContDiffWithinAt 𝕜 n f s x

Tactic:
rcases h x xs with ⟨u, u_open, xu, hu⟩

Result:
case intro.intro.intro
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
s : Set E
f : E → F
n : WithTop ℕ∞
h : ∀ x ∈ s, ∃ u, IsOpen u ∧ x ∈ u ∧ ContDiffOn 𝕜 n f (s ∩ u)
x : E
xs : x ∈ s
u : Set E
u_open : IsOpen u
xu : x ∈ u
hu : ContDiffOn 𝕜 n f (s ∩ u)
⊢ ContDiffWithinAt 𝕜 n f s x
-- Mathlib/Algebra/Group/Subgroup/Finsupp.lean
theorem mem_closure_range_iff :
    x ∈ closure (Set.range f) ↔ ∃ a : ι →₀ ℤ, x = a.prod (f · ^ ·)

Proof state:
M : Type u_1
inst✝ : CommGroup M
ι : Type u_2
f : ι → M
x : M
⊢ x ∈ closure (Set.range f) ↔ ∃ a, x = a.prod fun x1 x2 => f x1 ^ x2

Tactic:
refine ⟨exists_finsupp_of_mem_closure_range f x, ?_⟩

Result:
M : Type u_1
inst✝ : CommGroup M
ι : Type u_2
f : ι → M
x : M
⊢ (∃ a, x = a.prod fun x1 x2 => f x1 ^ x2) → x ∈ closure (Set.range f)

Proof state:
M : Type u_1
inst✝ : CommGroup M
ι : Type u_2
f : ι → M
x : M
⊢ (∃ a, x = a.prod fun x1 x2 => f x1 ^ x2) → x ∈ closure (Set.range f)

Tactic:
rintro ⟨a, rfl⟩

Result:
case intro
M : Type u_1
inst✝ : CommGroup M
ι : Type u_2
f : ι → M
a : ι →₀ ℤ
⊢ (a.prod fun x1 x2 => f x1 ^ x2) ∈ closure (Set.range f)

Proof state:
case intro
M : Type u_1
inst✝ : CommGroup M
ι : Type u_2
f : ι → M
a : ι →₀ ℤ
⊢ (a.prod fun x1 x2 => f x1 ^ x2) ∈ closure (Set.range f)

Tactic:
exact Submonoid.prod_mem _ fun i hi ↦ zpow_mem (subset_closure (Set.mem_range_self i)) _

Result:
no goals
-- Mathlib/Topology/MetricSpace/Infsep.lean
theorem einfsep_pair_le_right (hxy : x ≠ y) : ({x, y} : Set α).einfsep ≤ edist y x

Proof state:
α : Type u_1
inst✝ : EDist α
x y : α
hxy : x ≠ y
⊢ {x, y}.einfsep ≤ edist y x

Tactic:
rw [pair_comm]

Result:
α : Type u_1
inst✝ : EDist α
x y : α
hxy : x ≠ y
⊢ {y, x}.einfsep ≤ edist y x

Proof state:
α : Type u_1
inst✝ : EDist α
x y : α
hxy : x ≠ y
⊢ {y, x}.einfsep ≤ edist y x

Tactic:
exact einfsep_pair_le_left hxy.symm

Result:
no goals
-- Mathlib/Algebra/Module/Submodule/Range.lean
theorem range_le_iff_comap [RingHomSurjective τ₁₂] {f : F} {p : Submodule R₂ M₂} :
    range f ≤ p ↔ comap f p = ⊤

Proof state:
R : Type u_1
R₂ : Type u_2
M : Type u_5
M₂ : Type u_6
inst✝⁸ : Semiring R
inst✝⁷ : Semiring R₂
inst✝⁶ : AddCommMonoid M
inst✝⁵ : AddCommMonoid M₂
inst✝⁴ : Module R M
inst✝³ : Module R₂ M₂
τ₁₂ : R →+* R₂
F : Type u_10
inst✝² : FunLike F M M₂
inst✝¹ : SemilinearMapClass F τ₁₂ M M₂
inst✝ : RingHomSurjective τ₁₂
f : F
p : Submodule R₂ M₂
⊢ range f ≤ p ↔ comap f p = ⊤

Tactic:
rw [range_eq_map, map_le_iff_le_comap, eq_top_iff]

Result:
no goals
-- Mathlib/Probability/Kernel/Composition/Prod.lean
theorem lintegral_deterministic_prod {f : α → β} (hf : Measurable f) (κ : Kernel α γ)
    [IsSFiniteKernel κ] (a : α) {g : (β × γ) → ℝ≥0∞} (hg : Measurable g) :
    ∫⁻ p, g p ∂((deterministic f hf) ×ₖ κ) a = ∫⁻ c, g (f a, c) ∂κ a

Proof state:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
γ : Type u_4
mγ : MeasurableSpace γ
f : α → β
hf : Measurable f
κ : Kernel α γ
inst✝ : IsSFiniteKernel κ
a : α
g : β × γ → ℝ≥0∞
hg : Measurable g
⊢ ∫⁻ (p : β × γ), g p ∂(deterministic f hf ×ₖ κ) a = ∫⁻ (c : γ), g (f a, c) ∂κ a

Tactic:
rw [lintegral_prod _ _ _ hg, lintegral_deterministic' _ hg.lintegral_prod_right']

Result:
no goals
-- Mathlib/Data/Set/Subsingleton.lean
protected lemma subsingleton_or_nontrivial (s : Set α) : s.Subsingleton ∨ s.Nontrivial

Proof state:
α : Type u
s : Set α
⊢ s.Subsingleton ∨ s.Nontrivial

Tactic:
simp [or_iff_not_imp_right]

Result:
no goals
-- Mathlib/LinearAlgebra/Dimension/Finite.lean
theorem Module.nontrivial_of_finrank_eq_succ {n : ℕ}
    (hn : finrank R M = n.succ) : Nontrivial M :=
  nontrivial_of_finrank_pos (R := R) (by rw [hn]; exact n.succ_pos)

Proof state:
R : Type u
M : Type v
inst✝⁴ : Ring R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : Nontrivial R
inst✝ : NoZeroSMulDivisors R M
n : ℕ
hn : finrank R M = n.succ
⊢ 0 < n.succ

Tactic:
exact n.succ_pos

Result:
no goals

Proof state:
R : Type u
M : Type v
inst✝⁴ : Ring R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : Nontrivial R
inst✝ : NoZeroSMulDivisors R M
n : ℕ
hn : finrank R M = n.succ
⊢ 0 < finrank R M

Tactic:
rw [hn]

Result:
R : Type u
M : Type v
inst✝⁴ : Ring R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : Nontrivial R
inst✝ : NoZeroSMulDivisors R M
n : ℕ
hn : finrank R M = n.succ
⊢ 0 < n.succ
-- Mathlib/Topology/Filter.lean
theorem nhds_pure (x : α) : 𝓝 (pure x : Filter α) = 𝓟 {⊥, pure x}

Proof state:
α : Type u_2
x : α
⊢ 𝓝 (pure x) = 𝓟 {⊥, pure x}

Tactic:
rw [← principal_singleton, nhds_principal, principal_singleton, Iic_pure]

Result:
no goals
-- Mathlib/Algebra/Group/Basic.lean
@[to_additive]
lemma mul_left_iterate_apply_one (a : M) : (a * ·)^[n] 1 = a ^ n

Proof state:
M : Type u_4
inst✝ : Monoid M
n : ℕ
a : M
⊢ (fun x => a * x)^[n] 1 = a ^ n

Tactic:
simp [mul_right_iterate]

Result:
no goals
-- Mathlib/LinearAlgebra/Finsupp/Supported.lean
theorem supported_iInter {ι : Type*} (s : ι → Set α) :
    supported M R (⋂ i, s i) = ⨅ i, supported M R (s i) :=
  Submodule.ext fun x => by simp [mem_supported, subset_iInter_iff]

Proof state:
α : Type u_1
M : Type u_2
R : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
ι : Type u_7
s : ι → Set α
x : α →₀ M
⊢ x ∈ supported M R (⋂ i, s i) ↔ x ∈ ⨅ i, supported M R (s i)

Tactic:
simp [mem_supported, subset_iInter_iff]

Result:
no goals
-- Mathlib/RingTheory/LinearDisjoint.lean
theorem rank_sup_of_free [Module.Free R A] [Module.Free R B] :
    Module.rank R ↥(A ⊔ B) = Module.rank R A * Module.rank R B

Proof state:
R : Type u
S : Type v
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
A B : Subalgebra R S
H : A.LinearDisjoint B
inst✝¹ : Module.Free R ↥A
inst✝ : Module.Free R ↥B
a✝ : Nontrivial R
⊢ Module.rank R ↥(A ⊔ B) = Module.rank R ↥A * Module.rank R ↥B

Tactic:
rw [← rank_tensorProduct', H.mulMap.toLinearEquiv.rank_eq]

Result:
no goals

Proof state:
R : Type u
S : Type v
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
A B : Subalgebra R S
H : A.LinearDisjoint B
inst✝¹ : Module.Free R ↥A
inst✝ : Module.Free R ↥B
⊢ Module.rank R ↥(A ⊔ B) = Module.rank R ↥A * Module.rank R ↥B

Tactic:
nontriviality R

Result:
R : Type u
S : Type v
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
A B : Subalgebra R S
H : A.LinearDisjoint B
inst✝¹ : Module.Free R ↥A
inst✝ : Module.Free R ↥B
a✝ : Nontrivial R
⊢ Module.rank R ↥(A ⊔ B) = Module.rank R ↥A * Module.rank R ↥B