harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Topology/Constructions.lean
theorem Sigma.nhds_eq (x : Sigma σ) : 𝓝 x = Filter.map (Sigma.mk x.1) (𝓝 x.2)

Proof state:
ι : Type u_5
σ : ι → Type u_7
inst✝ : (i : ι) → TopologicalSpace (σ i)
x : Sigma σ
⊢ 𝓝 x = Filter.map (mk x.fst) (𝓝 x.snd)

Tactic:
cases x

Result:
case mk
ι : Type u_5
σ : ι → Type u_7
inst✝ : (i : ι) → TopologicalSpace (σ i)
fst✝ : ι
snd✝ : σ fst✝
⊢ 𝓝 ⟨fst✝, snd✝⟩ = Filter.map (mk ⟨fst✝, snd✝⟩.fst) (𝓝 ⟨fst✝, snd✝⟩.snd)

Proof state:
case mk
ι : Type u_5
σ : ι → Type u_7
inst✝ : (i : ι) → TopologicalSpace (σ i)
fst✝ : ι
snd✝ : σ fst✝
⊢ 𝓝 ⟨fst✝, snd✝⟩ = Filter.map (mk ⟨fst✝, snd✝⟩.fst) (𝓝 ⟨fst✝, snd✝⟩.snd)

Tactic:
apply Sigma.nhds_mk

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Integrals.lean
theorem integral_cpow {r : ℂ} (h : -1 < r.re ∨ r ≠ -1 ∧ (0 : ℝ) ∉ [[a, b]]) :
    (∫ x : ℝ in a..b, (x : ℂ) ^ r) = ((b : ℂ) ^ (r + 1) - (a : ℂ) ^ (r + 1)) / (r + 1)

Proof state:
case neg
a b : ℝ
r : ℂ
hr : r + 1 ≠ 0
hab : ¬0 ∉ [[a, b]]
h : -1 < r.re
⊢ ∀ (c : ℝ), ∫ (x : ℝ) in 0 ..c, ↑x ^ r = ↑c ^ (r + 1) / (r + 1) - 0 ^ (r + 1) / (r + 1)

Tactic:
intro c

Result:
case neg
a b : ℝ
r : ℂ
hr : r + 1 ≠ 0
hab : ¬0 ∉ [[a, b]]
h : -1 < r.re
c : ℝ
⊢ ∫ (x : ℝ) in 0 ..c, ↑x ^ r = ↑c ^ (r + 1) / (r + 1) - 0 ^ (r + 1) / (r + 1)

Proof state:
a b : ℝ
r : ℂ
h : -1 < r.re ∨ r ≠ -1 ∧ 0 ∉ [[a, b]]
⊢ ∫ (x : ℝ) in a..b, ↑x ^ r = (↑b ^ (r + 1) - ↑a ^ (r + 1)) / (r + 1)

Tactic:
rw [sub_div]

Result:
a b : ℝ
r : ℂ
h : -1 < r.re ∨ r ≠ -1 ∧ 0 ∉ [[a, b]]
⊢ ∫ (x : ℝ) in a..b, ↑x ^ r = ↑b ^ (r + 1) / (r + 1) - ↑a ^ (r + 1) / (r + 1)

Proof state:
case neg.hint
a b : ℝ
r : ℂ
hr : r + 1 ≠ 0
hab : ¬0 ∉ [[a, b]]
h : -1 < r.re
c : ℝ
⊢ IntervalIntegrable (fun y => ↑y ^ r) MeasureTheory.volume 0 c

Tactic:
exact intervalIntegrable_cpow' h

Result:
no goals

Proof state:
case neg
a b : ℝ
r : ℂ
hr : r + 1 ≠ 0
hab : ¬0 ∉ [[a, b]]
h : -1 < r.re
c : ℝ
⊢ ∫ (x : ℝ) in 0 ..c, ↑x ^ r = ↑c ^ (r + 1) / (r + 1) - 0 ^ (r + 1) / (r + 1)

Tactic:
apply integral_eq_sub_of_hasDeriv_right

Result:
case neg.hcont
a b : ℝ
r : ℂ
hr : r + 1 ≠ 0
hab : ¬0 ∉ [[a, b]]
h : -1 < r.re
c : ℝ
⊢ ContinuousOn (fun c => ↑c ^ (r + 1) / (r + 1)) [[0, c]]

case neg.hderiv
a b : ℝ
r : ℂ
hr : r + 1 ≠ 0
hab : ¬0 ∉ [[a, b]]
h : -1 < r.re
c : ℝ
⊢ ∀ x ∈ Set.Ioo (0 ⊓ c) (0 ⊔ c), HasDerivWithinAt (fun c => ↑c ^ (r + 1) / (r + 1)) (↑x ^ r) (Set.Ioi x) x

case neg.hint
a b : ℝ
r : ℂ
hr : r + 1 ≠ 0
hab : ¬0 ∉ [[a, b]]
h : -1 < r.re
c : ℝ
⊢ IntervalIntegrable (fun y => ↑y ^ r) MeasureTheory.volume 0 c

Proof state:
case neg.hcont
a b : ℝ
r : ℂ
hr : r + 1 ≠ 0
hab : ¬0 ∉ [[a, b]]
h : -1 < r.re
c : ℝ
⊢ ContinuousOn (fun c => ↑c ^ (r + 1) / (r + 1)) [[0, c]]

Tactic:
refine ((Complex.continuous_ofReal_cpow_const ?_).div_const _).continuousOn

Result:
case neg.hcont
a b : ℝ
r : ℂ
hr : r + 1 ≠ 0
hab : ¬0 ∉ [[a, b]]
h : -1 < r.re
c : ℝ
⊢ 0 < (r + 1).re

Proof state:
case neg.hderiv.refine_1.inl
a b : ℝ
r : ℂ
hr : r + 1 ≠ 0
hab : ¬0 ∉ [[a, b]]
h : -1 < r.re
c x : ℝ
hx : x ∈ Set.Ioo (0 ⊓ c) 0
hc : c ≤ 0
⊢ x ≠ 0

Tactic:
exact hx.2.ne

Result:
no goals

Proof state:
a b : ℝ
r : ℂ
h : -1 < r.re ∨ r ≠ -1 ∧ 0 ∉ [[a, b]]
hr : r + 1 ≠ 0
hab : 0 ∉ [[a, b]]
x : ℝ
hx : x ∈ [[a, b]]
⊢ HasDerivAt (fun {b} => ↑b ^ (r + 1) / (r + 1)) (↑x ^ r) x

Tactic:
refine hasDerivAt_ofReal_cpow_const' (ne_of_mem_of_not_mem hx hab) ?_

Result:
a b : ℝ
r : ℂ
h : -1 < r.re ∨ r ≠ -1 ∧ 0 ∉ [[a, b]]
hr : r + 1 ≠ 0
hab : 0 ∉ [[a, b]]
x : ℝ
hx : x ∈ [[a, b]]
⊢ r ≠ -1

Proof state:
a b : ℝ
r : ℂ
h : -1 < r.re ∨ r ≠ -1 ∧ 0 ∉ [[a, b]]
⊢ r + 1 ≠ 0

Tactic:
rcases h with h | h

Result:
case inl
a b : ℝ
r : ℂ
h : -1 < r.re
⊢ r + 1 ≠ 0

case inr
a b : ℝ
r : ℂ
h : r ≠ -1 ∧ 0 ∉ [[a, b]]
⊢ r + 1 ≠ 0
-- Mathlib/Combinatorics/SimpleGraph/Walk.lean
theorem append_nil {u v : V} (p : G.Walk u v) : p.append nil = p

Proof state:
case nil
V : Type u
G : SimpleGraph V
u v u✝ : V
⊢ nil.append nil = nil

Tactic:
rw [nil_append]

Result:
no goals

Proof state:
case cons
V : Type u
G : SimpleGraph V
u v u✝ v✝ w✝ : V
h✝ : G.Adj u✝ v✝
p✝ : G.Walk v✝ w✝
ih : p✝.append nil = p✝
⊢ (cons h✝ p✝).append nil = cons h✝ p✝

Tactic:
rw [cons_append, ih]

Result:
no goals

Proof state:
V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
⊢ p.append nil = p

Tactic:
induction p with
| nil => rw [nil_append]
| cons _ _ ih => rw [cons_append, ih]

Result:
no goals
-- Mathlib/Topology/Algebra/Module/Basic.lean
theorem Submodule.isClosed_or_dense_of_isCoatom (s : Submodule R M) (hs : IsCoatom s) :
    IsClosed (s : Set M) ∨ Dense (s : Set M)

Proof state:
R : Type u
M : Type v
inst✝⁵ : Semiring R
inst✝⁴ : TopologicalSpace M
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : ContinuousConstSMul R M
inst✝ : ContinuousAdd M
s : Submodule R M
hs : IsCoatom s
⊢ s.topologicalClosure = s → IsClosed ↑s

Tactic:
exact fun h ↦ h ▸ isClosed_closure

Result:
no goals

Proof state:
R : Type u
M : Type v
inst✝⁵ : Semiring R
inst✝⁴ : TopologicalSpace M
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : ContinuousConstSMul R M
inst✝ : ContinuousAdd M
s : Submodule R M
hs : IsCoatom s
⊢ IsClosed ↑s ∨ Dense ↑s

Tactic:
refine (hs.le_iff.mp s.le_topologicalClosure).symm.imp ?_ dense_iff_topologicalClosure_eq_top.mpr

Result:
R : Type u
M : Type v
inst✝⁵ : Semiring R
inst✝⁴ : TopologicalSpace M
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : ContinuousConstSMul R M
inst✝ : ContinuousAdd M
s : Submodule R M
hs : IsCoatom s
⊢ s.topologicalClosure = s → IsClosed ↑s
-- Mathlib/InformationTheory/KullbackLeibler/Basic.lean
lemma klDiv_eq_top_iff : klDiv μ ν = ∞ ↔ μ ≪ ν → ¬ Integrable (llr μ ν) μ

Proof state:
case mp
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
h : μ ≪ ν ∧ Integrable (llr μ ν) μ
⊢ klDiv μ ν ≠ ⊤

Tactic:
simp [klDiv_of_ac_of_integrable h.1 h.2]

Result:
no goals

Proof state:
case mpr
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
h : μ ≪ ν → ¬Integrable (llr μ ν) μ
⊢ klDiv μ ν = ⊤

Tactic:
rcases or_not_of_imp h with (h | h) <;> simp [h]

Result:
no goals

Proof state:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
⊢ klDiv μ ν = ⊤ ↔ μ ≪ ν → ¬Integrable (llr μ ν) μ

Tactic:
constructor <;> intro h

Result:
case mp
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
h : klDiv μ ν = ⊤
⊢ μ ≪ ν → ¬Integrable (llr μ ν) μ

case mpr
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
h : μ ≪ ν → ¬Integrable (llr μ ν) μ
⊢ klDiv μ ν = ⊤

Proof state:
case mp
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
h : klDiv μ ν = ⊤
⊢ μ ≪ ν → ¬Integrable (llr μ ν) μ

Tactic:
contrapose! h

Result:
case mp
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
h : μ ≪ ν ∧ Integrable (llr μ ν) μ
⊢ klDiv μ ν ≠ ⊤
-- Mathlib/Geometry/RingedSpace/PresheafedSpace/Gluing.lean
theorem snd_invApp_t_app' (i j k : D.J) (U : Opens (pullback (D.f i j) (D.f i k)).carrier) :
    ∃ eq,
      (π₂⁻¹ i, j, k) U ≫ (D.t k i).c.app _ ≫ (D.V (k, i)).presheaf.map (eqToHom eq) =
        (D.t' k i j).c.app _ ≫ (π₁⁻¹ k, j, i) (unop _)

Proof state:
case w.e_unop.e_carrier
C : Type u
inst✝ : Category.{v, u} C
D : GlueData C
i j k : D.J
U : Opens ↑↑(pullback (D.f i j) (D.f i k))
this : pullback.fst (D.f k i) (D.f k j) ≫ D.t k i = D.t' k i j ≫ pullback.snd (D.f i j) (D.f i k)
⊢ ⇑(ConcreteCategory.hom (D.t k i).base) ⁻¹' (⇑(ConcreteCategory.hom (pullback.snd (D.f i j) (D.f i k)).base) '' ↑U) =
    ⇑(ConcreteCategory.hom (pullback.fst (D.f k i) (D.f k j)).base) ''
      (⇑(ConcreteCategory.hom (D.t' k i j).base) ⁻¹' ↑U)

Tactic:
rw [← IsIso.inv_comp_eq] at this

Result:
case w.e_unop.e_carrier
C : Type u
inst✝ : Category.{v, u} C
D : GlueData C
i j k : D.J
U : Opens ↑↑(pullback (D.f i j) (D.f i k))
this : inv (D.t' k i j) ≫ pullback.fst (D.f k i) (D.f k j) ≫ D.t k i = pullback.snd (D.f i j) (D.f i k)
⊢ ⇑(ConcreteCategory.hom (D.t k i).base) ⁻¹' (⇑(ConcreteCategory.hom (pullback.snd (D.f i j) (D.f i k)).base) '' ↑U) =
    ⇑(ConcreteCategory.hom (pullback.fst (D.f k i) (D.f k j)).base) ''
      (⇑(ConcreteCategory.hom (D.t' k i j).base) ⁻¹' ↑U)

Proof state:
case h
C : Type u
inst✝ : Category.{v, u} C
D : GlueData C
i j k : D.J
U : Opens ↑↑(pullback (D.f i j) (D.f i k))
y : ↑↑(pullback (D.f i j) (D.f i k))
⊢ (ConcreteCategory.hom (inv (D.t' k i j) ≫ pullback.fst (D.f k i) (D.f k j)).base) y =
    (ConcreteCategory.hom (pullback.snd (D.f i j) (D.f i k) ≫ D.t i k).base) y

Tactic:
congr 3

Result:
case h.e_a.e_a.e_self
C : Type u
inst✝ : Category.{v, u} C
D : GlueData C
i j k : D.J
U : Opens ↑↑(pullback (D.f i j) (D.f i k))
y : ↑↑(pullback (D.f i j) (D.f i k))
⊢ inv (D.t' k i j) ≫ pullback.fst (D.f k i) (D.f k j) = pullback.snd (D.f i j) (D.f i k) ≫ D.t i k
-- Mathlib/Data/Finset/Lattice/Fold.lean
theorem sup'_const (a : α) : s.sup' H (fun _ => a) = a

Proof state:
α : Type u_2
β : Type u_3
inst✝ : SemilatticeSup α
s : Finset β
H : s.Nonempty
a : α
⊢ (s.sup' H fun x => a) = a

Tactic:
apply le_antisymm

Result:
case a
α : Type u_2
β : Type u_3
inst✝ : SemilatticeSup α
s : Finset β
H : s.Nonempty
a : α
⊢ (s.sup' H fun x => a) ≤ a

case a
α : Type u_2
β : Type u_3
inst✝ : SemilatticeSup α
s : Finset β
H : s.Nonempty
a : α
⊢ a ≤ s.sup' H fun x => a

Proof state:
case a.a
α : Type u_2
β : Type u_3
inst✝ : SemilatticeSup α
s : Finset β
H : s.Nonempty
a : α
b✝ : β
a✝ : b✝ ∈ s
⊢ a ≤ a

Tactic:
exact le_rfl

Result:
no goals

Proof state:
case a
α : Type u_2
β : Type u_3
inst✝ : SemilatticeSup α
s : Finset β
H : s.Nonempty
a : α
⊢ (s.sup' H fun x => a) ≤ a

Tactic:
apply sup'_le

Result:
case a.a
α : Type u_2
β : Type u_3
inst✝ : SemilatticeSup α
s : Finset β
H : s.Nonempty
a : α
⊢ ∀ b ∈ s, a ≤ a

Proof state:
case a.a
α : Type u_2
β : Type u_3
inst✝ : SemilatticeSup α
s : Finset β
H : s.Nonempty
a : α
⊢ ∀ b ∈ s, a ≤ a

Tactic:
intros

Result:
case a.a
α : Type u_2
β : Type u_3
inst✝ : SemilatticeSup α
s : Finset β
H : s.Nonempty
a : α
b✝ : β
a✝ : b✝ ∈ s
⊢ a ≤ a

Proof state:
case a
α : Type u_2
β : Type u_3
inst✝ : SemilatticeSup α
s : Finset β
H : s.Nonempty
a : α
⊢ a ≤ s.sup' H fun x => a

Tactic:
apply le_sup' (fun _ => a) H.choose_spec

Result:
no goals
-- Mathlib/ModelTheory/FinitelyGenerated.lean
theorem Substructure.fg_iff_structure_fg (S : L.Substructure M) : S.FG ↔ Structure.FG L S

Proof state:
case refine_1
L : Language
M : Type u_1
inst✝ : L.Structure M
S : L.Substructure M
h : S.FG
⊢ (map S.subtype.toHom ⊤).FG

Tactic:
rw [← Hom.range_eq_map, range_subtype]

Result:
case refine_1
L : Language
M : Type u_1
inst✝ : L.Structure M
S : L.Substructure M
h : S.FG
⊢ S.FG

Proof state:
case refine_2
L : Language
M : Type u_1
inst✝ : L.Structure M
S : L.Substructure M
h✝ : ⊤.FG
h : S.FG
⊢ S.FG

Tactic:
exact h

Result:
no goals

Proof state:
L : Language
M : Type u_1
inst✝ : L.Structure M
S : L.Substructure M
⊢ S.FG ↔ Structure.FG L ↥S

Tactic:
rw [Structure.fg_def]

Result:
L : Language
M : Type u_1
inst✝ : L.Structure M
S : L.Substructure M
⊢ S.FG ↔ ⊤.FG

Proof state:
case refine_1
L : Language
M : Type u_1
inst✝ : L.Structure M
S : L.Substructure M
h : S.FG
⊢ S.FG

Tactic:
exact h

Result:
no goals

Proof state:
L : Language
M : Type u_1
inst✝ : L.Structure M
S : L.Substructure M
⊢ S.FG ↔ ⊤.FG

Tactic:
refine ⟨fun h => FG.of_map_embedding S.subtype ?_, fun h => ?_⟩

Result:
case refine_1
L : Language
M : Type u_1
inst✝ : L.Structure M
S : L.Substructure M
h : S.FG
⊢ (map S.subtype.toHom ⊤).FG

case refine_2
L : Language
M : Type u_1
inst✝ : L.Structure M
S : L.Substructure M
h : ⊤.FG
⊢ S.FG

Proof state:
case refine_2
L : Language
M : Type u_1
inst✝ : L.Structure M
S : L.Substructure M
h✝ : ⊤.FG
h : (map S.subtype.toHom ⊤).FG
⊢ S.FG

Tactic:
rw [← Hom.range_eq_map, range_subtype] at h

Result:
case refine_2
L : Language
M : Type u_1
inst✝ : L.Structure M
S : L.Substructure M
h✝ : ⊤.FG
h : S.FG
⊢ S.FG

Proof state:
case refine_2
L : Language
M : Type u_1
inst✝ : L.Structure M
S : L.Substructure M
h : ⊤.FG
⊢ S.FG

Tactic:
have h := h.map S.subtype.toHom

Result:
case refine_2
L : Language
M : Type u_1
inst✝ : L.Structure M
S : L.Substructure M
h✝ : ⊤.FG
h : (map S.subtype.toHom ⊤).FG
⊢ S.FG
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Monadic.lean
theorem mapM'_eq_mapM [Monad m] [LawfulMonad m] (f : α → m β) (l : List α) :
    mapM' f l = mapM f l

Proof state:
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : α → m β
l : List α
⊢ mapM' f l = mapM f l

Tactic:
simp [go, mapM]

Result:
no goals

Proof state:
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : α → m β
l : List α
acc : List β
⊢ mapM.loop f [] acc = do
    let __do_lift ← mapM' f []
    pure (acc.reverse ++ __do_lift)

Tactic:
simp [mapM.loop, mapM']

Result:
no goals

Proof state:
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : α → m β
l✝ : List α
a : α
l : List α
acc : List β
⊢ mapM.loop f (a :: l) acc = do
    let __do_lift ← mapM' f (a :: l)
    pure (acc.reverse ++ __do_lift)

Tactic:
simp [go l, mapM.loop, mapM']

Result:
no goals
-- Mathlib/GroupTheory/GroupAction/Hom.lean
theorem comp_inverse' {f : X →ₑ[φ] Y} {g : Y → X}
    {k₁ : Function.LeftInverse φ' φ} {k₂ : Function.RightInverse φ' φ}
    {h₁ : Function.LeftInverse g f} {h₂ : Function.RightInverse g f} :
    (inverse' f g k₂ h₁ h₂).comp f (κ := CompTriple.comp_inv k₁)
      = MulActionHom.id M

Proof state:
M : Type u_2
N : Type u_3
φ : M → N
X : Type u_5
inst✝¹ : SMul M X
Y : Type u_6
inst✝ : SMul N Y
φ' : N → M
f : X →ₑ[φ] Y
g : Y → X
k₁ : Function.LeftInverse φ' φ
k₂ : Function.RightInverse φ' φ
h₁ : Function.LeftInverse g ⇑f
h₂ : Function.RightInverse g ⇑f
⊢ ∀ (x : X), ((f.inverse' g k₂ h₁ h₂).comp f) x = (MulActionHom.id M) x

Tactic:
intro x

Result:
M : Type u_2
N : Type u_3
φ : M → N
X : Type u_5
inst✝¹ : SMul M X
Y : Type u_6
inst✝ : SMul N Y
φ' : N → M
f : X →ₑ[φ] Y
g : Y → X
k₁ : Function.LeftInverse φ' φ
k₂ : Function.RightInverse φ' φ
h₁ : Function.LeftInverse g ⇑f
h₂ : Function.RightInverse g ⇑f
x : X
⊢ ((f.inverse' g k₂ h₁ h₂).comp f) x = (MulActionHom.id M) x

Proof state:
M : Type u_2
N : Type u_3
φ : M → N
X : Type u_5
inst✝¹ : SMul M X
Y : Type u_6
inst✝ : SMul N Y
φ' : N → M
f : X →ₑ[φ] Y
g : Y → X
k₁ : Function.LeftInverse φ' φ
k₂ : Function.RightInverse φ' φ
h₁ : Function.LeftInverse g ⇑f
h₂ : Function.RightInverse g ⇑f
x : X
⊢ (f.inverse' g k₂ h₁ h₂) (f x) = x

Tactic:
exact h₁ x

Result:
no goals

Proof state:
M : Type u_2
N : Type u_3
φ : M → N
X : Type u_5
inst✝¹ : SMul M X
Y : Type u_6
inst✝ : SMul N Y
φ' : N → M
f : X →ₑ[φ] Y
g : Y → X
k₁ : Function.LeftInverse φ' φ
k₂ : Function.RightInverse φ' φ
h₁ : Function.LeftInverse g ⇑f
h₂ : Function.RightInverse g ⇑f
⊢ (f.inverse' g k₂ h₁ h₂).comp f = MulActionHom.id M

Tactic:
rw [MulActionHom.ext_iff]

Result:
M : Type u_2
N : Type u_3
φ : M → N
X : Type u_5
inst✝¹ : SMul M X
Y : Type u_6
inst✝ : SMul N Y
φ' : N → M
f : X →ₑ[φ] Y
g : Y → X
k₁ : Function.LeftInverse φ' φ
k₂ : Function.RightInverse φ' φ
h₁ : Function.LeftInverse g ⇑f
h₂ : Function.RightInverse g ⇑f
⊢ ∀ (x : X), ((f.inverse' g k₂ h₁ h₂).comp f) x = (MulActionHom.id M) x

Proof state:
M : Type u_2
N : Type u_3
φ : M → N
X : Type u_5
inst✝¹ : SMul M X
Y : Type u_6
inst✝ : SMul N Y
φ' : N → M
f : X →ₑ[φ] Y
g : Y → X
k₁ : Function.LeftInverse φ' φ
k₂ : Function.RightInverse φ' φ
h₁ : Function.LeftInverse g ⇑f
h₂ : Function.RightInverse g ⇑f
x : X
⊢ ((f.inverse' g k₂ h₁ h₂).comp f) x = (MulActionHom.id M) x

Tactic:
simp only [comp_apply, inverse_apply, id_apply]

Result:
M : Type u_2
N : Type u_3
φ : M → N
X : Type u_5
inst✝¹ : SMul M X
Y : Type u_6
inst✝ : SMul N Y
φ' : N → M
f : X →ₑ[φ] Y
g : Y → X
k₁ : Function.LeftInverse φ' φ
k₂ : Function.RightInverse φ' φ
h₁ : Function.LeftInverse g ⇑f
h₂ : Function.RightInverse g ⇑f
x : X
⊢ (f.inverse' g k₂ h₁ h₂) (f x) = x
-- Mathlib/Algebra/Order/Floor.lean
theorem lt_floor_iff : z < ⌊a⌋ ↔ z + 1 ≤ a

Proof state:
α : Type u_2
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
z : ℤ
a : α
⊢ ↑(z + 1) ≤ a ↔ ↑z + 1 ≤ a

Tactic:
norm_cast

Result:
no goals

Proof state:
α : Type u_2
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
z : ℤ
a : α
⊢ z < ⌊a⌋ ↔ ↑z + 1 ≤ a

Tactic:
rw [← add_one_le_iff, le_floor]

Result:
α : Type u_2
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
z : ℤ
a : α
⊢ ↑(z + 1) ≤ a ↔ ↑z + 1 ≤ a
-- Mathlib/Combinatorics/Hindman.lean
theorem exists_FP_of_large {M} [Semigroup M] (U : Ultrafilter M) (U_idem : U * U = U) (s₀ : Set M)
    (sU : s₀ ∈ U) : ∃ a, FP a ⊆ s₀

Proof state:
case h
M : Type u_1
inst✝ : Semigroup M
U : Ultrafilter M
U_idem : U * U = U
s₀ : Set M
sU : s₀ ∈ U
exists_elem : ∀ {s : Set M}, s ∈ U → (s ∩ {m | ∀ᶠ (m' : M) in ↑U, m * m' ∈ s}).Nonempty
elem : { s // s ∈ U } → M := fun p => ⋯.some
succ : { s // s ∈ U } → { s // s ∈ U } := fun p => ⟨↑p ∩ {m | elem p * m ∈ ↑p}, ⋯⟩
⊢ ∀ (a : Stream' M), ∀ m ∈ FP a, ∀ (p : { s // s ∈ U }), a = Stream'.corec elem succ p → m ∈ ↑p

Tactic:
clear sU s₀

Result:
case h
M : Type u_1
inst✝ : Semigroup M
U : Ultrafilter M
U_idem : U * U = U
exists_elem : ∀ {s : Set M}, s ∈ U → (s ∩ {m | ∀ᶠ (m' : M) in ↑U, m * m' ∈ s}).Nonempty
elem : { s // s ∈ U } → M := fun p => ⋯.some
succ : { s // s ∈ U } → { s // s ∈ U } := fun p => ⟨↑p ∩ {m | elem p * m ∈ ↑p}, ⋯⟩
⊢ ∀ (a : Stream' M), ∀ m ∈ FP a, ∀ (p : { s // s ∈ U }), a = Stream'.corec elem succ p → m ∈ ↑p

Proof state:
M : Type u_1
inst✝ : Semigroup M
U : Ultrafilter M
U_idem : U * U = U
s₀ : Set M
sU : s₀ ∈ U
exists_elem : ∀ {s : Set M}, s ∈ U → (s ∩ {m | ∀ᶠ (m' : M) in ↑U, m * m' ∈ s}).Nonempty
⊢ ∃ a, FP a ⊆ s₀

Tactic:
let elem : { s // s ∈ U } → M := fun p => (exists_elem p.property).some

Result:
M : Type u_1
inst✝ : Semigroup M
U : Ultrafilter M
U_idem : U * U = U
s₀ : Set M
sU : s₀ ∈ U
exists_elem : ∀ {s : Set M}, s ∈ U → (s ∩ {m | ∀ᶠ (m' : M) in ↑U, m * m' ∈ s}).Nonempty
elem : { s // s ∈ U } → M := fun p => ⋯.some
⊢ ∃ a, FP a ⊆ s₀
-- Mathlib/RingTheory/Jacobson/Radical.lean
theorem map_jacobson_of_ker_le (surj : Function.Surjective f)
    (le : LinearMap.ker f ≤ jacobson R M) :
    map f (jacobson R M) = jacobson R₂ M₂ :=
  le_antisymm (map_jacobson_le f) <| by
    rw [jacobson, sInf_eq_iInf'] at le
    conv_rhs => rw [jacobson, sInf_eq_iInf', map_iInf_of_ker_le surj le]
    exact le_iInf fun m ↦ sInf_le (isCoatom_map_of_ker_le surj (le_iInf_iff.mp le m) m.2)

Proof state:
R : Type u_1
R₂ : Type u_2
M : Type u_3
M₂ : Type u_4
inst✝⁸ : Ring R
inst✝⁷ : Ring R₂
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module R M
inst✝⁴ : AddCommGroup M₂
inst✝³ : Module R₂ M₂
τ₁₂ : R →+* R₂
inst✝² : RingHomSurjective τ₁₂
F : Type u_5
inst✝¹ : FunLike F M M₂
inst✝ : SemilinearMapClass F τ₁₂ M M₂
f : F
surj : Function.Surjective ⇑f
le : LinearMap.ker f ≤ ⨅ a, ↑a
⊢ jacobson R₂ M₂ ≤ map f (jacobson R M)

Tactic:
conv_rhs => rw [jacobson, sInf_eq_iInf', map_iInf_of_ker_le surj le]

Result:
R : Type u_1
R₂ : Type u_2
M : Type u_3
M₂ : Type u_4
inst✝⁸ : Ring R
inst✝⁷ : Ring R₂
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module R M
inst✝⁴ : AddCommGroup M₂
inst✝³ : Module R₂ M₂
τ₁₂ : R →+* R₂
inst✝² : RingHomSurjective τ₁₂
F : Type u_5
inst✝¹ : FunLike F M M₂
inst✝ : SemilinearMapClass F τ₁₂ M M₂
f : F
surj : Function.Surjective ⇑f
le : LinearMap.ker f ≤ ⨅ a, ↑a
⊢ jacobson R₂ M₂ ≤ ⨅ i, map f ↑i

Proof state:
R : Type u_1
R₂ : Type u_2
M : Type u_3
M₂ : Type u_4
inst✝⁸ : Ring R
inst✝⁷ : Ring R₂
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module R M
inst✝⁴ : AddCommGroup M₂
inst✝³ : Module R₂ M₂
τ₁₂ : R →+* R₂
inst✝² : RingHomSurjective τ₁₂
F : Type u_5
inst✝¹ : FunLike F M M₂
inst✝ : SemilinearMapClass F τ₁₂ M M₂
f : F
surj : Function.Surjective ⇑f
le : LinearMap.ker f ≤ jacobson R M
⊢ jacobson R₂ M₂ ≤ map f (jacobson R M)

Tactic:
rw [jacobson, sInf_eq_iInf'] at le

Result:
R : Type u_1
R₂ : Type u_2
M : Type u_3
M₂ : Type u_4
inst✝⁸ : Ring R
inst✝⁷ : Ring R₂
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module R M
inst✝⁴ : AddCommGroup M₂
inst✝³ : Module R₂ M₂
τ₁₂ : R →+* R₂
inst✝² : RingHomSurjective τ₁₂
F : Type u_5
inst✝¹ : FunLike F M M₂
inst✝ : SemilinearMapClass F τ₁₂ M M₂
f : F
surj : Function.Surjective ⇑f
le : LinearMap.ker f ≤ ⨅ a, ↑a
⊢ jacobson R₂ M₂ ≤ map f (jacobson R M)

Proof state:
R : Type u_1
R₂ : Type u_2
M : Type u_3
M₂ : Type u_4
inst✝⁸ : Ring R
inst✝⁷ : Ring R₂
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module R M
inst✝⁴ : AddCommGroup M₂
inst✝³ : Module R₂ M₂
τ₁₂ : R →+* R₂
inst✝² : RingHomSurjective τ₁₂
F : Type u_5
inst✝¹ : FunLike F M M₂
inst✝ : SemilinearMapClass F τ₁₂ M M₂
f : F
surj : Function.Surjective ⇑f
le : LinearMap.ker f ≤ ⨅ a, ↑a
⊢ jacobson R₂ M₂ ≤ ⨅ i, map f ↑i

Tactic:
exact le_iInf fun m ↦ sInf_le (isCoatom_map_of_ker_le surj (le_iInf_iff.mp le m) m.2)

Result:
no goals
-- Mathlib/Algebra/Order/Ring/Abs.lean
lemma abs_eq_iff_mul_self_eq : |a| = |b| ↔ a * a = b * b

Proof state:
α : Type u_1
inst✝ : LinearOrderedRing α
a b : α
⊢ |a| = |b| ↔ a * a = b * b

Tactic:
rw [← abs_mul_abs_self, ← abs_mul_abs_self b]

Result:
α : Type u_1
inst✝ : LinearOrderedRing α
a b : α
⊢ |a| = |b| ↔ |a| * |a| = |b| * |b|

Proof state:
α : Type u_1
inst✝ : LinearOrderedRing α
a b : α
⊢ |a| = |b| ↔ |a| * |a| = |b| * |b|

Tactic:
exact (mul_self_inj (abs_nonneg a) (abs_nonneg b)).symm

Result:
no goals
-- Mathlib/GroupTheory/Perm/Cycle/Factors.lean
theorem mem_cycleFactorsFinset_support_le {p f : Perm α} (h : p ∈ cycleFactorsFinset f) :
    p.support ≤ f.support

Proof state:
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
p f : Perm α
h : p.IsCycle ∧ ∀ a ∈ p.support, p a = f a
⊢ p.support ≤ f.support

Tactic:
intro x hx

Result:
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
p f : Perm α
h : p.IsCycle ∧ ∀ a ∈ p.support, p a = f a
x : α
hx : x ∈ p.support
⊢ x ∈ f.support

Proof state:
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
p f : Perm α
h : p ∈ f.cycleFactorsFinset
⊢ p.support ≤ f.support

Tactic:
rw [mem_cycleFactorsFinset_iff] at h

Result:
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
p f : Perm α
h : p.IsCycle ∧ ∀ a ∈ p.support, p a = f a
⊢ p.support ≤ f.support

Proof state:
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
p f : Perm α
h : p.IsCycle ∧ ∀ a ∈ p.support, p a = f a
x : α
hx : x ∈ p.support
⊢ x ∈ f.support

Tactic:
rwa [mem_support, ← h.right x hx, ← mem_support]

Result:
no goals
-- Mathlib/Algebra/Homology/HomotopyCategory/MappingCone.lean
@[simp]
lemma inr_descCochain :
    (Cochain.ofHom (inr φ)).comp (descCochain φ α β h) (zero_add n) = β

Proof state:
C : Type u_1
inst✝² : Category.{u_3, u_1} C
inst✝¹ : Preadditive C
F G : CochainComplex C ℤ
φ : F ⟶ G
inst✝ : HasHomotopyCofiber φ
K : CochainComplex C ℤ
n m : ℤ
α : Cochain F K m
β : Cochain G K n
h : m + 1 = n
⊢ (Cochain.ofHom (inr φ)).comp (descCochain φ α β h) ⋯ = β

Tactic:
simp [descCochain]

Result:
no goals