harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/RingTheory/Jacobson/Ring.lean
theorem RingHom.finite_of_algHom_finiteType_of_isJacobsonRing
    {K L A : Type*} [CommRing K] [Field L] [CommRing A]
    [IsJacobsonRing K] [IsNoetherianRing K] [Nontrivial A]
    (f : K →+* L) (g : L →+* A) (hfg : (g.comp f).FiniteType) :
    f.Finite

Proof state:
K : Type u_1
L : Type u_2
A : Type u_3
inst✝⁵ : CommRing K
inst✝⁴ : Field L
inst✝³ : CommRing A
inst✝² : IsJacobsonRing K
inst✝¹ : IsNoetherianRing K
inst✝ : Nontrivial A
f : K →+* L
g : L →+* A
hfg : (g.comp f).FiniteType
algInst✝¹ : Algebra K L := f.toAlgebra
algInst✝ : Algebra K A := (g.comp f).toAlgebra
algebraizeInst✝ : Algebra.FiniteType K A
⊢ f.Finite

Tactic:
exact finite_of_algHom_finiteType_of_isJacobsonRing ⟨g, fun _ ↦ rfl⟩

Result:
no goals

Proof state:
K : Type u_1
L : Type u_2
A : Type u_3
inst✝⁵ : CommRing K
inst✝⁴ : Field L
inst✝³ : CommRing A
inst✝² : IsJacobsonRing K
inst✝¹ : IsNoetherianRing K
inst✝ : Nontrivial A
f : K →+* L
g : L →+* A
hfg : (g.comp f).FiniteType
⊢ f.Finite

Tactic:
algebraize [f, (g.comp f)]

Result:
K : Type u_1
L : Type u_2
A : Type u_3
inst✝⁵ : CommRing K
inst✝⁴ : Field L
inst✝³ : CommRing A
inst✝² : IsJacobsonRing K
inst✝¹ : IsNoetherianRing K
inst✝ : Nontrivial A
f : K →+* L
g : L →+* A
hfg : (g.comp f).FiniteType
algInst✝¹ : Algebra K L := f.toAlgebra
algInst✝ : Algebra K A := (g.comp f).toAlgebra
algebraizeInst✝ : Algebra.FiniteType K A
⊢ f.Finite
-- Mathlib/Data/Finset/Sups.lean
lemma compls_subset_iff : sᶜˢ ⊆ t ↔ s ⊆ tᶜˢ

Proof state:
α : Type u_2
inst✝ : BooleanAlgebra α
s t : Finset α
⊢ sᶜˢ ⊆ t ↔ s ⊆ tᶜˢ

Tactic:
rw [← compls_subset_compls, compls_compls]

Result:
no goals
-- Mathlib/Analysis/InnerProductSpace/TwoDim.lean
theorem rightAngleRotation_rightAngleRotation (x : E) : J (J x) = -x

Proof state:
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
x : E
⊢ o.rightAngleRotation (o.rightAngleRotation x) = -x

Tactic:
rw [rightAngleRotation]

Result:
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
x : E
⊢ (LinearIsometryEquiv.ofLinearIsometry o.rightAngleRotationAux₂ (-o.rightAngleRotationAux₁) ⋯ ⋯)
      ((LinearIsometryEquiv.ofLinearIsometry o.rightAngleRotationAux₂ (-o.rightAngleRotationAux₁) ⋯ ⋯) x) =
    -x

Proof state:
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
x : E
⊢ (LinearIsometryEquiv.ofLinearIsometry o.rightAngleRotationAux₂ (-o.rightAngleRotationAux₁) ⋯ ⋯)
      ((LinearIsometryEquiv.ofLinearIsometry o.rightAngleRotationAux₂ (-o.rightAngleRotationAux₁) ⋯ ⋯) x) =
    -x

Tactic:
exact o.rightAngleRotationAux₁_rightAngleRotationAux₁ x

Result:
no goals
-- Mathlib/Topology/SeparatedMap.lean
theorem IsLocallyInjective_iff_isOpenEmbedding {f : X → Y} :
    IsLocallyInjective f ↔ IsOpenEmbedding (toPullbackDiag f)

Proof state:
X : Type u_1
Y : Type u_2
inst✝ : TopologicalSpace X
f : X → Y
⊢ IsLocallyInjective f ↔ IsOpenEmbedding (toPullbackDiag f)

Tactic:
rw [isLocallyInjective_iff_isOpen_diagonal, ← range_toPullbackDiag]

Result:
X : Type u_1
Y : Type u_2
inst✝ : TopologicalSpace X
f : X → Y
⊢ IsOpen (Set.range (toPullbackDiag f)) ↔ IsOpenEmbedding (toPullbackDiag f)

Proof state:
X : Type u_1
Y : Type u_2
inst✝ : TopologicalSpace X
f : X → Y
⊢ IsOpen (Set.range (toPullbackDiag f)) ↔ IsOpenEmbedding (toPullbackDiag f)

Tactic:
exact ⟨fun h ↦ ⟨.toPullbackDiag f, h⟩, fun h ↦ h.isOpen_range⟩

Result:
no goals
-- Mathlib/Data/Finset/Option.lean
theorem map_some_eraseNone [DecidableEq (Option α)] (s : Finset (Option α)) :
    (eraseNone s).map Embedding.some = s.erase none

Proof state:
α : Type u_1
inst✝ : DecidableEq (Option α)
s : Finset (Option α)
⊢ map Embedding.some (eraseNone s) = s.erase none

Tactic:
rw [map_eq_image, Embedding.some_apply, image_some_eraseNone]

Result:
no goals
-- Mathlib/AlgebraicTopology/SimplicialSet/HomotopyCat.lean
@[reassoc (attr := simp)]
lemma δ₂_two_comp_σ₂_one : δ₂ (2 : Fin 3) ≫ σ₂ 1 = 𝟙 _ := SimplexCategory.δ_comp_σ_succ' (by decide)

Proof state:
⊢ 2 = Fin.succ 1

Tactic:
decide

Result:
no goals
-- Mathlib/Algebra/Category/Semigrp/Basic.lean
@[to_additive]
lemma inv_hom_apply {M N : MagmaCat} (e : M ≅ N) (x : M) : e.inv (e.hom x) = x

Proof state:
M N : MagmaCat
e : M ≅ N
x : ↑M
⊢ (ConcreteCategory.hom e.inv) ((ConcreteCategory.hom e.hom) x) = x

Tactic:
simp

Result:
no goals
-- Mathlib/Algebra/Homology/Double.lean
@[simp, reassoc]
lemma mkHomFromDouble_f₁ :
    (mkHomFromDouble hi₀₁ h φ₀ φ₁ comm hφ).f i₁ =
      (doubleXIso₁ f hi₀₁ h).hom ≫ φ₁

Proof state:
C : Type u_1
inst✝² : Category.{u_3, u_1} C
inst✝¹ : HasZeroMorphisms C
inst✝ : HasZeroObject C
X₀ X₁ : C
f : X₀ ⟶ X₁
ι : Type u_2
c : ComplexShape ι
i₀ i₁ : ι
hi₀₁ : c.Rel i₀ i₁
h : i₀ ≠ i₁
K : HomologicalComplex C c
φ₀ : X₀ ⟶ K.X i₀
φ₁ : X₁ ⟶ K.X i₁
comm : φ₀ ≫ K.d i₀ i₁ = f ≫ φ₁
hφ : ∀ (k : ι), c.Rel i₁ k → φ₁ ≫ K.d i₁ k = 0
⊢ (mkHomFromDouble hi₀₁ h φ₀ φ₁ comm hφ).f i₁ = (doubleXIso₁ f hi₀₁ h).hom ≫ φ₁

Tactic:
dsimp [mkHomFromDouble]

Result:
C : Type u_1
inst✝² : Category.{u_3, u_1} C
inst✝¹ : HasZeroMorphisms C
inst✝ : HasZeroObject C
X₀ X₁ : C
f : X₀ ⟶ X₁
ι : Type u_2
c : ComplexShape ι
i₀ i₁ : ι
hi₀₁ : c.Rel i₀ i₁
h : i₀ ≠ i₁
K : HomologicalComplex C c
φ₀ : X₀ ⟶ K.X i₀
φ₁ : X₁ ⟶ K.X i₁
comm : φ₀ ≫ K.d i₀ i₁ = f ≫ φ₁
hφ : ∀ (k : ι), c.Rel i₁ k → φ₁ ≫ K.d i₁ k = 0
⊢ (if hk₀ : i₁ = i₀ then eqToHom ⋯ ≫ (doubleXIso₀ f hi₀₁).hom ≫ φ₀ ≫ eqToHom ⋯
    else if i₁ = i₁ then 𝟙 ((double f hi₀₁).X i₁) ≫ (doubleXIso₁ f hi₀₁ h).hom ≫ φ₁ ≫ 𝟙 (K.X i₁) else 0) =
    (doubleXIso₁ f hi₀₁ h).hom ≫ φ₁

Proof state:
C : Type u_1
inst✝² : Category.{u_3, u_1} C
inst✝¹ : HasZeroMorphisms C
inst✝ : HasZeroObject C
X₀ X₁ : C
f : X₀ ⟶ X₁
ι : Type u_2
c : ComplexShape ι
i₀ i₁ : ι
hi₀₁ : c.Rel i₀ i₁
h : i₀ ≠ i₁
K : HomologicalComplex C c
φ₀ : X₀ ⟶ K.X i₀
φ₁ : X₁ ⟶ K.X i₁
comm : φ₀ ≫ K.d i₀ i₁ = f ≫ φ₁
hφ : ∀ (k : ι), c.Rel i₁ k → φ₁ ≫ K.d i₁ k = 0
⊢ (if hk₀ : i₁ = i₀ then eqToHom ⋯ ≫ (doubleXIso₀ f hi₀₁).hom ≫ φ₀ ≫ eqToHom ⋯
    else if i₁ = i₁ then 𝟙 ((double f hi₀₁).X i₁) ≫ (doubleXIso₁ f hi₀₁ h).hom ≫ φ₁ ≫ 𝟙 (K.X i₁) else 0) =
    (doubleXIso₁ f hi₀₁ h).hom ≫ φ₁

Tactic:
rw [dif_neg h.symm, if_pos rfl, id_comp, comp_id]

Result:
no goals
-- Mathlib/CategoryTheory/SmallObject/Iteration/FunctorOfCocone.lean
lemma ofCocone_obj_eq_pt :
    (ofCocone c).obj ⟨j, by simp⟩ = c.pt :=
  dif_neg (by simp)

Proof state:
C : Type u_1
inst✝¹ : Category.{?u.36302, u_1} C
J : Type u
inst✝ : LinearOrder J
j : J
F : ↑(Set.Iio j) ⥤ C
c : Cocone F
⊢ j ∈ Set.Iic j

Tactic:
simp

Result:
no goals

Proof state:
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
J : Type u
inst✝ : LinearOrder J
j : J
F : ↑(Set.Iio j) ⥤ C
c : Cocone F
⊢ ¬↑⟨j, ⋯⟩ < j

Tactic:
simp

Result:
no goals
-- Mathlib/Algebra/BigOperators/Field.lean
lemma Finset.sum_div (s : Finset ι) (f : ι → K) (a : K) :
    (∑ i ∈ s, f i) / a = ∑ i ∈ s, f i / a

Proof state:
ι : Type u_1
K : Type u_2
inst✝ : DivisionSemiring K
s : Finset ι
f : ι → K
a : K
⊢ (∑ i ∈ s, f i) / a = ∑ i ∈ s, f i / a

Tactic:
simp only [div_eq_mul_inv, sum_mul]

Result:
no goals
-- Mathlib/Algebra/Ring/Equiv.lean
theorem toNonUnitalRingHomm_comp_symm_toNonUnitalRingHom (e : R ≃+* S) :
    e.toNonUnitalRingHom.comp e.symm.toNonUnitalRingHom = NonUnitalRingHom.id _

Proof state:
case a
R : Type u_4
S : Type u_5
inst✝¹ : NonUnitalNonAssocSemiring R
inst✝ : NonUnitalNonAssocSemiring S
e : R ≃+* S
x✝ : S
⊢ (e.toNonUnitalRingHom.comp e.symm.toNonUnitalRingHom) x✝ = (NonUnitalRingHom.id S) x✝

Tactic:
simp

Result:
no goals

Proof state:
R : Type u_4
S : Type u_5
inst✝¹ : NonUnitalNonAssocSemiring R
inst✝ : NonUnitalNonAssocSemiring S
e : R ≃+* S
⊢ e.toNonUnitalRingHom.comp e.symm.toNonUnitalRingHom = NonUnitalRingHom.id S

Tactic:
ext

Result:
case a
R : Type u_4
S : Type u_5
inst✝¹ : NonUnitalNonAssocSemiring R
inst✝ : NonUnitalNonAssocSemiring S
e : R ≃+* S
x✝ : S
⊢ (e.toNonUnitalRingHom.comp e.symm.toNonUnitalRingHom) x✝ = (NonUnitalRingHom.id S) x✝
-- Mathlib/MeasureTheory/Measure/AEMeasurable.lean
theorem aemeasurable_restrict_iff_comap_subtype {s : Set α} (hs : MeasurableSet s) {μ : Measure α}
    {f : α → β} : AEMeasurable f (μ.restrict s) ↔ AEMeasurable (f ∘ (↑) : s → β) (comap (↑) μ)

Proof state:
α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
inst✝ : MeasurableSpace β
s : Set α
hs : MeasurableSet s
μ : Measure α
f : α → β
⊢ AEMeasurable f (μ.restrict s) ↔ AEMeasurable (f ∘ Subtype.val) (Measure.comap Subtype.val μ)

Tactic:
rw [← map_comap_subtype_coe hs, (MeasurableEmbedding.subtype_coe hs).aemeasurable_map_iff]

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Maps.lean
theorem comap_monotone (f : V ↪ W) : Monotone (SimpleGraph.comap f)

Proof state:
V : Type u_1
W : Type u_2
f : V ↪ W
⊢ Monotone (SimpleGraph.comap ⇑f)

Tactic:
intro G G' h _ _ ha

Result:
V : Type u_1
W : Type u_2
f : V ↪ W
G G' : SimpleGraph W
h : G ≤ G'
v✝ w✝ : V
ha : (SimpleGraph.comap (⇑f) G).Adj v✝ w✝
⊢ (SimpleGraph.comap (⇑f) G').Adj v✝ w✝

Proof state:
V : Type u_1
W : Type u_2
f : V ↪ W
G G' : SimpleGraph W
h : G ≤ G'
v✝ w✝ : V
ha : (SimpleGraph.comap (⇑f) G).Adj v✝ w✝
⊢ (SimpleGraph.comap (⇑f) G').Adj v✝ w✝

Tactic:
exact h ha

Result:
no goals
-- Mathlib/Data/Sign.lean
theorem neg_eq_self_iff (a : SignType) : -a = a ↔ a = 0

Proof state:
a : SignType
⊢ -a = a ↔ a = 0

Tactic:
cases a <;> decide

Result:
no goals
-- Mathlib/Data/Set/Basic.lean
theorem eq_of_inclusion_surjective {s t : Set α} {h : s ⊆ t}
    (h_surj : Function.Surjective (inclusion h)) : s = t

Proof state:
case intro
α : Type u_1
s t : Set α
h : s ⊆ t
h_surj : Surjective (inclusion h)
x : α
hx : x ∈ t
y : ↑s
hy : inclusion h y = ⟨x, hx⟩
⊢ x ∈ s

Tactic:
exact mem_of_eq_of_mem (congr_arg Subtype.val hy).symm y.prop

Result:
no goals

Proof state:
α : Type u_1
s t : Set α
h : s ⊆ t
h_surj : Surjective (inclusion h)
x : α
hx : x ∈ t
⊢ x ∈ s

Tactic:
obtain ⟨y, hy⟩ := h_surj ⟨x, hx⟩

Result:
case intro
α : Type u_1
s t : Set α
h : s ⊆ t
h_surj : Surjective (inclusion h)
x : α
hx : x ∈ t
y : ↑s
hy : inclusion h y = ⟨x, hx⟩
⊢ x ∈ s

Proof state:
α : Type u_1
s t : Set α
h : s ⊆ t
h_surj : Surjective (inclusion h)
⊢ s = t

Tactic:
refine Set.Subset.antisymm h (fun x hx => ?_)

Result:
α : Type u_1
s t : Set α
h : s ⊆ t
h_surj : Surjective (inclusion h)
x : α
hx : x ∈ t
⊢ x ∈ s
-- Mathlib/Order/Lattice.lean
theorem sup_left_idem (a b : α) : a ⊔ (a ⊔ b) = a ⊔ b

Proof state:
α : Type u
inst✝ : SemilatticeSup α
a b : α
⊢ a ⊔ (a ⊔ b) = a ⊔ b

Tactic:
simp

Result:
no goals
-- Mathlib/Order/CompleteLattice.lean
theorem binary_relation_sSup_iff {α β : Type*} (s : Set (α → β → Prop)) {a : α} {b : β} :
    sSup s a b ↔ ∃ r : α → β → Prop, r ∈ s ∧ r a b

Proof state:
α : Type u_8
β : Type u_9
s : Set (α → β → Prop)
a : α
b : β
⊢ sSup s a b ↔ ∃ r ∈ s, r a b

Tactic:
rw [sSup_apply]

Result:
α : Type u_8
β : Type u_9
s : Set (α → β → Prop)
a : α
b : β
⊢ (⨆ f, ↑f a) b ↔ ∃ r ∈ s, r a b

Proof state:
α : Type u_8
β : Type u_9
s : Set (α → β → Prop)
a : α
b : β
⊢ (⨆ f, ↑f a) b ↔ ∃ r ∈ s, r a b

Tactic:
simp [← eq_iff_iff]

Result:
no goals
-- Mathlib/Topology/Category/Profinite/Nobeling.lean
theorem ord_term {o : Ordinal} (ho : o < Ordinal.type ((· < ·) : I → I → Prop)) (i : I) :
    ord I i = o ↔ term I ho = i

Proof state:
case refine_1
I : Type u
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
i : I
ho : ord I i < Ordinal.type fun x1 x2 => x1 < x2
⊢ term I ho = i

Tactic:
exact term_ord_aux ho

Result:
no goals

Proof state:
case refine_2
I : Type u
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
o : Ordinal.{u}
ho : o < Ordinal.type fun x1 x2 => x1 < x2
⊢ ord I (term I ho) = o

Tactic:
exact ord_term_aux ho

Result:
no goals

Proof state:
I : Type u
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
o : Ordinal.{u}
ho : o < Ordinal.type fun x1 x2 => x1 < x2
i : I
⊢ ord I i = o ↔ term I ho = i

Tactic:
refine ⟨fun h ↦ ?_, fun h ↦ ?_⟩

Result:
case refine_1
I : Type u
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
o : Ordinal.{u}
ho : o < Ordinal.type fun x1 x2 => x1 < x2
i : I
h : ord I i = o
⊢ term I ho = i

case refine_2
I : Type u
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
o : Ordinal.{u}
ho : o < Ordinal.type fun x1 x2 => x1 < x2
i : I
h : term I ho = i
⊢ ord I i = o

Proof state:
case refine_2
I : Type u
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
o : Ordinal.{u}
ho : o < Ordinal.type fun x1 x2 => x1 < x2
i : I
h : term I ho = i
⊢ ord I i = o

Tactic:
subst h

Result:
case refine_2
I : Type u
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
o : Ordinal.{u}
ho : o < Ordinal.type fun x1 x2 => x1 < x2
⊢ ord I (term I ho) = o

Proof state:
case refine_1
I : Type u
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
o : Ordinal.{u}
ho : o < Ordinal.type fun x1 x2 => x1 < x2
i : I
h : ord I i = o
⊢ term I ho = i

Tactic:
subst h

Result:
case refine_1
I : Type u
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
i : I
ho : ord I i < Ordinal.type fun x1 x2 => x1 < x2
⊢ term I ho = i
-- Mathlib/RingTheory/Spectrum/Prime/Basic.lean
theorem vanishingIdeal_empty : vanishingIdeal (∅ : Set (PrimeSpectrum R)) = ⊤

Proof state:
R : Type u
inst✝ : CommSemiring R
⊢ vanishingIdeal ∅ = ⊤

Tactic:
simpa using (gc R).u_top

Result:
no goals
-- Mathlib/Data/Fin/Rev.lean
theorem rev_eq_iff {i j : Fin n} : rev i = j ↔ i = rev j

Proof state:
n : ℕ
i j : Fin n
⊢ i.rev = j ↔ i = j.rev

Tactic:
rw [← rev_inj, rev_rev]

Result:
no goals
-- Mathlib/Data/Fin/Tuple/Basic.lean
theorem append_right_cons {n m} {α : Sort*} (xs : Fin n → α) (y : α) (ys : Fin m → α) :
    Fin.append xs (Fin.cons y ys) =
      Fin.append (Fin.snoc xs y) ys ∘ Fin.cast (Nat.succ_add_eq_add_succ ..).symm

Proof state:
n m : ℕ
α : Sort u_2
xs : Fin n → α
y : α
ys : Fin m → α
⊢ append xs (cons y ys) = append (snoc xs y) ys ∘ Fin.cast ⋯

Tactic:
rw [append_left_snoc]

Result:
n m : ℕ
α : Sort u_2
xs : Fin n → α
y : α
ys : Fin m → α
⊢ append xs (cons y ys) = (append xs (cons y ys) ∘ Fin.cast ⋯) ∘ Fin.cast ⋯

Proof state:
n m : ℕ
α : Sort u_2
xs : Fin n → α
y : α
ys : Fin m → α
⊢ append xs (cons y ys) = (append xs (cons y ys) ∘ Fin.cast ⋯) ∘ Fin.cast ⋯

Tactic:
rfl

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/LapMatrix.lean
theorem lapMatrix_toLin'_apply_eq_zero_iff_forall_reachable (x : V → ℝ) :
    Matrix.toLin' (G.lapMatrix ℝ) x = 0 ↔ ∀ i j : V, G.Reachable i j → x i = x j

Proof state:
V : Type u_1
inst✝² : Fintype V
G : SimpleGraph V
inst✝¹ : DecidableRel G.Adj
inst✝ : DecidableEq V
x : V → ℝ
⊢ (toLin' (lapMatrix ℝ G)) x = 0 ↔ ∀ (i j : V), G.Reachable i j → x i = x j

Tactic:
rw [← (posSemidef_lapMatrix ℝ G).toLinearMap₂'_zero_iff, star_trivial,
    lapMatrix_toLinearMap₂'_apply'_eq_zero_iff_forall_reachable]

Result:
no goals
-- Mathlib/Topology/MetricSpace/Lipschitz.lean
theorem lipschitzWith_iff_dist_le_mul [PseudoMetricSpace α] [PseudoMetricSpace β] {K : ℝ≥0}
    {f : α → β} : LipschitzWith K f ↔ ∀ x y, dist (f x) (f y) ≤ K * dist x y

Proof state:
α : Type u
β : Type v
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
K : ℝ≥0
f : α → β
⊢ LipschitzWith K f ↔ ∀ (x y : α), dist (f x) (f y) ≤ ↑K * dist x y

Tactic:
simp only [LipschitzWith, edist_nndist, dist_nndist]

Result:
α : Type u
β : Type v
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
K : ℝ≥0
f : α → β
⊢ (∀ (x y : α), ↑(nndist (f x) (f y)) ≤ ↑K * ↑(nndist x y)) ↔ ∀ (x y : α), ↑(nndist (f x) (f y)) ≤ ↑K * ↑(nndist x y)

Proof state:
α : Type u
β : Type v
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
K : ℝ≥0
f : α → β
⊢ (∀ (x y : α), ↑(nndist (f x) (f y)) ≤ ↑K * ↑(nndist x y)) ↔ ∀ (x y : α), ↑(nndist (f x) (f y)) ≤ ↑K * ↑(nndist x y)

Tactic:
norm_cast

Result:
no goals
-- Mathlib/Algebra/Group/Commute/Defs.lean
theorem mul_inv (hab : Commute a b) : (a * b)⁻¹ = a⁻¹ * b⁻¹

Proof state:
G : Type u_1
inst✝ : DivisionMonoid G
a b : G
hab : Commute a b
⊢ (a * b)⁻¹ = a⁻¹ * b⁻¹

Tactic:
rw [hab.eq, mul_inv_rev]

Result:
no goals
-- Mathlib/Topology/MetricSpace/Pseudo/Defs.lean
theorem Metric.emetric_ball {x : α} {ε : ℝ} : EMetric.ball x (ENNReal.ofReal ε) = ball x ε

Proof state:
α : Type u
inst✝ : PseudoMetricSpace α
x : α
ε : ℝ
⊢ EMetric.ball x (ENNReal.ofReal ε) = ball x ε

Tactic:
ext y

Result:
case h
α : Type u
inst✝ : PseudoMetricSpace α
x : α
ε : ℝ
y : α
⊢ y ∈ EMetric.ball x (ENNReal.ofReal ε) ↔ y ∈ ball x ε

Proof state:
case h
α : Type u
inst✝ : PseudoMetricSpace α
x : α
ε : ℝ
y : α
⊢ y ∈ EMetric.ball x (ENNReal.ofReal ε) ↔ y ∈ ball x ε

Tactic:
simp only [EMetric.mem_ball, mem_ball, edist_dist]

Result:
case h
α : Type u
inst✝ : PseudoMetricSpace α
x : α
ε : ℝ
y : α
⊢ ENNReal.ofReal (dist y x) < ENNReal.ofReal ε ↔ dist y x < ε

Proof state:
case h
α : Type u
inst✝ : PseudoMetricSpace α
x : α
ε : ℝ
y : α
⊢ ENNReal.ofReal (dist y x) < ENNReal.ofReal ε ↔ dist y x < ε

Tactic:
exact ENNReal.ofReal_lt_ofReal_iff_of_nonneg dist_nonneg

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem msb_eq_false_iff_two_mul_lt {x : BitVec w} : x.msb = false ↔ 2 * x.toNat < 2^w

Proof state:
w : Nat
x : BitVec w
⊢ x.msb = false ↔ 2 * x.toNat < 2 ^ w

Tactic:
cases w <;> simp [Nat.pow_succ, Nat.mul_comm _ 2, msb_eq_decide, toNat_of_zero_length]

Result:
no goals
-- Mathlib/LinearAlgebra/Alternating/Basic.lean
theorem coe_alternatization [DecidableEq ι] [Fintype ι] (a : M [⋀^ι]→ₗ[R] N') :
    MultilinearMap.alternatization (a : MultilinearMap R (fun _ => M) N')
    = Nat.factorial (Fintype.card ι) • a

Proof state:
case a
R : Type u_1
inst✝⁶ : Semiring R
M : Type u_2
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
N' : Type u_6
inst✝³ : AddCommGroup N'
inst✝² : Module R N'
ι : Type u_7
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
a : M [⋀^ι]→ₗ[R] N'
⊢ ⇑(MultilinearMap.alternatization ↑a) = ⇑((Fintype.card ι).factorial • a)

Tactic:
simp_rw [MultilinearMap.alternatization_def, ← coe_domDomCongr, domDomCongr_perm, coe_smul,
  smul_smul, Int.units_mul_self, one_smul, Finset.sum_const, Finset.card_univ, Fintype.card_perm,
  ← coe_multilinearMap, coe_smul]

Result:
no goals

Proof state:
R : Type u_1
inst✝⁶ : Semiring R
M : Type u_2
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
N' : Type u_6
inst✝³ : AddCommGroup N'
inst✝² : Module R N'
ι : Type u_7
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
a : M [⋀^ι]→ₗ[R] N'
⊢ MultilinearMap.alternatization ↑a = (Fintype.card ι).factorial • a

Tactic:
apply AlternatingMap.coe_injective

Result:
case a
R : Type u_1
inst✝⁶ : Semiring R
M : Type u_2
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
N' : Type u_6
inst✝³ : AddCommGroup N'
inst✝² : Module R N'
ι : Type u_7
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
a : M [⋀^ι]→ₗ[R] N'
⊢ ⇑(MultilinearMap.alternatization ↑a) = ⇑((Fintype.card ι).factorial • a)
-- Mathlib/MeasureTheory/Decomposition/Jordan.lean
theorem real_smul_posPart_neg (r : ℝ) (hr : r < 0) :
    (r • j).posPart = (-r).toNNReal • j.negPart

Proof state:
α : Type u_1
inst✝ : MeasurableSpace α
j : JordanDecomposition α
r : ℝ
hr : r < 0
⊢ (r • j).posPart = (-r).toNNReal • j.negPart

Tactic:
rw [real_smul_def, ← smul_negPart, if_neg (not_le.2 hr), neg_posPart]

Result:
no goals
-- Mathlib/Topology/MetricSpace/Isometry.lean
theorem ediam_range (hf : Isometry f) : EMetric.diam (range f) = EMetric.diam (univ : Set α)

Proof state:
α : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
f : α → β
hf : Isometry f
⊢ EMetric.diam (range f) = EMetric.diam univ

Tactic:
rw [← image_univ]

Result:
α : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
f : α → β
hf : Isometry f
⊢ EMetric.diam (f '' univ) = EMetric.diam univ

Proof state:
α : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
f : α → β
hf : Isometry f
⊢ EMetric.diam (f '' univ) = EMetric.diam univ

Tactic:
exact hf.ediam_image univ

Result:
no goals
-- Mathlib/ModelTheory/Definability.lean
theorem Definable.preimage_comp (f : α → β) {s : Set (α → M)} (h : A.Definable L s) :
    A.Definable L ((fun g : β → M => g ∘ f) ⁻¹' s)

Proof state:
case intro.h
M : Type w
A : Set M
L : Language
inst✝ : L.Structure M
α : Type u₁
β : Type u_1
f : α → β
φ : L[[↑A]].Formula α
x✝ : β → M
⊢ x✝ ∈ (fun g => g ∘ f) ⁻¹' setOf φ.Realize ↔ x✝ ∈ setOf (Formula.relabel f φ).Realize

Tactic:
simp only [Set.preimage_setOf_eq, mem_setOf_eq, Formula.realize_relabel]

Result:
no goals

Proof state:
case intro
M : Type w
A : Set M
L : Language
inst✝ : L.Structure M
α : Type u₁
β : Type u_1
f : α → β
φ : L[[↑A]].Formula α
⊢ A.Definable L ((fun g => g ∘ f) ⁻¹' setOf φ.Realize)

Tactic:
refine ⟨φ.relabel f, ?_⟩

Result:
case intro
M : Type w
A : Set M
L : Language
inst✝ : L.Structure M
α : Type u₁
β : Type u_1
f : α → β
φ : L[[↑A]].Formula α
⊢ (fun g => g ∘ f) ⁻¹' setOf φ.Realize = setOf (Formula.relabel f φ).Realize

Proof state:
case intro
M : Type w
A : Set M
L : Language
inst✝ : L.Structure M
α : Type u₁
β : Type u_1
f : α → β
φ : L[[↑A]].Formula α
⊢ (fun g => g ∘ f) ⁻¹' setOf φ.Realize = setOf (Formula.relabel f φ).Realize

Tactic:
ext

Result:
case intro.h
M : Type w
A : Set M
L : Language
inst✝ : L.Structure M
α : Type u₁
β : Type u_1
f : α → β
φ : L[[↑A]].Formula α
x✝ : β → M
⊢ x✝ ∈ (fun g => g ∘ f) ⁻¹' setOf φ.Realize ↔ x✝ ∈ setOf (Formula.relabel f φ).Realize

Proof state:
M : Type w
A : Set M
L : Language
inst✝ : L.Structure M
α : Type u₁
β : Type u_1
f : α → β
s : Set (α → M)
h : A.Definable L s
⊢ A.Definable L ((fun g => g ∘ f) ⁻¹' s)

Tactic:
obtain ⟨φ, rfl⟩ := h

Result:
case intro
M : Type w
A : Set M
L : Language
inst✝ : L.Structure M
α : Type u₁
β : Type u_1
f : α → β
φ : L[[↑A]].Formula α
⊢ A.Definable L ((fun g => g ∘ f) ⁻¹' setOf φ.Realize)
-- Mathlib/Data/Matroid/Closure.lean
lemma IsFlat.closure (hF : M.IsFlat F) : M.closure F = F :=
  (sInter_subset_of_mem (by simpa)).antisymm (M.subset_closure F)

Proof state:
α : Type u_2
M : Matroid α
F : Set α
hF : M.IsFlat F
⊢ F ∈ {F_1 | M.IsFlat F_1 ∧ F ∩ M.E ⊆ F_1}

Tactic:
simpa

Result:
no goals
-- Mathlib/Data/Set/Lattice.lean
theorem preimage_iInter₂ {f : α → β} {s : ∀ i, κ i → Set β} :
    (f ⁻¹' ⋂ (i) (j), s i j) = ⋂ (i) (j), f ⁻¹' s i j

Proof state:
α : Type u_1
β : Type u_2
ι : Sort u_5
κ : ι → Sort u_8
f : α → β
s : (i : ι) → κ i → Set β
⊢ f ⁻¹' ⋂ i, ⋂ j, s i j = ⋂ i, ⋂ j, f ⁻¹' s i j

Tactic:
simp_rw [preimage_iInter]

Result:
no goals
-- Mathlib/Geometry/Euclidean/Angle/Oriented/Rotation.lean
theorem inner_smul_rotation_pi_div_two_smul_left (x : V) (r₁ r₂ : ℝ) :
    ⟪r₁ • o.rotation (π / 2 : ℝ) x, r₂ • x⟫ = 0

Proof state:
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x : V
r₁ r₂ : ℝ
⊢ inner (r₁ • (o.rotation ↑(π / 2)) x) (r₂ • x) = 0

Tactic:
rw [inner_smul_right, inner_smul_rotation_pi_div_two_left, mul_zero]

Result:
no goals
-- Mathlib/Algebra/Group/Basic.lean
theorem div_mul_mul_cancel (a b c : G) : a / c * (b * c) = a * b

Proof state:
G : Type u_3
inst✝ : CommGroup G
a b c : G
⊢ a / c * (b * c) = a * b

Tactic:
rw [mul_left_comm, div_mul_cancel, mul_comm]

Result:
no goals
-- Mathlib/Data/Finset/Preimage.lean
lemma preimage_subset_of_subset_image [DecidableEq β] {f : α → β} {s : Finset β} {t : Finset α}
    (hs : s ⊆ t.image f) {hf} : s.preimage f hf ⊆ t

Proof state:
α : Type u
β : Type v
inst✝ : DecidableEq β
f : α → β
s : Finset β
t : Finset α
hs : s ⊆ image f t
hf : InjOn f (f ⁻¹' ↑s)
⊢ f ⁻¹' ↑s ⊆ ↑t

Tactic:
exact Set.preimage_subset (mod_cast hs) hf

Result:
no goals

Proof state:
α : Type u
β : Type v
inst✝ : DecidableEq β
f : α → β
s : Finset β
t : Finset α
hs : s ⊆ image f t
hf : InjOn f (f ⁻¹' ↑s)
⊢ s.preimage f hf ⊆ t

Tactic:
rw [← coe_subset, coe_preimage]

Result:
α : Type u
β : Type v
inst✝ : DecidableEq β
f : α → β
s : Finset β
t : Finset α
hs : s ⊆ image f t
hf : InjOn f (f ⁻¹' ↑s)
⊢ f ⁻¹' ↑s ⊆ ↑t