harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Topology/Semicontinuous.lean
theorem lowerSemicontinuous_iff_isClosed_preimage {f : α → γ} :
    LowerSemicontinuous f ↔ ∀ y, IsClosed (f ⁻¹' Iic y)

Proof state:
α : Type u_1
inst✝¹ : TopologicalSpace α
γ : Type u_3
inst✝ : LinearOrder γ
f : α → γ
⊢ (∀ (y : γ), IsOpen (f ⁻¹' Ioi y)) ↔ ∀ (y : γ), IsClosed (f ⁻¹' Iic y)

Tactic:
simp only [← isOpen_compl_iff, ← preimage_compl, compl_Iic]

Result:
no goals

Proof state:
α : Type u_1
inst✝¹ : TopologicalSpace α
γ : Type u_3
inst✝ : LinearOrder γ
f : α → γ
⊢ LowerSemicontinuous f ↔ ∀ (y : γ), IsClosed (f ⁻¹' Iic y)

Tactic:
rw [lowerSemicontinuous_iff_isOpen_preimage]

Result:
α : Type u_1
inst✝¹ : TopologicalSpace α
γ : Type u_3
inst✝ : LinearOrder γ
f : α → γ
⊢ (∀ (y : γ), IsOpen (f ⁻¹' Ioi y)) ↔ ∀ (y : γ), IsClosed (f ⁻¹' Iic y)
-- Mathlib/RingTheory/HahnSeries/Addition.lean
theorem min_le_min_add {Γ} [LinearOrder Γ] {x y : HahnSeries Γ R} (hx : x ≠ 0)
    (hy : y ≠ 0) (hxy : x + y ≠ 0) :
    min (Set.IsWF.min x.isWF_support (support_nonempty_iff.2 hx))
      (Set.IsWF.min y.isWF_support (support_nonempty_iff.2 hy)) ≤
      Set.IsWF.min (x + y).isWF_support (support_nonempty_iff.2 hxy)

Proof state:
R : Type u_3
inst✝¹ : AddMonoid R
Γ : Type u_8
inst✝ : LinearOrder Γ
x y : HahnSeries Γ R
hx : x ≠ 0
hy : y ≠ 0
hxy : x + y ≠ 0
⊢ ⋯.min ⋯ ⊓ ⋯.min ⋯ ≤ ⋯.min ⋯

Tactic:
rw [← Set.IsWF.min_union]

Result:
R : Type u_3
inst✝¹ : AddMonoid R
Γ : Type u_8
inst✝ : LinearOrder Γ
x y : HahnSeries Γ R
hx : x ≠ 0
hy : y ≠ 0
hxy : x + y ≠ 0
⊢ ⋯.min ⋯ ≤ ⋯.min ⋯

Proof state:
R : Type u_3
inst✝¹ : AddMonoid R
Γ : Type u_8
inst✝ : LinearOrder Γ
x y : HahnSeries Γ R
hx : x ≠ 0
hy : y ≠ 0
hxy : x + y ≠ 0
⊢ ⋯.min ⋯ ≤ ⋯.min ⋯

Tactic:
exact Set.IsWF.min_le_min_of_subset (support_add_subset (x := x) (y := y))

Result:
no goals
-- Mathlib/SetTheory/Game/PGame.lean
theorem identical_of_eq {x y : PGame} (h : x = y) : x ≡ y

Proof state:
x : PGame
⊢ x ≡ x

Tactic:
rfl

Result:
no goals

Proof state:
x y : PGame
h : x = y
⊢ x ≡ y

Tactic:
subst h

Result:
x : PGame
⊢ x ≡ x
-- Mathlib/Data/NNRat/Defs.lean
theorem le_toNNRat_iff_coe_le' {q : ℚ≥0} (hq : 0 < q) : q ≤ toNNRat p ↔ ↑q ≤ p :=
  (le_or_lt 0 p).elim le_toNNRat_iff_coe_le fun hp ↦ by
    simp only [(hp.trans_le q.coe_nonneg).not_le, toNNRat_eq_zero.2 hp.le, hq.not_le]

Proof state:
p : ℚ
q : ℚ≥0
hq : 0 < q
hp : p < 0
⊢ q ≤ p.toNNRat ↔ ↑q ≤ p

Tactic:
simp only [(hp.trans_le q.coe_nonneg).not_le, toNNRat_eq_zero.2 hp.le, hq.not_le]

Result:
no goals
-- Mathlib/GroupTheory/MonoidLocalization/Basic.lean
theorem mk'_spec' (x) (y : S) : f.toMap y * f.mk' x y = f.toMap x

Proof state:
M : Type u_1
inst✝¹ : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝ : CommMonoid N
f : S.LocalizationMap N
x : M
y : ↥S
⊢ f.toMap ↑y * f.mk' x y = f.toMap x

Tactic:
rw [mul_comm, mk'_spec]

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Subgraph.lean
@[mono]
lemma deleteVerts_mono' {G' : SimpleGraph V} (u : Set V) (h : G ≤ G') :
    ((⊤ : Subgraph G).deleteVerts u).coe ≤ ((⊤ : Subgraph G').deleteVerts u).coe

Proof state:
V : Type u
G G' : SimpleGraph V
u : Set V
h : G ≤ G'
⊢ (⊤.deleteVerts u).coe ≤ (⊤.deleteVerts u).coe

Tactic:
intro v w hvw

Result:
V : Type u
G G' : SimpleGraph V
u : Set V
h : G ≤ G'
v w : ↑(⊤.deleteVerts u).verts
hvw : (⊤.deleteVerts u).coe.Adj v w
⊢ (⊤.deleteVerts u).coe.Adj v w

Proof state:
V : Type u
G G' : SimpleGraph V
u : Set V
h : G ≤ G'
v w : ↑(⊤.deleteVerts u).verts
hvw : (⊤.deleteVerts u).coe.Adj v w
⊢ (⊤.deleteVerts u).coe.Adj v w

Tactic:
aesop

Result:
no goals
-- Mathlib/Analysis/BoxIntegral/Partition/Basic.lean
theorem iUnion_single (h : J ≤ I) : (single I J h).iUnion = J

Proof state:
ι : Type u_1
I J : Box ι
h : J ≤ I
⊢ (single I J h).iUnion = ↑J

Tactic:
simp [iUnion_def]

Result:
no goals
-- Mathlib/FieldTheory/Minpoly/IsIntegrallyClosed.lean
theorem prime_of_isIntegrallyClosed {x : S} (hx : IsIntegral R x) : Prime (minpoly R x)

Proof state:
R : Type u_1
S : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : IsDomain R
inst✝³ : Algebra R S
inst✝² : IsDomain S
inst✝¹ : NoZeroSMulDivisors R S
inst✝ : IsIntegrallyClosed R
x : S
hx : IsIntegral R x
a b : R[X]
h : (Polynomial.aeval x) a * (Polynomial.aeval x) b = 0
h' : ¬(Polynomial.aeval x) a = 0
⊢ (Polynomial.aeval x) b = 0

Tactic:
exact eq_zero_of_ne_zero_of_mul_left_eq_zero h' h

Result:
no goals

Proof state:
R : Type u_1
S : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : IsDomain R
inst✝³ : Algebra R S
inst✝² : IsDomain S
inst✝¹ : NoZeroSMulDivisors R S
inst✝ : IsIntegrallyClosed R
x : S
hx : IsIntegral R x
a b : R[X]
h : minpoly R x ∣ a * b
h' : ¬minpoly R x ∣ a
⊢ minpoly R x ∣ b

Tactic:
rw [← minpoly.isIntegrallyClosed_dvd_iff hx] at h' h ⊢

Result:
R : Type u_1
S : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : IsDomain R
inst✝³ : Algebra R S
inst✝² : IsDomain S
inst✝¹ : NoZeroSMulDivisors R S
inst✝ : IsIntegrallyClosed R
x : S
hx : IsIntegral R x
a b : R[X]
h : (Polynomial.aeval x) (a * b) = 0
h' : ¬(Polynomial.aeval x) a = 0
⊢ (Polynomial.aeval x) b = 0

Proof state:
R : Type u_1
S : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : IsDomain R
inst✝³ : Algebra R S
inst✝² : IsDomain S
inst✝¹ : NoZeroSMulDivisors R S
inst✝ : IsIntegrallyClosed R
x : S
hx : IsIntegral R x
⊢ Prime (minpoly R x)

Tactic:
refine
  ⟨(minpoly.monic hx).ne_zero,
    ⟨fun h_contra => (ne_of_lt (minpoly.degree_pos hx)) (degree_eq_zero_of_isUnit h_contra).symm,
      fun a b h => or_iff_not_imp_left.mpr fun h' => ?_⟩⟩

Result:
R : Type u_1
S : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : IsDomain R
inst✝³ : Algebra R S
inst✝² : IsDomain S
inst✝¹ : NoZeroSMulDivisors R S
inst✝ : IsIntegrallyClosed R
x : S
hx : IsIntegral R x
a b : R[X]
h : minpoly R x ∣ a * b
h' : ¬minpoly R x ∣ a
⊢ minpoly R x ∣ b

Proof state:
R : Type u_1
S : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : IsDomain R
inst✝³ : Algebra R S
inst✝² : IsDomain S
inst✝¹ : NoZeroSMulDivisors R S
inst✝ : IsIntegrallyClosed R
x : S
hx : IsIntegral R x
a b : R[X]
h : (Polynomial.aeval x) (a * b) = 0
h' : ¬(Polynomial.aeval x) a = 0
⊢ (Polynomial.aeval x) b = 0

Tactic:
rw [aeval_mul] at h

Result:
R : Type u_1
S : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : IsDomain R
inst✝³ : Algebra R S
inst✝² : IsDomain S
inst✝¹ : NoZeroSMulDivisors R S
inst✝ : IsIntegrallyClosed R
x : S
hx : IsIntegral R x
a b : R[X]
h : (Polynomial.aeval x) a * (Polynomial.aeval x) b = 0
h' : ¬(Polynomial.aeval x) a = 0
⊢ (Polynomial.aeval x) b = 0
-- Mathlib/Analysis/BoxIntegral/Partition/Basic.lean
theorem le_ofWithBot {boxes : Finset (WithBot (Box ι))}
    {le_of_mem : ∀ J ∈ boxes, (J : WithBot (Box ι)) ≤ I}
    {pairwise_disjoint : Set.Pairwise (boxes : Set (WithBot (Box ι))) Disjoint}
    (H : ∀ J ∈ π, ∃ J' ∈ boxes, ↑J ≤ J') : π ≤ ofWithBot boxes le_of_mem pairwise_disjoint

Proof state:
case intro.intro
ι : Type u_1
I : Box ι
π : Prepartition I
boxes : Finset (WithBot (Box ι))
le_of_mem : ∀ J ∈ boxes, J ≤ ↑I
pairwise_disjoint : (↑boxes).Pairwise Disjoint
H : ∀ J ∈ π, ∃ J' ∈ boxes, ↑J ≤ J'
J : Box ι
hJ : J ∈ π
J' : WithBot (Box ι)
J'mem : J' ∈ boxes
hle : ↑J ≤ J'
⊢ ∃ I' ∈ ofWithBot boxes le_of_mem pairwise_disjoint, J ≤ I'

Tactic:
lift J' to Box ι using ne_bot_of_le_ne_bot WithBot.coe_ne_bot hle

Result:
case intro.intro.intro
ι : Type u_1
I : Box ι
π : Prepartition I
boxes : Finset (WithBot (Box ι))
le_of_mem : ∀ J ∈ boxes, J ≤ ↑I
pairwise_disjoint : (↑boxes).Pairwise Disjoint
H : ∀ J ∈ π, ∃ J' ∈ boxes, ↑J ≤ J'
J : Box ι
hJ : J ∈ π
J' : Box ι
J'mem : ↑J' ∈ boxes
hle : ↑J ≤ ↑J'
⊢ ∃ I' ∈ ofWithBot boxes le_of_mem pairwise_disjoint, J ≤ I'

Proof state:
ι : Type u_1
I : Box ι
π : Prepartition I
boxes : Finset (WithBot (Box ι))
le_of_mem : ∀ J ∈ boxes, J ≤ ↑I
pairwise_disjoint : (↑boxes).Pairwise Disjoint
H : ∀ J ∈ π, ∃ J' ∈ boxes, ↑J ≤ J'
J : Box ι
hJ : J ∈ π
⊢ ∃ I' ∈ ofWithBot boxes le_of_mem pairwise_disjoint, J ≤ I'

Tactic:
rcases H J hJ with ⟨J', J'mem, hle⟩

Result:
case intro.intro
ι : Type u_1
I : Box ι
π : Prepartition I
boxes : Finset (WithBot (Box ι))
le_of_mem : ∀ J ∈ boxes, J ≤ ↑I
pairwise_disjoint : (↑boxes).Pairwise Disjoint
H : ∀ J ∈ π, ∃ J' ∈ boxes, ↑J ≤ J'
J : Box ι
hJ : J ∈ π
J' : WithBot (Box ι)
J'mem : J' ∈ boxes
hle : ↑J ≤ J'
⊢ ∃ I' ∈ ofWithBot boxes le_of_mem pairwise_disjoint, J ≤ I'

Proof state:
case intro.intro.intro
ι : Type u_1
I : Box ι
π : Prepartition I
boxes : Finset (WithBot (Box ι))
le_of_mem : ∀ J ∈ boxes, J ≤ ↑I
pairwise_disjoint : (↑boxes).Pairwise Disjoint
H : ∀ J ∈ π, ∃ J' ∈ boxes, ↑J ≤ J'
J : Box ι
hJ : J ∈ π
J' : Box ι
J'mem : ↑J' ∈ boxes
hle : ↑J ≤ ↑J'
⊢ ∃ I' ∈ ofWithBot boxes le_of_mem pairwise_disjoint, J ≤ I'

Tactic:
exact ⟨J', mem_ofWithBot.2 J'mem, WithBot.coe_le_coe.1 hle⟩

Result:
no goals

Proof state:
ι : Type u_1
I : Box ι
π : Prepartition I
boxes : Finset (WithBot (Box ι))
le_of_mem : ∀ J ∈ boxes, J ≤ ↑I
pairwise_disjoint : (↑boxes).Pairwise Disjoint
H : ∀ J ∈ π, ∃ J' ∈ boxes, ↑J ≤ J'
⊢ π ≤ ofWithBot boxes le_of_mem pairwise_disjoint

Tactic:
intro J hJ

Result:
ι : Type u_1
I : Box ι
π : Prepartition I
boxes : Finset (WithBot (Box ι))
le_of_mem : ∀ J ∈ boxes, J ≤ ↑I
pairwise_disjoint : (↑boxes).Pairwise Disjoint
H : ∀ J ∈ π, ∃ J' ∈ boxes, ↑J ≤ J'
J : Box ι
hJ : J ∈ π
⊢ ∃ I' ∈ ofWithBot boxes le_of_mem pairwise_disjoint, J ≤ I'
-- Mathlib/Algebra/Order/Interval/Set/Instances.lean
theorem coe_eq_one {x : Icc (0 : α) 1} : (x : α) = 1 ↔ x = 1

Proof state:
α : Type u_1
inst✝ : OrderedSemiring α
x : ↑(Icc 0 1)
⊢ x = 1 ↔ ↑x = 1

Tactic:
exact Subtype.ext_iff

Result:
no goals

Proof state:
α : Type u_1
inst✝ : OrderedSemiring α
x : ↑(Icc 0 1)
⊢ ↑x = 1 ↔ x = 1

Tactic:
symm

Result:
α : Type u_1
inst✝ : OrderedSemiring α
x : ↑(Icc 0 1)
⊢ x = 1 ↔ ↑x = 1
-- Mathlib/Topology/ContinuousMap/StoneWeierstrass.lean
theorem polynomial_comp_attachBound_mem (A : Subalgebra ℝ C(X, ℝ)) (f : A) (g : ℝ[X]) :
    (g.toContinuousMapOn (Set.Icc (-‖f‖) ‖f‖)).comp (f : C(X, ℝ)).attachBound ∈ A

Proof state:
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : CompactSpace X
A : Subalgebra ℝ C(X, ℝ)
f : ↥A
g : ℝ[X]
⊢ (g.toContinuousMapOn (Set.Icc (-‖f‖) ‖f‖)).comp (↑f).attachBound ∈ A

Tactic:
rw [polynomial_comp_attachBound]

Result:
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : CompactSpace X
A : Subalgebra ℝ C(X, ℝ)
f : ↥A
g : ℝ[X]
⊢ ↑((Polynomial.aeval f) g) ∈ A

Proof state:
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : CompactSpace X
A : Subalgebra ℝ C(X, ℝ)
f : ↥A
g : ℝ[X]
⊢ ↑((Polynomial.aeval f) g) ∈ A

Tactic:
apply SetLike.coe_mem

Result:
no goals
-- Mathlib/Order/Interval/Finset/Nat.lean
theorem Ico_succ_singleton : Ico a (a + 1) = {a}

Proof state:
a : ℕ
⊢ Ico a (a + 1) = {a}

Tactic:
rw [Ico_succ_right, Icc_self]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Nat/Simproc.lean
theorem eq_add_gt (a : Nat) {b c : Nat} (h : c > a) : (a = b + c) = False

Proof state:
a b c : Nat
h : c > a
⊢ (a = b + c) = False

Tactic:
rw [@Eq.comm Nat a (b + c)]

Result:
a b c : Nat
h : c > a
⊢ (b + c = a) = False

Proof state:
a b c : Nat
h : c > a
⊢ (b + c = a) = False

Tactic:
exact add_eq_gt b h

Result:
no goals
-- Mathlib/Order/KrullDimension.lean
lemma exists_series_of_le_coheight (a : α) {n : ℕ} (h : n ≤ coheight a) :
    ∃ p : LTSeries α, p.head = a ∧ p.length = n

Proof state:
case intro.intro
α : Type u_1
inst✝ : Preorder α
a : α
n : ℕ
h : ↑n ≤ coheight a
p : LTSeries αᵒᵈ
hp : RelSeries.last p = a
hl : p.length = n
⊢ ∃ p, RelSeries.head p = a ∧ p.length = n

Tactic:
exact ⟨p.reverse, by simpa, by simpa⟩

Result:
no goals

Proof state:
α : Type u_1
inst✝ : Preorder α
a : α
n : ℕ
h : ↑n ≤ coheight a
⊢ ∃ p, RelSeries.head p = a ∧ p.length = n

Tactic:
obtain ⟨p, hp, hl⟩ := exists_series_of_le_height (α := αᵒᵈ) a h

Result:
case intro.intro
α : Type u_1
inst✝ : Preorder α
a : α
n : ℕ
h : ↑n ≤ coheight a
p : LTSeries αᵒᵈ
hp : RelSeries.last p = a
hl : p.length = n
⊢ ∃ p, RelSeries.head p = a ∧ p.length = n

Proof state:
α : Type u_1
inst✝ : Preorder α
a : α
n : ℕ
h : ↑n ≤ coheight a
p : LTSeries αᵒᵈ
hp : RelSeries.last p = a
hl : p.length = n
⊢ (RelSeries.reverse p).length = n

Tactic:
simpa

Result:
no goals

Proof state:
α : Type u_1
inst✝ : Preorder α
a : α
n : ℕ
h : ↑n ≤ coheight a
p : LTSeries αᵒᵈ
hp : RelSeries.last p = a
hl : p.length = n
⊢ (RelSeries.reverse p).head = a

Tactic:
simpa

Result:
no goals
-- Mathlib/LinearAlgebra/CliffordAlgebra/BaseChange.lean
theorem ofBaseChange_tmul_ι (Q : QuadraticForm R V) (z : A) (v : V) :
    ofBaseChange A Q (z ⊗ₜ ι Q v) = ι (Q.baseChange A) (z ⊗ₜ v)

Proof state:
R : Type u_1
A : Type u_2
V : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : AddCommGroup V
inst✝² : Algebra R A
inst✝¹ : Module R V
inst✝ : Invertible 2
Q : QuadraticForm R V
z : A
v : V
⊢ (algebraMap A (CliffordAlgebra (QuadraticForm.baseChange A Q))) z * (ofBaseChangeAux A Q) ((ι Q) v) =
    (ι (QuadraticForm.baseChange A Q)) (z ⊗ₜ[R] v)

Tactic:
rw [ofBaseChangeAux_ι, ← Algebra.smul_def, ← map_smul, TensorProduct.smul_tmul', smul_eq_mul,
  mul_one]

Result:
no goals

Proof state:
R : Type u_1
A : Type u_2
V : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : AddCommGroup V
inst✝² : Algebra R A
inst✝¹ : Module R V
inst✝ : Invertible 2
Q : QuadraticForm R V
z : A
v : V
⊢ (ofBaseChange A Q) (z ⊗ₜ[R] (ι Q) v) = (ι (QuadraticForm.baseChange A Q)) (z ⊗ₜ[R] v)

Tactic:
show algebraMap _ _ z * ofBaseChangeAux A Q (ι Q v) = ι (Q.baseChange A) (z ⊗ₜ[R] v)

Result:
R : Type u_1
A : Type u_2
V : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : AddCommGroup V
inst✝² : Algebra R A
inst✝¹ : Module R V
inst✝ : Invertible 2
Q : QuadraticForm R V
z : A
v : V
⊢ (algebraMap A (CliffordAlgebra (QuadraticForm.baseChange A Q))) z * (ofBaseChangeAux A Q) ((ι Q) v) =
    (ι (QuadraticForm.baseChange A Q)) (z ⊗ₜ[R] v)
-- Mathlib/Data/Finset/Lattice/Fold.lean
theorem disjoint_sup_right : Disjoint a (s.sup f) ↔ ∀ ⦃i⦄, i ∈ s → Disjoint a (f i)

Proof state:
α : Type u_2
ι : Type u_5
inst✝¹ : DistribLattice α
inst✝ : OrderBot α
s : Finset ι
f : ι → α
a : α
⊢ Disjoint a (s.sup f) ↔ ∀ ⦃i : ι⦄, i ∈ s → Disjoint a (f i)

Tactic:
simp only [disjoint_iff, sup_inf_distrib_left, Finset.sup_eq_bot_iff]

Result:
no goals
-- Mathlib/RingTheory/Ideal/Norm/AbsNorm.lean
theorem span_singleton_absNorm_le (I : Ideal S) : Ideal.span {(Ideal.absNorm I : S)} ≤ I

Proof state:
S : Type u_1
inst✝³ : CommRing S
inst✝² : Nontrivial S
inst✝¹ : IsDedekindDomain S
inst✝ : Module.Free ℤ S
I : Ideal S
⊢ span {↑(absNorm I)} ≤ I

Tactic:
simp only [Ideal.span_le, Set.singleton_subset_iff, SetLike.mem_coe, Ideal.absNorm_mem I]

Result:
no goals
-- Mathlib/.lake/packages/batteries/Batteries/Data/List/Lemmas.lean
theorem exists_of_replaceF : ∀ {l : List α} {a a'} (_ : a ∈ l) (_ : p a = some a'),
    ∃ a a' l₁ l₂,
      (∀ b ∈ l₁, p b = none) ∧ p a = some a' ∧ l = l₁ ++ a :: l₂ ∧ l.replaceF p = l₁ ++ a' :: l₂
  | b :: l, _, _, al, pa =>
    match pb : p b with
    | some b' => ⟨b, b', [], l, forall_mem_nil _, pb, by simp [pb]⟩
    | none =>
      match al with
      | .head .. => nomatch pb.symm.trans pa
      | .tail _ al =>
        let ⟨c, c', l₁, l₂, h₁, h₂, h₃, h₄⟩ := exists_of_replaceF al pa
        ⟨c, c', b::l₁, l₂, (forall_mem_cons ..).2 ⟨pb, h₁⟩,
          h₂, by rw [h₃, cons_append], by simp [pb, h₄]⟩

Proof state:
α : Type u_1
p : α → Option α
b✝ : α
l : List α
x✝¹ x✝ : α
al✝ : x✝¹ ∈ b✝ :: l
pa : p x✝¹ = some x✝
b : α
al : Mem x✝¹ l
pb : p b = none
c c' : α
l₁ l₂ : List α
h₁ : ∀ (b : α), b ∈ l₁ → p b = none
h₂ : p c = some c'
h₃ : l = l₁ ++ c :: l₂
h₄ : replaceF p l = l₁ ++ c' :: l₂
⊢ b :: l = b :: l₁ ++ c :: l₂

Tactic:
rw [h₃, cons_append]

Result:
no goals

Proof state:
α : Type u_1
p : α → Option α
b : α
l : List α
x✝¹ x✝ : α
al : x✝¹ ∈ b :: l
pa : p x✝¹ = some x✝
b' : α
pb : p b = some b'
⊢ b :: l = [] ++ b :: l ∧ replaceF p (b :: l) = [] ++ b' :: l

Tactic:
simp [pb]

Result:
no goals

Proof state:
α : Type u_1
p : α → Option α
b✝ : α
l : List α
x✝¹ x✝ : α
al✝ : x✝¹ ∈ b✝ :: l
pa : p x✝¹ = some x✝
b : α
al : Mem x✝¹ l
pb : p b = none
c c' : α
l₁ l₂ : List α
h₁ : ∀ (b : α), b ∈ l₁ → p b = none
h₂ : p c = some c'
h₃ : l = l₁ ++ c :: l₂
h₄ : replaceF p l = l₁ ++ c' :: l₂
⊢ replaceF p (b :: l) = b :: l₁ ++ c' :: l₂

Tactic:
simp [pb, h₄]

Result:
no goals
-- Mathlib/Algebra/Category/ModuleCat/Presheaf/Free.lean
@[simp]
lemma freeAdjunction_homEquiv : (freeAdjunction R).homEquiv F G = freeHomEquiv

Proof state:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
R : Cᵒᵖ ⥤ RingCat
F : Cᵒᵖ ⥤ Type u
G : PresheafOfModules R
⊢ (freeAdjunction R).homEquiv F G = freeHomEquiv

Tactic:
simp [freeAdjunction, Adjunction.mkOfHomEquiv_homEquiv]

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Coloring.lean
theorem chromaticNumber_ne_top_iff_exists : G.chromaticNumber ≠ ⊤ ↔ ∃ n, G.Colorable n

Proof state:
case convert_2
V : Type u
G : SimpleGraph V
⊢ ⨅ n, ↑↑n ≠ ⊤ ↔ ∃ n, G.Colorable n

Tactic:
rw [← lt_top_iff_ne_top, ENat.iInf_coe_lt_top]

Result:
case convert_2
V : Type u
G : SimpleGraph V
⊢ Nonempty ↑{m | G.Colorable m} ↔ ∃ n, G.Colorable n

Proof state:
V : Type u
G : SimpleGraph V
⊢ G.chromaticNumber ≠ ⊤ ↔ ∃ n, G.Colorable n

Tactic:
rw [chromaticNumber]

Result:
V : Type u
G : SimpleGraph V
⊢ ⨅ n ∈ setOf G.Colorable, ↑n ≠ ⊤ ↔ ∃ n, G.Colorable n

Proof state:
V : Type u
G : SimpleGraph V
⊢ ⨅ n ∈ setOf G.Colorable, ↑n ≠ ⊤ ↔ ∃ n, G.Colorable n

Tactic:
convert_to ⨅ n : {m | G.Colorable m}, (n : ℕ∞) ≠ ⊤ ↔ _

Result:
case h.e'_1.a
V : Type u
G : SimpleGraph V
⊢ ⨅ n ∈ setOf G.Colorable, ↑n ≠ ⊤ ↔ ⨅ n, ↑↑n ≠ ⊤

case convert_2
V : Type u
G : SimpleGraph V
⊢ ⨅ n, ↑↑n ≠ ⊤ ↔ ∃ n, G.Colorable n

Proof state:
case convert_2
V : Type u
G : SimpleGraph V
⊢ Nonempty ↑{m | G.Colorable m} ↔ ∃ n, G.Colorable n

Tactic:
simp

Result:
no goals

Proof state:
case h.e'_1.a
V : Type u
G : SimpleGraph V
⊢ ⨅ n ∈ setOf G.Colorable, ↑n ≠ ⊤ ↔ ⨅ n, ↑↑n ≠ ⊤

Tactic:
rw [iInf_subtype]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Nat/Linear.lean
theorem Poly.of_denote_eq_cancel {ctx : Context} {m₁ m₂ : Poly} (h : denote_eq ctx (cancel m₁ m₂)) : denote_eq ctx (m₁, m₂)

Proof state:
ctx : Context
m₁ m₂ : Poly
h : denote_eq ctx (m₁.cancel m₂)
this : denote_eq ctx (m₁, m₂)
⊢ denote_eq ctx (m₁, m₂)

Tactic:
assumption

Result:
no goals

Proof state:
ctx : Context
m₁ m₂ : Poly
h : denote_eq ctx (m₁.cancel m₂)
this : denote_eq ctx ([].reverse ++ m₁, [].reverse ++ m₂)
⊢ denote_eq ctx (m₁, m₂)

Tactic:
simp at this

Result:
ctx : Context
m₁ m₂ : Poly
h : denote_eq ctx (m₁.cancel m₂)
this : denote_eq ctx (m₁, m₂)
⊢ denote_eq ctx (m₁, m₂)

Proof state:
ctx : Context
m₁ m₂ : Poly
h : denote_eq ctx (m₁.cancel m₂)
⊢ denote_eq ctx (m₁, m₂)

Tactic:
have := Poly.of_denote_eq_cancelAux (h := h)

Result:
ctx : Context
m₁ m₂ : Poly
h : denote_eq ctx (m₁.cancel m₂)
this : denote_eq ctx ([].reverse ++ m₁, [].reverse ++ m₂)
⊢ denote_eq ctx (m₁, m₂)
-- Mathlib/Geometry/Manifold/Instances/Real.lean
theorem closure_open_halfSpace {n : ℕ} (p : ℝ≥0∞) (a : ℝ) (i : Fin n) :
    closure { y : PiLp p (fun _ : Fin n ↦ ℝ) | a < y i } = { y | a ≤ y i }

Proof state:
n : ℕ
p : ℝ≥0∞
a : ℝ
i : Fin n
⊢ closure {y | a < y i} = {y | a ≤ y i}

Tactic:
let f : (Π _ : Fin n, ℝ) →L[ℝ] ℝ := ContinuousLinearMap.proj i

Result:
n : ℕ
p : ℝ≥0∞
a : ℝ
i : Fin n
f : (Fin n → ℝ) →L[ℝ] ℝ := ContinuousLinearMap.proj i
⊢ closure {y | a < y i} = {y | a ≤ y i}

Proof state:
n : ℕ
p : ℝ≥0∞
a : ℝ
i : Fin n
f : (Fin n → ℝ) →L[ℝ] ℝ := ContinuousLinearMap.proj i
⊢ closure {y | a < y i} = {y | a ≤ y i}

Tactic:
change closure (f ⁻¹' Ioi a) = f ⁻¹' Ici a

Result:
n : ℕ
p : ℝ≥0∞
a : ℝ
i : Fin n
f : (Fin n → ℝ) →L[ℝ] ℝ := ContinuousLinearMap.proj i
⊢ closure (⇑f ⁻¹' Ioi a) = ⇑f ⁻¹' Ici a

Proof state:
case hsurj
n : ℕ
p : ℝ≥0∞
a : ℝ
i : Fin n
f : (Fin n → ℝ) →L[ℝ] ℝ := ContinuousLinearMap.proj i
⊢ Surjective ⇑f

Tactic:
apply Function.surjective_eval

Result:
no goals

Proof state:
n : ℕ
p : ℝ≥0∞
a : ℝ
i : Fin n
f : (Fin n → ℝ) →L[ℝ] ℝ := ContinuousLinearMap.proj i
⊢ closure (⇑f ⁻¹' Ioi a) = ⇑f ⁻¹' Ici a

Tactic:
rw [f.closure_preimage, closure_Ioi]

Result:
case hsurj
n : ℕ
p : ℝ≥0∞
a : ℝ
i : Fin n
f : (Fin n → ℝ) →L[ℝ] ℝ := ContinuousLinearMap.proj i
⊢ Surjective ⇑f
-- Mathlib/Data/Int/Bitwise.lean
theorem shiftLeft_eq_mul_pow : ∀ (m : ℤ) (n : ℕ), m <<< (n : ℤ) = m * (2 ^ n : ℕ)
  | (m : ℕ), _ => congr_arg ((↑) : ℕ → ℤ) (by simp [Nat.shiftLeft_eq])
  | -[_+1], _ => @congr_arg ℕ ℤ _ _ (fun i => -i) (Nat.shiftLeft'_tt_eq_mul_pow _ _)

Proof state:
m x✝ : ℕ
⊢ Nat.shiftLeft' false m x✝ = m * 2 ^ x✝

Tactic:
simp [Nat.shiftLeft_eq]

Result:
no goals
-- Mathlib/GroupTheory/NoncommCoprod.lean
theorem noncommCoprod_comp_inr : (f.noncommCoprod g comm).comp (inr M N) = g :=
  ext fun x => by simp

Proof state:
M : Type u_1
N : Type u_2
P : Type u_3
inst✝² : MulOneClass M
inst✝¹ : MulOneClass N
inst✝ : Monoid P
f : M →* P
g : N →* P
comm : ∀ (m : M) (n : N), Commute (f m) (g n)
x : N
⊢ ((f.noncommCoprod g comm).comp (inr M N)) x = g x

Tactic:
simp

Result:
no goals
-- Mathlib/Analysis/Calculus/FDeriv/Equiv.lean
theorem HasFDerivAt.of_local_left_inverse {f : E → F} {f' : E ≃L[𝕜] F} {g : F → E} {a : F}
    (hg : ContinuousAt g a) (hf : HasFDerivAt f (f' : E →L[𝕜] F) (g a))
    (hfg : ∀ᶠ y in 𝓝 a, f (g y) = y) : HasFDerivAt g (f'.symm : F →L[𝕜] E) a

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
f' : E ≃L[𝕜] F
g : F → E
a : F
hg : ContinuousAt g a
hf : HasFDerivWithinAt f (↑f') univ (g a)
hfg : ∀ᶠ (y : F) in 𝓝[univ] a, f (g y) = y
⊢ Tendsto g (𝓟 univ) (𝓟 univ)

Tactic:
simp

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
f' : E ≃L[𝕜] F
g : F → E
a : F
hg : ContinuousAt g a
hf : HasFDerivWithinAt f (↑f') univ (g a)
hfg : ∀ᶠ (y : F) in 𝓝[univ] a, f (g y) = y
⊢ HasFDerivWithinAt g (↑f'.symm) univ a

Tactic:
exact hf.of_local_left_inverse (.inf hg (by simp)) (mem_univ _) hfg

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
f' : E ≃L[𝕜] F
g : F → E
a : F
hg : ContinuousAt g a
hf : HasFDerivAt f (↑f') (g a)
hfg : ∀ᶠ (y : F) in 𝓝 a, f (g y) = y
⊢ HasFDerivAt g (↑f'.symm) a

Tactic:
simp only [← hasFDerivWithinAt_univ, ← nhdsWithin_univ] at hf hfg ⊢

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
f' : E ≃L[𝕜] F
g : F → E
a : F
hg : ContinuousAt g a
hf : HasFDerivWithinAt f (↑f') univ (g a)
hfg : ∀ᶠ (y : F) in 𝓝[univ] a, f (g y) = y
⊢ HasFDerivWithinAt g (↑f'.symm) univ a
-- Mathlib/SetTheory/Cardinal/Basic.lean
theorem nat_succ (n : ℕ) : (n.succ : Cardinal) = succ ↑n

Proof state:
n : ℕ
⊢ ↑n < ↑n.succ

Tactic:
exact Nat.cast_lt.2 (Nat.lt_succ_self _)

Result:
no goals

Proof state:
n : ℕ
⊢ ↑n < ↑n + 1

Tactic:
rw [← Nat.cast_succ]

Result:
n : ℕ
⊢ ↑n < ↑n.succ

Proof state:
n : ℕ
⊢ ↑n.succ = succ ↑n

Tactic:
rw [Nat.cast_succ]

Result:
n : ℕ
⊢ ↑n + 1 = succ ↑n

Proof state:
n : ℕ
⊢ ↑n + 1 = succ ↑n

Tactic:
refine (add_one_le_succ _).antisymm (succ_le_of_lt ?_)

Result:
n : ℕ
⊢ ↑n < ↑n + 1
-- Mathlib/Analysis/SpecificLimits/Normed.lean
theorem geom_series_mul_shift (x : R) (h : ‖x‖ < 1) :
    x * ∑' i : ℕ, x ^ i = ∑' i : ℕ, x ^ (i + 1)

Proof state:
R : Type u_2
inst✝¹ : NormedRing R
inst✝ : HasSummableGeomSeries R
x : R
h : ‖x‖ < 1
⊢ x * ∑' (i : ℕ), x ^ i = ∑' (i : ℕ), x ^ (i + 1)

Tactic:
simp_rw [← (summable_geometric_of_norm_lt_one h).tsum_mul_left, ← _root_.pow_succ']

Result:
no goals