harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Topology/Algebra/Module/Equiv.lean
lemma inverse_eq {f : M →L[R] M₂} {g : M₂ →L[R] M} (hf : f ∘L g = id R M₂) (hg : g ∘L f = id R M) :
    f.inverse = g

Proof state:
R : Type u_3
M : Type u_4
M₂ : Type u_5
inst✝⁶ : TopologicalSpace M
inst✝⁵ : TopologicalSpace M₂
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid M₂
inst✝ : Module R M₂
f : M →L[R] M₂
g : M₂ →L[R] M
hf : f.comp g = id R M₂
hg : g.comp f = id R M
⊢ f.inverse = g

Tactic:
have : f = ContinuousLinearEquiv.equivOfInverse' f g hf hg := rfl

Result:
R : Type u_3
M : Type u_4
M₂ : Type u_5
inst✝⁶ : TopologicalSpace M
inst✝⁵ : TopologicalSpace M₂
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid M₂
inst✝ : Module R M₂
f : M →L[R] M₂
g : M₂ →L[R] M
hf : f.comp g = id R M₂
hg : g.comp f = id R M
this : f = ↑(ContinuousLinearEquiv.equivOfInverse' f g hf hg)
⊢ f.inverse = g

Proof state:
R : Type u_3
M : Type u_4
M₂ : Type u_5
inst✝⁶ : TopologicalSpace M
inst✝⁵ : TopologicalSpace M₂
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid M₂
inst✝ : Module R M₂
f : M →L[R] M₂
g : M₂ →L[R] M
hf : f.comp g = id R M₂
hg : g.comp f = id R M
this : f = ↑(ContinuousLinearEquiv.equivOfInverse' f g hf hg)
⊢ ↑(ContinuousLinearEquiv.equivOfInverse' f g hf hg).symm = g

Tactic:
rfl

Result:
no goals

Proof state:
R : Type u_3
M : Type u_4
M₂ : Type u_5
inst✝⁶ : TopologicalSpace M
inst✝⁵ : TopologicalSpace M₂
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid M₂
inst✝ : Module R M₂
f : M →L[R] M₂
g : M₂ →L[R] M
hf : f.comp g = id R M₂
hg : g.comp f = id R M
this : f = ↑(ContinuousLinearEquiv.equivOfInverse' f g hf hg)
⊢ f.inverse = g

Tactic:
rw [this, inverse_equiv]

Result:
R : Type u_3
M : Type u_4
M₂ : Type u_5
inst✝⁶ : TopologicalSpace M
inst✝⁵ : TopologicalSpace M₂
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid M₂
inst✝ : Module R M₂
f : M →L[R] M₂
g : M₂ →L[R] M
hf : f.comp g = id R M₂
hg : g.comp f = id R M
this : f = ↑(ContinuousLinearEquiv.equivOfInverse' f g hf hg)
⊢ ↑(ContinuousLinearEquiv.equivOfInverse' f g hf hg).symm = g
-- Mathlib/NumberTheory/Zsqrtd/Basic.lean
theorem intCast_im (n : ℤ) : (n : ℤ√d).im = 0

Proof state:
d n : ℤ
⊢ (↑n).im = 0

Tactic:
cases n <;> rfl

Result:
no goals
-- Mathlib/Analysis/RCLike/Basic.lean
theorem normSq_conj (z : K) : normSq (conj z) = normSq z

Proof state:
K : Type u_1
inst✝ : RCLike K
z : K
⊢ normSq ((starRingEnd K) z) = normSq z

Tactic:
simp only [normSq_apply, neg_mul, mul_neg, neg_neg, rclike_simps]

Result:
no goals
-- Mathlib/Data/Nat/Nth.lean
theorem nth_eq_orderEmbOfFin (hf : (setOf p).Finite) {n : ℕ} (hn : n < #hf.toFinset) :
    nth p n = hf.toFinset.orderEmbOfFin rfl ⟨n, hn⟩

Proof state:
p : ℕ → Prop
hf : (setOf p).Finite
n : ℕ
hn : n < #hf.toFinset
⊢ nth p n = (hf.toFinset.orderEmbOfFin ⋯) ⟨n, hn⟩

Tactic:
rw [nth_eq_getD_sort hf, Finset.orderEmbOfFin_apply, List.getD_eq_getElem, Fin.getElem_fin]

Result:
no goals
-- Mathlib/MeasureTheory/Integral/Lebesgue.lean
theorem lintegral_zero : ∫⁻ _ : α, 0 ∂μ = 0

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
⊢ ∫⁻ (x : α), 0 ∂μ = 0

Tactic:
simp

Result:
no goals
-- Mathlib/RingTheory/Valuation/ValuationSubring.lean
theorem monotone_mapOfLE (R S : ValuationSubring K) (h : R ≤ S) : Monotone (R.mapOfLE S h)

Proof state:
K : Type u
inst✝ : Field K
R S : ValuationSubring K
h : R ≤ S
⊢ Monotone ⇑(R.mapOfLE S h)

Tactic:
rintro ⟨⟩ ⟨⟩ ⟨a, ha⟩

Result:
case mk.mk.intro
K : Type u
inst✝ : Field K
R S : ValuationSubring K
h : R ≤ S
a✝² : R.ValueGroup
a✝¹ : K
b✝ : R.ValueGroup
a✝ : K
a : ↥R
ha : a • a✝ = a✝¹
⊢ (R.mapOfLE S h) (Quot.mk (⇑(MulAction.orbitRel (↥R)ˣ K)) a✝¹) ≤
    (R.mapOfLE S h) (Quot.mk (⇑(MulAction.orbitRel (↥R)ˣ K)) a✝)

Proof state:
case mk.mk.intro
K : Type u
inst✝ : Field K
R S : ValuationSubring K
h : R ≤ S
a✝² : R.ValueGroup
a✝¹ : K
b✝ : R.ValueGroup
a✝ : K
a : ↥R
ha : a • a✝ = a✝¹
⊢ (R.mapOfLE S h) (Quot.mk (⇑(MulAction.orbitRel (↥R)ˣ K)) a✝¹) ≤
    (R.mapOfLE S h) (Quot.mk (⇑(MulAction.orbitRel (↥R)ˣ K)) a✝)

Tactic:
exact ⟨R.inclusion S h a, ha⟩

Result:
no goals
-- Mathlib/Algebra/Order/Group/Pointwise/CompleteLattice.lean
@[to_additive]
lemma csSup_inv (hs₀ : s.Nonempty) (hs₁ : BddBelow s) : sSup s⁻¹ = (sInf s)⁻¹

Proof state:
M : Type u_1
inst✝³ : ConditionallyCompleteLattice M
inst✝² : Group M
inst✝¹ : MulLeftMono M
inst✝ : MulRightMono M
s : Set M
hs₀ : s.Nonempty
hs₁ : BddBelow s
⊢ sSup ((fun x => x⁻¹) '' s) = (sInf s)⁻¹

Tactic:
exact ((OrderIso.inv _).map_csInf' hs₀ hs₁).symm

Result:
no goals

Proof state:
M : Type u_1
inst✝³ : ConditionallyCompleteLattice M
inst✝² : Group M
inst✝¹ : MulLeftMono M
inst✝ : MulRightMono M
s : Set M
hs₀ : s.Nonempty
hs₁ : BddBelow s
⊢ sSup s⁻¹ = (sInf s)⁻¹

Tactic:
rw [← image_inv_eq_inv]

Result:
M : Type u_1
inst✝³ : ConditionallyCompleteLattice M
inst✝² : Group M
inst✝¹ : MulLeftMono M
inst✝ : MulRightMono M
s : Set M
hs₀ : s.Nonempty
hs₁ : BddBelow s
⊢ sSup ((fun x => x⁻¹) '' s) = (sInf s)⁻¹
-- Mathlib/CategoryTheory/Comma/Basic.lean
@[simp]
lemma inv_left [IsIso e] : (inv e).left = inv e.left

Proof state:
case hom_inv_id
A : Type u₁
inst✝³ : Category.{v₁, u₁} A
B : Type u₂
inst✝² : Category.{v₂, u₂} B
T : Type u₃
inst✝¹ : Category.{v₃, u₃} T
L : A ⥤ T
R : B ⥤ T
X Y : Comma L R
e : X ⟶ Y
inst✝ : IsIso e
⊢ e.left ≫ (inv e).left = 𝟙 X.left

Tactic:
rw [← Comma.comp_left, IsIso.hom_inv_id, id_left]

Result:
no goals

Proof state:
A : Type u₁
inst✝³ : Category.{v₁, u₁} A
B : Type u₂
inst✝² : Category.{v₂, u₂} B
T : Type u₃
inst✝¹ : Category.{v₃, u₃} T
L : A ⥤ T
R : B ⥤ T
X Y : Comma L R
e : X ⟶ Y
inst✝ : IsIso e
⊢ (inv e).left = inv e.left

Tactic:
apply IsIso.eq_inv_of_hom_inv_id

Result:
case hom_inv_id
A : Type u₁
inst✝³ : Category.{v₁, u₁} A
B : Type u₂
inst✝² : Category.{v₂, u₂} B
T : Type u₃
inst✝¹ : Category.{v₃, u₃} T
L : A ⥤ T
R : B ⥤ T
X Y : Comma L R
e : X ⟶ Y
inst✝ : IsIso e
⊢ e.left ≫ (inv e).left = 𝟙 X.left
-- Mathlib/LinearAlgebra/Matrix/ToLin.lean
lemma linearMap_apply (ij : ι₂ × ι₁) :
    (b₁.linearMap b₂ ij) = (Matrix.toLin b₁ b₂) (Matrix.stdBasis R ι₂ ι₁ ij)

Proof state:
R : Type u_1
M₁ : Type u_3
M₂ : Type u_4
ι₁ : Type u_6
ι₂ : Type u_7
inst✝⁷ : CommSemiring R
inst✝⁶ : AddCommMonoid M₁
inst✝⁵ : AddCommMonoid M₂
inst✝⁴ : Module R M₁
inst✝³ : Module R M₂
inst✝² : Fintype ι₁
inst✝¹ : Fintype ι₂
inst✝ : DecidableEq ι₁
b₁ : Basis ι₁ R M₁
b₂ : Basis ι₂ R M₂
ij : ι₂ × ι₁
⊢ (b₁.linearMap b₂) ij = (toLin b₁ b₂) ((Matrix.stdBasis R ι₂ ι₁) ij)

Tactic:
simp [linearMap]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Count.lean
theorem countP_mono_left (h : ∀ x ∈ l, p x → q x) : countP p l ≤ countP q l

Proof state:
case mk
α : Type u_1
p q : α → Bool
n✝ : Nat
toArray✝ : Array α
size_toArray✝ : toArray✝.size = n✝
h : ∀ (x : α), x ∈ { toArray := toArray✝, size_toArray := size_toArray✝ } → p x = true → q x = true
⊢ countP p { toArray := toArray✝, size_toArray := size_toArray✝ } ≤
    countP q { toArray := toArray✝, size_toArray := size_toArray✝ }

Tactic:
simpa using Array.countP_mono_left (by simpa using h)

Result:
no goals

Proof state:
α : Type u_1
p q : α → Bool
n✝ : Nat
toArray✝ : Array α
size_toArray✝ : toArray✝.size = n✝
h : ∀ (x : α), x ∈ { toArray := toArray✝, size_toArray := size_toArray✝ } → p x = true → q x = true
⊢ ∀ (x : α), x ∈ toArray✝ → p x = true → q x = true

Tactic:
simpa using h

Result:
no goals

Proof state:
α : Type u_1
p q : α → Bool
n✝ : Nat
l : Vector α n✝
h : ∀ (x : α), x ∈ l → p x = true → q x = true
⊢ countP p l ≤ countP q l

Tactic:
cases l

Result:
case mk
α : Type u_1
p q : α → Bool
n✝ : Nat
toArray✝ : Array α
size_toArray✝ : toArray✝.size = n✝
h : ∀ (x : α), x ∈ { toArray := toArray✝, size_toArray := size_toArray✝ } → p x = true → q x = true
⊢ countP p { toArray := toArray✝, size_toArray := size_toArray✝ } ≤
    countP q { toArray := toArray✝, size_toArray := size_toArray✝ }
-- Mathlib/Algebra/Module/LinearMap/Polynomial.lean
lemma polyCharpoly_coeff_nilRank_ne_zero :
    (polyCharpoly φ b).coeff (nilRank φ) ≠ 0

Proof state:
R : Type u_1
L : Type u_2
M : Type u_3
ι : Type u_5
inst✝¹¹ : CommRing R
inst✝¹⁰ : AddCommGroup L
inst✝⁹ : Module R L
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
φ : L →ₗ[R] End R M
inst✝⁶ : Fintype ι
inst✝⁵ : DecidableEq ι
inst✝⁴ : Free R M
inst✝³ : Module.Finite R M
b : Basis ι R L
inst✝² : Module.Finite R L
inst✝¹ : Free R L
inst✝ : Nontrivial R
⊢ (φ.polyCharpoly b).coeff φ.nilRank ≠ 0

Tactic:
rw [nilRank_eq_polyCharpoly_natTrailingDegree _ b]

Result:
R : Type u_1
L : Type u_2
M : Type u_3
ι : Type u_5
inst✝¹¹ : CommRing R
inst✝¹⁰ : AddCommGroup L
inst✝⁹ : Module R L
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
φ : L →ₗ[R] End R M
inst✝⁶ : Fintype ι
inst✝⁵ : DecidableEq ι
inst✝⁴ : Free R M
inst✝³ : Module.Finite R M
b : Basis ι R L
inst✝² : Module.Finite R L
inst✝¹ : Free R L
inst✝ : Nontrivial R
⊢ (φ.polyCharpoly b).coeff (φ.polyCharpoly b).natTrailingDegree ≠ 0

Proof state:
R : Type u_1
L : Type u_2
M : Type u_3
ι : Type u_5
inst✝¹¹ : CommRing R
inst✝¹⁰ : AddCommGroup L
inst✝⁹ : Module R L
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
φ : L →ₗ[R] End R M
inst✝⁶ : Fintype ι
inst✝⁵ : DecidableEq ι
inst✝⁴ : Free R M
inst✝³ : Module.Finite R M
b : Basis ι R L
inst✝² : Module.Finite R L
inst✝¹ : Free R L
inst✝ : Nontrivial R
⊢ (φ.polyCharpoly b).coeff (φ.polyCharpoly b).natTrailingDegree ≠ 0

Tactic:
apply polyCharpoly_coeff_nilRankAux_ne_zero

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Find.lean
theorem findIdx?_flatten {l : Array (Array α)} {p : α → Bool} :
    l.flatten.findIdx? p =
      (l.findIdx? (·.any p)).map
        fun i => ((l.take i).map Array.size).sum +
          (l[i]?.map fun xs => xs.findIdx p).getD 0

Proof state:
case of
α : Type u_1
p : α → Bool
xss✝ : List (List α)
⊢ findIdx? p (List.map List.toArray xss✝).toArray.flatten =
    Option.map
      (fun i =>
        (map size ((List.map List.toArray xss✝).toArray.take i)).sum +
          (Option.map (fun xs => findIdx p xs) (List.map List.toArray xss✝).toArray[i]?).getD 0)
      (findIdx? (fun x => x.any p) (List.map List.toArray xss✝).toArray)

Tactic:
simp [List.findIdx?_flatten, Function.comp_def]

Result:
no goals

Proof state:
α : Type u_1
l : Array (Array α)
p : α → Bool
⊢ findIdx? p l.flatten =
    Option.map (fun i => (map size (l.take i)).sum + (Option.map (fun xs => findIdx p xs) l[i]?).getD 0)
      (findIdx? (fun x => x.any p) l)

Tactic:
cases l using array₂_induction

Result:
case of
α : Type u_1
p : α → Bool
xss✝ : List (List α)
⊢ findIdx? p (List.map List.toArray xss✝).toArray.flatten =
    Option.map
      (fun i =>
        (map size ((List.map List.toArray xss✝).toArray.take i)).sum +
          (Option.map (fun xs => findIdx p xs) (List.map List.toArray xss✝).toArray[i]?).getD 0)
      (findIdx? (fun x => x.any p) (List.map List.toArray xss✝).toArray)
-- Mathlib/Probability/Kernel/Composition/CompProd.lean
theorem setLIntegral_compProd (κ : Kernel α β) [IsSFiniteKernel κ] (η : Kernel (α × β) γ)
    [IsSFiniteKernel η] (a : α) {f : β × γ → ℝ≥0∞} (hf : Measurable f) {s : Set β} {t : Set γ}
    (hs : MeasurableSet s) (ht : MeasurableSet t) :
    ∫⁻ z in s ×ˢ t, f z ∂(κ ⊗ₖ η) a = ∫⁻ x in s, ∫⁻ y in t, f (x, y) ∂η (a, x) ∂κ a

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : Kernel α β
inst✝¹ : IsSFiniteKernel κ
η : Kernel (α × β) γ
inst✝ : IsSFiniteKernel η
a : α
f : β × γ → ℝ≥0∞
hf : Measurable f
s : Set β
t : Set γ
hs : MeasurableSet s
ht : MeasurableSet t
⊢ ∫⁻ (z : β × γ) in s ×ˢ t, f z ∂(κ ⊗ₖ η) a = ∫⁻ (x : β) in s, ∫⁻ (y : γ) in t, f (x, y) ∂η (a, x) ∂κ a

Tactic:
simp_rw [← Kernel.restrict_apply (κ ⊗ₖ η) (hs.prod ht), ← compProd_restrict hs ht,
  lintegral_compProd _ _ _ hf, Kernel.restrict_apply]

Result:
no goals
-- Mathlib/AlgebraicTopology/SimplicialObject/Basic.lean
theorem δ_comp_σ_of_gt' {n} {i : Fin (n + 3)} {j : Fin (n + 2)} (H : j.succ < i) :
    X.δ i ≫ X.σ j =
      X.σ (j.castLT ((add_lt_add_iff_right 1).mp (lt_of_lt_of_le H i.is_le))) ≫
        X.δ (i.pred <|
          fun (hi : i = 0) => by simp only [Fin.not_lt_zero, hi] at H)

Proof state:
C : Type u
inst✝ : Category.{v, u} C
X : CosimplicialObject C
n : ℕ
i : Fin (n + 3)
j : Fin (n + 2)
H : j.succ < i
⊢ X.δ i ≫ X.σ j = X.σ (j.castLT ⋯) ≫ X.δ (i.pred ⋯)

Tactic:
dsimp [δ, σ]

Result:
C : Type u
inst✝ : Category.{v, u} C
X : CosimplicialObject C
n : ℕ
i : Fin (n + 3)
j : Fin (n + 2)
H : j.succ < i
⊢ X.map (SimplexCategory.δ i) ≫ X.map (SimplexCategory.σ j) =
    X.map (SimplexCategory.σ (j.castLT ⋯)) ≫ X.map (SimplexCategory.δ (i.pred ⋯))

Proof state:
C : Type u
inst✝ : Category.{v, u} C
X : CosimplicialObject C
n : ℕ
i : Fin (n + 3)
j : Fin (n + 2)
H : j.succ < i
hi : i = 0
⊢ False

Tactic:
simp only [Fin.not_lt_zero, hi] at H

Result:
no goals

Proof state:
C : Type u
inst✝ : Category.{v, u} C
X : CosimplicialObject C
n : ℕ
i : Fin (n + 3)
j : Fin (n + 2)
H : j.succ < i
⊢ X.map (SimplexCategory.δ i) ≫ X.map (SimplexCategory.σ j) =
    X.map (SimplexCategory.σ (j.castLT ⋯)) ≫ X.map (SimplexCategory.δ (i.pred ⋯))

Tactic:
simp only [← X.map_comp, ← op_comp, SimplexCategory.δ_comp_σ_of_gt' H]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem size_modify (a : Array α) (i : Nat) (f : α → α) : (a.modify i f).size = a.size

Proof state:
α : Type u_1
a : Array α
i : Nat
f : α → α
⊢ size
      (if h : i < a.size then
        let v := a[i];
        do
        let v ← f v
        pure (a.set i v h)
      else pure a) =
    a.size

Tactic:
split <;> simp

Result:
no goals

Proof state:
α : Type u_1
a : Array α
i : Nat
f : α → α
⊢ (a.modify i f).size = a.size

Tactic:
unfold modify modifyM Id.run

Result:
α : Type u_1
a : Array α
i : Nat
f : α → α
⊢ size
      (if h : i < a.size then
        let v := a[i];
        do
        let v ← f v
        pure (a.set i v h)
      else pure a) =
    a.size
-- Mathlib/Data/Multiset/Dedup.lean
theorem dedup_ext {s t : Multiset α} : dedup s = dedup t ↔ ∀ a, a ∈ s ↔ a ∈ t

Proof state:
α : Type u_1
inst✝ : DecidableEq α
s t : Multiset α
⊢ s.dedup = t.dedup ↔ ∀ (a : α), a ∈ s ↔ a ∈ t

Tactic:
simp [Nodup.ext]

Result:
no goals
-- Mathlib/LinearAlgebra/Finsupp/LinearCombination.lean
theorem top_le_span_range_iff_forall_exists_fun :
    ⊤ ≤ span R (range v) ↔ ∀ x, ∃ c : α → R, ∑ i, c i • v i = x

Proof state:
α : Type u_1
M : Type u_2
R : Type u_3
inst✝³ : Fintype α
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
v : α → M
⊢ ⊤ ≤ span R (Set.range v) ↔ ∀ (x : M), x ∈ span R (Set.range v)

Tactic:
exact ⟨fun h x => h trivial, fun h x _ => h x⟩

Result:
no goals

Proof state:
α : Type u_1
M : Type u_2
R : Type u_3
inst✝³ : Fintype α
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
v : α → M
⊢ ⊤ ≤ span R (Set.range v) ↔ ∀ (x : M), ∃ c, ∑ i : α, c i • v i = x

Tactic:
simp_rw [← mem_span_range_iff_exists_fun]

Result:
α : Type u_1
M : Type u_2
R : Type u_3
inst✝³ : Fintype α
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
v : α → M
⊢ ⊤ ≤ span R (Set.range v) ↔ ∀ (x : M), x ∈ span R (Set.range v)
-- Mathlib/Algebra/Order/Field/Basic.lean
theorem sub_one_div_inv_le_two (a2 : 2 ≤ a) : (1 - 1 / a)⁻¹ ≤ 2

Proof state:
α : Type u_2
inst✝ : LinearOrderedField α
a : α
a2 : 2 ≤ a
⊢ 2⁻¹ ≤ 1 - 1 / a

Tactic:
rw [le_sub_iff_add_le, add_comm, ← le_sub_iff_add_le]

Result:
α : Type u_2
inst✝ : LinearOrderedField α
a : α
a2 : 2 ≤ a
⊢ 1 / a ≤ 1 - 2⁻¹

Proof state:
α : Type u_2
inst✝ : LinearOrderedField α
a : α
a2 : 2 ≤ a
⊢ (1 - 1 / a)⁻¹ ≤ 2

Tactic:
refine (inv_anti₀ (inv_pos.2 <| zero_lt_two' α) ?_).trans_eq (inv_inv (2 : α))

Result:
α : Type u_2
inst✝ : LinearOrderedField α
a : α
a2 : 2 ≤ a
⊢ 2⁻¹ ≤ 1 - 1 / a

Proof state:
case h.e'_4
α : Type u_2
inst✝ : LinearOrderedField α
a : α
a2 : 2 ≤ a
⊢ 1 - 2⁻¹ = 2⁻¹

Tactic:
rw [sub_eq_iff_eq_add, ← two_mul, mul_inv_cancel₀ two_ne_zero]

Result:
no goals

Proof state:
α : Type u_2
inst✝ : LinearOrderedField α
a : α
a2 : 2 ≤ a
⊢ 1 / a ≤ 1 - 2⁻¹

Tactic:
convert (one_div a).le.trans (inv_anti₀ zero_lt_two a2) using 1

Result:
case h.e'_4
α : Type u_2
inst✝ : LinearOrderedField α
a : α
a2 : 2 ≤ a
⊢ 1 - 2⁻¹ = 2⁻¹
-- Mathlib/Algebra/Module/Torsion.lean
theorem torsionBySet_singleton_eq : torsionBySet R M {a} = torsionBy R M a

Proof state:
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
a : R
⊢ torsionBySet R M {a} = torsionBy R M a

Tactic:
ext x

Result:
case h
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
a : R
x : M
⊢ x ∈ torsionBySet R M {a} ↔ x ∈ torsionBy R M a

Proof state:
case h
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
a : R
x : M
⊢ x ∈ torsionBySet R M {a} ↔ x ∈ torsionBy R M a

Tactic:
simp only [mem_torsionBySet_iff, SetCoe.forall, Subtype.coe_mk, Set.mem_singleton_iff,
  forall_eq, mem_torsionBy_iff]

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Clique.lean
theorem isNClique_one : G.IsNClique 1 s ↔ ∃ a, s = {a}

Proof state:
α : Type u_1
G : SimpleGraph α
s : Finset α
⊢ (∃ a, s = {a}) → G.IsClique ↑s

Tactic:
rintro ⟨a, rfl⟩

Result:
case intro
α : Type u_1
G : SimpleGraph α
a : α
⊢ G.IsClique ↑{a}

Proof state:
α : Type u_1
G : SimpleGraph α
s : Finset α
⊢ G.IsNClique 1 s ↔ ∃ a, s = {a}

Tactic:
simp only [isNClique_iff, card_eq_one, and_iff_right_iff_imp]

Result:
α : Type u_1
G : SimpleGraph α
s : Finset α
⊢ (∃ a, s = {a}) → G.IsClique ↑s

Proof state:
case intro
α : Type u_1
G : SimpleGraph α
a : α
⊢ G.IsClique ↑{a}

Tactic:
simp

Result:
no goals
-- Mathlib/Topology/Order/DenselyOrdered.lean
theorem tendsto_Ioo_atTop {f : β → Ioo a b} :
    Tendsto f l atTop ↔ Tendsto (fun x => (f x : α)) l (𝓝[<] b)

Proof state:
α : Type u_1
β : Type u_2
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : DenselyOrdered α
a b : α
l : Filter β
f : β → ↑(Ioo a b)
⊢ Tendsto (Subtype.val ∘ f) l (𝓝[<] b) ↔ Tendsto (fun x => ↑(f x)) l (𝓝[<] b)

Tactic:
rfl

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : DenselyOrdered α
a b : α
l : Filter β
f : β → ↑(Ioo a b)
⊢ Tendsto f l atTop ↔ Tendsto (fun x => ↑(f x)) l (𝓝[<] b)

Tactic:
rw [← comap_coe_Ioo_nhdsLT, tendsto_comap_iff]

Result:
α : Type u_1
β : Type u_2
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : DenselyOrdered α
a b : α
l : Filter β
f : β → ↑(Ioo a b)
⊢ Tendsto (Subtype.val ∘ f) l (𝓝[<] b) ↔ Tendsto (fun x => ↑(f x)) l (𝓝[<] b)
-- Mathlib/Combinatorics/Quiver/Cast.lean
theorem Path.cast_cast {u v u' v' u'' v'' : U} (p : Path u v) (hu : u = u') (hv : v = v')
    (hu' : u' = u'') (hv' : v' = v'') :
    (p.cast hu hv).cast hu' hv' = p.cast (hu.trans hu') (hv.trans hv')

Proof state:
U : Type u_1
inst✝ : Quiver U
u'' v'' : U
p : Path u'' v''
⊢ cast ⋯ ⋯ (cast ⋯ ⋯ p) = cast ⋯ ⋯ p

Tactic:
rfl

Result:
no goals

Proof state:
U : Type u_1
inst✝ : Quiver U
u v u' v' u'' v'' : U
p : Path u v
hu : u = u'
hv : v = v'
hu' : u' = u''
hv' : v' = v''
⊢ cast hu' hv' (cast hu hv p) = cast ⋯ ⋯ p

Tactic:
subst_vars

Result:
U : Type u_1
inst✝ : Quiver U
u'' v'' : U
p : Path u'' v''
⊢ cast ⋯ ⋯ (cast ⋯ ⋯ p) = cast ⋯ ⋯ p
-- Mathlib/AlgebraicGeometry/Morphisms/Finite.lean
lemma iff_isIntegralHom_and_locallyOfFiniteType :
    IsFinite f ↔ IsIntegralHom f ∧ LocallyOfFiniteType f

Proof state:
X Y : Scheme
f : X ⟶ Y
⊢ IsFinite f ↔ IsIntegralHom f ∧ LocallyOfFiniteType f

Tactic:
wlog hY : IsAffine Y

Result:
case inr
X Y : Scheme
f : X ⟶ Y
this : ∀ {X Y : Scheme} (f : X ⟶ Y), IsAffine Y → (IsFinite f ↔ IsIntegralHom f ∧ LocallyOfFiniteType f)
hY : ¬IsAffine Y
⊢ IsFinite f ↔ IsIntegralHom f ∧ LocallyOfFiniteType f

X✝ Y✝ : Scheme
f✝ : X✝ ⟶ Y✝
X Y : Scheme
f : X ⟶ Y
hY : IsAffine Y
⊢ IsFinite f ↔ IsIntegralHom f ∧ LocallyOfFiniteType f

Proof state:
case inr
X Y : Scheme
f : X ⟶ Y
this : ∀ {X Y : Scheme} (f : X ⟶ Y), IsAffine Y → (IsFinite f ↔ IsIntegralHom f ∧ LocallyOfFiniteType f)
hY : ¬IsAffine Y
⊢ IsFinite f ↔ IsIntegralHom f ∧ LocallyOfFiniteType f

Tactic:
rw [IsLocalAtTarget.iff_of_openCover (P := @IsFinite) Y.affineCover,
  IsLocalAtTarget.iff_of_openCover (P := @IsIntegralHom) Y.affineCover,
  IsLocalAtTarget.iff_of_openCover (P := @LocallyOfFiniteType) Y.affineCover]

Result:
case inr
X Y : Scheme
f : X ⟶ Y
this : ∀ {X Y : Scheme} (f : X ⟶ Y), IsAffine Y → (IsFinite f ↔ IsIntegralHom f ∧ LocallyOfFiniteType f)
hY : ¬IsAffine Y
⊢ (∀ (i : Y.affineCover.1), IsFinite (Scheme.Cover.pullbackHom Y.affineCover f i)) ↔
    (∀ (i : Y.affineCover.1), IsIntegralHom (Scheme.Cover.pullbackHom Y.affineCover f i)) ∧
      ∀ (i : Y.affineCover.1), LocallyOfFiniteType (Scheme.Cover.pullbackHom Y.affineCover f i)

Proof state:
X✝ Y✝ : Scheme
f✝ : X✝ ⟶ Y✝
X Y : Scheme
f : X ⟶ Y
hY : IsAffine Y
⊢ (IsAffine X ∧ (CommRingCat.Hom.hom (Scheme.Hom.appTop f)).IsIntegral) ∧
      (CommRingCat.Hom.hom (Scheme.Hom.appTop f)).FiniteType ↔
    (IsAffine X ∧ (CommRingCat.Hom.hom (Scheme.Hom.app f ⊤)).IsIntegral) ∧ LocallyOfFiniteType f

Tactic:
refine and_congr_right fun ⟨_, _⟩ ↦
  (HasRingHomProperty.iff_of_isAffine (P := @LocallyOfFiniteType)).symm

Result:
no goals

Proof state:
X✝ Y✝ : Scheme
f✝ : X✝ ⟶ Y✝
X Y : Scheme
f : X ⟶ Y
hY : IsAffine Y
⊢ IsFinite f ↔ IsIntegralHom f ∧ LocallyOfFiniteType f

Tactic:
rw [HasAffineProperty.iff_of_isAffine (P := @IsFinite),
  HasAffineProperty.iff_of_isAffine (P := @IsIntegralHom),
  RingHom.finite_iff_isIntegral_and_finiteType, ← and_assoc]

Result:
X✝ Y✝ : Scheme
f✝ : X✝ ⟶ Y✝
X Y : Scheme
f : X ⟶ Y
hY : IsAffine Y
⊢ (IsAffine X ∧ (CommRingCat.Hom.hom (Scheme.Hom.appTop f)).IsIntegral) ∧
      (CommRingCat.Hom.hom (Scheme.Hom.appTop f)).FiniteType ↔
    (IsAffine X ∧ (CommRingCat.Hom.hom (Scheme.Hom.app f ⊤)).IsIntegral) ∧ LocallyOfFiniteType f

Proof state:
case inr
X Y : Scheme
f : X ⟶ Y
this : ∀ {X Y : Scheme} (f : X ⟶ Y), IsAffine Y → (IsFinite f ↔ IsIntegralHom f ∧ LocallyOfFiniteType f)
hY : ¬IsAffine Y
⊢ (∀ (i : Y.affineCover.1), IsFinite (Scheme.Cover.pullbackHom Y.affineCover f i)) ↔
    (∀ (i : Y.affineCover.1), IsIntegralHom (Scheme.Cover.pullbackHom Y.affineCover f i)) ∧
      ∀ (i : Y.affineCover.1), LocallyOfFiniteType (Scheme.Cover.pullbackHom Y.affineCover f i)

Tactic:
simp_rw [this, forall_and]

Result:
no goals
-- Mathlib/Order/Interval/Set/OrdConnected.lean
@[simp]
lemma image_subtype_val_Icc {s : Set α} [OrdConnected s] (x y : s) :
    Subtype.val '' Icc x y = Icc x.1 y :=
  (OrderEmbedding.subtype (· ∈ s)).image_Icc (by simpa) x y

Proof state:
α : Type u_1
inst✝¹ : Preorder α
s : Set α
inst✝ : s.OrdConnected
x y : ↑s
⊢ (range ⇑(OrderEmbedding.subtype fun x => x ∈ s)).OrdConnected

Tactic:
simpa

Result:
no goals
-- Mathlib/Algebra/Polynomial/Derivative.lean
theorem derivative_monomial (a : R) (n : ℕ) :
    derivative (monomial n a) = monomial (n - 1) (a * n)

Proof state:
R : Type u
inst✝ : Semiring R
a : R
n : ℕ
⊢ derivative ((monomial n) a) = (monomial (n - 1)) (a * ↑n)

Tactic:
rw [derivative_apply, sum_monomial_index, C_mul_X_pow_eq_monomial]

Result:
case hf
R : Type u
inst✝ : Semiring R
a : R
n : ℕ
⊢ C (0 * ↑n) * X ^ (n - 1) = 0

Proof state:
case hf
R : Type u
inst✝ : Semiring R
a : R
n : ℕ
⊢ C (0 * ↑n) * X ^ (n - 1) = 0

Tactic:
simp

Result:
no goals