harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Topology/Compactness/Compact.lean
protected lemma Pi.exists_compact_superset_iff {s : Set (Π i, X i)} :
    (∃ K, IsCompact K ∧ s ⊆ K) ↔ ∀ i, ∃ Ki, IsCompact Ki ∧ s ⊆ eval i ⁻¹' Ki

Proof state:
ι : Type u_1
X : ι → Type u_2
inst✝ : (i : ι) → TopologicalSpace (X i)
s : Set ((i : ι) → X i)
⊢ (∃ K, IsCompact K ∧ s ⊆ K) ↔ ∀ (i : ι), ∃ Ki, IsCompact Ki ∧ s ⊆ eval i ⁻¹' Ki

Tactic:
constructor

Result:
case mp
ι : Type u_1
X : ι → Type u_2
inst✝ : (i : ι) → TopologicalSpace (X i)
s : Set ((i : ι) → X i)
⊢ (∃ K, IsCompact K ∧ s ⊆ K) → ∀ (i : ι), ∃ Ki, IsCompact Ki ∧ s ⊆ eval i ⁻¹' Ki

case mpr
ι : Type u_1
X : ι → Type u_2
inst✝ : (i : ι) → TopologicalSpace (X i)
s : Set ((i : ι) → X i)
⊢ (∀ (i : ι), ∃ Ki, IsCompact Ki ∧ s ⊆ eval i ⁻¹' Ki) → ∃ K, IsCompact K ∧ s ⊆ K

Proof state:
case mpr
ι : Type u_1
X : ι → Type u_2
inst✝ : (i : ι) → TopologicalSpace (X i)
s : Set ((i : ι) → X i)
⊢ (∀ (i : ι), ∃ Ki, IsCompact Ki ∧ s ⊆ eval i ⁻¹' Ki) → ∃ K, IsCompact K ∧ s ⊆ K

Tactic:
intro H

Result:
case mpr
ι : Type u_1
X : ι → Type u_2
inst✝ : (i : ι) → TopologicalSpace (X i)
s : Set ((i : ι) → X i)
H : ∀ (i : ι), ∃ Ki, IsCompact Ki ∧ s ⊆ eval i ⁻¹' Ki
⊢ ∃ K, IsCompact K ∧ s ⊆ K

Proof state:
case mpr
ι : Type u_1
X : ι → Type u_2
inst✝ : (i : ι) → TopologicalSpace (X i)
s : Set ((i : ι) → X i)
H : ∀ (i : ι), ∃ Ki, IsCompact Ki ∧ s ⊆ eval i ⁻¹' Ki
⊢ ∃ K, IsCompact K ∧ s ⊆ K

Tactic:
choose K hK hsK using H

Result:
case mpr
ι : Type u_1
X : ι → Type u_2
inst✝ : (i : ι) → TopologicalSpace (X i)
s : Set ((i : ι) → X i)
K : (i : ι) → Set (X i)
hK : ∀ (i : ι), IsCompact (K i)
hsK : ∀ (i : ι), s ⊆ eval i ⁻¹' K i
⊢ ∃ K, IsCompact K ∧ s ⊆ K

Proof state:
case mpr
ι : Type u_1
X : ι → Type u_2
inst✝ : (i : ι) → TopologicalSpace (X i)
s : Set ((i : ι) → X i)
K : (i : ι) → Set (X i)
hK : ∀ (i : ι), IsCompact (K i)
hsK : ∀ (i : ι), s ⊆ eval i ⁻¹' K i
⊢ ∃ K, IsCompact K ∧ s ⊆ K

Tactic:
exact ⟨pi univ K, isCompact_univ_pi hK, fun _ hx i _ ↦ hsK i hx⟩

Result:
no goals

Proof state:
case mp
ι : Type u_1
X : ι → Type u_2
inst✝ : (i : ι) → TopologicalSpace (X i)
s : Set ((i : ι) → X i)
⊢ (∃ K, IsCompact K ∧ s ⊆ K) → ∀ (i : ι), ∃ Ki, IsCompact Ki ∧ s ⊆ eval i ⁻¹' Ki

Tactic:
intro ⟨K, hK, hsK⟩ i

Result:
case mp
ι : Type u_1
X : ι → Type u_2
inst✝ : (i : ι) → TopologicalSpace (X i)
s K : Set ((i : ι) → X i)
hK : IsCompact K
hsK : s ⊆ K
i : ι
⊢ ∃ Ki, IsCompact Ki ∧ s ⊆ eval i ⁻¹' Ki

Proof state:
case mp
ι : Type u_1
X : ι → Type u_2
inst✝ : (i : ι) → TopologicalSpace (X i)
s K : Set ((i : ι) → X i)
hK : IsCompact K
hsK : s ⊆ K
i : ι
⊢ ∃ Ki, IsCompact Ki ∧ s ⊆ eval i ⁻¹' Ki

Tactic:
exact ⟨eval i '' K, hK.image <| continuous_apply i, hsK.trans <| K.subset_preimage_image _⟩

Result:
no goals
-- Mathlib/Analysis/InnerProductSpace/TwoDim.lean
theorem normSq_kahler (x y : E) : Complex.normSq (o.kahler x y) = ‖x‖ ^ 2 * ‖y‖ ^ 2

Proof state:
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
x y : E
⊢ Complex.normSq ((o.kahler x) y) = ‖x‖ ^ 2 * ‖y‖ ^ 2

Tactic:
simpa [kahler_apply_apply, Complex.normSq, sq] using o.inner_sq_add_areaForm_sq x y

Result:
no goals
-- Mathlib/GroupTheory/Schreier.lean
theorem rank_le_index_mul_rank [hG : Group.FG G] [FiniteIndex H] :
    Group.rank H ≤ H.index * Group.rank G

Proof state:
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
hG : Group.FG G
inst✝ : H.FiniteIndex
this : Group.FG ↥H
⊢ Group.rank ↥H ≤ H.index * Group.rank G

Tactic:
obtain ⟨S, hS₀, hS⟩ := Group.rank_spec G

Result:
case intro.intro
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
hG : Group.FG G
inst✝ : H.FiniteIndex
this : Group.FG ↥H
S : Finset G
hS₀ : S.card = Group.rank G
hS : closure ↑S = ⊤
⊢ Group.rank ↥H ≤ H.index * Group.rank G

Proof state:
case intro.intro
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
hG : Group.FG G
inst✝ : H.FiniteIndex
this : Group.FG ↥H
S : Finset G
hS₀ : S.card = Group.rank G
hS : closure ↑S = ⊤
⊢ Group.rank ↥H ≤ H.index * Group.rank G

Tactic:
obtain ⟨T, hT₀, hT⟩ := exists_finset_card_le_mul H hS

Result:
case intro.intro.intro.intro
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
hG : Group.FG G
inst✝ : H.FiniteIndex
this : Group.FG ↥H
S : Finset G
hS₀ : S.card = Group.rank G
hS : closure ↑S = ⊤
T : Finset ↥H
hT₀ : T.card ≤ H.index * S.card
hT : closure ↑T = ⊤
⊢ Group.rank ↥H ≤ H.index * Group.rank G

Proof state:
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
hG : Group.FG G
inst✝ : H.FiniteIndex
⊢ Group.rank ↥H ≤ H.index * Group.rank G

Tactic:
haveI := H.fg_of_index_ne_zero

Result:
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
hG : Group.FG G
inst✝ : H.FiniteIndex
this : Group.FG ↥H
⊢ Group.rank ↥H ≤ H.index * Group.rank G
-- Mathlib/Topology/Constructions.lean
@[simp] lemma IsClosed.inter_preimage_val_iff {s t : Set X} (hs : IsClosed s) :
    IsClosed (s ↓∩ t) ↔ IsClosed (s ∩ t) :=
  ⟨fun h ↦ by simpa using hs.isClosedMap_subtype_val _ h,
    fun h ↦ (Subtype.preimage_coe_self_inter _ _).symm ▸ h.preimage_val⟩

Proof state:
X : Type u
inst✝ : TopologicalSpace X
s t : Set X
hs : IsClosed s
h : IsClosed (s ↓∩ t)
⊢ IsClosed (s ∩ t)

Tactic:
simpa using hs.isClosedMap_subtype_val _ h

Result:
no goals
-- Mathlib/RingTheory/DedekindDomain/Factorization.lean
theorem count_zpow_self (n : ℤ) :
    count K v ((v.asIdeal : FractionalIdeal R⁰ K) ^ n) = n

Proof state:
R : Type u_1
inst✝⁴ : CommRing R
K : Type u_2
inst✝³ : Field K
inst✝² : Algebra R K
inst✝¹ : IsFractionRing R K
inst✝ : IsDedekindDomain R
v : HeightOneSpectrum R
n : ℤ
⊢ count K v (↑v.asIdeal ^ n) = n

Tactic:
rw [count_zpow, count_self, mul_one]

Result:
no goals
-- Mathlib/MeasureTheory/Constructions/Polish/Basic.lean
theorem _root_.MeasurableSet.standardBorel {s : Set α} (hs : MeasurableSet s) :
    StandardBorelSpace s

Proof state:
case intro.intro.intro.intro
α : Type u_1
inst✝¹ : MeasurableSpace α
inst✝ : StandardBorelSpace α
s : Set α
hs : MeasurableSet s
w✝ : TopologicalSpace α
left✝¹ : BorelSpace α
left✝ : PolishSpace α
s_closed : IsClosed s
right✝ : IsOpen s
this : PolishSpace ↑s
⊢ StandardBorelSpace ↑s

Tactic:
infer_instance

Result:
no goals

Proof state:
α : Type u_1
inst✝¹ : MeasurableSpace α
inst✝ : StandardBorelSpace α
s : Set α
hs : MeasurableSet s
⊢ StandardBorelSpace ↑s

Tactic:
obtain ⟨_, _, _, s_closed, _⟩ := hs.isClopenable'

Result:
case intro.intro.intro.intro
α : Type u_1
inst✝¹ : MeasurableSpace α
inst✝ : StandardBorelSpace α
s : Set α
hs : MeasurableSet s
w✝ : TopologicalSpace α
left✝¹ : BorelSpace α
left✝ : PolishSpace α
s_closed : IsClosed s
right✝ : IsOpen s
⊢ StandardBorelSpace ↑s

Proof state:
case intro.intro.intro.intro
α : Type u_1
inst✝¹ : MeasurableSpace α
inst✝ : StandardBorelSpace α
s : Set α
hs : MeasurableSet s
w✝ : TopologicalSpace α
left✝¹ : BorelSpace α
left✝ : PolishSpace α
s_closed : IsClosed s
right✝ : IsOpen s
⊢ StandardBorelSpace ↑s

Tactic:
haveI := s_closed.polishSpace

Result:
case intro.intro.intro.intro
α : Type u_1
inst✝¹ : MeasurableSpace α
inst✝ : StandardBorelSpace α
s : Set α
hs : MeasurableSet s
w✝ : TopologicalSpace α
left✝¹ : BorelSpace α
left✝ : PolishSpace α
s_closed : IsClosed s
right✝ : IsOpen s
this : PolishSpace ↑s
⊢ StandardBorelSpace ↑s
-- Mathlib/Analysis/SpecialFunctions/ImproperIntegrals.lean
theorem integral_exp_neg_Ioi_zero : (∫ x : ℝ in Ioi 0, exp (-x)) = 1

Proof state:
⊢ ∫ (x : ℝ) in Ioi 0, rexp (-x) = 1

Tactic:
simpa only [neg_zero, exp_zero] using integral_exp_neg_Ioi 0

Result:
no goals
-- Mathlib/CategoryTheory/Abelian/Basic.lean
theorem coimageIsoImage'_hom :
    (coimageIsoImage' f).hom =
      cokernel.desc _ (factorThruImage f) (by simp [← cancel_mono (Limits.image.ι f)])

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X Y : C
f : X ⟶ Y
⊢ kernel.ι f ≫ factorThruImage f = 0

Tactic:
simp [← cancel_mono (Limits.image.ι f)]

Result:
no goals

Proof state:
case h
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X Y : C
f : X ⟶ Y
⊢ coequalizer.π (kernel.ι f) 0 ≫ (coimageIsoImage' f).hom =
    coequalizer.π (kernel.ι f) 0 ≫ cokernel.desc (kernel.ι f) (factorThruImage f) ⋯

Tactic:
simp only [← cancel_mono (Limits.image.ι f), IsImage.isoExt_hom, cokernel.π_desc,
  Category.assoc, IsImage.lift_ι, coimageStrongEpiMonoFactorisation_m,
  Limits.image.fac]

Result:
no goals

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X Y : C
f : X ⟶ Y
⊢ (coimageIsoImage' f).hom = cokernel.desc (kernel.ι f) (factorThruImage f) ⋯

Tactic:
ext

Result:
case h
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X Y : C
f : X ⟶ Y
⊢ coequalizer.π (kernel.ι f) 0 ≫ (coimageIsoImage' f).hom =
    coequalizer.π (kernel.ι f) 0 ≫ cokernel.desc (kernel.ι f) (factorThruImage f) ⋯
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/ToArray.lean
theorem pop_toArray (l : List α) : l.toArray.pop = l.dropLast.toArray

Proof state:
case h
α : Type u_1
l : List α
⊢ l.toArray.pop.toList = l.dropLast.toArray.toList

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
l : List α
⊢ l.toArray.pop = l.dropLast.toArray

Tactic:
apply ext'

Result:
case h
α : Type u_1
l : List α
⊢ l.toArray.pop.toList = l.dropLast.toArray.toList
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/RawLemmas.lean
theorem length_keys [EquivBEq α] [LawfulHashable α] (h : m.WF) :
    m.keys.length = m.size

Proof state:
α : Type u
β : α → Type v
m : Raw α β
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
h : m.WF
⊢ m.keys.length = m.size

Tactic:
simp_to_raw using Raw₀.length_keys ⟨m, h.size_buckets_pos⟩ h

Result:
no goals
-- Mathlib/Geometry/Euclidean/MongePoint.lean
theorem mongePoint_eq_of_range_eq {n : ℕ} {s₁ s₂ : Simplex ℝ P n}
    (h : Set.range s₁.points = Set.range s₂.points) : s₁.mongePoint = s₂.mongePoint

Proof state:
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
n : ℕ
s₁ s₂ : Simplex ℝ P n
h : Set.range s₁.points = Set.range s₂.points
⊢ s₁.mongePoint = s₂.mongePoint

Tactic:
simp_rw [mongePoint_eq_smul_vsub_vadd_circumcenter, centroid_eq_of_range_eq h,
  circumcenter_eq_of_range_eq h]

Result:
no goals
-- Mathlib/RingTheory/Ideal/Quotient/Operations.lean
theorem mk_ker {I : Ideal R} [I.IsTwoSided] : ker (Quotient.mk I) = I

Proof state:
R : Type u
inst✝¹ : Ring R
I : Ideal R
inst✝ : I.IsTwoSided
⊢ ker (Quotient.mk I) = I

Tactic:
ext

Result:
case h
R : Type u
inst✝¹ : Ring R
I : Ideal R
inst✝ : I.IsTwoSided
x✝ : R
⊢ x✝ ∈ ker (Quotient.mk I) ↔ x✝ ∈ I

Proof state:
case h
R : Type u
inst✝¹ : Ring R
I : Ideal R
inst✝ : I.IsTwoSided
x✝ : R
⊢ x✝ ∈ ker (Quotient.mk I) ↔ x✝ ∈ I

Tactic:
rw [ker, mem_comap, Submodule.mem_bot, Quotient.eq_zero_iff_mem]

Result:
no goals
-- Mathlib/Order/Interval/Finset/Basic.lean
/-- In a locally finite partial order, `≤` is the reflexive transitive closure of `⋖`. -/
lemma le_iff_reflTransGen_covBy [PartialOrder α] [LocallyFiniteOrder α] {x y : α} :
    x ≤ y ↔ ReflTransGen (· ⋖ ·) x y

Proof state:
α : Type u_2
inst✝¹ : PartialOrder α
inst✝ : LocallyFiniteOrder α
x y : α
⊢ x ≤ y ↔ ReflTransGen (fun x1 x2 => x1 ⋖ x2) x y

Tactic:
rw [le_iff_transGen_wcovBy, wcovBy_eq_reflGen_covBy, transGen_reflGen]

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/ConcreteColorings.lean
theorem Coloring.even_length_iff_congr {α} {G : SimpleGraph α}
    (c : G.Coloring Bool) {u v : α} (p : G.Walk u v) :
    Even p.length ↔ (c u ↔ c v)

Proof state:
α : Type u_1
G : SimpleGraph α
c : G.Coloring Bool
u v : α
p : G.Walk u v
⊢ Even p.length ↔ (c u = true ↔ c v = true)

Tactic:
induction p with
| nil => simp
| @cons u v w h p ih =>
  simp only [Walk.length_cons, Nat.even_add_one]
  have : ¬ c u = true ↔ c v = true := by
    rw [← not_iff, ← Bool.eq_iff_iff]
    exact c.valid h
  tauto

Result:
no goals

Proof state:
α : Type u_1
G : SimpleGraph α
c : G.Coloring Bool
u✝ v✝ u v w : α
h : G.Adj u v
p : G.Walk v w
ih : Even p.length ↔ (c v = true ↔ c w = true)
⊢ ¬c u = c v

Tactic:
exact c.valid h

Result:
no goals

Proof state:
α : Type u_1
G : SimpleGraph α
c : G.Coloring Bool
u✝ v✝ u v w : α
h : G.Adj u v
p : G.Walk v w
ih : Even p.length ↔ (c v = true ↔ c w = true)
⊢ ¬c u = true ↔ c v = true

Tactic:
rw [← not_iff, ← Bool.eq_iff_iff]

Result:
α : Type u_1
G : SimpleGraph α
c : G.Coloring Bool
u✝ v✝ u v w : α
h : G.Adj u v
p : G.Walk v w
ih : Even p.length ↔ (c v = true ↔ c w = true)
⊢ ¬c u = c v

Proof state:
case cons
α : Type u_1
G : SimpleGraph α
c : G.Coloring Bool
u✝ v✝ u v w : α
h : G.Adj u v
p : G.Walk v w
ih : Even p.length ↔ (c v = true ↔ c w = true)
⊢ Even (Walk.cons h p).length ↔ (c u = true ↔ c w = true)

Tactic:
simp only [Walk.length_cons, Nat.even_add_one]

Result:
case cons
α : Type u_1
G : SimpleGraph α
c : G.Coloring Bool
u✝ v✝ u v w : α
h : G.Adj u v
p : G.Walk v w
ih : Even p.length ↔ (c v = true ↔ c w = true)
⊢ ¬Even p.length ↔ (c u = true ↔ c w = true)

Proof state:
case cons
α : Type u_1
G : SimpleGraph α
c : G.Coloring Bool
u✝ v✝ u v w : α
h : G.Adj u v
p : G.Walk v w
ih : Even p.length ↔ (c v = true ↔ c w = true)
⊢ ¬Even p.length ↔ (c u = true ↔ c w = true)

Tactic:
have : ¬ c u = true ↔ c v = true := by
  rw [← not_iff, ← Bool.eq_iff_iff]
  exact c.valid h

Result:
case cons
α : Type u_1
G : SimpleGraph α
c : G.Coloring Bool
u✝ v✝ u v w : α
h : G.Adj u v
p : G.Walk v w
ih : Even p.length ↔ (c v = true ↔ c w = true)
this : ¬c u = true ↔ c v = true
⊢ ¬Even p.length ↔ (c u = true ↔ c w = true)

Proof state:
case cons
α : Type u_1
G : SimpleGraph α
c : G.Coloring Bool
u✝ v✝ u v w : α
h : G.Adj u v
p : G.Walk v w
ih : Even p.length ↔ (c v = true ↔ c w = true)
this : ¬c u = true ↔ c v = true
⊢ ¬Even p.length ↔ (c u = true ↔ c w = true)

Tactic:
tauto

Result:
no goals

Proof state:
case nil
α : Type u_1
G : SimpleGraph α
c : G.Coloring Bool
u v u✝ : α
⊢ Even Walk.nil.length ↔ (c u✝ = true ↔ c u✝ = true)

Tactic:
simp

Result:
no goals
-- Mathlib/RingTheory/Algebraic/Basic.lean
theorem IsAlgebraic.of_aeval_of_transcendental {r : A} {f : R[X]}
    (H : IsAlgebraic R (aeval r f)) (hf : Transcendental R f) : IsAlgebraic R r

Proof state:
R : Type u
A : Type v
inst✝² : CommRing R
inst✝¹ : Ring A
inst✝ : Algebra R A
r : A
f : R[X]
hf : Transcendental R f
H : ¬IsAlgebraic R r
⊢ ¬IsAlgebraic R ((aeval r) f)

Tactic:
exact Transcendental.aeval_of_transcendental H hf

Result:
no goals

Proof state:
R : Type u
A : Type v
inst✝² : CommRing R
inst✝¹ : Ring A
inst✝ : Algebra R A
r : A
f : R[X]
H : IsAlgebraic R ((aeval r) f)
hf : Transcendental R f
⊢ IsAlgebraic R r

Tactic:
contrapose H

Result:
R : Type u
A : Type v
inst✝² : CommRing R
inst✝¹ : Ring A
inst✝ : Algebra R A
r : A
f : R[X]
hf : Transcendental R f
H : ¬IsAlgebraic R r
⊢ ¬IsAlgebraic R ((aeval r) f)
-- Mathlib/Combinatorics/SimpleGraph/Clique.lean
theorem IsNClique.map (h : G.IsNClique n s) {f : α ↪ β} :
    (G.map f).IsNClique n (s.map f) :=
  ⟨by rw [coe_map]; exact h.1.map, (card_map _).trans h.2⟩

Proof state:
α : Type u_1
β : Type u_2
G : SimpleGraph α
n : ℕ
s : Finset α
h : G.IsNClique n s
f : α ↪ β
⊢ (SimpleGraph.map f G).IsClique (⇑f '' ↑s)

Tactic:
exact h.1.map

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
G : SimpleGraph α
n : ℕ
s : Finset α
h : G.IsNClique n s
f : α ↪ β
⊢ (SimpleGraph.map f G).IsClique ↑(map f s)

Tactic:
rw [coe_map]

Result:
α : Type u_1
β : Type u_2
G : SimpleGraph α
n : ℕ
s : Finset α
h : G.IsNClique n s
f : α ↪ β
⊢ (SimpleGraph.map f G).IsClique (⇑f '' ↑s)
-- Mathlib/Algebra/Lie/OfAssociative.lean
theorem LieModule.toEnd_module_end :
    LieModule.toEnd R (Module.End R M) M = LieHom.id

Proof state:
R : Type u
M : Type w
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
⊢ toEnd R (Module.End R M) M = LieHom.id

Tactic:
ext g m

Result:
case h.h
R : Type u
M : Type w
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
g : Module.End R M
m : M
⊢ ((toEnd R (Module.End R M) M) g) m = (LieHom.id g) m

Proof state:
case h.h
R : Type u
M : Type w
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
g : Module.End R M
m : M
⊢ ((toEnd R (Module.End R M) M) g) m = (LieHom.id g) m

Tactic:
simp [lie_eq_smul]

Result:
no goals
-- Mathlib/Data/Fin/Basic.lean
/-- Sending `Fin (n+1)` to `Fin n` by subtracting one from anything above `p`
then back to `Fin (n+1)` with a gap around `p.succ` is the identity away from `p.succ`. -/
@[simp]
lemma succ_succAbove_predAbove {n : ℕ} {p : Fin n} {i : Fin (n + 1)} (h : i ≠ p.succ) :
    p.succ.succAbove (p.predAbove i) = i

Proof state:
case inl
n : ℕ
p : Fin n
i : Fin (n + 1)
h✝ : i ≠ p.succ
h : i < p.succ
⊢ p.succ.succAbove (p.predAbove i) = i

Tactic:
rw [predAbove_of_le_castSucc _ _ (le_castSucc_iff.2 h),
  succAbove_castPred_of_lt _ _ h]

Result:
no goals

Proof state:
case inr
n : ℕ
p : Fin n
i : Fin (n + 1)
h✝ : i ≠ p.succ
h : p.succ < i
⊢ p.succ.succAbove (p.predAbove i) = i

Tactic:
rw [predAbove_of_castSucc_lt _ _ (Fin.lt_of_le_of_lt (p.castSucc_le_succ) h),
  succAbove_pred_of_lt _ _ h]

Result:
no goals

Proof state:
n : ℕ
p : Fin n
i : Fin (n + 1)
h : i ≠ p.succ
⊢ p.succ.succAbove (p.predAbove i) = i

Tactic:
obtain h | h := Fin.lt_or_lt_of_ne h

Result:
case inl
n : ℕ
p : Fin n
i : Fin (n + 1)
h✝ : i ≠ p.succ
h : i < p.succ
⊢ p.succ.succAbove (p.predAbove i) = i

case inr
n : ℕ
p : Fin n
i : Fin (n + 1)
h✝ : i ≠ p.succ
h : p.succ < i
⊢ p.succ.succAbove (p.predAbove i) = i
-- Mathlib/Analysis/SpecialFunctions/Trigonometric/Deriv.lean
@[simp] lemma sinh_eq_zero : sinh x = 0 ↔ x = 0

Proof state:
x : ℝ
⊢ sinh x = 0 ↔ x = 0

Tactic:
rw [← @sinh_inj x, sinh_zero]

Result:
no goals
-- Mathlib/Probability/ProbabilityMassFunction/Integrals.lean
theorem integral_eq_sum [Fintype α] (p : PMF α) (f : α → E) :
    ∫ a, f a ∂(p.toMeasure) = ∑ a, (p a).toReal • f a

Proof state:
case e_f.h
α : Type u_1
inst✝⁵ : MeasurableSpace α
inst✝⁴ : MeasurableSingletonClass α
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : Fintype α
p : PMF α
f : α → E
x : α
⊢ (p.toMeasure {x}).toReal • f x = (p x).toReal • f x

Tactic:
congr 2

Result:
case e_f.h.e_a.e_a
α : Type u_1
inst✝⁵ : MeasurableSpace α
inst✝⁴ : MeasurableSingletonClass α
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : Fintype α
p : PMF α
f : α → E
x : α
⊢ p.toMeasure {x} = p x

Proof state:
α : Type u_1
inst✝⁵ : MeasurableSpace α
inst✝⁴ : MeasurableSingletonClass α
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : Fintype α
p : PMF α
f : α → E
⊢ ∫ (a : α), f a ∂p.toMeasure = ∑ a : α, (p a).toReal • f a

Tactic:
rw [integral_fintype _ .of_finite]

Result:
α : Type u_1
inst✝⁵ : MeasurableSpace α
inst✝⁴ : MeasurableSingletonClass α
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : Fintype α
p : PMF α
f : α → E
⊢ ∑ x : α, (p.toMeasure {x}).toReal • f x = ∑ a : α, (p a).toReal • f a

Proof state:
case e_f.h.e_a.e_a
α : Type u_1
inst✝⁵ : MeasurableSpace α
inst✝⁴ : MeasurableSingletonClass α
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : Fintype α
p : PMF α
f : α → E
x : α
⊢ p.toMeasure {x} = p x

Tactic:
exact PMF.toMeasure_apply_singleton p x (MeasurableSet.singleton _)

Result:
no goals

Proof state:
α : Type u_1
inst✝⁵ : MeasurableSpace α
inst✝⁴ : MeasurableSingletonClass α
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : Fintype α
p : PMF α
f : α → E
⊢ ∑ x : α, (p.toMeasure {x}).toReal • f x = ∑ a : α, (p a).toReal • f a

Tactic:
congr with x

Result:
case e_f.h
α : Type u_1
inst✝⁵ : MeasurableSpace α
inst✝⁴ : MeasurableSingletonClass α
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : Fintype α
p : PMF α
f : α → E
x : α
⊢ (p.toMeasure {x}).toReal • f x = (p x).toReal • f x
-- Mathlib/FieldTheory/IntermediateField/Adjoin/Defs.lean
theorem fg_sup {S T : IntermediateField F E} (hS : S.FG) (hT : T.FG) : (S ⊔ T).FG

Proof state:
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
S T : IntermediateField F E
hS : S.FG
hT : T.FG
⊢ (S ⊔ T).FG

Tactic:
obtain ⟨s, rfl⟩ := hS

Result:
case intro
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
T : IntermediateField F E
hT : T.FG
s : Finset E
⊢ (adjoin F ↑s ⊔ T).FG

Proof state:
case intro.intro
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
s t : Finset E
⊢ (adjoin F ↑(s ∪ t)).FG

Tactic:
exact fg_adjoin_finset _

Result:
no goals

Proof state:
case intro.intro
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
s t : Finset E
⊢ (adjoin F ↑s ⊔ adjoin F ↑t).FG

Tactic:
classical rw [← adjoin_union, ← Finset.coe_union]

Result:
case intro.intro
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
s t : Finset E
⊢ (adjoin F ↑(s ∪ t)).FG

Proof state:
case intro
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
T : IntermediateField F E
hT : T.FG
s : Finset E
⊢ (adjoin F ↑s ⊔ T).FG

Tactic:
obtain ⟨t, rfl⟩ := hT

Result:
case intro.intro
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
s t : Finset E
⊢ (adjoin F ↑s ⊔ adjoin F ↑t).FG

Proof state:
case intro.intro
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
s t : Finset E
⊢ (adjoin F ↑s ⊔ adjoin F ↑t).FG

Tactic:
rw [← adjoin_union, ← Finset.coe_union]

Result:
case intro.intro
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
s t : Finset E
⊢ (adjoin F ↑(s ∪ t)).FG
-- Mathlib/RingTheory/Ideal/Operations.lean
theorem map_le_smul_top (I : Ideal R) (f : R →ₗ[R] M) :
    Submodule.map f I ≤ I • (⊤ : Submodule R M)

Proof state:
R : Type u
M : Type v
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
I : Ideal R
f : R →ₗ[R] M
⊢ map f I ≤ I • ⊤

Tactic:
rintro _ ⟨y, hy, rfl⟩

Result:
case intro.intro
R : Type u
M : Type v
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
I : Ideal R
f : R →ₗ[R] M
y : R
hy : y ∈ ↑I
⊢ f y ∈ I • ⊤

Proof state:
case intro.intro
R : Type u
M : Type v
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
I : Ideal R
f : R →ₗ[R] M
y : R
hy : y ∈ ↑I
⊢ y • f 1 ∈ I • ⊤

Tactic:
exact smul_mem_smul hy mem_top

Result:
no goals

Proof state:
case intro.intro
R : Type u
M : Type v
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
I : Ideal R
f : R →ₗ[R] M
y : R
hy : y ∈ ↑I
⊢ f y ∈ I • ⊤

Tactic:
rw [← mul_one y, ← smul_eq_mul, f.map_smul]

Result:
case intro.intro
R : Type u
M : Type v
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
I : Ideal R
f : R →ₗ[R] M
y : R
hy : y ∈ ↑I
⊢ y • f 1 ∈ I • ⊤
-- Mathlib/Order/WellFoundedSet.lean
theorem isPWO_insert {a} : IsPWO (insert a s) ↔ IsPWO s

Proof state:
α : Type u_2
inst✝ : Preorder α
s : Set α
a : α
⊢ (insert a s).IsPWO ↔ s.IsPWO

Tactic:
simp only [← singleton_union, isPWO_union, isPWO_singleton, true_and]

Result:
no goals
-- Mathlib/Algebra/Polynomial/Degree/Definitions.lean
theorem natDegree_monomial_le (a : R) {m : ℕ} : (monomial m a).natDegree ≤ m

Proof state:
R : Type u
inst✝ : Semiring R
a : R
m : ℕ
⊢ ((monomial m) a).natDegree ≤ m

Tactic:
classical
rw [Polynomial.natDegree_monomial]
split_ifs
exacts [Nat.zero_le _, le_rfl]

Result:
no goals

Proof state:
case pos
R : Type u
inst✝ : Semiring R
a : R
m : ℕ
h✝ : a = 0
⊢ 0 ≤ m

case neg
R : Type u
inst✝ : Semiring R
a : R
m : ℕ
h✝ : ¬a = 0
⊢ m ≤ m

Tactic:
exacts [Nat.zero_le _, le_rfl]

Result:
no goals

Proof state:
R : Type u
inst✝ : Semiring R
a : R
m : ℕ
⊢ (if a = 0 then 0 else m) ≤ m

Tactic:
split_ifs

Result:
case pos
R : Type u
inst✝ : Semiring R
a : R
m : ℕ
h✝ : a = 0
⊢ 0 ≤ m

case neg
R : Type u
inst✝ : Semiring R
a : R
m : ℕ
h✝ : ¬a = 0
⊢ m ≤ m

Proof state:
R : Type u
inst✝ : Semiring R
a : R
m : ℕ
⊢ ((monomial m) a).natDegree ≤ m

Tactic:
rw [Polynomial.natDegree_monomial]

Result:
R : Type u
inst✝ : Semiring R
a : R
m : ℕ
⊢ (if a = 0 then 0 else m) ≤ m