harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Algebra/Lie/Subalgebra.lean
theorem coe_lieSpan_submodule_eq_iff {p : Submodule R L} :
    (lieSpan R L (p : Set L) : Submodule R L) = p ↔ ∃ K : LieSubalgebra R L, ↑K = p

Proof state:
case mp
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
p : Submodule R L
h : (lieSpan R L ↑p).toSubmodule = p
x m : L
hm : x ∈ p
⊢ m ∈ lieSpan R L ↑p → ⁅x, m⁆ ∈ (lieSpan R L ↑p).toSubmodule

Tactic:
exact lie_mem _ (subset_lieSpan hm)

Result:
no goals

Proof state:
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
p : Submodule R L
⊢ (lieSpan R L ↑p).toSubmodule = p ↔ ∀ (x y : L), x ∈ p → y ∈ p → ⁅x, y⁆ ∈ p

Tactic:
constructor <;> intro h

Result:
case mp
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
p : Submodule R L
h : (lieSpan R L ↑p).toSubmodule = p
⊢ ∀ (x y : L), x ∈ p → y ∈ p → ⁅x, y⁆ ∈ p

case mpr
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
p : Submodule R L
h : ∀ (x y : L), x ∈ p → y ∈ p → ⁅x, y⁆ ∈ p
⊢ (lieSpan R L ↑p).toSubmodule = p

Proof state:
case mp
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
p : Submodule R L
h : (lieSpan R L ↑p).toSubmodule = p
⊢ ∀ (x y : L), x ∈ p → y ∈ p → ⁅x, y⁆ ∈ p

Tactic:
intro x m hm

Result:
case mp
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
p : Submodule R L
h : (lieSpan R L ↑p).toSubmodule = p
x m : L
hm : x ∈ p
⊢ m ∈ p → ⁅x, m⁆ ∈ p

Proof state:
case mp
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
p : Submodule R L
h : (lieSpan R L ↑p).toSubmodule = p
x m : L
hm : x ∈ p
⊢ m ∈ p → ⁅x, m⁆ ∈ p

Tactic:
rw [← h, mem_toSubmodule]

Result:
case mp
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
p : Submodule R L
h : (lieSpan R L ↑p).toSubmodule = p
x m : L
hm : x ∈ p
⊢ m ∈ lieSpan R L ↑p → ⁅x, m⁆ ∈ (lieSpan R L ↑p).toSubmodule

Proof state:
case mpr
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
p : Submodule R L
h : ∀ (x y : L), x ∈ p → y ∈ p → ⁅x, y⁆ ∈ p
⊢ (lieSpan R L ↑p).toSubmodule = p

Tactic:
rw [← toSubmodule_mk p @h, coe_toSubmodule, toSubmodule_inj, lieSpan_eq]

Result:
no goals

Proof state:
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
p : Submodule R L
⊢ (lieSpan R L ↑p).toSubmodule = p ↔ ∃ K, K.toSubmodule = p

Tactic:
rw [p.exists_lieSubalgebra_coe_eq_iff]

Result:
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
p : Submodule R L
⊢ (lieSpan R L ↑p).toSubmodule = p ↔ ∀ (x y : L), x ∈ p → y ∈ p → ⁅x, y⁆ ∈ p
-- Mathlib/LinearAlgebra/Dual.lean
theorem comap_dualAnnihilator_dualAnnihilator (W : Subspace K V) :
    W.dualAnnihilator.dualAnnihilator.comap (Module.Dual.eval K V) = W

Proof state:
K : Type u
V : Type v
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
W : Subspace K V
⊢ comap (Dual.eval K V) (dualAnnihilator W).dualAnnihilator = W

Tactic:
ext

Result:
case h
K : Type u
V : Type v
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
W : Subspace K V
x✝ : V
⊢ x✝ ∈ comap (Dual.eval K V) (dualAnnihilator W).dualAnnihilator ↔ x✝ ∈ W

Proof state:
case h
K : Type u
V : Type v
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
W : Subspace K V
x✝ : V
⊢ (∀ φ ∈ dualAnnihilator W, φ x✝ = 0) ↔ x✝ ∈ comap (Dual.eval K V) (dualAnnihilator W).dualAnnihilator

Tactic:
simp

Result:
no goals

Proof state:
case h
K : Type u
V : Type v
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
W : Subspace K V
x✝ : V
⊢ x✝ ∈ comap (Dual.eval K V) (dualAnnihilator W).dualAnnihilator ↔ x✝ ∈ W

Tactic:
rw [Iff.comm, ← forall_mem_dualAnnihilator_apply_eq_zero_iff]

Result:
case h
K : Type u
V : Type v
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
W : Subspace K V
x✝ : V
⊢ (∀ φ ∈ dualAnnihilator W, φ x✝ = 0) ↔ x✝ ∈ comap (Dual.eval K V) (dualAnnihilator W).dualAnnihilator
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Lemmas.lean
theorem findM?_toArray [Monad m] (p : α → m Bool) (v : Vector α n) :
    v.toArray.findM? p = v.findM? p

Proof state:
case mk
m : Type → Type
α : Type
n : Nat
inst✝ : Monad m
p : α → m Bool
toArray✝ : Array α
size_toArray✝ : toArray✝.size = n
⊢ Array.findM? p { toArray := toArray✝, size_toArray := size_toArray✝ }.toArray =
    findM? p { toArray := toArray✝, size_toArray := size_toArray✝ }

Tactic:
simp

Result:
no goals

Proof state:
m : Type → Type
α : Type
n : Nat
inst✝ : Monad m
p : α → m Bool
v : Vector α n
⊢ Array.findM? p v.toArray = findM? p v

Tactic:
cases v

Result:
case mk
m : Type → Type
α : Type
n : Nat
inst✝ : Monad m
p : α → m Bool
toArray✝ : Array α
size_toArray✝ : toArray✝.size = n
⊢ Array.findM? p { toArray := toArray✝, size_toArray := size_toArray✝ }.toArray =
    findM? p { toArray := toArray✝, size_toArray := size_toArray✝ }
-- Mathlib/Geometry/Manifold/MFDeriv/Basic.lean
theorem hasMFDerivWithinAt_insert {y : M} :
    HasMFDerivWithinAt I I' f (insert y s) x f' ↔ HasMFDerivWithinAt I I' f s x f'

Proof state:
𝕜 : Type u_1
inst✝¹⁰ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace 𝕜 E
H : Type u_3
inst✝⁷ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝⁶ : TopologicalSpace M
inst✝⁵ : ChartedSpace H M
E' : Type u_5
inst✝⁴ : NormedAddCommGroup E'
inst✝³ : NormedSpace 𝕜 E'
H' : Type u_6
inst✝² : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst✝¹ : TopologicalSpace M'
inst✝ : ChartedSpace H' M'
f : M → M'
x : M
s : Set M
f' : TangentSpace I x →L[𝕜] TangentSpace I' (f x)
y : M
⊢ HasMFDerivWithinAt I I' f (insert y s) x f' ↔ HasMFDerivWithinAt I I' f s x f'

Tactic:
have : T1Space M := I.t1Space M

Result:
𝕜 : Type u_1
inst✝¹⁰ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace 𝕜 E
H : Type u_3
inst✝⁷ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝⁶ : TopologicalSpace M
inst✝⁵ : ChartedSpace H M
E' : Type u_5
inst✝⁴ : NormedAddCommGroup E'
inst✝³ : NormedSpace 𝕜 E'
H' : Type u_6
inst✝² : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst✝¹ : TopologicalSpace M'
inst✝ : ChartedSpace H' M'
f : M → M'
x : M
s : Set M
f' : TangentSpace I x →L[𝕜] TangentSpace I' (f x)
y : M
this : T1Space M
⊢ HasMFDerivWithinAt I I' f (insert y s) x f' ↔ HasMFDerivWithinAt I I' f s x f'
-- Mathlib/Algebra/Polynomial/Lifts.lean
theorem C_mem_lifts (f : R →+* S) (r : R) : C (f r) ∈ lifts f :=
  ⟨C r, by
    simp only [coe_mapRingHom, map_C, Set.mem_univ, Subsemiring.coe_top, eq_self_iff_true,
      and_self_iff]⟩

Proof state:
R : Type u
inst✝¹ : Semiring R
S : Type v
inst✝ : Semiring S
f : R →+* S
r : R
⊢ (mapRingHom f) (C r) = C (f r)

Tactic:
simp only [coe_mapRingHom, map_C, Set.mem_univ, Subsemiring.coe_top, eq_self_iff_true,
  and_self_iff]

Result:
no goals
-- Mathlib/.lake/packages/batteries/Batteries/Lean/EStateM.lean
theorem map_eq_error {ε σ α β} (f : α → β) {x : Result ε σ α} {e : ε} {s : σ} :
    x.map f = .error e s ↔ x = .error e s

Proof state:
ε σ α β : Type u_1
f : α → β
x : Result ε σ α
e : ε
s : σ
⊢ map f x = error e s ↔ x = error e s

Tactic:
cases x <;> simp [eq_comm]

Result:
no goals
-- Mathlib/Topology/Algebra/Monoid.lean
theorem continuous_pow : ∀ n : ℕ, Continuous fun a : M => a ^ n
  | 0 => by simpa using continuous_const
  | k + 1 => by
    simp only [pow_succ']
    exact continuous_id.mul (continuous_pow _)

Proof state:
M : Type u_3
inst✝² : TopologicalSpace M
inst✝¹ : Monoid M
inst✝ : ContinuousMul M
k : ℕ
⊢ Continuous fun a => a ^ (k + 1)

Tactic:
simp only [pow_succ']

Result:
M : Type u_3
inst✝² : TopologicalSpace M
inst✝¹ : Monoid M
inst✝ : ContinuousMul M
k : ℕ
⊢ Continuous fun a => a * a ^ k

Proof state:
M : Type u_3
inst✝² : TopologicalSpace M
inst✝¹ : Monoid M
inst✝ : ContinuousMul M
⊢ Continuous fun a => a ^ 0

Tactic:
simpa using continuous_const

Result:
no goals

Proof state:
M : Type u_3
inst✝² : TopologicalSpace M
inst✝¹ : Monoid M
inst✝ : ContinuousMul M
k : ℕ
⊢ Continuous fun a => a * a ^ k

Tactic:
exact continuous_id.mul (continuous_pow _)

Result:
no goals
-- Mathlib/GroupTheory/Archimedean.lean
theorem Subgroup.exists_isLeast_one_lt {H : Subgroup G} (hbot : H ≠ ⊥) {a : G} (h₀ : 1 < a)
    (hd : Disjoint (H : Set G) (Ioo 1 a)) : ∃ b, IsLeast { g : G | g ∈ H ∧ 1 < g } b

Proof state:
G : Type u_1
inst✝¹ : LinearOrderedCommGroup G
inst✝ : MulArchimedean G
H : Subgroup G
hbot : H ≠ ⊥
a : G
h₀ : 1 < a
hd : Disjoint (↑H) (Ioo 1 a)
hex : ∀ g > 1, ∃ n, g ∈ Ioc (a ^ n) (a ^ (n + 1))
this : ∃ n, (↑H ∩ Ioc (a ^ n) (a ^ (n + 1))).Nonempty
⊢ ∃ b, IsLeast {g | g ∈ H ∧ 1 < g} b

Tactic:
classical rcases Nat.findX this with ⟨n, ⟨x, hxH, hnx, hxn⟩, hmin⟩

Result:
case mk.intro.intro.intro.intro
G : Type u_1
inst✝¹ : LinearOrderedCommGroup G
inst✝ : MulArchimedean G
H : Subgroup G
hbot : H ≠ ⊥
a : G
h₀ : 1 < a
hd : Disjoint (↑H) (Ioo 1 a)
hex : ∀ g > 1, ∃ n, g ∈ Ioc (a ^ n) (a ^ (n + 1))
this : ∃ n, (↑H ∩ Ioc (a ^ n) (a ^ (n + 1))).Nonempty
n : ℕ
hmin : ∀ m < n, ¬(↑H ∩ Ioc (a ^ m) (a ^ (m + 1))).Nonempty
x : G
hxH : x ∈ ↑H
hnx : a ^ n < x
hxn : x ≤ a ^ (n + 1)
⊢ ∃ b, IsLeast {g | g ∈ H ∧ 1 < g} b

Proof state:
case mk.intro.intro.intro.intro
G : Type u_1
inst✝¹ : LinearOrderedCommGroup G
inst✝ : MulArchimedean G
H : Subgroup G
hbot : H ≠ ⊥
a : G
h₀ : 1 < a
hd : Disjoint (↑H) (Ioo 1 a)
hex : ∀ g > 1, ∃ n, g ∈ Ioc (a ^ n) (a ^ (n + 1))
this : ∃ n, (↑H ∩ Ioc (a ^ n) (a ^ (n + 1))).Nonempty
n : ℕ
hmin : ∀ m < n, ¬(↑H ∩ Ioc (a ^ m) (a ^ (m + 1))).Nonempty
x : G
hxH : x ∈ ↑H
hnx : a ^ n < x
hxn : x ≤ a ^ (n + 1)
hxmin : ∀ (x : G), x ∈ H ∧ 1 < x → ∃ x_1, ∃ (_ : x_1 ∈ H ∧ 1 < x_1), x_1 < x
⊢ False

Tactic:
rcases hxmin x ⟨hxH, (one_le_pow_of_one_le'  h₀.le _).trans_lt hnx⟩ with ⟨y, ⟨hyH, hy₀⟩, hxy⟩

Result:
case mk.intro.intro.intro.intro.intro.intro.intro
G : Type u_1
inst✝¹ : LinearOrderedCommGroup G
inst✝ : MulArchimedean G
H : Subgroup G
hbot : H ≠ ⊥
a : G
h₀ : 1 < a
hd : Disjoint (↑H) (Ioo 1 a)
hex : ∀ g > 1, ∃ n, g ∈ Ioc (a ^ n) (a ^ (n + 1))
this : ∃ n, (↑H ∩ Ioc (a ^ n) (a ^ (n + 1))).Nonempty
n : ℕ
hmin : ∀ m < n, ¬(↑H ∩ Ioc (a ^ m) (a ^ (m + 1))).Nonempty
x : G
hxH : x ∈ ↑H
hnx : a ^ n < x
hxn : x ≤ a ^ (n + 1)
hxmin : ∀ (x : G), x ∈ H ∧ 1 < x → ∃ x_1, ∃ (_ : x_1 ∈ H ∧ 1 < x_1), x_1 < x
y : G
hxy : y < x
hyH : y ∈ H
hy₀ : 1 < y
⊢ False

Proof state:
case intro.intro.intro
G : Type u_1
inst✝¹ : LinearOrderedCommGroup G
inst✝ : MulArchimedean G
H : Subgroup G
hbot : H ≠ ⊥
a : G
h₀ : 1 < a
hd : Disjoint (↑H) (Ioo 1 a)
g : G
hg : g > 1
m : ℤ
hm : g ≤ a ^ (m + 1)
hm' : a ^ m < g
⊢ ∃ n, g ∈ Ioc (a ^ n) (a ^ (n + 1))

Tactic:
lift m to ℕ

Result:
G : Type u_1
inst✝¹ : LinearOrderedCommGroup G
inst✝ : MulArchimedean G
H : Subgroup G
hbot : H ≠ ⊥
a : G
h₀ : 1 < a
hd : Disjoint (↑H) (Ioo 1 a)
g : G
hg : g > 1
m : ℤ
hm : g ≤ a ^ (m + 1)
hm' : a ^ m < g
⊢ 0 ≤ m

case intro.intro.intro.intro
G : Type u_1
inst✝¹ : LinearOrderedCommGroup G
inst✝ : MulArchimedean G
H : Subgroup G
hbot : H ≠ ⊥
a : G
h₀ : 1 < a
hd : Disjoint (↑H) (Ioo 1 a)
g : G
hg : g > 1
m : ℕ
hm : g ≤ a ^ (↑m + 1)
hm' : a ^ ↑m < g
⊢ ∃ n, g ∈ Ioc (a ^ n) (a ^ (n + 1))
-- Mathlib/Algebra/Group/Support.lean
theorem range_subset_insert_image_mulSupport (f : α → M) :
    range f ⊆ insert 1 (f '' mulSupport f)

Proof state:
α : Type u_1
M : Type u_5
inst✝ : One M
f : α → M
⊢ range f ⊆ insert 1 (f '' mulSupport f)

Tactic:
simpa only [range_subset_iff, mem_insert_iff, or_iff_not_imp_left] using
  fun x (hx : x ∈ mulSupport f) => mem_image_of_mem f hx

Result:
no goals
-- Mathlib/RingTheory/Unramified/Finite.lean
lemma comp_sec :
    (TensorProduct.AlgebraTensorModule.lift
      ((lsmul S S M).toLinearMap.flip.restrictScalars R).flip).comp (sec R S M) =
      LinearMap.id

Proof state:
case zero
R : Type u_3
S : Type u_2
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
inst✝⁶ : Algebra R S
M : Type u_1
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : Module S M
inst✝² : IsScalarTower R S M
inst✝¹ : FormallyUnramified R S
inst✝ : EssFiniteType R S
x : M
⊢ (_root_.TensorProduct.lift (↑R (↑R (lsmul S S M).toLinearMap.flip).flip))
      ((TensorProduct.AlgebraTensorModule.map LinearMap.id ((lsmul R R M).toLinearMap.flip x)) 0) =
    (TensorProduct.lmul' R) 0 • x

Tactic:
simp

Result:
no goals
-- Mathlib/Combinatorics/SetFamily/Compression/UV.lean
theorem compress_sdiff_sdiff (a b : α) : compress (a \ b) (b \ a) b = a

Proof state:
α : Type u_1
inst✝² : GeneralizedBooleanAlgebra α
inst✝¹ : DecidableRel Disjoint
inst✝ : DecidableRel fun x1 x2 => x1 ≤ x2
a b : α
⊢ compress (a \ b) (b \ a) b = a

Tactic:
refine (compress_of_disjoint_of_le disjoint_sdiff_self_left sdiff_le).trans ?_

Result:
α : Type u_1
inst✝² : GeneralizedBooleanAlgebra α
inst✝¹ : DecidableRel Disjoint
inst✝ : DecidableRel fun x1 x2 => x1 ≤ x2
a b : α
⊢ (b ⊔ a \ b) \ (b \ a) = a

Proof state:
α : Type u_1
inst✝² : GeneralizedBooleanAlgebra α
inst✝¹ : DecidableRel Disjoint
inst✝ : DecidableRel fun x1 x2 => x1 ≤ x2
a b : α
⊢ b \ (b \ a) ≤ a

Tactic:
exact sdiff_sdiff_le

Result:
no goals

Proof state:
α : Type u_1
inst✝² : GeneralizedBooleanAlgebra α
inst✝¹ : DecidableRel Disjoint
inst✝ : DecidableRel fun x1 x2 => x1 ≤ x2
a b : α
⊢ (b ⊔ a \ b) \ (b \ a) = a

Tactic:
rw [sup_sdiff_self_right, sup_sdiff, disjoint_sdiff_self_right.sdiff_eq_left, sup_eq_right]

Result:
α : Type u_1
inst✝² : GeneralizedBooleanAlgebra α
inst✝¹ : DecidableRel Disjoint
inst✝ : DecidableRel fun x1 x2 => x1 ≤ x2
a b : α
⊢ b \ (b \ a) ≤ a
-- Mathlib/Analysis/Convex/Cone/Basic.lean
theorem pointed_zero : (0 : ConvexCone 𝕜 E).Pointed

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝² : OrderedSemiring 𝕜
inst✝¹ : AddCommMonoid E
inst✝ : Module 𝕜 E
⊢ Pointed 0

Tactic:
rw [Pointed, mem_zero]

Result:
no goals
-- Mathlib/Topology/LocalAtTarget.lean
theorem isClosedEmbedding_iff_restrictPreimage (h : Continuous f) :
    IsClosedEmbedding f ↔ ∀ i, IsClosedEmbedding ((U i).1.restrictPreimage f)

Proof state:
case h₁
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
ι : Type u_3
U : ι → Opens β
hU : IsOpenCover U
h : Continuous f
⊢ IsEmbedding f ↔ ∀ (x : ι), IsEmbedding ((U x).carrier.restrictPreimage f)

Tactic:
exact hU.isEmbedding_iff_restrictPreimage h

Result:
no goals

Proof state:
case h₂
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
ι : Type u_3
U : ι → Opens β
hU : IsOpenCover U
h : Continuous f
⊢ IsClosed (range f) ↔ ∀ (x : ι), IsClosed (range ((U x).carrier.restrictPreimage f))

Tactic:
simp_rw [range_restrictPreimage]

Result:
case h₂
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
ι : Type u_3
U : ι → Opens β
hU : IsOpenCover U
h : Continuous f
⊢ IsClosed (range f) ↔ ∀ (x : ι), IsClosed (Subtype.val ⁻¹' range f)

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
ι : Type u_3
U : ι → Opens β
hU : IsOpenCover U
h : Continuous f
⊢ IsEmbedding f ∧ IsClosed (range f) ↔
    (∀ (x : ι), IsEmbedding ((U x).carrier.restrictPreimage f)) ∧
      ∀ (x : ι), IsClosed (range ((U x).carrier.restrictPreimage f))

Tactic:
apply and_congr

Result:
case h₁
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
ι : Type u_3
U : ι → Opens β
hU : IsOpenCover U
h : Continuous f
⊢ IsEmbedding f ↔ ∀ (x : ι), IsEmbedding ((U x).carrier.restrictPreimage f)

case h₂
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
ι : Type u_3
U : ι → Opens β
hU : IsOpenCover U
h : Continuous f
⊢ IsClosed (range f) ↔ ∀ (x : ι), IsClosed (range ((U x).carrier.restrictPreimage f))

Proof state:
case h₂
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
ι : Type u_3
U : ι → Opens β
hU : IsOpenCover U
h : Continuous f
⊢ IsClosed (range f) ↔ ∀ (x : ι), IsClosed (Subtype.val ⁻¹' range f)

Tactic:
exact hU.isClosed_iff_coe_preimage

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
ι : Type u_3
U : ι → Opens β
hU : IsOpenCover U
h : Continuous f
⊢ IsClosedEmbedding f ↔ ∀ (i : ι), IsClosedEmbedding ((U i).carrier.restrictPreimage f)

Tactic:
simp_rw [isClosedEmbedding_iff, forall_and]

Result:
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
ι : Type u_3
U : ι → Opens β
hU : IsOpenCover U
h : Continuous f
⊢ IsEmbedding f ∧ IsClosed (range f) ↔
    (∀ (x : ι), IsEmbedding ((U x).carrier.restrictPreimage f)) ∧
      ∀ (x : ι), IsClosed (range ((U x).carrier.restrictPreimage f))
-- Mathlib/LinearAlgebra/Matrix/Transvection.lean
theorem exists_list_transvec_mul_mul_list_transvec_eq_diagonal_aux (n : Type) [Fintype n]
    [DecidableEq n] (M : Matrix n n 𝕜) :
    ∃ (L L' : List (TransvectionStruct n 𝕜)) (D : n → 𝕜),
      (L.map toMatrix).prod * M * (L'.map toMatrix).prod = diagonal D

Proof state:
𝕜 : Type u_3
inst✝² : Field 𝕜
r : ℕ
IH :
  ∀ (n : Type) [inst : Fintype n] [inst_1 : DecidableEq n] (M : Matrix n n 𝕜),
    Fintype.card n = r → ∃ L L' D, (List.map toMatrix L).prod * M * (List.map toMatrix L').prod = diagonal D
n : Type
inst✝¹ : Fintype n
inst✝ : DecidableEq n
M : Matrix n n 𝕜
hn : Fintype.card n = r + 1
⊢ r + 1 = Fintype.card (Fin r) + Fintype.card Unit

Tactic:
simp

Result:
no goals

Proof state:
𝕜 : Type u_3
inst✝² : Field 𝕜
r : ℕ
IH :
  ∀ (n : Type) [inst : Fintype n] [inst_1 : DecidableEq n] (M : Matrix n n 𝕜),
    Fintype.card n = r → ∃ L L' D, (List.map toMatrix L).prod * M * (List.map toMatrix L').prod = diagonal D
n : Type
inst✝¹ : Fintype n
inst✝ : DecidableEq n
M : Matrix n n 𝕜
hn : Fintype.card n = r + 1
⊢ n ≃ Fin r ⊕ Unit

Tactic:
refine Fintype.equivOfCardEq ?_

Result:
𝕜 : Type u_3
inst✝² : Field 𝕜
r : ℕ
IH :
  ∀ (n : Type) [inst : Fintype n] [inst_1 : DecidableEq n] (M : Matrix n n 𝕜),
    Fintype.card n = r → ∃ L L' D, (List.map toMatrix L).prod * M * (List.map toMatrix L').prod = diagonal D
n : Type
inst✝¹ : Fintype n
inst✝ : DecidableEq n
M : Matrix n n 𝕜
hn : Fintype.card n = r + 1
⊢ Fintype.card n = Fintype.card (Fin r ⊕ Unit)

Proof state:
case zero.a
𝕜 : Type u_3
inst✝² : Field 𝕜
n : Type
inst✝¹ : Fintype n
inst✝ : DecidableEq n
M : Matrix n n 𝕜
hn : IsEmpty n
i j : n
⊢ ((List.map toMatrix []).prod * M * (List.map toMatrix []).prod) i j = diagonal (fun x => 1) i j

Tactic:
exact hn.elim' i

Result:
no goals

Proof state:
case zero
𝕜 : Type u_3
inst✝² : Field 𝕜
n : Type
inst✝¹ : Fintype n
inst✝ : DecidableEq n
M : Matrix n n 𝕜
hn : Fintype.card n = 0
⊢ ∃ L L' D, (List.map toMatrix L).prod * M * (List.map toMatrix L').prod = diagonal D

Tactic:
refine ⟨List.nil, List.nil, fun _ => 1, ?_⟩

Result:
case zero
𝕜 : Type u_3
inst✝² : Field 𝕜
n : Type
inst✝¹ : Fintype n
inst✝ : DecidableEq n
M : Matrix n n 𝕜
hn : Fintype.card n = 0
⊢ (List.map toMatrix []).prod * M * (List.map toMatrix []).prod = diagonal fun x => 1

Proof state:
case succ
𝕜 : Type u_3
inst✝² : Field 𝕜
r : ℕ
IH :
  ∀ (n : Type) [inst : Fintype n] [inst_1 : DecidableEq n] (M : Matrix n n 𝕜),
    Fintype.card n = r → ∃ L L' D, (List.map toMatrix L).prod * M * (List.map toMatrix L').prod = diagonal D
n : Type
inst✝¹ : Fintype n
inst✝ : DecidableEq n
M : Matrix n n 𝕜
hn : Fintype.card n = r + 1
e : n ≃ Fin r ⊕ Unit
⊢ ∃ L L' D, (List.map toMatrix L).prod * (reindexAlgEquiv 𝕜 𝕜 e) M * (List.map toMatrix L').prod = diagonal D

Tactic:
apply
  exists_list_transvec_mul_mul_list_transvec_eq_diagonal_induction fun N =>
    IH (Fin r) N (by simp)

Result:
no goals
-- Mathlib/RingTheory/Polynomial/Chebyshev.lean
theorem U_eq (n : ℤ) : U R n = 2 * X * U R (n - 1) - U R (n - 2)

Proof state:
R : Type u_1
inst✝ : CommRing R
n : ℤ
⊢ U R n = 2 * X * U R (n - 1) - U R (n - 2)

Tactic:
linear_combination (norm := ring_nf) U_add_two R (n - 2)

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Find.lean
theorem IsPrefix.findIdx_eq_of_findIdx_lt_length {l₁ l₂ : List α} {p : α → Bool} (h : l₁ <+: l₂)
    (lt : l₁.findIdx p < l₁.length) : l₂.findIdx p = l₁.findIdx p

Proof state:
α : Type u_1
l₁ l₂ : List α
p : α → Bool
h : ∃ t, l₁ ++ t = l₂
lt : findIdx p l₁ < l₁.length
⊢ findIdx p l₂ = findIdx p l₁

Tactic:
obtain ⟨t, rfl⟩ := h

Result:
case intro
α : Type u_1
l₁ : List α
p : α → Bool
lt : findIdx p l₁ < l₁.length
t : List α
⊢ findIdx p (l₁ ++ t) = findIdx p l₁

Proof state:
case intro.isFalse
α : Type u_1
l₁ : List α
p : α → Bool
lt : findIdx p l₁ < l₁.length
t : List α
h✝ : ¬∃ x, x ∈ l₁ ∧ p x = true
⊢ findIdx p t + l₁.length = findIdx p l₁

Tactic:
simp_all

Result:
no goals

Proof state:
α : Type u_1
l₁ l₂ : List α
p : α → Bool
h : l₁ <+: l₂
lt : findIdx p l₁ < l₁.length
⊢ findIdx p l₂ = findIdx p l₁

Tactic:
rw [IsPrefix] at h

Result:
α : Type u_1
l₁ l₂ : List α
p : α → Bool
h : ∃ t, l₁ ++ t = l₂
lt : findIdx p l₁ < l₁.length
⊢ findIdx p l₂ = findIdx p l₁

Proof state:
case intro
α : Type u_1
l₁ : List α
p : α → Bool
lt : findIdx p l₁ < l₁.length
t : List α
⊢ (if ∃ x, x ∈ l₁ ∧ p x = true then findIdx p l₁ else findIdx p t + l₁.length) = findIdx p l₁

Tactic:
split

Result:
case intro.isTrue
α : Type u_1
l₁ : List α
p : α → Bool
lt : findIdx p l₁ < l₁.length
t : List α
h✝ : ∃ x, x ∈ l₁ ∧ p x = true
⊢ findIdx p l₁ = findIdx p l₁

case intro.isFalse
α : Type u_1
l₁ : List α
p : α → Bool
lt : findIdx p l₁ < l₁.length
t : List α
h✝ : ¬∃ x, x ∈ l₁ ∧ p x = true
⊢ findIdx p t + l₁.length = findIdx p l₁

Proof state:
case intro.isTrue
α : Type u_1
l₁ : List α
p : α → Bool
lt : findIdx p l₁ < l₁.length
t : List α
h✝ : ∃ x, x ∈ l₁ ∧ p x = true
⊢ findIdx p l₁ = findIdx p l₁

Tactic:
rfl

Result:
no goals

Proof state:
case intro
α : Type u_1
l₁ : List α
p : α → Bool
lt : findIdx p l₁ < l₁.length
t : List α
⊢ findIdx p (l₁ ++ t) = findIdx p l₁

Tactic:
simp only [findIdx_append, findIdx_lt_length]

Result:
case intro
α : Type u_1
l₁ : List α
p : α → Bool
lt : findIdx p l₁ < l₁.length
t : List α
⊢ (if ∃ x, x ∈ l₁ ∧ p x = true then findIdx p l₁ else findIdx p t + l₁.length) = findIdx p l₁