harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Probability/Kernel/Disintegration/Integral.lean
lemma integral_condKernel (hf : Integrable f ρ) :
    ∫ b, ∫ ω, f (b, ω) ∂(ρ.condKernel b) ∂ρ.fst = ∫ x, f x ∂ρ

Proof state:
β : Type u_1
Ω : Type u_2
mβ : MeasurableSpace β
inst✝⁵ : MeasurableSpace Ω
inst✝⁴ : StandardBorelSpace Ω
inst✝³ : Nonempty Ω
ρ : Measure (β × Ω)
inst✝² : IsFiniteMeasure ρ
E : Type u_3
f : β × Ω → E
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
hf : Integrable f ρ
⊢ ∫ (b : β), ∫ (ω : Ω), f (b, ω) ∂ρ.condKernel b ∂ρ.fst = ∫ (x : β × Ω), f x ∂ρ.fst ⊗ₘ ρ.condKernel

Tactic:
rw [← ρ.disintegrate ρ.condKernel] at hf

Result:
β : Type u_1
Ω : Type u_2
mβ : MeasurableSpace β
inst✝⁵ : MeasurableSpace Ω
inst✝⁴ : StandardBorelSpace Ω
inst✝³ : Nonempty Ω
ρ : Measure (β × Ω)
inst✝² : IsFiniteMeasure ρ
E : Type u_3
f : β × Ω → E
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
hf : Integrable f (ρ.fst ⊗ₘ ρ.condKernel)
⊢ ∫ (b : β), ∫ (ω : Ω), f (b, ω) ∂ρ.condKernel b ∂ρ.fst = ∫ (x : β × Ω), f x ∂ρ.fst ⊗ₘ ρ.condKernel

Proof state:
β : Type u_1
Ω : Type u_2
mβ : MeasurableSpace β
inst✝⁵ : MeasurableSpace Ω
inst✝⁴ : StandardBorelSpace Ω
inst✝³ : Nonempty Ω
ρ : Measure (β × Ω)
inst✝² : IsFiniteMeasure ρ
E : Type u_3
f : β × Ω → E
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
hf : Integrable f (ρ.fst ⊗ₘ ρ.condKernel)
⊢ ∫ (b : β), ∫ (ω : Ω), f (b, ω) ∂ρ.condKernel b ∂ρ.fst = ∫ (x : β × Ω), f x ∂ρ.fst ⊗ₘ ρ.condKernel

Tactic:
rw [integral_compProd hf]

Result:
no goals

Proof state:
β : Type u_1
Ω : Type u_2
mβ : MeasurableSpace β
inst✝⁵ : MeasurableSpace Ω
inst✝⁴ : StandardBorelSpace Ω
inst✝³ : Nonempty Ω
ρ : Measure (β × Ω)
inst✝² : IsFiniteMeasure ρ
E : Type u_3
f : β × Ω → E
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
hf : Integrable f ρ
⊢ ∫ (b : β), ∫ (ω : Ω), f (b, ω) ∂ρ.condKernel b ∂ρ.fst = ∫ (x : β × Ω), f x ∂ρ

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

Result:
β : Type u_1
Ω : Type u_2
mβ : MeasurableSpace β
inst✝⁵ : MeasurableSpace Ω
inst✝⁴ : StandardBorelSpace Ω
inst✝³ : Nonempty Ω
ρ : Measure (β × Ω)
inst✝² : IsFiniteMeasure ρ
E : Type u_3
f : β × Ω → E
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
hf : Integrable f ρ
⊢ ∫ (b : β), ∫ (ω : Ω), f (b, ω) ∂ρ.condKernel b ∂ρ.fst = ∫ (x : β × Ω), f x ∂ρ.fst ⊗ₘ ρ.condKernel
-- Mathlib/Data/Set/Function.lean
theorem EqOn.inter_preimage_eq (heq : EqOn f₁ f₂ s) (t : Set β) : s ∩ f₁ ⁻¹' t = s ∩ f₂ ⁻¹' t :=
  ext fun x => and_congr_right_iff.2 fun hx => by rw [mem_preimage, mem_preimage, heq hx]

Proof state:
α : Type u_1
β : Type u_2
s : Set α
f₁ f₂ : α → β
heq : EqOn f₁ f₂ s
t : Set β
x : α
hx : x ∈ s
⊢ x ∈ f₁ ⁻¹' t ↔ x ∈ f₂ ⁻¹' t

Tactic:
rw [mem_preimage, mem_preimage, heq hx]

Result:
no goals
-- Mathlib/NumberTheory/LSeries/Convolution.lean
@[simp]
lemma convolution_map_zero {R : Type*} [Semiring R] (f g : ℕ → R) : (f ⍟ g) 0 = 0

Proof state:
R : Type u_1
inst✝ : Semiring R
f g : ℕ → R
⊢ (f ⍟ g) 0 = 0

Tactic:
simp [convolution_def]

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Operations.lean
lemma edge_edgeSet_of_ne (h : s ≠ t) : (edge s t).edgeSet = {s(s, t)}

Proof state:
V : Type u_1
s t : V
h : s ≠ t
⊢ (edge s t).edgeSet = {s(s, t)}

Tactic:
rwa [edge, edgeSet_fromEdgeSet, sdiff_eq_left, Set.disjoint_singleton_left, Set.mem_setOf_eq,
  Sym2.isDiag_iff_proj_eq]

Result:
no goals
-- Mathlib/Analysis/Convex/Between.lean
lemma mem_segment_iff_wbtw {x y z : V} : y ∈ segment R x z ↔ Wbtw R x y z

Proof state:
R : Type u_1
V : Type u_2
inst✝² : OrderedRing R
inst✝¹ : AddCommGroup V
inst✝ : Module R V
x y z : V
⊢ y ∈ segment R x z ↔ Wbtw R x y z

Tactic:
rw [Wbtw, affineSegment_eq_segment]

Result:
no goals
-- Mathlib/RingTheory/MvPolynomial/MonomialOrder.lean
theorem monic_monomial {d : σ →₀ ℕ} {c : R} :
    m.Monic (monomial d c) ↔ c = 1

Proof state:
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
d : σ →₀ ℕ
c : R
⊢ m.Monic ((monomial d) c) ↔ c = 1

Tactic:
rw [Monic, m.leadingCoeff_monomial]

Result:
no goals
-- Mathlib/NumberTheory/Multiplicity.lean
theorem emultiplicity_pow_prime_sub_pow_prime :
    emultiplicity (↑p) (x ^ p - y ^ p) = emultiplicity (↑p) (x - y) + 1

Proof state:
R : Type u_1
inst✝¹ : CommRing R
x y : R
p : ℕ
inst✝ : IsDomain R
hp : Prime ↑p
hp1 : Odd p
hxy : ↑p ∣ x - y
hx : ¬↑p ∣ x
⊢ emultiplicity (↑p) (x ^ p - y ^ p) = emultiplicity (↑p) (x - y) + 1

Tactic:
rw [← geom_sum₂_mul, emultiplicity_mul hp, emultiplicity_geom_sum₂_eq_one hp hp1 hxy hx, add_comm]

Result:
no goals
-- Mathlib/Algebra/Module/Submodule/Map.lean
theorem map_smul' (f : V →ₗ[K] V₂) (p : Submodule K V) (a : K) :
    p.map (a • f) = ⨆ _ : a ≠ 0, map f p

Proof state:
K : Type u_9
V : Type u_10
V₂ : Type u_11
inst✝⁴ : Semifield K
inst✝³ : AddCommMonoid V
inst✝² : Module K V
inst✝¹ : AddCommMonoid V₂
inst✝ : Module K V₂
f : V →ₗ[K] V₂
p : Submodule K V
a : K
⊢ map (a • f) p = ⨆ (_ : a ≠ 0), map f p

Tactic:
by_cases h : a = 0 <;> simp [h, Submodule.map_smul]

Result:
no goals

Proof state:
K : Type u_9
V : Type u_10
V₂ : Type u_11
inst✝⁴ : Semifield K
inst✝³ : AddCommMonoid V
inst✝² : Module K V
inst✝¹ : AddCommMonoid V₂
inst✝ : Module K V₂
f : V →ₗ[K] V₂
p : Submodule K V
a : K
⊢ map (a • f) p = ⨆ (_ : a ≠ 0), map f p

Tactic:
classical by_cases h : a = 0 <;> simp [h, Submodule.map_smul]

Result:
no goals
-- Mathlib/FieldTheory/Separable.lean
theorem AlgHom.card_of_powerBasis (pb : PowerBasis K S) (h_sep : IsSeparable K pb.gen)
    (h_splits : (minpoly K pb.gen).Splits (algebraMap K L)) :
    @Fintype.card (S →ₐ[K] L) (PowerBasis.AlgHom.fintype pb) = pb.dim

Proof state:
S : Type u_2
inst✝⁴ : CommRing S
K : Type u_4
L : Type u_5
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K S
inst✝ : Algebra K L
pb : PowerBasis K S
h_sep : IsSeparable K pb.gen
h_splits : Splits (algebraMap K L) (minpoly K pb.gen)
⊢ Fintype.card (S →ₐ[K] L) = pb.dim

Tactic:
let _ := (PowerBasis.AlgHom.fintype pb : Fintype (S →ₐ[K] L))

Result:
S : Type u_2
inst✝⁴ : CommRing S
K : Type u_4
L : Type u_5
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K S
inst✝ : Algebra K L
pb : PowerBasis K S
h_sep : IsSeparable K pb.gen
h_splits : Splits (algebraMap K L) (minpoly K pb.gen)
x✝ : Fintype (S →ₐ[K] L) := PowerBasis.AlgHom.fintype pb
⊢ Fintype.card (S →ₐ[K] L) = pb.dim

Proof state:
S : Type u_2
inst✝⁴ : CommRing S
K : Type u_4
L : Type u_5
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K S
inst✝ : Algebra K L
pb : PowerBasis K S
h_sep : IsSeparable K pb.gen
h_splits : Splits (algebraMap K L) (minpoly K pb.gen)
⊢ Fintype.card (S →ₐ[K] L) = pb.dim

Tactic:
classical
let _ := (PowerBasis.AlgHom.fintype pb : Fintype (S →ₐ[K] L))
rw [Fintype.card_congr pb.liftEquiv', Fintype.card_of_subtype _ (fun x => Multiset.mem_toFinset),
  ← pb.natDegree_minpoly, natDegree_eq_card_roots h_splits, Multiset.toFinset_card_of_nodup]
exact nodup_roots ((separable_map (algebraMap K L)).mpr h_sep)

Result:
no goals

Proof state:
S : Type u_2
inst✝⁴ : CommRing S
K : Type u_4
L : Type u_5
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K S
inst✝ : Algebra K L
pb : PowerBasis K S
h_sep : IsSeparable K pb.gen
h_splits : Splits (algebraMap K L) (minpoly K pb.gen)
x✝ : Fintype (S →ₐ[K] L) := PowerBasis.AlgHom.fintype pb
⊢ Fintype.card (S →ₐ[K] L) = pb.dim

Tactic:
rw [Fintype.card_congr pb.liftEquiv', Fintype.card_of_subtype _ (fun x => Multiset.mem_toFinset),
  ← pb.natDegree_minpoly, natDegree_eq_card_roots h_splits, Multiset.toFinset_card_of_nodup]

Result:
S : Type u_2
inst✝⁴ : CommRing S
K : Type u_4
L : Type u_5
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K S
inst✝ : Algebra K L
pb : PowerBasis K S
h_sep : IsSeparable K pb.gen
h_splits : Splits (algebraMap K L) (minpoly K pb.gen)
x✝ : Fintype (S →ₐ[K] L) := PowerBasis.AlgHom.fintype pb
⊢ ((minpoly K pb.gen).aroots L).Nodup

Proof state:
S : Type u_2
inst✝⁴ : CommRing S
K : Type u_4
L : Type u_5
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K S
inst✝ : Algebra K L
pb : PowerBasis K S
h_sep : IsSeparable K pb.gen
h_splits : Splits (algebraMap K L) (minpoly K pb.gen)
x✝ : Fintype (S →ₐ[K] L) := PowerBasis.AlgHom.fintype pb
⊢ ((minpoly K pb.gen).aroots L).Nodup

Tactic:
exact nodup_roots ((separable_map (algebraMap K L)).mpr h_sep)

Result:
no goals
-- Mathlib/Order/Interval/Set/Basic.lean
theorem left_mem_Ico : a ∈ Ico a b ↔ a < b

Proof state:
α : Type u_1
inst✝ : Preorder α
a b : α
⊢ a ∈ Ico a b ↔ a < b

Tactic:
simp [le_refl]

Result:
no goals
-- Mathlib/Data/Set/Image.lean
theorem range_inclusion (h : s ⊆ t) : range (inclusion h) = { x : t | (x : α) ∈ s }

Proof state:
α : Type u_1
s t : Set α
h : s ⊆ t
⊢ range (inclusion h) = {x | ↑x ∈ s}

Tactic:
ext ⟨x, hx⟩

Result:
case h.mk
α : Type u_1
s t : Set α
h : s ⊆ t
x : α
hx : x ∈ t
⊢ ⟨x, hx⟩ ∈ range (inclusion h) ↔ ⟨x, hx⟩ ∈ {x | ↑x ∈ s}

Proof state:
case h.mk
α : Type u_1
s t : Set α
h : s ⊆ t
x : α
hx : x ∈ t
⊢ ⟨x, hx⟩ ∈ range (inclusion h) ↔ ⟨x, hx⟩ ∈ {x | ↑x ∈ s}

Tactic:
simp

Result:
no goals
-- Mathlib/Algebra/Ring/Subsemiring/Basic.lean
theorem coe_iSup_of_directed {ι} [hι : Nonempty ι] {S : ι → Subsemiring R}
    (hS : Directed (· ≤ ·) S) : ((⨆ i, S i : Subsemiring R) : Set R) = ⋃ i, S i :=
  Set.ext fun x ↦ by simp [mem_iSup_of_directed hS]

Proof state:
R : Type u
inst✝ : NonAssocSemiring R
ι : Sort u_1
hι : Nonempty ι
S : ι → Subsemiring R
hS : Directed (fun x1 x2 => x1 ≤ x2) S
x : R
⊢ x ∈ ↑(⨆ i, S i) ↔ x ∈ ⋃ i, ↑(S i)

Tactic:
simp [mem_iSup_of_directed hS]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/Raw.lean
theorem ofList_eq [BEq α] [Hashable α] {l : List ((a : α) × β a)} :
    Raw.ofList l = Raw₀.insertMany Raw₀.empty l

Proof state:
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : Hashable α
l : List ((a : α) × β a)
⊢ (Raw₀.insertMany ⟨∅, ⋯⟩ l).val.val = (Raw₀.empty.insertMany l).val.val

Tactic:
congr

Result:
no goals

Proof state:
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : Hashable α
l : List ((a : α) × β a)
⊢ Raw.ofList l = (Raw₀.empty.insertMany l).val.val

Tactic:
simp only [Raw.ofList, Raw.insertMany, (Raw.WF.empty).size_buckets_pos ∅, ↓reduceDIte]

Result:
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : Hashable α
l : List ((a : α) × β a)
⊢ (Raw₀.insertMany ⟨∅, ⋯⟩ l).val.val = (Raw₀.empty.insertMany l).val.val
-- Mathlib/Data/Finset/Filter.lean
theorem disjoint_filter_and_not_filter :
    Disjoint (s.filter (fun x ↦ p x ∧ ¬q x)) (s.filter (fun x ↦ q x ∧ ¬p x))

Proof state:
α : Type u_1
p q : α → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
s x✝ : Finset α
htp : x✝ ≤ filter (fun x => p x ∧ ¬q x) s
htq : x✝ ≤ filter (fun x => q x ∧ ¬p x) s
⊢ x✝ ≤ ⊥

Tactic:
simp only [bot_eq_empty, le_eq_subset, subset_empty, ← not_nonempty_iff_eq_empty]

Result:
α : Type u_1
p q : α → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
s x✝ : Finset α
htp : x✝ ≤ filter (fun x => p x ∧ ¬q x) s
htq : x✝ ≤ filter (fun x => q x ∧ ¬p x) s
⊢ ¬x✝.Nonempty

Proof state:
case intro
α : Type u_1
p q : α → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
s x✝ : Finset α
htp : x✝ ≤ filter (fun x => p x ∧ ¬q x) s
htq : x✝ ≤ filter (fun x => q x ∧ ¬p x) s
w✝ : α
hx : w✝ ∈ x✝
⊢ False

Tactic:
exact (mem_filter.mp (htq hx)).2.2 (mem_filter.mp (htp hx)).2.1

Result:
no goals

Proof state:
α : Type u_1
p q : α → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
s x✝ : Finset α
htp : x✝ ≤ filter (fun x => p x ∧ ¬q x) s
htq : x✝ ≤ filter (fun x => q x ∧ ¬p x) s
⊢ ¬x✝.Nonempty

Tactic:
rintro ⟨_, hx⟩

Result:
case intro
α : Type u_1
p q : α → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
s x✝ : Finset α
htp : x✝ ≤ filter (fun x => p x ∧ ¬q x) s
htq : x✝ ≤ filter (fun x => q x ∧ ¬p x) s
w✝ : α
hx : w✝ ∈ x✝
⊢ False

Proof state:
α : Type u_1
p q : α → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
s : Finset α
⊢ Disjoint (filter (fun x => p x ∧ ¬q x) s) (filter (fun x => q x ∧ ¬p x) s)

Tactic:
intro _ htp htq

Result:
α : Type u_1
p q : α → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
s x✝ : Finset α
htp : x✝ ≤ filter (fun x => p x ∧ ¬q x) s
htq : x✝ ≤ filter (fun x => q x ∧ ¬p x) s
⊢ x✝ ≤ ⊥
-- Mathlib/Algebra/Group/Semiconj/Basic.lean
@[to_additive (attr := simp)] lemma zpow_right (h : SemiconjBy a x y) :
    ∀ m : ℤ, SemiconjBy a (x ^ m) (y ^ m)
  | (n : ℕ)    => by simp [zpow_natCast, h.pow_right n]
  | .negSucc n => by
    simp only [zpow_negSucc, inv_right_iff]
    apply pow_right h

Proof state:
G : Type u_1
inst✝ : Group G
a x y : G
h : SemiconjBy a x y
n : ℕ
⊢ SemiconjBy a (x ^ ↑n) (y ^ ↑n)

Tactic:
simp [zpow_natCast, h.pow_right n]

Result:
no goals

Proof state:
G : Type u_1
inst✝ : Group G
a x y : G
h : SemiconjBy a x y
n : ℕ
⊢ SemiconjBy a (x ^ (n + 1)) (y ^ (n + 1))

Tactic:
apply pow_right h

Result:
no goals

Proof state:
G : Type u_1
inst✝ : Group G
a x y : G
h : SemiconjBy a x y
n : ℕ
⊢ SemiconjBy a (x ^ Int.negSucc n) (y ^ Int.negSucc n)

Tactic:
simp only [zpow_negSucc, inv_right_iff]

Result:
G : Type u_1
inst✝ : Group G
a x y : G
h : SemiconjBy a x y
n : ℕ
⊢ SemiconjBy a (x ^ (n + 1)) (y ^ (n + 1))
-- Mathlib/CategoryTheory/Galois/IsFundamentalgroup.lean
/-- If `toAut F G` is surjective, then `G` acts transitively on the fibers of connected objects.
For a converse see `toAut_surjective`. -/
lemma isPretransitive_of_surjective (h : Function.Surjective (toAut F G)) (X : C)
    [IsConnected X] : MulAction.IsPretransitive G (F.obj X) where
  exists_smul_eq x y

Proof state:
case intro.intro
C : Type u₁
inst✝⁶ : Category.{u₂, u₁} C
F : C ⥤ FintypeCat
G : Type u_1
inst✝⁵ : Group G
inst✝⁴ : (X : C) → MulAction G (F.obj X).carrier
inst✝³ : IsNaturalSMul F G
inst✝² : GaloisCategory C
inst✝¹ : FiberFunctor F
h : Function.Surjective ⇑(toAut F G)
X : C
inst✝ : IsConnected X
x y : (F.obj X).carrier
g : G
ht : (toAut F G) g • x = y
⊢ ∃ g, g • x = y

Tactic:
exact ⟨g, ht⟩

Result:
no goals

Proof state:
case intro
C : Type u₁
inst✝⁶ : Category.{u₂, u₁} C
F : C ⥤ FintypeCat
G : Type u_1
inst✝⁵ : Group G
inst✝⁴ : (X : C) → MulAction G (F.obj X).carrier
inst✝³ : IsNaturalSMul F G
inst✝² : GaloisCategory C
inst✝¹ : FiberFunctor F
h : Function.Surjective ⇑(toAut F G)
X : C
inst✝ : IsConnected X
x y : (F.obj X).carrier
t : Aut F
ht : t • x = y
⊢ ∃ g, g • x = y

Tactic:
obtain ⟨g, rfl⟩ := h t

Result:
case intro.intro
C : Type u₁
inst✝⁶ : Category.{u₂, u₁} C
F : C ⥤ FintypeCat
G : Type u_1
inst✝⁵ : Group G
inst✝⁴ : (X : C) → MulAction G (F.obj X).carrier
inst✝³ : IsNaturalSMul F G
inst✝² : GaloisCategory C
inst✝¹ : FiberFunctor F
h : Function.Surjective ⇑(toAut F G)
X : C
inst✝ : IsConnected X
x y : (F.obj X).carrier
g : G
ht : (toAut F G) g • x = y
⊢ ∃ g, g • x = y

Proof state:
C : Type u₁
inst✝⁶ : Category.{u₂, u₁} C
F : C ⥤ FintypeCat
G : Type u_1
inst✝⁵ : Group G
inst✝⁴ : (X : C) → MulAction G (F.obj X).carrier
inst✝³ : IsNaturalSMul F G
inst✝² : GaloisCategory C
inst✝¹ : FiberFunctor F
h : Function.Surjective ⇑(toAut F G)
X : C
inst✝ : IsConnected X
x y : (F.obj X).carrier
⊢ ∃ g, g • x = y

Tactic:
obtain ⟨t, ht⟩ := MulAction.exists_smul_eq (Aut F) x y

Result:
case intro
C : Type u₁
inst✝⁶ : Category.{u₂, u₁} C
F : C ⥤ FintypeCat
G : Type u_1
inst✝⁵ : Group G
inst✝⁴ : (X : C) → MulAction G (F.obj X).carrier
inst✝³ : IsNaturalSMul F G
inst✝² : GaloisCategory C
inst✝¹ : FiberFunctor F
h : Function.Surjective ⇑(toAut F G)
X : C
inst✝ : IsConnected X
x y : (F.obj X).carrier
t : Aut F
ht : t • x = y
⊢ ∃ g, g • x = y
-- Mathlib/Data/List/Basic.lean
theorem subset_singleton_iff {a : α} {L : List α} : L ⊆ [a] ↔ ∃ n, L = replicate n a

Proof state:
α : Type u
a : α
L : List α
⊢ L ⊆ [a] ↔ ∃ n, L = replicate n a

Tactic:
simp only [eq_replicate_iff, subset_def, mem_singleton, exists_eq_left']

Result:
no goals
-- Mathlib/Algebra/Regular/Basic.lean
theorem isLeftRegular_of_mul_eq_one (h : b * a = 1) : IsLeftRegular a :=
  IsLeftRegular.of_mul (a := b) (by rw [h]; exact isRegular_one.left)

Proof state:
R : Type u_1
inst✝ : Monoid R
a b : R
h : b * a = 1
⊢ IsLeftRegular 1

Tactic:
exact isRegular_one.left

Result:
no goals

Proof state:
R : Type u_1
inst✝ : Monoid R
a b : R
h : b * a = 1
⊢ IsLeftRegular (b * a)

Tactic:
rw [h]

Result:
R : Type u_1
inst✝ : Monoid R
a b : R
h : b * a = 1
⊢ IsLeftRegular 1
-- Mathlib/FieldTheory/PurelyInseparable/Basic.lean
theorem isSepClosed_iff_isPurelyInseparable_algebraicClosure [IsAlgClosure F E] :
    IsSepClosed F ↔ IsPurelyInseparable F E :=
  ⟨fun _ ↦ inferInstance, fun H ↦ by
    haveI := IsAlgClosure.isAlgClosed F (K := E)
    rwa [← separableClosure.eq_bot_iff, IsSepClosed.separableClosure_eq_bot_iff] at H⟩

Proof state:
F : Type u
E : Type v
inst✝³ : Field F
inst✝² : Field E
inst✝¹ : Algebra F E
inst✝ : IsAlgClosure F E
H : IsPurelyInseparable F E
this : IsAlgClosed E
⊢ IsSepClosed F

Tactic:
rwa [← separableClosure.eq_bot_iff, IsSepClosed.separableClosure_eq_bot_iff] at H

Result:
no goals

Proof state:
F : Type u
E : Type v
inst✝³ : Field F
inst✝² : Field E
inst✝¹ : Algebra F E
inst✝ : IsAlgClosure F E
H : IsPurelyInseparable F E
⊢ IsSepClosed F

Tactic:
haveI := IsAlgClosure.isAlgClosed F (K := E)

Result:
F : Type u
E : Type v
inst✝³ : Field F
inst✝² : Field E
inst✝¹ : Algebra F E
inst✝ : IsAlgClosure F E
H : IsPurelyInseparable F E
this : IsAlgClosed E
⊢ IsSepClosed F
-- Mathlib/RingTheory/Polynomial/Content.lean
theorem content_X : content (X : R[X]) = 1

Proof state:
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
⊢ X.content = 1

Tactic:
rw [← mul_one X, content_X_mul, content_one]

Result:
no goals
-- Mathlib/AlgebraicGeometry/EllipticCurve/NormalForms.lean
theorem b₈_of_isCharThreeJNeZeroNF_of_char_three : W.b₈ = W.a₂ * W.a₆

Proof state:
R : Type u_1
inst✝² : CommRing R
W : WeierstrassCurve R
inst✝¹ : W.IsCharThreeJNeZeroNF
inst✝ : CharP R 3
⊢ W.b₈ = W.a₂ * W.a₆

Tactic:
rw [b₈_of_isCharThreeJNeZeroNF]

Result:
R : Type u_1
inst✝² : CommRing R
W : WeierstrassCurve R
inst✝¹ : W.IsCharThreeJNeZeroNF
inst✝ : CharP R 3
⊢ 4 * W.a₂ * W.a₆ = W.a₂ * W.a₆

Proof state:
R : Type u_1
inst✝² : CommRing R
W : WeierstrassCurve R
inst✝¹ : W.IsCharThreeJNeZeroNF
inst✝ : CharP R 3
⊢ 4 * W.a₂ * W.a₆ = W.a₂ * W.a₆

Tactic:
linear_combination W.a₂ * W.a₆ * CharP.cast_eq_zero R 3

Result:
no goals
-- Mathlib/Algebra/Category/ModuleCat/Adjunctions.lean
@[simp]
lemma free_map_apply {X Y : Type u} (f : X → Y) (x : X) :
    (free R).map f (freeMk x) = freeMk (f x)

Proof state:
R : Type u
inst✝ : Ring R
X Y : Type u
f : X → Y
x : X
⊢ (ConcreteCategory.hom ((free R).map f)) (freeMk x) = freeMk (f x)

Tactic:
apply Finsupp.mapDomain_single

Result:
no goals
-- Mathlib/Algebra/Order/Sub/Defs.lean
theorem lt_tsub_of_add_lt_left (ha : AddLECancellable a) (h : a + c < b) : c < b - a :=
  ha.lt_tsub_of_add_lt_right <| by rwa [add_comm]

Proof state:
α : Type u_1
inst✝³ : PartialOrder α
inst✝² : AddCommSemigroup α
inst✝¹ : Sub α
inst✝ : OrderedSub α
a b c : α
ha : AddLECancellable a
h : a + c < b
⊢ c + a < b

Tactic:
rwa [add_comm]

Result:
no goals
-- Mathlib/Analysis/Asymptotics/AsymptoticEquivalent.lean
theorem IsEquivalent.sub_isLittleO (huv : u ~[l] v) (hwv : w =o[l] v) : u - w ~[l] v

Proof state:
α : Type u_1
β : Type u_2
inst✝ : NormedAddCommGroup β
u v w : α → β
l : Filter α
huv : u ~[l] v
hwv : w =o[l] v
⊢ u - w ~[l] v

Tactic:
simpa only [sub_eq_add_neg] using huv.add_isLittleO hwv.neg_left

Result:
no goals
-- Mathlib/LinearAlgebra/Matrix/Basis.lean
theorem basis_toMatrix_mul [Fintype κ] [Finite ι] [DecidableEq κ]
    (b₁ : Basis ι R M) (b₂ : Basis ι' R M) (b₃ : Basis κ R N) (A : Matrix ι' κ R) :
    b₁.toMatrix b₂ * A = LinearMap.toMatrix b₃ b₁ (toLin b₃ b₂ A)

Proof state:
ι : Type u_1
ι' : Type u_2
κ : Type u_3
R : Type u_5
M : Type u_6
inst✝⁸ : CommSemiring R
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R M
N : Type u_9
inst✝⁵ : AddCommMonoid N
inst✝⁴ : Module R N
inst✝³ : Fintype ι'
inst✝² : Fintype κ
inst✝¹ : Finite ι
inst✝ : DecidableEq κ
b₁ : Basis ι R M
b₂ : Basis ι' R M
b₃ : Basis κ R N
A : Matrix ι' κ R
this : b₁.toMatrix ⇑b₂ * (toMatrix b₃ b₂) ((toLin b₃ b₂) A) = (toMatrix b₃ b₁) ((toLin b₃ b₂) A)
⊢ b₁.toMatrix ⇑b₂ * A = (toMatrix b₃ b₁) ((toLin b₃ b₂) A)

Tactic:
rwa [LinearMap.toMatrix_toLin] at this

Result:
no goals

Proof state:
ι : Type u_1
ι' : Type u_2
κ : Type u_3
R : Type u_5
M : Type u_6
inst✝⁸ : CommSemiring R
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R M
N : Type u_9
inst✝⁵ : AddCommMonoid N
inst✝⁴ : Module R N
inst✝³ : Fintype ι'
inst✝² : Fintype κ
inst✝¹ : Finite ι
inst✝ : DecidableEq κ
b₁ : Basis ι R M
b₂ : Basis ι' R M
b₃ : Basis κ R N
A : Matrix ι' κ R
⊢ b₁.toMatrix ⇑b₂ * A = (toMatrix b₃ b₁) ((toLin b₃ b₂) A)

Tactic:
have := basis_toMatrix_mul_linearMap_toMatrix b₃ b₁ b₂ (Matrix.toLin b₃ b₂ A)

Result:
ι : Type u_1
ι' : Type u_2
κ : Type u_3
R : Type u_5
M : Type u_6
inst✝⁸ : CommSemiring R
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R M
N : Type u_9
inst✝⁵ : AddCommMonoid N
inst✝⁴ : Module R N
inst✝³ : Fintype ι'
inst✝² : Fintype κ
inst✝¹ : Finite ι
inst✝ : DecidableEq κ
b₁ : Basis ι R M
b₂ : Basis ι' R M
b₃ : Basis κ R N
A : Matrix ι' κ R
this : b₁.toMatrix ⇑b₂ * (toMatrix b₃ b₂) ((toLin b₃ b₂) A) = (toMatrix b₃ b₁) ((toLin b₃ b₂) A)
⊢ b₁.toMatrix ⇑b₂ * A = (toMatrix b₃ b₁) ((toLin b₃ b₂) A)
-- Mathlib/Data/Set/Card.lean
theorem encard_add_encard_compl (s : Set α) : s.encard + sᶜ.encard = (univ : Set α).encard

Proof state:
α : Type u_1
s : Set α
⊢ s.encard + sᶜ.encard = univ.encard

Tactic:
rw [← encard_union_eq disjoint_compl_right, union_compl_self]

Result:
no goals
-- Mathlib/Analysis/Calculus/FDeriv/Basic.lean
theorem differentiableAt_of_isInvertible_fderiv
    (hf : (fderiv 𝕜 f x).IsInvertible) : DifferentiableAt 𝕜 f x

Proof state:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
x : E
hf : (fderivWithin 𝕜 f univ x).IsInvertible
⊢ DifferentiableWithinAt 𝕜 f univ x

Tactic:
exact differentiableWithinAt_of_isInvertible_fderivWithin hf

Result:
no goals

Proof state:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
x : E
hf : (fderiv 𝕜 f x).IsInvertible
⊢ DifferentiableAt 𝕜 f x

Tactic:
simp only [← differentiableWithinAt_univ, ← fderivWithin_univ] at hf ⊢

Result:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
x : E
hf : (fderivWithin 𝕜 f univ x).IsInvertible
⊢ DifferentiableWithinAt 𝕜 f univ x
-- Mathlib/Topology/Semicontinuous.lean
theorem lowerSemicontinuousAt_iff_le_liminf {f : α → γ} :
    LowerSemicontinuousAt f x ↔ f x ≤ liminf f (𝓝 x)

Proof state:
α : Type u_1
inst✝² : TopologicalSpace α
x : α
γ : Type u_3
inst✝¹ : CompleteLinearOrder γ
inst✝ : DenselyOrdered γ
f : α → γ
⊢ LowerSemicontinuousAt f x ↔ f x ≤ liminf f (𝓝 x)

Tactic:
rw [← lowerSemicontinuousWithinAt_univ_iff, lowerSemicontinuousWithinAt_iff_le_liminf,
  ← nhdsWithin_univ]

Result:
no goals