harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Order/Atoms.lean
theorem Set.OrdConnected.isStronglyAtomic [IsStronglyAtomic α] {s : Set α}
    (h : Set.OrdConnected s) : IsStronglyAtomic s where
  exists_covBy_le_of_lt

Proof state:
α : Type u_4
inst✝¹ : Preorder α
inst✝ : IsStronglyAtomic α
s : Set α
h : s.OrdConnected
c : α
hc : c ∈ s
d : α
hd : d ∈ s
hcd : ⟨c, hc⟩ < ⟨d, hd⟩
x : α
hcx : c ⋖ x
hxd : x ≤ d
⊢ ⟨c, hc⟩ < ⟨x, ⋯⟩

Tactic:
simpa using hcx.lt

Result:
no goals

Proof state:
case mk.mk.intro.intro
α : Type u_4
inst✝¹ : Preorder α
inst✝ : IsStronglyAtomic α
s : Set α
h : s.OrdConnected
c : α
hc : c ∈ s
d : α
hd : d ∈ s
hcd : ⟨c, hc⟩ < ⟨d, hd⟩
x : α
hcx : c ⋖ x
hxd : x ≤ d
⊢ ∃ x, ⟨c, hc⟩ ⋖ x ∧ x ≤ ⟨d, hd⟩

Tactic:
exact ⟨⟨x, h.out' hc hd ⟨hcx.le, hxd⟩⟩,
  ⟨by simpa using hcx.lt, fun y hy hy' ↦ hcx.2 (by simpa using hy) (by simpa using hy')⟩, hxd⟩

Result:
no goals

Proof state:
α : Type u_4
inst✝¹ : Preorder α
inst✝ : IsStronglyAtomic α
s : Set α
h : s.OrdConnected
c : α
hc : c ∈ s
d : α
hd : d ∈ s
hcd : ⟨c, hc⟩ < ⟨d, hd⟩
x : α
hcx : c ⋖ x
hxd : x ≤ d
y : ↑s
hy : ⟨c, hc⟩ < y
hy' : y < ⟨x, ⋯⟩
⊢ c < ?m.50417 y hy hy'

Tactic:
simpa using hy

Result:
no goals

Proof state:
α : Type u_4
inst✝¹ : Preorder α
inst✝ : IsStronglyAtomic α
s : Set α
h : s.OrdConnected
⊢ ∀ (a b : ↑s), a < b → ∃ x, a ⋖ x ∧ x ≤ b

Tactic:
rintro ⟨c, hc⟩ ⟨d, hd⟩ hcd

Result:
case mk.mk
α : Type u_4
inst✝¹ : Preorder α
inst✝ : IsStronglyAtomic α
s : Set α
h : s.OrdConnected
c : α
hc : c ∈ s
d : α
hd : d ∈ s
hcd : ⟨c, hc⟩ < ⟨d, hd⟩
⊢ ∃ x, ⟨c, hc⟩ ⋖ x ∧ x ≤ ⟨d, hd⟩

Proof state:
α : Type u_4
inst✝¹ : Preorder α
inst✝ : IsStronglyAtomic α
s : Set α
h : s.OrdConnected
c : α
hc : c ∈ s
d : α
hd : d ∈ s
hcd : ⟨c, hc⟩ < ⟨d, hd⟩
x : α
hcx : c ⋖ x
hxd : x ≤ d
y : ↑s
hy : ⟨c, hc⟩ < y
hy' : y < ⟨x, ⋯⟩
⊢ (fun a => ↑a) y < x

Tactic:
simpa using hy'

Result:
no goals

Proof state:
case mk.mk
α : Type u_4
inst✝¹ : Preorder α
inst✝ : IsStronglyAtomic α
s : Set α
h : s.OrdConnected
c : α
hc : c ∈ s
d : α
hd : d ∈ s
hcd : ⟨c, hc⟩ < ⟨d, hd⟩
⊢ ∃ x, ⟨c, hc⟩ ⋖ x ∧ x ≤ ⟨d, hd⟩

Tactic:
obtain ⟨x, hcx, hxd⟩ := (Subtype.mk_lt_mk.1 hcd).exists_covby_le

Result:
case mk.mk.intro.intro
α : Type u_4
inst✝¹ : Preorder α
inst✝ : IsStronglyAtomic α
s : Set α
h : s.OrdConnected
c : α
hc : c ∈ s
d : α
hd : d ∈ s
hcd : ⟨c, hc⟩ < ⟨d, hd⟩
x : α
hcx : c ⋖ x
hxd : x ≤ d
⊢ ∃ x, ⟨c, hc⟩ ⋖ x ∧ x ≤ ⟨d, hd⟩
-- Mathlib/LinearAlgebra/Lagrange.lean
theorem eq_interpolate_iff {f : F[X]} (hvs : Set.InjOn v s) :
    (f.degree < #s ∧ ∀ i ∈ s, eval (v i) f = r i) ↔ f = interpolate s v r

Proof state:
F : Type u_1
inst✝¹ : Field F
ι : Type u_2
inst✝ : DecidableEq ι
s : Finset ι
v r : ι → F
f : F[X]
hvs : Set.InjOn v ↑s
⊢ (f.degree < ↑(#s) ∧ ∀ i ∈ s, eval (v i) f = r i) ↔ f = (interpolate s v) r

Tactic:
constructor <;> intro h

Result:
case mp
F : Type u_1
inst✝¹ : Field F
ι : Type u_2
inst✝ : DecidableEq ι
s : Finset ι
v r : ι → F
f : F[X]
hvs : Set.InjOn v ↑s
h : f.degree < ↑(#s) ∧ ∀ i ∈ s, eval (v i) f = r i
⊢ f = (interpolate s v) r

case mpr
F : Type u_1
inst✝¹ : Field F
ι : Type u_2
inst✝ : DecidableEq ι
s : Finset ι
v r : ι → F
f : F[X]
hvs : Set.InjOn v ↑s
h : f = (interpolate s v) r
⊢ f.degree < ↑(#s) ∧ ∀ i ∈ s, eval (v i) f = r i

Proof state:
case mpr
F : Type u_1
inst✝¹ : Field F
ι : Type u_2
inst✝ : DecidableEq ι
s : Finset ι
v r : ι → F
f : F[X]
hvs : Set.InjOn v ↑s
h : f = (interpolate s v) r
⊢ ((interpolate s v) r).degree < ↑(#s) ∧ ∀ i ∈ s, eval (v i) ((interpolate s v) r) = r i

Tactic:
exact ⟨degree_interpolate_lt _ hvs, fun _ hi => eval_interpolate_at_node _ hvs hi⟩

Result:
no goals

Proof state:
case mp
F : Type u_1
inst✝¹ : Field F
ι : Type u_2
inst✝ : DecidableEq ι
s : Finset ι
v r : ι → F
f : F[X]
hvs : Set.InjOn v ↑s
h : f.degree < ↑(#s) ∧ ∀ i ∈ s, eval (v i) f = r i
⊢ f = (interpolate s v) r

Tactic:
exact eq_interpolate_of_eval_eq _ hvs h.1 h.2

Result:
no goals

Proof state:
case mpr
F : Type u_1
inst✝¹ : Field F
ι : Type u_2
inst✝ : DecidableEq ι
s : Finset ι
v r : ι → F
f : F[X]
hvs : Set.InjOn v ↑s
h : f = (interpolate s v) r
⊢ f.degree < ↑(#s) ∧ ∀ i ∈ s, eval (v i) f = r i

Tactic:
rw [h]

Result:
case mpr
F : Type u_1
inst✝¹ : Field F
ι : Type u_2
inst✝ : DecidableEq ι
s : Finset ι
v r : ι → F
f : F[X]
hvs : Set.InjOn v ↑s
h : f = (interpolate s v) r
⊢ ((interpolate s v) r).degree < ↑(#s) ∧ ∀ i ∈ s, eval (v i) ((interpolate s v) r) = r i
-- Mathlib/RingTheory/DedekindDomain/Different.lean
lemma self_mul_dual (hI : I ≠ 0) :
    I * dual A K I = dual A K 1

Proof state:
A : Type u_1
K : Type u_2
L : Type u
B : Type u_3
inst✝¹⁸ : CommRing A
inst✝¹⁷ : Field K
inst✝¹⁶ : CommRing B
inst✝¹⁵ : Field L
inst✝¹⁴ : Algebra A K
inst✝¹³ : Algebra B L
inst✝¹² : Algebra A B
inst✝¹¹ : Algebra K L
inst✝¹⁰ : Algebra A L
inst✝⁹ : IsScalarTower A K L
inst✝⁸ : IsScalarTower A B L
inst✝⁷ : IsDomain A
inst✝⁶ : IsFractionRing A K
inst✝⁵ : FiniteDimensional K L
inst✝⁴ : Algebra.IsSeparable K L
inst✝³ : IsIntegralClosure B A L
inst✝² : IsFractionRing B L
inst✝¹ : IsIntegrallyClosed A
inst✝ : IsDedekindDomain B
I : FractionalIdeal B⁰ L
hI : I ≠ 0
⊢ I * dual A K I = dual A K 1

Tactic:
rw [mul_comm, dual_mul_self A K hI]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Lemmas.lean
theorem concat_inj_right {l : List α} {a a' : α} : concat l a = concat l a' ↔ a = a' :=
  ⟨last_eq_of_concat_eq, by simp⟩

Proof state:
α : Type u_1
l : List α
a a' : α
⊢ a = a' → l.concat a = l.concat a'

Tactic:
simp

Result:
no goals
-- Mathlib/Data/Fintype/EquivFin.lean
theorem one_lt_card_iff_nontrivial : 1 < card α ↔ Nontrivial α

Proof state:
α : Type u_1
inst✝ : Fintype α
⊢ 1 < card α ↔ Nontrivial α

Tactic:
rw [← not_iff_not, not_lt, not_nontrivial_iff_subsingleton, card_le_one_iff_subsingleton]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Option/Attach.lean
theorem map_attach {o : Option α} (f : { x // x ∈ o } → β) :
    o.attach.map f = o.pmap (fun a (h : a ∈ o) => f ⟨a, h⟩) (fun _ h => h)

Proof state:
α : Type u_1
β : Type u_2
o : Option α
f : { x // x ∈ o } → β
⊢ Option.map f o.attach = pmap (fun a h => f ⟨a, h⟩) o ⋯

Tactic:
cases o <;> simp

Result:
no goals
-- Mathlib/MeasureTheory/Measure/Map.lean
theorem map_ae (f : α ≃ᵐ β) (μ : Measure α) : Filter.map f (ae μ) = ae (map f μ)

Proof state:
case h
α : Type u_1
β : Type u_2
x✝ : MeasurableSpace α
inst✝ : MeasurableSpace β
f : α ≃ᵐ β
μ : Measure α
s : Set β
⊢ s ∈ Filter.map (⇑f) (ae μ) ↔ s ∈ ae (map (⇑f) μ)

Tactic:
simp_rw [mem_map, mem_ae_iff, ← preimage_compl, f.map_apply]

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
x✝ : MeasurableSpace α
inst✝ : MeasurableSpace β
f : α ≃ᵐ β
μ : Measure α
⊢ Filter.map (⇑f) (ae μ) = ae (map (⇑f) μ)

Tactic:
ext s

Result:
case h
α : Type u_1
β : Type u_2
x✝ : MeasurableSpace α
inst✝ : MeasurableSpace β
f : α ≃ᵐ β
μ : Measure α
s : Set β
⊢ s ∈ Filter.map (⇑f) (ae μ) ↔ s ∈ ae (map (⇑f) μ)
-- Mathlib/RingTheory/Trace/Basic.lean
theorem sum_embeddings_eq_finrank_mul [FiniteDimensional K F] [Algebra.IsSeparable K F]
    (pb : PowerBasis K L) :
    ∑ σ : F →ₐ[K] E, σ (algebraMap L F pb.gen) =
      finrank L F •
        (@Finset.univ _ (PowerBasis.AlgHom.fintype pb)).sum fun σ : L →ₐ[K] E => σ pb.gen

Proof state:
K : Type u_4
L : Type u_5
inst✝¹¹ : Field K
inst✝¹⁰ : Field L
inst✝⁹ : Algebra K L
F : Type u_6
inst✝⁸ : Field F
inst✝⁷ : Algebra L F
inst✝⁶ : Algebra K F
inst✝⁵ : IsScalarTower K L F
E : Type u_7
inst✝⁴ : Field E
inst✝³ : Algebra K E
inst✝² : IsAlgClosed E
inst✝¹ : FiniteDimensional K F
inst✝ : Algebra.IsSeparable K F
pb : PowerBasis K L
this : FiniteDimensional L F
⊢ ∑ σ : F →ₐ[K] E, σ ((algebraMap L F) pb.gen) = finrank L F • ∑ σ : L →ₐ[K] E, σ pb.gen

Tactic:
haveI : Algebra.IsSeparable L F := Algebra.isSeparable_tower_top_of_isSeparable K L F

Result:
K : Type u_4
L : Type u_5
inst✝¹¹ : Field K
inst✝¹⁰ : Field L
inst✝⁹ : Algebra K L
F : Type u_6
inst✝⁸ : Field F
inst✝⁷ : Algebra L F
inst✝⁶ : Algebra K F
inst✝⁵ : IsScalarTower K L F
E : Type u_7
inst✝⁴ : Field E
inst✝³ : Algebra K E
inst✝² : IsAlgClosed E
inst✝¹ : FiniteDimensional K F
inst✝ : Algebra.IsSeparable K F
pb : PowerBasis K L
this✝ : FiniteDimensional L F
this : Algebra.IsSeparable L F
⊢ ∑ σ : F →ₐ[K] E, σ ((algebraMap L F) pb.gen) = finrank L F • ∑ σ : L →ₐ[K] E, σ pb.gen

Proof state:
K : Type u_4
L : Type u_5
inst✝¹¹ : Field K
inst✝¹⁰ : Field L
inst✝⁹ : Algebra K L
F : Type u_6
inst✝⁸ : Field F
inst✝⁷ : Algebra L F
inst✝⁶ : Algebra K F
inst✝⁵ : IsScalarTower K L F
E : Type u_7
inst✝⁴ : Field E
inst✝³ : Algebra K E
inst✝² : IsAlgClosed E
inst✝¹ : FiniteDimensional K F
inst✝ : Algebra.IsSeparable K F
pb : PowerBasis K L
this✝ : FiniteDimensional L F
this : Algebra.IsSeparable L F
⊢ ∑ σ : F →ₐ[K] E, σ ((algebraMap L F) pb.gen) = finrank L F • ∑ σ : L →ₐ[K] E, σ pb.gen

Tactic:
letI : Fintype (L →ₐ[K] E) := PowerBasis.AlgHom.fintype pb

Result:
K : Type u_4
L : Type u_5
inst✝¹¹ : Field K
inst✝¹⁰ : Field L
inst✝⁹ : Algebra K L
F : Type u_6
inst✝⁸ : Field F
inst✝⁷ : Algebra L F
inst✝⁶ : Algebra K F
inst✝⁵ : IsScalarTower K L F
E : Type u_7
inst✝⁴ : Field E
inst✝³ : Algebra K E
inst✝² : IsAlgClosed E
inst✝¹ : FiniteDimensional K F
inst✝ : Algebra.IsSeparable K F
pb : PowerBasis K L
this✝¹ : FiniteDimensional L F
this✝ : Algebra.IsSeparable L F
this : Fintype (L →ₐ[K] E) := PowerBasis.AlgHom.fintype pb
⊢ ∑ σ : F →ₐ[K] E, σ ((algebraMap L F) pb.gen) = finrank L F • ∑ σ : L →ₐ[K] E, σ pb.gen
-- Mathlib/FieldTheory/SeparableClosure.lean
theorem separableClosure.map_eq_of_separableClosure_eq_bot [Algebra E K] [IsScalarTower F E K]
    (h : separableClosure E K = ⊥) :
    (separableClosure F E).map (IsScalarTower.toAlgHom F E K) = separableClosure F K

Proof state:
F : Type u
E : Type v
inst✝⁶ : Field F
inst✝⁵ : Field E
inst✝⁴ : Algebra F E
K : Type w
inst✝³ : Field K
inst✝² : Algebra F K
inst✝¹ : Algebra E K
inst✝ : IsScalarTower F E K
h : separableClosure E K = ⊥
⊢ IntermediateField.map (IsScalarTower.toAlgHom F E K) (separableClosure F E) = separableClosure F K

Tactic:
refine le_antisymm (map_le_of_algHom _) (fun x hx ↦ ?_)

Result:
F : Type u
E : Type v
inst✝⁶ : Field F
inst✝⁵ : Field E
inst✝⁴ : Algebra F E
K : Type w
inst✝³ : Field K
inst✝² : Algebra F K
inst✝¹ : Algebra E K
inst✝ : IsScalarTower F E K
h : separableClosure E K = ⊥
x : K
hx : x ∈ separableClosure F K
⊢ x ∈ IntermediateField.map (IsScalarTower.toAlgHom F E K) (separableClosure F E)

Proof state:
F : Type u
E : Type v
inst✝⁶ : Field F
inst✝⁵ : Field E
inst✝⁴ : Algebra F E
K : Type w
inst✝³ : Field K
inst✝² : Algebra F K
inst✝¹ : Algebra E K
inst✝ : IsScalarTower F E K
h : separableClosure E K = ⊥
x : K
hx : x ∈ separableClosure F K
⊢ x ∈ IntermediateField.map (IsScalarTower.toAlgHom F E K) (separableClosure F E)

Tactic:
obtain ⟨y, rfl⟩ := mem_bot.1 <| h ▸ mem_separableClosure_iff.2
  (IsSeparable.tower_top E <| mem_separableClosure_iff.1 hx)

Result:
case intro
F : Type u
E : Type v
inst✝⁶ : Field F
inst✝⁵ : Field E
inst✝⁴ : Algebra F E
K : Type w
inst✝³ : Field K
inst✝² : Algebra F K
inst✝¹ : Algebra E K
inst✝ : IsScalarTower F E K
h : separableClosure E K = ⊥
y : E
hx : (algebraMap E K) y ∈ separableClosure F K
⊢ (algebraMap E K) y ∈ IntermediateField.map (IsScalarTower.toAlgHom F E K) (separableClosure F E)

Proof state:
case intro
F : Type u
E : Type v
inst✝⁶ : Field F
inst✝⁵ : Field E
inst✝⁴ : Algebra F E
K : Type w
inst✝³ : Field K
inst✝² : Algebra F K
inst✝¹ : Algebra E K
inst✝ : IsScalarTower F E K
h : separableClosure E K = ⊥
y : E
hx : (algebraMap E K) y ∈ separableClosure F K
⊢ (algebraMap E K) y ∈ IntermediateField.map (IsScalarTower.toAlgHom F E K) (separableClosure F E)

Tactic:
exact ⟨y, (map_mem_separableClosure_iff <| IsScalarTower.toAlgHom F E K).mp hx, rfl⟩

Result:
no goals
-- Mathlib/CategoryTheory/Localization/CalculusOfFractions/Preadditive.lean
lemma zero_add' (f : L.obj X ⟶ L.obj Y) :
    add' W (L.map 0) f = f

Proof state:
C : Type u_1
D : Type u_2
inst✝⁴ : Category.{u_4, u_1} C
inst✝³ : Category.{u_3, u_2} D
inst✝² : Preadditive C
L : C ⥤ D
W : MorphismProperty C
inst✝¹ : L.IsLocalization W
inst✝ : W.HasLeftCalculusOfFractions
X Y : C
f : L.obj X ⟶ L.obj Y
⊢ add' W (L.map 0) f = f

Tactic:
rw [add'_comm, add'_zero]

Result:
no goals
-- Mathlib/GroupTheory/MonoidLocalization/Basic.lean
theorem lift_mk' (x y) : f.lift hg (f.mk' x y) = g x * (IsUnit.liftRight (g.restrict S) hg y)⁻¹ :=
  (mul_inv hg).2 <|
    f.eq_of_eq hg <| by
      simp_rw [f.toMap.map_mul, sec_spec', mul_assoc, f.mk'_spec, mul_comm]

Proof state:
M : Type u_1
inst✝² : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝¹ : CommMonoid N
P : Type u_3
inst✝ : CommMonoid P
f : S.LocalizationMap N
g : M →* P
hg : ∀ (y : ↥S), IsUnit (g ↑y)
x : M
y : ↥S
⊢ f.toMap ((f.sec (f.mk' x y)).1 * ↑y) = f.toMap (x * ↑(f.sec (f.mk' x y)).2)

Tactic:
simp_rw [f.toMap.map_mul, sec_spec', mul_assoc, f.mk'_spec, mul_comm]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Lemmas.lean
theorem reverse_reverse (as : List α) : as.reverse.reverse = as

Proof state:
α : Type u_1
as : List α
⊢ as.reverse.reverse = as

Tactic:
simp only [reverse]

Result:
α : Type u_1
as : List α
⊢ (as.reverseAux []).reverseAux [] = as

Proof state:
α : Type u_1
as : List α
⊢ (as.reverseAux []).reverseAux [] = as

Tactic:
rw [reverseAux_reverseAux_nil]

Result:
α : Type u_1
as : List α
⊢ [].reverseAux as = as

Proof state:
α : Type u_1
as : List α
⊢ [].reverseAux as = as

Tactic:
rfl

Result:
no goals
-- Mathlib/MeasureTheory/Measure/Stieltjes.lean
theorem measure_Icc (a b : ℝ) : f.measure (Icc a b) = ofReal (f b - leftLim f a)

Proof state:
case inl
f : StieltjesFunction
a b : ℝ
hab : a ≤ b
A : Disjoint {a} (Ioc a b)
⊢ f.measure (Icc a b) = ofReal (↑f b - leftLim (↑f) a)

Tactic:
simp [← Icc_union_Ioc_eq_Icc le_rfl hab, -singleton_union, ← ENNReal.ofReal_add,
  f.mono.leftLim_le, measure_union A measurableSet_Ioc, f.mono hab]

Result:
no goals

Proof state:
f : StieltjesFunction
a b : ℝ
⊢ f.measure (Icc a b) = ofReal (↑f b - leftLim (↑f) a)

Tactic:
rcases le_or_lt a b with (hab | hab)

Result:
case inl
f : StieltjesFunction
a b : ℝ
hab : a ≤ b
⊢ f.measure (Icc a b) = ofReal (↑f b - leftLim (↑f) a)

case inr
f : StieltjesFunction
a b : ℝ
hab : b < a
⊢ f.measure (Icc a b) = ofReal (↑f b - leftLim (↑f) a)

Proof state:
case inr
f : StieltjesFunction
a b : ℝ
hab : b < a
⊢ ofReal (↑f b - leftLim (↑f) a) = 0

Tactic:
simp [ENNReal.ofReal_eq_zero, f.mono.le_leftLim hab]

Result:
no goals

Proof state:
case inr
f : StieltjesFunction
a b : ℝ
hab : b < a
⊢ f.measure (Icc a b) = ofReal (↑f b - leftLim (↑f) a)

Tactic:
simp only [hab, measure_empty, Icc_eq_empty, not_le]

Result:
case inr
f : StieltjesFunction
a b : ℝ
hab : b < a
⊢ 0 = ofReal (↑f b - leftLim (↑f) a)

Proof state:
f : StieltjesFunction
a b : ℝ
hab : a ≤ b
⊢ Disjoint {a} (Ioc a b)

Tactic:
simp

Result:
no goals

Proof state:
case inl
f : StieltjesFunction
a b : ℝ
hab : a ≤ b
⊢ f.measure (Icc a b) = ofReal (↑f b - leftLim (↑f) a)

Tactic:
have A : Disjoint {a} (Ioc a b) := by simp

Result:
case inl
f : StieltjesFunction
a b : ℝ
hab : a ≤ b
A : Disjoint {a} (Ioc a b)
⊢ f.measure (Icc a b) = ofReal (↑f b - leftLim (↑f) a)

Proof state:
case inr
f : StieltjesFunction
a b : ℝ
hab : b < a
⊢ 0 = ofReal (↑f b - leftLim (↑f) a)

Tactic:
symm

Result:
case inr
f : StieltjesFunction
a b : ℝ
hab : b < a
⊢ ofReal (↑f b - leftLim (↑f) a) = 0
-- Mathlib/GroupTheory/FreeAbelianGroupFinsupp.lean
theorem Finsupp.toFreeAbelianGroup_comp_toFinsupp :
    toFreeAbelianGroup.comp toFinsupp = AddMonoidHom.id (FreeAbelianGroup X)

Proof state:
X : Type u_1
⊢ toFreeAbelianGroup.comp toFinsupp = AddMonoidHom.id (FreeAbelianGroup X)

Tactic:
ext

Result:
case H
X : Type u_1
x✝ : X
⊢ (toFreeAbelianGroup.comp toFinsupp) (of x✝) = (AddMonoidHom.id (FreeAbelianGroup X)) (of x✝)

Proof state:
case H
X : Type u_1
x✝ : X
⊢ (toFreeAbelianGroup.comp toFinsupp) (of x✝) = (AddMonoidHom.id (FreeAbelianGroup X)) (of x✝)

Tactic:
rw [toFreeAbelianGroup, toFinsupp, AddMonoidHom.comp_apply, lift.of,
  liftAddHom_apply_single, AddMonoidHom.flip_apply, smulAddHom_apply, one_smul,
  AddMonoidHom.id_apply]

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Walk.lean
@[simp] lemma getVert_copy {u v w x : V} (p : G.Walk u v) (i : ℕ) (h : u = w) (h' : v = x) :
    (p.copy h h').getVert i = p.getVert i

Proof state:
V : Type u
G : SimpleGraph V
w x : V
i : ℕ
p : G.Walk w x
⊢ (p.copy ⋯ ⋯).getVert i = p.getVert i

Tactic:
rfl

Result:
no goals

Proof state:
V : Type u
G : SimpleGraph V
u v w x : V
p : G.Walk u v
i : ℕ
h : u = w
h' : v = x
⊢ (p.copy h h').getVert i = p.getVert i

Tactic:
subst_vars

Result:
V : Type u
G : SimpleGraph V
w x : V
i : ℕ
p : G.Walk w x
⊢ (p.copy ⋯ ⋯).getVert i = p.getVert i
-- Mathlib/.lake/packages/lean4/src/lean/Init/Grind/Lemmas.lean
theorem Bool.and_eq_of_eq_true_left {a b : Bool} (h : a = true) : (a && b) = b

Proof state:
a b : Bool
h : a = true
⊢ (a && b) = b

Tactic:
simp [h]

Result:
no goals
-- Mathlib/Data/Matroid/Basic.lean
theorem Indep.subset (hJ : M.Indep J) (hIJ : I ⊆ J) : M.Indep I

Proof state:
α : Type u_1
M : Matroid α
I J : Set α
hJ : M.Indep J
hIJ : I ⊆ J
⊢ M.Indep I

Tactic:
obtain ⟨B, hB, hJB⟩ := hJ.exists_isBase_superset

Result:
case intro.intro
α : Type u_1
M : Matroid α
I J : Set α
hJ : M.Indep J
hIJ : I ⊆ J
B : Set α
hB : M.IsBase B
hJB : J ⊆ B
⊢ M.Indep I

Proof state:
case intro.intro
α : Type u_1
M : Matroid α
I J : Set α
hJ : M.Indep J
hIJ : I ⊆ J
B : Set α
hB : M.IsBase B
hJB : J ⊆ B
⊢ M.Indep I

Tactic:
exact indep_iff.2 ⟨B, hB, hIJ.trans hJB⟩

Result:
no goals
-- Mathlib/MeasureTheory/Constructions/BorelSpace/Real.lean
theorem EReal.measurable_of_measurable_real {f : EReal → α} (h : Measurable fun p : ℝ => f p) :
    Measurable f :=
  measurable_of_measurable_on_compl_finite {⊥, ⊤} (by simp)
    (MeasurableEquiv.erealEquivReal.symm.measurable_comp_iff.1 h)

Proof state:
α : Type u_1
mα : MeasurableSpace α
f : EReal → α
h : Measurable fun p => f ↑p
⊢ {⊥, ⊤}.Finite

Tactic:
simp

Result:
no goals
-- Mathlib/MeasureTheory/Function/L1Space/Integrable.lean
theorem MemLp.integrable_norm_rpow {f : α → β} {p : ℝ≥0∞} (hf : MemLp f p μ) (hp_ne_zero : p ≠ 0)
    (hp_ne_top : p ≠ ∞) : Integrable (fun x : α => ‖f x‖ ^ p.toReal) μ

Proof state:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
f : α → β
p : ℝ≥0∞
hf : MemLp f p μ
hp_ne_zero : p ≠ 0
hp_ne_top : p ≠ ⊤
⊢ Integrable (fun x => ‖f x‖ ^ p.toReal) μ

Tactic:
rw [← memLp_one_iff_integrable]

Result:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
f : α → β
p : ℝ≥0∞
hf : MemLp f p μ
hp_ne_zero : p ≠ 0
hp_ne_top : p ≠ ⊤
⊢ MemLp (fun x => ‖f x‖ ^ p.toReal) 1 μ

Proof state:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
f : α → β
p : ℝ≥0∞
hf : MemLp f p μ
hp_ne_zero : p ≠ 0
hp_ne_top : p ≠ ⊤
⊢ MemLp (fun x => ‖f x‖ ^ p.toReal) 1 μ

Tactic:
exact hf.norm_rpow hp_ne_zero hp_ne_top

Result:
no goals
-- Mathlib/MeasureTheory/Integral/SetToL1.lean
theorem smul [Monoid 𝕜] [DistribMulAction 𝕜 β] (hT : FinMeasAdditive μ T) (c : 𝕜) :
    FinMeasAdditive μ fun s => c • T s := fun s t hs ht hμs hμt hst => by
  simp [hT s t hs ht hμs hμt hst]

Proof state:
α : Type u_1
𝕜 : Type u_6
m : MeasurableSpace α
μ : Measure α
β : Type u_7
inst✝² : AddCommMonoid β
T : Set α → β
inst✝¹ : Monoid 𝕜
inst✝ : DistribMulAction 𝕜 β
hT : FinMeasAdditive μ T
c : 𝕜
s t : Set α
hs : MeasurableSet s
ht : MeasurableSet t
hμs : μ s ≠ ⊤
hμt : μ t ≠ ⊤
hst : Disjoint s t
⊢ (fun s => c • T s) (s ∪ t) = (fun s => c • T s) s + (fun s => c • T s) t

Tactic:
simp [hT s t hs ht hμs hμt hst]

Result:
no goals
-- Mathlib/Probability/Independence/ZeroOne.lean
theorem measure_zero_or_one_of_measurableSet_limsup
    (h_le : ∀ n, s n ≤ m0) (h_indep : iIndep s μ)
    (hf : ∀ t, p t → tᶜ ∈ f) (hns : Directed (· ≤ ·) ns) (hnsp : ∀ a, p (ns a))
    (hns_univ : ∀ n, ∃ a, n ∈ ns a) {t : Set Ω} (ht_tail : MeasurableSet[limsup s f] t) :
    μ t = 0 ∨ μ t = 1

Proof state:
Ω : Type u_2
ι : Type u_3
s : ι → MeasurableSpace Ω
m0 : MeasurableSpace Ω
μ : Measure Ω
β : Type u_4
p : Set ι → Prop
f : Filter ι
ns : β → Set ι
h_le : ∀ (n : ι), s n ≤ m0
h_indep : iIndep s μ
hf : ∀ (t : Set ι), p t → tᶜ ∈ f
hns : Directed (fun x1 x2 => x1 ≤ x2) ns
hnsp : ∀ (a : β), p (ns a)
hns_univ : ∀ (n : ι), ∃ a, n ∈ ns a
t : Set Ω
ht_tail : MeasurableSet t
⊢ μ t = 0 ∨ μ t = 1

Tactic:
simpa only [ae_dirac_eq, Filter.eventually_pure]
  using Kernel.measure_zero_or_one_of_measurableSet_limsup h_le h_indep hf hns hnsp hns_univ
    ht_tail

Result:
no goals
-- Mathlib/Data/Int/GCD.lean
theorem gcd_div {i j k : ℤ} (H1 : k ∣ i) (H2 : k ∣ j) :
    gcd (i / k) (j / k) = gcd i j / natAbs k

Proof state:
i j k : ℤ
H1 : k ∣ i
H2 : k ∣ j
⊢ (i.natAbs / k.natAbs).gcd (j.natAbs / k.natAbs) = i.gcd j / k.natAbs

Tactic:
exact Nat.gcd_div (natAbs_dvd_natAbs.mpr H1) (natAbs_dvd_natAbs.mpr H2)

Result:
no goals

Proof state:
i j k : ℤ
H1 : k ∣ i
H2 : k ∣ j
⊢ (i / k).gcd (j / k) = i.gcd j / k.natAbs

Tactic:
rw [gcd, natAbs_ediv i k H1, natAbs_ediv j k H2]

Result:
i j k : ℤ
H1 : k ∣ i
H2 : k ∣ j
⊢ (i.natAbs / k.natAbs).gcd (j.natAbs / k.natAbs) = i.gcd j / k.natAbs
-- Mathlib/RingTheory/AlgebraicIndependent/Transcendental.lean
theorem isEmpty_of_isAlgebraic [Algebra.IsAlgebraic R A] : IsEmpty ι

Proof state:
case inl
ι : Type u_1
R : Type u_2
A : Type u_3
x : ι → A
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
hx : AlgebraicIndependent R x
inst✝ : Algebra.IsAlgebraic R A
h : IsEmpty ι
⊢ IsEmpty ι

Tactic:
exact h

Result:
no goals

Proof state:
case inr.intro
ι : Type u_1
R : Type u_2
A : Type u_3
x : ι → A
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
hx : AlgebraicIndependent R x
inst✝ : Algebra.IsAlgebraic R A
i : ι
⊢ IsEmpty ι

Tactic:
exact False.elim (hx.transcendental i (Algebra.IsAlgebraic.isAlgebraic _))

Result:
no goals

Proof state:
ι : Type u_1
R : Type u_2
A : Type u_3
x : ι → A
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
hx : AlgebraicIndependent R x
inst✝ : Algebra.IsAlgebraic R A
⊢ IsEmpty ι

Tactic:
rcases isEmpty_or_nonempty ι with h | ⟨⟨i⟩⟩

Result:
case inl
ι : Type u_1
R : Type u_2
A : Type u_3
x : ι → A
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
hx : AlgebraicIndependent R x
inst✝ : Algebra.IsAlgebraic R A
h : IsEmpty ι
⊢ IsEmpty ι

case inr.intro
ι : Type u_1
R : Type u_2
A : Type u_3
x : ι → A
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
hx : AlgebraicIndependent R x
inst✝ : Algebra.IsAlgebraic R A
i : ι
⊢ IsEmpty ι
-- Mathlib/Data/Seq/Seq.lean
theorem head_cons (a : α) (s) : head (cons a s) = some a

Proof state:
α : Type u
a : α
s : Seq α
⊢ (cons a s).head = some a

Tactic:
rw [head_eq_destruct, destruct_cons, Option.map_eq_map, Option.map_some']

Result:
no goals
-- Mathlib/Data/Real/EReal.lean
lemma left_distrib_of_nonneg_of_ne_top {x : EReal} (hx_nonneg : 0 ≤ x)
    (hx_ne_top : x ≠ ⊤) (y z : EReal) :
    x * (y + z) = x * y + x * z

Proof state:
x : EReal
hx_nonneg : 0 ≤ x
hx_ne_top : x ≠ ⊤
y z : EReal
⊢ x * (y + z) = x * y + x * z

Tactic:
cases hx_nonneg.eq_or_gt with
| inl hx0 => simp [hx0]
| inr hx0 =>
lift x to ℝ using ⟨hx_ne_top, hx0.ne_bot⟩
cases y <;> cases z <;>
  simp [mul_bot_of_pos hx0, mul_top_of_pos hx0, ← coe_mul];
  rw_mod_cast [mul_add]

Result:
no goals

Proof state:
case inr.intro
y z : EReal
x : ℝ
hx_nonneg : 0 ≤ ↑x
hx_ne_top : ↑x ≠ ⊤
hx0 : 0 < ↑x
⊢ ↑x * (y + z) = ↑x * y + ↑x * z

Tactic:
cases y <;> cases z <;>
  simp [mul_bot_of_pos hx0, mul_top_of_pos hx0, ← coe_mul]

Result:
case inr.intro.h_real.h_real
x : ℝ
hx_nonneg : 0 ≤ ↑x
hx_ne_top : ↑x ≠ ⊤
hx0 : 0 < ↑x
a✝¹ a✝ : ℝ
⊢ ↑x * (↑a✝¹ + ↑a✝) = ↑(x * a✝¹) + ↑(x * a✝)

Proof state:
case inl
x : EReal
hx_nonneg : 0 ≤ x
hx_ne_top : x ≠ ⊤
y z : EReal
hx0 : x = 0
⊢ x * (y + z) = x * y + x * z

Tactic:
simp [hx0]

Result:
no goals

Proof state:
case inr.intro.h_real.h_real
x : ℝ
hx_nonneg : 0 ≤ ↑x
hx_ne_top : ↑x ≠ ⊤
hx0 : 0 < ↑x
a✝¹ a✝ : ℝ
⊢ ↑x * (↑a✝¹ + ↑a✝) = ↑(x * a✝¹) + ↑(x * a✝)

Tactic:
rw_mod_cast [mul_add]

Result:
no goals

Proof state:
case inr
x : EReal
hx_nonneg : 0 ≤ x
hx_ne_top : x ≠ ⊤
y z : EReal
hx0 : 0 < x
⊢ x * (y + z) = x * y + x * z

Tactic:
lift x to ℝ using ⟨hx_ne_top, hx0.ne_bot⟩

Result:
case inr.intro
y z : EReal
x : ℝ
hx_nonneg : 0 ≤ ↑x
hx_ne_top : ↑x ≠ ⊤
hx0 : 0 < ↑x
⊢ ↑x * (y + z) = ↑x * y + ↑x * z