harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Topology/Maps/Basic.lean
lemma of_continuous_injective_isClosedMap (h₁ : Continuous f) (h₂ : Injective f)
    (h₃ : IsClosedMap f) : IsClosedEmbedding f

Proof state:
X : Type u_1
Y : Type u_2
f : X → Y
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
h₁ : Continuous f
h₂ : Injective f
h₃ : IsClosedMap f
s : Set X
hs : IsOpen s
⊢ IsOpen s

Tactic:
refine ⟨(f '' sᶜ)ᶜ, (h₃ _ hs.isClosed_compl).isOpen_compl, ?_⟩

Result:
X : Type u_1
Y : Type u_2
f : X → Y
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
h₁ : Continuous f
h₂ : Injective f
h₃ : IsClosedMap f
s : Set X
hs : IsOpen s
⊢ f ⁻¹' (f '' sᶜ)ᶜ = s

Proof state:
X : Type u_1
Y : Type u_2
f : X → Y
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
h₁ : Continuous f
h₂ : Injective f
h₃ : IsClosedMap f
⊢ inst✝¹ = induced f inst✝

Tactic:
refine h₁.le_induced.antisymm fun s hs => ?_

Result:
X : Type u_1
Y : Type u_2
f : X → Y
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
h₁ : Continuous f
h₂ : Injective f
h₃ : IsClosedMap f
s : Set X
hs : IsOpen s
⊢ IsOpen s

Proof state:
X : Type u_1
Y : Type u_2
f : X → Y
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
h₁ : Continuous f
h₂ : Injective f
h₃ : IsClosedMap f
s : Set X
hs : IsOpen s
⊢ f ⁻¹' (f '' sᶜ)ᶜ = s

Tactic:
rw [preimage_compl, preimage_image_eq _ h₂, compl_compl]

Result:
no goals

Proof state:
X : Type u_1
Y : Type u_2
f : X → Y
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
h₁ : Continuous f
h₂ : Injective f
h₃ : IsClosedMap f
⊢ IsClosedEmbedding f

Tactic:
refine .of_isEmbedding_isClosedMap ⟨⟨?_⟩, h₂⟩ h₃

Result:
X : Type u_1
Y : Type u_2
f : X → Y
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
h₁ : Continuous f
h₂ : Injective f
h₃ : IsClosedMap f
⊢ inst✝¹ = induced f inst✝
-- Mathlib/CategoryTheory/Limits/Shapes/Images.lean
theorem image.map_comp [HasImageMap (sq ≫ sq')] :
    image.map (sq ≫ sq') = image.map sq ≫ image.map sq' :=
  show (HasImageMap.imageMap (sq ≫ sq')).map = (imageMapComp sq sq').map by
    congr; simp only [eq_iff_true_of_subsingleton]

Proof state:
case e_self
C : Type u
inst✝⁶ : Category.{v, u} C
f g : Arrow C
inst✝⁵ : HasImage f.hom
inst✝⁴ : HasImage g.hom
sq : f ⟶ g
inst✝³ : HasImageMap sq
h : Arrow C
inst✝² : HasImage h.hom
sq' : g ⟶ h
inst✝¹ : HasImageMap sq'
inst✝ : HasImageMap (sq ≫ sq')
⊢ HasImageMap.imageMap (sq ≫ sq') = imageMapComp sq sq'

Tactic:
simp only [eq_iff_true_of_subsingleton]

Result:
no goals

Proof state:
C : Type u
inst✝⁶ : Category.{v, u} C
f g : Arrow C
inst✝⁵ : HasImage f.hom
inst✝⁴ : HasImage g.hom
sq : f ⟶ g
inst✝³ : HasImageMap sq
h : Arrow C
inst✝² : HasImage h.hom
sq' : g ⟶ h
inst✝¹ : HasImageMap sq'
inst✝ : HasImageMap (sq ≫ sq')
⊢ (HasImageMap.imageMap (sq ≫ sq')).map = (imageMapComp sq sq').map

Tactic:
congr

Result:
case e_self
C : Type u
inst✝⁶ : Category.{v, u} C
f g : Arrow C
inst✝⁵ : HasImage f.hom
inst✝⁴ : HasImage g.hom
sq : f ⟶ g
inst✝³ : HasImageMap sq
h : Arrow C
inst✝² : HasImage h.hom
sq' : g ⟶ h
inst✝¹ : HasImageMap sq'
inst✝ : HasImageMap (sq ≫ sq')
⊢ HasImageMap.imageMap (sq ≫ sq') = imageMapComp sq sq'
-- Mathlib/Algebra/ContinuedFractions/Translations.lean
theorem exists_s_b_of_partDen {b : α}
    (nth_partDen_eq : g.partDens.get? n = some b) :
    ∃ gp, g.s.get? n = some gp ∧ gp.b = b

Proof state:
α : Type u_1
g : GenContFract α
n : ℕ
b : α
nth_partDen_eq : g.partDens.get? n = some b
⊢ ∃ gp, g.s.get? n = some gp ∧ gp.b = b

Tactic:
simpa [partDens, Stream'.Seq.map_get?] using nth_partDen_eq

Result:
no goals
-- Mathlib/.lake/packages/batteries/Batteries/Data/Fin/Fold.lean
theorem foldrM_eq_foldrM_finRange [Monad m] [LawfulMonad m] (f : Fin n → α → m α) (x) :
    foldrM n f x = (List.finRange n).foldrM f x

Proof state:
case zero
m : Type u_1 → Type u_2
α : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
x : α
f : Fin 0 → α → m α
⊢ foldrM 0 f x = List.foldrM f x (List.finRange 0)

Tactic:
simp

Result:
no goals

Proof state:
case succ
m : Type u_1 → Type u_2
α : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
x : α
n : Nat
ih : ∀ (f : Fin n → α → m α), foldrM n f x = List.foldrM f x (List.finRange n)
f : Fin (n + 1) → α → m α
⊢ foldrM (n + 1) f x = List.foldrM f x (List.finRange (n + 1))

Tactic:
rw [foldrM_succ, ih, List.finRange_succ, List.foldrM_cons, List.foldrM_map]

Result:
no goals

Proof state:
m : Type u_1 → Type u_2
n : Nat
α : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : Fin n → α → m α
x : α
⊢ foldrM n f x = List.foldrM f x (List.finRange n)

Tactic:
induction n with
| zero => simp
| succ n ih => rw [foldrM_succ, ih, List.finRange_succ, List.foldrM_cons, List.foldrM_map]

Result:
no goals
-- Mathlib/CategoryTheory/Limits/Shapes/ZeroMorphisms.lean
theorem zero_of_from_zero {X : C} (f : 0 ⟶ X) : f = 0

Proof state:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
X : C
f : 0 ⟶ X
⊢ f = 0

Tactic:
ext

Result:
no goals
-- Mathlib/Probability/Kernel/Composition/MapComap.lean
@[simp]
lemma map_id (κ : Kernel α β) : map κ id = κ

Proof state:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
⊢ κ.map id = κ

Tactic:
ext a

Result:
case h.h
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
a : α
s✝ : Set β
a✝ : MeasurableSet s✝
⊢ ((κ.map id) a) s✝ = (κ a) s✝

Proof state:
case h.h
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
a : α
s✝ : Set β
a✝ : MeasurableSet s✝
⊢ ((κ.map id) a) s✝ = (κ a) s✝

Tactic:
simp [map_apply, measurable_id]

Result:
no goals
-- Mathlib/RingTheory/Derivation/MapCoeffs.lean
@[simp]
lemma mapCoeffs_C (x : A) :
    d.mapCoeffs (C x) = .single A 0 (d x)

Proof state:
R : Type u_1
A : Type u_2
M : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : Algebra R A
inst✝² : AddCommGroup M
inst✝¹ : Module A M
inst✝ : Module R M
d : Derivation R A M
x : A
⊢ d.mapCoeffs (C x) = (PolynomialModule.single A 0) (d x)

Tactic:
simp [← monomial_zero_left]

Result:
no goals
-- Mathlib/Geometry/Manifold/BumpFunction.lean
theorem support_mem_nhds : support f ∈ 𝓝 c :=
  f.eventuallyEq_one.mono fun x hx => by rw [hx]; exact one_ne_zero

Proof state:
E : Type uE
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
H : Type uH
inst✝³ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type uM
inst✝² : TopologicalSpace M
inst✝¹ : ChartedSpace H M
c : M
f : SmoothBumpFunction I c
inst✝ : FiniteDimensional ℝ E
x : M
hx : ↑f x = 1 x
⊢ 1 x ≠ 0

Tactic:
exact one_ne_zero

Result:
no goals

Proof state:
E : Type uE
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
H : Type uH
inst✝³ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type uM
inst✝² : TopologicalSpace M
inst✝¹ : ChartedSpace H M
c : M
f : SmoothBumpFunction I c
inst✝ : FiniteDimensional ℝ E
x : M
hx : ↑f x = 1 x
⊢ ↑f x ≠ 0

Tactic:
rw [hx]

Result:
E : Type uE
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
H : Type uH
inst✝³ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type uM
inst✝² : TopologicalSpace M
inst✝¹ : ChartedSpace H M
c : M
f : SmoothBumpFunction I c
inst✝ : FiniteDimensional ℝ E
x : M
hx : ↑f x = 1 x
⊢ 1 x ≠ 0
-- Mathlib/Algebra/MvPolynomial/Degrees.lean
theorem monomial_le_degreeOf (i : σ) {f : MvPolynomial σ R} {m : σ →₀ ℕ} (h_m : m ∈ f.support) :
    m i ≤ degreeOf i f

Proof state:
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
i : σ
f : MvPolynomial σ R
m : σ →₀ ℕ
h_m : m ∈ f.support
⊢ m i ≤ degreeOf i f

Tactic:
rw [degreeOf_eq_sup i]

Result:
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
i : σ
f : MvPolynomial σ R
m : σ →₀ ℕ
h_m : m ∈ f.support
⊢ m i ≤ f.support.sup fun m => m i

Proof state:
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
i : σ
f : MvPolynomial σ R
m : σ →₀ ℕ
h_m : m ∈ f.support
⊢ m i ≤ f.support.sup fun m => m i

Tactic:
apply Finset.le_sup h_m

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Sublist.lean
theorem subset_reverse {l₁ l₂ : List α} : l₁ ⊆ reverse l₂ ↔ l₁ ⊆ l₂

Proof state:
α : Type u_1
l₁ l₂ : List α
⊢ l₁ ⊆ l₂.reverse ↔ l₁ ⊆ l₂

Tactic:
simp [subset_def]

Result:
no goals
-- Mathlib/Algebra/Group/Pointwise/Set/Basic.lean
@[to_additive]
lemma smul_set_sUnion (a : α) (S : Set (Set β)) : a • ⋃₀ S = ⋃ s ∈ S, a • s

Proof state:
α : Type u_2
β : Type u_3
inst✝ : SMul α β
a : α
S : Set (Set β)
⊢ a • ⋃₀ S = ⋃ s ∈ S, a • s

Tactic:
rw [sUnion_eq_biUnion, smul_set_iUnion₂]

Result:
no goals
-- Mathlib/Algebra/Order/Floor.lean
theorem floor_of_nonpos (ha : a ≤ 0) : ⌊a⌋₊ = 0 :=
  ha.lt_or_eq.elim FloorSemiring.floor_of_neg <| by
    rintro rfl
    exact floor_zero

Proof state:
α : Type u_2
inst✝¹ : LinearOrderedSemiring α
inst✝ : FloorSemiring α
a : α
ha : a ≤ 0
⊢ a = 0 → ⌊a⌋₊ = 0

Tactic:
rintro rfl

Result:
α : Type u_2
inst✝¹ : LinearOrderedSemiring α
inst✝ : FloorSemiring α
ha : 0 ≤ 0
⊢ ⌊0⌋₊ = 0

Proof state:
α : Type u_2
inst✝¹ : LinearOrderedSemiring α
inst✝ : FloorSemiring α
ha : 0 ≤ 0
⊢ ⌊0⌋₊ = 0

Tactic:
exact floor_zero

Result:
no goals
-- Mathlib/SetTheory/Game/PGame.lean
theorem zero_lf_neg_iff {x : PGame} : 0 ⧏ -x ↔ x ⧏ 0

Proof state:
x : PGame
⊢ 0 ⧏ -x ↔ x ⧏ 0

Tactic:
rw [lf_neg_iff, neg_zero]

Result:
no goals
-- Mathlib/RingTheory/Valuation/Basic.lean
theorem map_add' : ∀ x y, v (x + y) ≤ v x ∨ v (x + y) ≤ v y

Proof state:
R : Type u_3
Γ₀ : Type u_4
inst✝¹ : Ring R
inst✝ : LinearOrderedCommMonoidWithZero Γ₀
v : Valuation R Γ₀
x y : R
⊢ v (x + y) ≤ v x ∨ v (x + y) ≤ v y

Tactic:
rw [← le_max_iff, ← ge_iff_le]

Result:
R : Type u_3
Γ₀ : Type u_4
inst✝¹ : Ring R
inst✝ : LinearOrderedCommMonoidWithZero Γ₀
v : Valuation R Γ₀
x y : R
⊢ v x ⊔ v y ≥ v (x + y)

Proof state:
R : Type u_3
Γ₀ : Type u_4
inst✝¹ : Ring R
inst✝ : LinearOrderedCommMonoidWithZero Γ₀
v : Valuation R Γ₀
x y : R
⊢ v x ⊔ v y ≥ v (x + y)

Tactic:
apply map_add

Result:
no goals

Proof state:
R : Type u_3
Γ₀ : Type u_4
inst✝¹ : Ring R
inst✝ : LinearOrderedCommMonoidWithZero Γ₀
v : Valuation R Γ₀
⊢ ∀ (x y : R), v (x + y) ≤ v x ∨ v (x + y) ≤ v y

Tactic:
intro x y

Result:
R : Type u_3
Γ₀ : Type u_4
inst✝¹ : Ring R
inst✝ : LinearOrderedCommMonoidWithZero Γ₀
v : Valuation R Γ₀
x y : R
⊢ v (x + y) ≤ v x ∨ v (x + y) ≤ v y
-- Mathlib/GroupTheory/GroupExtension/Defs.lean
theorem rightHom_comp_splitting : S.rightHom.comp s = MonoidHom.id G

Proof state:
N : Type u_1
E : Type u_2
G : Type u_3
inst✝² : Group N
inst✝¹ : Group E
inst✝ : Group G
S : GroupExtension N E G
s : S.Splitting
⊢ S.rightHom.comp ↑s = MonoidHom.id G

Tactic:
ext g

Result:
case h
N : Type u_1
E : Type u_2
G : Type u_3
inst✝² : Group N
inst✝¹ : Group E
inst✝ : Group G
S : GroupExtension N E G
s : S.Splitting
g : G
⊢ (S.rightHom.comp ↑s) g = (MonoidHom.id G) g

Proof state:
case h
N : Type u_1
E : Type u_2
G : Type u_3
inst✝² : Group N
inst✝¹ : Group E
inst✝ : Group G
S : GroupExtension N E G
s : S.Splitting
g : G
⊢ (S.rightHom.comp ↑s) g = (MonoidHom.id G) g

Tactic:
simp only [MonoidHom.comp_apply, MonoidHom.id_apply, MonoidHom.coe_coe, rightHom_splitting]

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/IncMatrix.lean
theorem incMatrix_of_mem_incidenceSet (h : e ∈ G.incidenceSet a) : G.incMatrix R a e = 1

Proof state:
R : Type u_1
α : Type u_2
G : SimpleGraph α
inst✝ : MulZeroOneClass R
a : α
e : Sym2 α
h : e ∈ G.incidenceSet a
⊢ incMatrix R G a e = 1

Tactic:
rw [incMatrix_apply, Set.indicator_of_mem h, Pi.one_apply]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem getLsbD_append {x : BitVec n} {y : BitVec m} :
    getLsbD (x ++ y) i = if i < m then getLsbD y i else getLsbD x (i - m)

Proof state:
n m i : Nat
x : BitVec n
y : BitVec m
⊢ (!decide (i < m) && x.getLsbD (i - m) || y.getLsbD i) = if i < m then y.getLsbD i else x.getLsbD (i - m)

Tactic:
by_cases h : i < m

Result:
case pos
n m i : Nat
x : BitVec n
y : BitVec m
h : i < m
⊢ (!decide (i < m) && x.getLsbD (i - m) || y.getLsbD i) = if i < m then y.getLsbD i else x.getLsbD (i - m)

case neg
n m i : Nat
x : BitVec n
y : BitVec m
h : ¬i < m
⊢ (!decide (i < m) && x.getLsbD (i - m) || y.getLsbD i) = if i < m then y.getLsbD i else x.getLsbD (i - m)

Proof state:
case neg
n m i : Nat
x : BitVec n
y : BitVec m
h : ¬i < m
⊢ (!decide (i < m) && x.getLsbD (i - m) || y.getLsbD i) = if i < m then y.getLsbD i else x.getLsbD (i - m)

Tactic:
simp_all [h]

Result:
no goals

Proof state:
case pos
n m i : Nat
x : BitVec n
y : BitVec m
h : i < m
⊢ (!decide (i < m) && x.getLsbD (i - m) || y.getLsbD i) = if i < m then y.getLsbD i else x.getLsbD (i - m)

Tactic:
simp [h]

Result:
no goals

Proof state:
n m i : Nat
x : BitVec n
y : BitVec m
⊢ (x ++ y).getLsbD i = if i < m then y.getLsbD i else x.getLsbD (i - m)

Tactic:
simp only [append_def, getLsbD_or, getLsbD_shiftLeftZeroExtend, getLsbD_setWidth']

Result:
n m i : Nat
x : BitVec n
y : BitVec m
⊢ (!decide (i < m) && x.getLsbD (i - m) || y.getLsbD i) = if i < m then y.getLsbD i else x.getLsbD (i - m)
-- Mathlib/CategoryTheory/SmallObject/IsCardinalForSmallObjectArgument.lean
lemma llp_rlp_ιObj : I.rlp.llp (ιObj I κ f)

Proof state:
C : Type u
inst✝³ : Category.{v, u} C
I : MorphismProperty C
κ : Cardinal.{w}
inst✝² : Fact κ.IsRegular
inst✝¹ : OrderBot κ.ord.toType
inst✝ : I.IsCardinalForSmallObjectArgument κ
X Y : C
f : X ⟶ Y
⊢ I.rlp.llp (ιObj I κ f)

Tactic:
apply I.transfiniteCompositionsOfShape_pushouts_coproducts_le_llp_rlp κ.ord.toType

Result:
case a
C : Type u
inst✝³ : Category.{v, u} C
I : MorphismProperty C
κ : Cardinal.{w}
inst✝² : Fact κ.IsRegular
inst✝¹ : OrderBot κ.ord.toType
inst✝ : I.IsCardinalForSmallObjectArgument κ
X Y : C
f : X ⟶ Y
⊢ (coproducts.{w, v, u} I).pushouts.transfiniteCompositionsOfShape κ.ord.toType (ιObj I κ f)

Proof state:
case a
C : Type u
inst✝³ : Category.{v, u} C
I : MorphismProperty C
κ : Cardinal.{w}
inst✝² : Fact κ.IsRegular
inst✝¹ : OrderBot κ.ord.toType
inst✝ : I.IsCardinalForSmallObjectArgument κ
X Y : C
f : X ⟶ Y
⊢ (coproducts.{w, v, u} I).pushouts.transfiniteCompositionsOfShape κ.ord.toType (ιObj I κ f)

Tactic:
apply transfiniteCompositionsOfShape_ιObj

Result:
no goals
-- Mathlib/Data/Multiset/Bind.lean
theorem rel_join {r : α → β → Prop} {s t} (h : Rel (Rel r) s t) : Rel r s.join t.join

Proof state:
case zero
α : Type u_1
β : Type v
r : α → β → Prop
s : Multiset (Multiset α)
t : Multiset (Multiset β)
⊢ Rel r (join 0) (join 0)

Tactic:
simp

Result:
no goals

Proof state:
case cons
α : Type u_1
β : Type v
r : α → β → Prop
s : Multiset (Multiset α)
t : Multiset (Multiset β)
a✝ : Multiset α
b✝ : Multiset β
as✝ : Multiset (Multiset α)
bs✝ : Multiset (Multiset β)
hab : Rel r a✝ b✝
hst : Rel (Rel r) as✝ bs✝
ih : Rel r as✝.join bs✝.join
⊢ Rel r (a✝ ::ₘ as✝).join (b✝ ::ₘ bs✝).join

Tactic:
simpa using hab.add ih

Result:
no goals

Proof state:
α : Type u_1
β : Type v
r : α → β → Prop
s : Multiset (Multiset α)
t : Multiset (Multiset β)
h : Rel (Rel r) s t
⊢ Rel r s.join t.join

Tactic:
induction h with
| zero => simp
| cons hab hst ih => simpa using hab.add ih

Result:
no goals
-- Mathlib/Topology/ContinuousMap/Ideals.lean
theorem setOfIdeal_eq_compl_singleton (I : Ideal C(X, 𝕜)) [hI : I.IsMaximal] :
    ∃ x : X, setOfIdeal I = {x}ᶜ

Proof state:
X : Type u_1
𝕜 : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : TopologicalSpace X
inst✝¹ : CompactSpace X
inst✝ : T2Space X
I : Ideal C(X, 𝕜)
hI : I.IsMaximal
h : (idealOfSet 𝕜 (setOfIdeal I)).IsMaximal
⊢ ∃ x, setOfIdeal I = {x}ᶜ

Tactic:
obtain ⟨x, hx⟩ := Opens.isCoatom_iff.1 ((idealOfSet_isMaximal_iff 𝕜 (opensOfIdeal I)).1 h)

Result:
case intro
X : Type u_1
𝕜 : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : TopologicalSpace X
inst✝¹ : CompactSpace X
inst✝ : T2Space X
I : Ideal C(X, 𝕜)
hI : I.IsMaximal
h : (idealOfSet 𝕜 (setOfIdeal I)).IsMaximal
x : X
hx : opensOfIdeal I = (Closeds.singleton x).compl
⊢ ∃ x, setOfIdeal I = {x}ᶜ

Proof state:
X : Type u_1
𝕜 : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : TopologicalSpace X
inst✝¹ : CompactSpace X
inst✝ : T2Space X
I : Ideal C(X, 𝕜)
hI : I.IsMaximal
⊢ ∃ x, setOfIdeal I = {x}ᶜ

Tactic:
have h : (idealOfSet 𝕜 (setOfIdeal I)).IsMaximal :=
  (idealOfSet_ofIdeal_isClosed (inferInstance : IsClosed (I : Set C(X, 𝕜)))).symm ▸ hI

Result:
X : Type u_1
𝕜 : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : TopologicalSpace X
inst✝¹ : CompactSpace X
inst✝ : T2Space X
I : Ideal C(X, 𝕜)
hI : I.IsMaximal
h : (idealOfSet 𝕜 (setOfIdeal I)).IsMaximal
⊢ ∃ x, setOfIdeal I = {x}ᶜ

Proof state:
case intro
X : Type u_1
𝕜 : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : TopologicalSpace X
inst✝¹ : CompactSpace X
inst✝ : T2Space X
I : Ideal C(X, 𝕜)
hI : I.IsMaximal
h : (idealOfSet 𝕜 (setOfIdeal I)).IsMaximal
x : X
hx : opensOfIdeal I = (Closeds.singleton x).compl
⊢ ∃ x, setOfIdeal I = {x}ᶜ

Tactic:
exact ⟨x, congr_arg (fun (s : Opens X) => (s : Set X)) hx⟩

Result:
no goals
-- Mathlib/Data/Real/Sqrt.lean
theorem sqrt_sq_eq_abs (x : ℝ) : √(x ^ 2) = |x|

Proof state:
x : ℝ
⊢ √(x ^ 2) = |x|

Tactic:
rw [sq, sqrt_mul_self_eq_abs]

Result:
no goals
-- Mathlib/AlgebraicGeometry/EllipticCurve/Weierstrass.lean
lemma b₂_of_char_three : W.b₂ = W.a₁ ^ 2 + W.a₂

Proof state:
R : Type u
inst✝¹ : CommRing R
W : WeierstrassCurve R
inst✝ : CharP R 3
⊢ W.b₂ = W.a₁ ^ 2 + W.a₂

Tactic:
rw [b₂]

Result:
R : Type u
inst✝¹ : CommRing R
W : WeierstrassCurve R
inst✝ : CharP R 3
⊢ W.a₁ ^ 2 + 4 * W.a₂ = W.a₁ ^ 2 + W.a₂

Proof state:
R : Type u
inst✝¹ : CommRing R
W : WeierstrassCurve R
inst✝ : CharP R 3
⊢ W.a₁ ^ 2 + 4 * W.a₂ = W.a₁ ^ 2 + W.a₂

Tactic:
linear_combination W.a₂ * CharP.cast_eq_zero R 3

Result:
no goals
-- Mathlib/Topology/Category/TopCat/Opens.lean
theorem op_map_id_obj (U : (Opens X)ᵒᵖ) : (map (𝟙 X)).op.obj U = U

Proof state:
X : TopCat
U : (Opens ↑X)ᵒᵖ
⊢ (map (𝟙 X)).op.obj U = U

Tactic:
simp

Result:
no goals
-- Mathlib/Geometry/Manifold/MFDeriv/Basic.lean
theorem tangentMapWithin_subset {p : TangentBundle I M} (st : s ⊆ t)
    (hs : UniqueMDiffWithinAt I s p.1) (h : MDifferentiableWithinAt I I' f t p.1) :
    tangentMapWithin I I' f s p = tangentMapWithin I I' f t p

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'
s t : Set M
p : TangentBundle I M
st : s ⊆ t
hs : UniqueMDiffWithinAt I s p.proj
h : MDifferentiableWithinAt I I' f t p.proj
⊢ tangentMapWithin I I' f s p = tangentMapWithin I I' f t p

Tactic:
simp only [tangentMapWithin, mfld_simps]

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'
s t : Set M
p : TangentBundle I M
st : s ⊆ t
hs : UniqueMDiffWithinAt I s p.proj
h : MDifferentiableWithinAt I I' f t p.proj
⊢ (mfderivWithin I I' f s p.proj) p.snd = (mfderivWithin I I' f t p.proj) p.snd

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'
s t : Set M
p : TangentBundle I M
st : s ⊆ t
hs : UniqueMDiffWithinAt I s p.proj
h : MDifferentiableWithinAt I I' f t p.proj
⊢ (mfderivWithin I I' f s p.proj) p.snd = (mfderivWithin I I' f t p.proj) p.snd

Tactic:
rw [mfderivWithin_subset st hs h]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem msb_intMin {w : Nat} : (intMin w).msb = decide (0 < w)

Proof state:
w : Nat
⊢ (intMin w).msb = decide (0 < w)

Tactic:
simp only [msb_eq_decide, toNat_intMin, decide_eq_decide]

Result:
w : Nat
⊢ 2 ^ (w - 1) ≤ 2 ^ (w - 1) % 2 ^ w ↔ 0 < w

Proof state:
w : Nat
⊢ 2 ^ (w - 1) ≤ 2 ^ (w - 1) % 2 ^ w ↔ 0 < w

Tactic:
by_cases h : 0 < w <;> simp_all

Result:
no goals
-- Mathlib/Data/Int/GCD.lean
theorem dvd_of_dvd_mul_left_of_gcd_one {a b c : ℤ} (habc : a ∣ b * c) (hab : gcd a c = 1) :
    a ∣ b

Proof state:
a b c : ℤ
habc : a ∣ b * c
hab : a.gcd c = 1
this : ↑(a.gcd c) = a * a.gcdA c + c * a.gcdB c
⊢ a ∣ b

Tactic:
simp only [hab, Int.ofNat_zero, Int.ofNat_succ, zero_add] at this

Result:
a b c : ℤ
habc : a ∣ b * c
hab : a.gcd c = 1
this : 1 = a * a.gcdA c + c * a.gcdB c
⊢ a ∣ b

Proof state:
a b c : ℤ
habc : a ∣ b * c
hab : a.gcd c = 1
this : 1 = a * a.gcdA c + c * a.gcdB c
⊢ a ∣ b

Tactic:
have : b * a * gcdA a c + b * c * gcdB a c = b := by simp [mul_assoc, ← Int.mul_add, ← this]

Result:
a b c : ℤ
habc : a ∣ b * c
hab : a.gcd c = 1
this✝ : 1 = a * a.gcdA c + c * a.gcdB c
this : b * a * a.gcdA c + b * c * a.gcdB c = b
⊢ a ∣ b

Proof state:
a b c : ℤ
habc : a ∣ b * c
hab : a.gcd c = 1
⊢ a ∣ b

Tactic:
have := gcd_eq_gcd_ab a c

Result:
a b c : ℤ
habc : a ∣ b * c
hab : a.gcd c = 1
this : ↑(a.gcd c) = a * a.gcdA c + c * a.gcdB c
⊢ a ∣ b

Proof state:
a b c : ℤ
habc : a ∣ b * c
hab : a.gcd c = 1
this : 1 = a * a.gcdA c + c * a.gcdB c
⊢ b * a * a.gcdA c + b * c * a.gcdB c = b

Tactic:
simp [mul_assoc, ← Int.mul_add, ← this]

Result:
no goals

Proof state:
a b c : ℤ
habc : a ∣ b * c
hab : a.gcd c = 1
this✝ : 1 = a * a.gcdA c + c * a.gcdB c
this : b * a * a.gcdA c + b * c * a.gcdB c = b
⊢ a ∣ b * a * a.gcdA c + b * c * a.gcdB c

Tactic:
exact Int.dvd_add (dvd_mul_of_dvd_left (dvd_mul_left a b) _) (dvd_mul_of_dvd_left habc _)

Result:
no goals

Proof state:
a b c : ℤ
habc : a ∣ b * c
hab : a.gcd c = 1
this✝ : 1 = a * a.gcdA c + c * a.gcdB c
this : b * a * a.gcdA c + b * c * a.gcdB c = b
⊢ a ∣ b

Tactic:
rw [← this]

Result:
a b c : ℤ
habc : a ∣ b * c
hab : a.gcd c = 1
this✝ : 1 = a * a.gcdA c + c * a.gcdB c
this : b * a * a.gcdA c + b * c * a.gcdB c = b
⊢ a ∣ b * a * a.gcdA c + b * c * a.gcdB c
-- Mathlib/Analysis/Calculus/Deriv/Comp.lean
theorem HasDerivAt.scomp_hasDerivWithinAt_of_eq (hg : HasDerivAt g₁ g₁' y)
    (hh : HasDerivWithinAt h h' s x) (hy : y = h x) :
    HasDerivWithinAt (g₁ ∘ h) (h' • g₁') s x

Proof state:
𝕜 : Type u
inst✝⁶ : NontriviallyNormedField 𝕜
F : Type v
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
x : 𝕜
s : Set 𝕜
𝕜' : Type u_1
inst✝³ : NontriviallyNormedField 𝕜'
inst✝² : NormedAlgebra 𝕜 𝕜'
inst✝¹ : NormedSpace 𝕜' F
inst✝ : IsScalarTower 𝕜 𝕜' F
h : 𝕜 → 𝕜'
h' : 𝕜'
g₁ : 𝕜' → F
g₁' : F
y : 𝕜'
hg : HasDerivAt g₁ g₁' y
hh : HasDerivWithinAt h h' s x
hy : y = h x
⊢ HasDerivWithinAt (g₁ ∘ h) (h' • g₁') s x

Tactic:
rw [hy] at hg

Result:
𝕜 : Type u
inst✝⁶ : NontriviallyNormedField 𝕜
F : Type v
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
x : 𝕜
s : Set 𝕜
𝕜' : Type u_1
inst✝³ : NontriviallyNormedField 𝕜'
inst✝² : NormedAlgebra 𝕜 𝕜'
inst✝¹ : NormedSpace 𝕜' F
inst✝ : IsScalarTower 𝕜 𝕜' F
h : 𝕜 → 𝕜'
h' : 𝕜'
g₁ : 𝕜' → F
g₁' : F
y : 𝕜'
hg : HasDerivAt g₁ g₁' (h x)
hh : HasDerivWithinAt h h' s x
hy : y = h x
⊢ HasDerivWithinAt (g₁ ∘ h) (h' • g₁') s x

Proof state:
𝕜 : Type u
inst✝⁶ : NontriviallyNormedField 𝕜
F : Type v
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
x : 𝕜
s : Set 𝕜
𝕜' : Type u_1
inst✝³ : NontriviallyNormedField 𝕜'
inst✝² : NormedAlgebra 𝕜 𝕜'
inst✝¹ : NormedSpace 𝕜' F
inst✝ : IsScalarTower 𝕜 𝕜' F
h : 𝕜 → 𝕜'
h' : 𝕜'
g₁ : 𝕜' → F
g₁' : F
y : 𝕜'
hg : HasDerivAt g₁ g₁' (h x)
hh : HasDerivWithinAt h h' s x
hy : y = h x
⊢ HasDerivWithinAt (g₁ ∘ h) (h' • g₁') s x

Tactic:
exact hg.scomp_hasDerivWithinAt x hh

Result:
no goals