harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Order/UpperLower/Basic.lean
theorem coe_iInf (f : ι → UpperSet α) : (↑(⨅ i, f i) : Set α) = ⋃ i, f i

Proof state:
α : Type u_1
ι : Sort u_4
inst✝ : LE α
f : ι → UpperSet α
⊢ ↑(⨅ i, f i) = ⋃ i, ↑(f i)

Tactic:
simp [iInf]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Lemmas.lean
theorem mem_dite_empty_right {x : α} [Decidable p] {l : p → Vector α 0} :
    (x ∈ if h : p then l h else #v[]) ↔ ∃ h : p, x ∈ l h

Proof state:
α : Type u_1
p : Prop
x : α
inst✝ : Decidable p
l : p → Vector α 0
⊢ (x ∈ if h : p then l h else { toArray := #[], size_toArray := ⋯ }) ↔ ∃ h, x ∈ l h

Tactic:
split <;> simp_all

Result:
no goals
-- Mathlib/GroupTheory/Perm/Cycle/Basic.lean
theorem sameCycle_extendDomain {p : β → Prop} [DecidablePred p] {f : α ≃ Subtype p} :
    SameCycle (g.extendDomain f) (f x) (f y) ↔ g.SameCycle x y :=
  exists_congr fun n => by
    rw [← extendDomain_zpow, extendDomain_apply_image, Subtype.coe_inj, f.injective.eq_iff]

Proof state:
α : Type u_2
β : Type u_3
g : Perm α
x y : α
p : β → Prop
inst✝ : DecidablePred p
f : α ≃ Subtype p
n : ℤ
⊢ (g.extendDomain f ^ n) ↑(f x) = ↑(f y) ↔ (g ^ n) x = y

Tactic:
rw [← extendDomain_zpow, extendDomain_apply_image, Subtype.coe_inj, f.injective.eq_iff]

Result:
no goals
-- Mathlib/Algebra/Order/GroupWithZero/Unbundled.lean
@[simp] lemma inv_nonneg : 0 ≤ a⁻¹ ↔ 0 ≤ a

Proof state:
G₀ : Type u_2
inst✝³ : GroupWithZero G₀
inst✝² : PartialOrder G₀
inst✝¹ : ZeroLEOneClass G₀
inst✝ : PosMulReflectLT G₀
a : G₀
⊢ 0 ≤ a⁻¹ ↔ 0 ≤ a

Tactic:
simp only [le_iff_eq_or_lt, inv_pos, zero_eq_inv]

Result:
no goals
-- Mathlib/Geometry/Manifold/VectorBundle/FiberwiseLinear.lean
theorem mem_aux {e : PartialHomeomorph (B × F) (B × F)} {n : WithTop ℕ∞} :
    (e ∈ ⋃ (φ : B → F ≃L[𝕜] F) (U : Set B) (hU : IsOpen U)
      (hφ : ContMDiffOn IB 𝓘(𝕜, F →L[𝕜] F) n (fun x => φ x : B → F →L[𝕜] F) U)
      (h2φ : ContMDiffOn IB 𝓘(𝕜, F →L[𝕜] F) n (fun x => (φ x).symm : B → F →L[𝕜] F) U),
        {e | e.EqOnSource (FiberwiseLinear.partialHomeomorph φ hU hφ.continuousOn
          h2φ.continuousOn)}) ↔
      ∃ (φ : B → F ≃L[𝕜] F) (U : Set B) (hU : IsOpen U)
        (hφ : ContMDiffOn IB 𝓘(𝕜, F →L[𝕜] F) n (fun x => φ x : B → F →L[𝕜] F) U)
        (h2φ : ContMDiffOn IB 𝓘(𝕜, F →L[𝕜] F) n (fun x => (φ x).symm : B → F →L[𝕜] F) U),
          e.EqOnSource
            (FiberwiseLinear.partialHomeomorph φ hU hφ.continuousOn h2φ.continuousOn)

Proof state:
𝕜 : Type u_1
B : Type u_2
F : Type u_3
inst✝⁷ : TopologicalSpace B
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
EB : Type u_4
inst✝³ : NormedAddCommGroup EB
inst✝² : NormedSpace 𝕜 EB
HB : Type u_5
inst✝¹ : TopologicalSpace HB
inst✝ : ChartedSpace HB B
IB : ModelWithCorners 𝕜 EB HB
e : PartialHomeomorph (B × F) (B × F)
n : WithTop ℕ∞
⊢ e ∈
      ⋃ φ,
        ⋃ U,
          ⋃ (hU : IsOpen U),
            ⋃ (hφ : ContMDiffOn IB 𝓘(𝕜, F →L[𝕜] F) n (fun x => ↑(φ x)) U),
              ⋃ (h2φ : ContMDiffOn IB 𝓘(𝕜, F →L[𝕜] F) n (fun x => ↑(φ x).symm) U),
                {e | e.EqOnSource (FiberwiseLinear.partialHomeomorph φ hU ⋯ ⋯)} ↔
    ∃ φ U,
      ∃ (hU : IsOpen U) (hφ : ContMDiffOn IB 𝓘(𝕜, F →L[𝕜] F) n (fun x => ↑(φ x)) U) (h2φ :
        ContMDiffOn IB 𝓘(𝕜, F →L[𝕜] F) n (fun x => ↑(φ x).symm) U),
        e.EqOnSource (FiberwiseLinear.partialHomeomorph φ hU ⋯ ⋯)

Tactic:
simp only [mem_iUnion, mem_setOf_eq]

Result:
no goals
-- Mathlib/Data/Matroid/Restrict.lean
theorem IsBase.isBasis_of_isRestriction (hI : N.IsBase I) (hNM : N ≤r M) : M.IsBasis I N.E

Proof state:
α : Type u_1
M : Matroid α
I : Set α
N : Matroid α
hI : N.IsBase I
hNM : N ≤r M
⊢ M.IsBasis I N.E

Tactic:
obtain ⟨R, hR, rfl⟩ := hNM

Result:
case intro.intro
α : Type u_1
M : Matroid α
I R : Set α
hR : R ⊆ M.E
hI : (M ↾ R).IsBase I
⊢ M.IsBasis I (M ↾ R).E

Proof state:
case intro.intro
α : Type u_1
M : Matroid α
I R : Set α
hR : R ⊆ M.E
hI : (M ↾ R).IsBase I
⊢ M.IsBasis I (M ↾ R).E

Tactic:
rwa [isBase_restrict_iff] at hI

Result:
no goals
-- Mathlib/Topology/Instances/ENNReal/Defs.lean
theorem isOpenEmbedding_coe : IsOpenEmbedding ((↑) : ℝ≥0 → ℝ≥0∞) :=
  ⟨isEmbedding_coe, by rw [range_coe']; exact isOpen_Iio⟩

Proof state:
⊢ IsOpen (Iio ⊤)

Tactic:
exact isOpen_Iio

Result:
no goals

Proof state:
⊢ IsOpen (range ofNNReal)

Tactic:
rw [range_coe']

Result:
⊢ IsOpen (Iio ⊤)
-- Mathlib/Analysis/Convex/Visible.lean
/-- One cannot see any point of an open set. -/
lemma IsOpen.eq_of_isVisible_of_left_mem (hs : IsOpen s) (hsxy : IsVisible 𝕜 s x y) (hy : y ∈ s) :
    x = y :=
  hsxy.eq_of_mem_interior (by simpa [hs.interior_eq])

Proof state:
𝕜 : Type u_1
V : Type u_2
inst✝⁷ : LinearOrderedField 𝕜
inst✝⁶ : AddCommGroup V
inst✝⁵ : Module 𝕜 V
s : Set V
x y : V
inst✝⁴ : TopologicalSpace 𝕜
inst✝³ : OrderTopology 𝕜
inst✝² : TopologicalSpace V
inst✝¹ : IsTopologicalAddGroup V
inst✝ : ContinuousSMul 𝕜 V
hs : IsOpen s
hsxy : IsVisible 𝕜 s x y
hy : y ∈ s
⊢ y ∈ interior s

Tactic:
simpa [hs.interior_eq]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Int/DivModLemmas.lean
theorem neg_dvd {a b : Int} : -a ∣ b ↔ a ∣ b

Proof state:
a b : Int
x✝ : a ∣ b
k : Int
e : b = a * k
⊢ b = -a * -k

Tactic:
simp [e, Int.neg_mul, Int.mul_neg, Int.neg_neg]

Result:
no goals

Proof state:
a b : Int
⊢ -a ∣ b ↔ a ∣ b

Tactic:
constructor <;> exact fun ⟨k, e⟩ =>
  ⟨-k, by simp [e, Int.neg_mul, Int.mul_neg, Int.neg_neg]⟩

Result:
no goals
-- Mathlib/Analysis/Normed/Group/Pointwise.lean
theorem ball_div : ball x δ / s = x • thickening δ s⁻¹

Proof state:
E : Type u_1
inst✝ : SeminormedCommGroup E
δ : ℝ
s : Set E
x : E
⊢ ball x δ / s = x • thickening δ s⁻¹

Tactic:
simp [div_eq_mul_inv]

Result:
no goals
-- Mathlib/RingTheory/LaurentSeries.lean
theorem X_order_mul_powerSeriesPart {n : ℕ} {f : R⸨X⸩} (hn : n = f.order) :
    (PowerSeries.X ^ n * f.powerSeriesPart : R⟦X⟧) = f

Proof state:
R : Type u_1
inst✝ : Semiring R
n : ℕ
f : R⸨X⸩
hn : ↑n = order f
⊢ (ofPowerSeries ℤ R) (PowerSeries.X ^ n * f.powerSeriesPart) = f

Tactic:
simp only [map_mul, map_pow, ofPowerSeries_X, single_pow, nsmul_eq_mul, mul_one, one_pow, hn,
  single_order_mul_powerSeriesPart]

Result:
no goals
-- Mathlib/Algebra/Order/Field/Basic.lean
@[simp] lemma div_pos_iff_of_pos_right (hb : 0 < b) : 0 < a / b ↔ 0 < a

Proof state:
α : Type u_2
inst✝ : LinearOrderedSemifield α
a b : α
hb : 0 < b
⊢ 0 < a / b ↔ 0 < a

Tactic:
simp only [div_eq_mul_inv, mul_pos_iff_of_pos_right (inv_pos.2 hb)]

Result:
no goals
-- Mathlib/Data/List/TFAE.lean
theorem tfae_cons_self {a} {l : List Prop} : TFAE (a :: a :: l) ↔ TFAE (a :: l)

Proof state:
a : Prop
l : List Prop
⊢ (a :: a :: l).TFAE ↔ (a :: l).TFAE

Tactic:
simp [tfae_cons_cons]

Result:
no goals
-- Mathlib/Logic/Equiv/List.lean
theorem lower_raise : ∀ l n, lower (raise l n) n = l
  | [], _ => rfl
  | m :: l, n => by rw [raise, lower, Nat.add_sub_cancel_right, lower_raise l]

Proof state:
m : ℕ
l : List ℕ
n : ℕ
⊢ lower (raise (m :: l) n) n = m :: l

Tactic:
rw [raise, lower, Nat.add_sub_cancel_right, lower_raise l]

Result:
no goals
-- Mathlib/Algebra/Order/Module/OrderedSMul.lean
lemma sup_eq_half_smul_add_add_abs_sub' (x y : β) : x ⊔ y = (2⁻¹ : α) • (x + y + |y - x|)

Proof state:
α : Type u_6
β : Type u_7
inst✝⁵ : DivisionSemiring α
inst✝⁴ : NeZero 2
inst✝³ : Lattice β
inst✝² : AddCommGroup β
inst✝¹ : Module α β
inst✝ : AddLeftMono β
x y : β
this : Invertible 2 := invertibleOfNonzero ⋯
⊢ x ⊔ y = 2⁻¹ • (x + y + |y - x|)

Tactic:
exact sup_eq_half_smul_add_add_abs_sub α x y

Result:
no goals

Proof state:
α : Type u_6
β : Type u_7
inst✝⁵ : DivisionSemiring α
inst✝⁴ : NeZero 2
inst✝³ : Lattice β
inst✝² : AddCommGroup β
inst✝¹ : Module α β
inst✝ : AddLeftMono β
x y : β
⊢ x ⊔ y = 2⁻¹ • (x + y + |y - x|)

Tactic:
letI := invertibleOfNonzero (two_ne_zero' α)

Result:
α : Type u_6
β : Type u_7
inst✝⁵ : DivisionSemiring α
inst✝⁴ : NeZero 2
inst✝³ : Lattice β
inst✝² : AddCommGroup β
inst✝¹ : Module α β
inst✝ : AddLeftMono β
x y : β
this : Invertible 2 := invertibleOfNonzero ⋯
⊢ x ⊔ y = 2⁻¹ • (x + y + |y - x|)
-- Mathlib/CategoryTheory/Limits/Shapes/Pullback/CommSq.lean
theorem of_top' {X₁₁ X₁₂ X₂₁ X₂₂ X₃₁ X₃₂ : C} {h₁₁ : X₁₁ ⟶ X₁₂} {h₂₁ : X₂₁ ⟶ X₂₂} {h₃₁ : X₃₁ ⟶ X₃₂}
    {v₁₁ : X₁₁ ⟶ X₂₁} {v₁₂ : X₁₂ ⟶ X₂₂} {v₁₃ : X₁₂ ⟶ X₃₂} {v₂₁ : X₂₁ ⟶ X₃₁}
    (s : IsPushout h₁₁ (v₁₁ ≫ v₂₁) v₁₃ h₃₁) (t : IsPushout h₁₁ v₁₁ v₁₂ h₂₁) :
      IsPushout h₂₁ v₂₁ (t.desc v₁₃ (v₂₁ ≫ h₃₁) (by rw [s.w, Category.assoc])) h₃₁ :=
  of_top ((t.inl_desc _ _ _).symm ▸ s) (t.inr_desc _ _ _) t

Proof state:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
Z X Y P : C
f : Z ⟶ X
g : Z ⟶ Y
inl : X ⟶ P
inr : Y ⟶ P
X₁₁ X₁₂ X₂₁ X₂₂ X₃₁ X₃₂ : C
h₁₁ : X₁₁ ⟶ X₁₂
h₂₁ : X₂₁ ⟶ X₂₂
h₃₁ : X₃₁ ⟶ X₃₂
v₁₁ : X₁₁ ⟶ X₂₁
v₁₂ : X₁₂ ⟶ X₂₂
v₁₃ : X₁₂ ⟶ X₃₂
v₂₁ : X₂₁ ⟶ X₃₁
s : IsPushout h₁₁ (v₁₁ ≫ v₂₁) v₁₃ h₃₁
t : IsPushout h₁₁ v₁₁ v₁₂ h₂₁
⊢ h₁₁ ≫ v₁₃ = v₁₁ ≫ v₂₁ ≫ h₃₁

Tactic:
rw [s.w, Category.assoc]

Result:
no goals
-- Mathlib/Algebra/Divisibility/Units.lean
theorem isRelPrime_mul_unit_left : IsRelPrime (x * y) (x * z) ↔ IsRelPrime y z

Proof state:
α : Type u_1
inst✝ : CommMonoid α
x y z : α
hu : IsUnit x
⊢ IsRelPrime (x * y) (x * z) ↔ IsRelPrime y z

Tactic:
rw [isRelPrime_mul_unit_left_left hu, isRelPrime_mul_unit_left_right hu]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Option/Lemmas.lean
theorem or_eq_none : or o o' = none ↔ o = none ∧ o' = none

Proof state:
α✝ : Type u_1
o o' : Option α✝
⊢ o.or o' = none ↔ o = none ∧ o' = none

Tactic:
cases o <;> simp

Result:
no goals
-- Mathlib/Data/Finset/Card.lean
lemma card_le_card_of_surjOn (f : α → β) (hf : Set.SurjOn f s t) : #t ≤ #s

Proof state:
α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
f : α → β
hf : Set.SurjOn f ↑s ↑t
⊢ #t ≤ #s

Tactic:
classical unfold Set.SurjOn at hf; exact (card_le_card (mod_cast hf)).trans card_image_le

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
f : α → β
hf : ↑t ⊆ f '' ↑s
⊢ #t ≤ #s

Tactic:
exact (card_le_card (mod_cast hf)).trans card_image_le

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
f : α → β
hf : Set.SurjOn f ↑s ↑t
⊢ #t ≤ #s

Tactic:
unfold Set.SurjOn at hf

Result:
α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
f : α → β
hf : ↑t ⊆ f '' ↑s
⊢ #t ≤ #s
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Int/Lemmas.lean
theorem add_neg_cancel_left (a b : Int) : a + (-a + b) = b

Proof state:
a b : Int
⊢ a + (-a + b) = b

Tactic:
rw [← Int.add_assoc, Int.add_right_neg, Int.zero_add]

Result:
no goals
-- Mathlib/Data/ENNReal/Order.lean
protected lemma mul_eq_left (ha₀ : a ≠ 0) (ha : a ≠ ∞) : a * b = a ↔ b = 1

Proof state:
a b : ℝ≥0∞
ha₀ : a ≠ 0
ha : a ≠ ⊤
⊢ a * b = a ↔ b = 1

Tactic:
simpa using ENNReal.mul_right_inj ha₀ ha (c := 1)

Result:
no goals
-- Mathlib/Analysis/RCLike/Basic.lean
lemma I_eq_zero_or_im_I_eq_one : (I : K) = 0 ∨ im (I : K) = 1 :=
  I_mul_I (K := K) |>.imp_right fun h ↦ by simpa [h] using (I_mul_re (I : K)).symm

Proof state:
K : Type u_1
inst✝ : RCLike K
h : I * I = -1
⊢ im I = 1

Tactic:
simpa [h] using (I_mul_re (I : K)).symm

Result:
no goals
-- Mathlib/AlgebraicGeometry/EllipticCurve/Affine.lean
lemma baseChange_addY : (W'.baseChange B).toAffine.addY (f x₁) (f x₂) (f y₁) (f ℓ) =
    f ((W'.baseChange A).toAffine.addY x₁ x₂ y₁ ℓ)

Proof state:
R : Type r
S : Type s
A : Type u
B : Type v
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing S
inst✝⁸ : CommRing A
inst✝⁷ : CommRing B
W' : Affine R
inst✝⁶ : Algebra R S
inst✝⁵ : Algebra R A
inst✝⁴ : Algebra S A
inst✝³ : IsScalarTower R S A
inst✝² : Algebra R B
inst✝¹ : Algebra S B
inst✝ : IsScalarTower R S B
f : A →ₐ[S] B
x₁ y₁ x₂ ℓ : A
⊢ (baseChange W' B).toAffine.addY (f x₁) (f x₂) (f y₁) (f ℓ) = f ((baseChange W' A).toAffine.addY x₁ x₂ y₁ ℓ)

Tactic:
rw [← RingHom.coe_coe, ← map_addY, map_baseChange]

Result:
no goals
-- Mathlib/LinearAlgebra/Matrix/GeneralLinearGroup/Defs.lean
lemma map_inv_mul_map (g : GL n R) : map f g⁻¹ * map f g = 1

Proof state:
n : Type u
inst✝³ : DecidableEq n
inst✝² : Fintype n
R : Type v
inst✝¹ : CommRing R
S : Type u_1
inst✝ : CommRing S
f : R →+* S
g : GL n R
⊢ (map f) g⁻¹ * (map f) g = 1

Tactic:
simp only [map_inv, inv_mul_cancel]

Result:
no goals
-- Mathlib/Data/Multiset/FinsetOps.lean
theorem mem_ndinsert_self (a : α) (s : Multiset α) : a ∈ ndinsert a s

Proof state:
α : Type u_1
inst✝ : DecidableEq α
a : α
s : Multiset α
⊢ a ∈ ndinsert a s

Tactic:
simp

Result:
no goals
-- Mathlib/Order/Bounds/Image.lean
theorem image_upperBounds_subset_upperBounds_image (Hf : MonotoneOn f t) (Hst : s ⊆ t) :
    f '' (upperBounds s ∩ t) ⊆ upperBounds (f '' s)

Proof state:
case intro.intro
α : Type u
β : Type v
inst✝¹ : Preorder α
inst✝ : Preorder β
f : α → β
s t : Set α
Hf : MonotoneOn f t
Hst : s ⊆ t
a : α
ha : a ∈ upperBounds s ∩ t
⊢ f a ∈ upperBounds (f '' s)

Tactic:
exact Hf.mem_upperBounds_image Hst ha.1 ha.2

Result:
no goals

Proof state:
α : Type u
β : Type v
inst✝¹ : Preorder α
inst✝ : Preorder β
f : α → β
s t : Set α
Hf : MonotoneOn f t
Hst : s ⊆ t
⊢ f '' (upperBounds s ∩ t) ⊆ upperBounds (f '' s)

Tactic:
rintro _ ⟨a, ha, rfl⟩

Result:
case intro.intro
α : Type u
β : Type v
inst✝¹ : Preorder α
inst✝ : Preorder β
f : α → β
s t : Set α
Hf : MonotoneOn f t
Hst : s ⊆ t
a : α
ha : a ∈ upperBounds s ∩ t
⊢ f a ∈ upperBounds (f '' s)
-- Mathlib/Algebra/Module/LocalizedModule/Basic.lean
@[simp]
lemma iso_mk_one (x : M) : (iso S f) (LocalizedModule.mk x 1) = f x

Proof state:
R : Type u_1
inst✝⁵ : CommSemiring R
S : Submonoid R
M : Type u_2
M' : Type u_3
inst✝⁴ : AddCommMonoid M
inst✝³ : AddCommMonoid M'
inst✝² : Module R M
inst✝¹ : Module R M'
f : M →ₗ[R] M'
inst✝ : IsLocalizedModule S f
x : M
⊢ (iso S f) (LocalizedModule.mk x 1) = f x

Tactic:
simp [iso_apply_mk]

Result:
no goals
-- Mathlib/Data/List/Intervals.lean
theorem nodup (n m : ℕ) : Nodup (Ico n m)

Proof state:
n m : ℕ
⊢ (range' n (m - n)).Nodup

Tactic:
simp [nodup_range']

Result:
no goals

Proof state:
n m : ℕ
⊢ (Ico n m).Nodup

Tactic:
dsimp [Ico]

Result:
n m : ℕ
⊢ (range' n (m - n)).Nodup
-- Mathlib/Data/List/Basic.lean
theorem Perm.disjoint_right {l₁ l₂ l : List α} (p : List.Perm l₁ l₂) :
    Disjoint l l₁ ↔ Disjoint l l₂

Proof state:
α : Type u
l₁ l₂ l : List α
p : l₁ ~ l₂
⊢ l.Disjoint l₁ ↔ l.Disjoint l₂

Tactic:
simp_rw [List.disjoint_right, p.mem_iff]

Result:
no goals
-- Mathlib/LinearAlgebra/AffineSpace/Slope.lean
theorem sub_smul_slope_vadd (f : k → PE) (a b : k) : (b - a) • slope f a b +ᵥ f a = f b

Proof state:
k : Type u_1
E : Type u_2
PE : Type u_3
inst✝³ : Field k
inst✝² : AddCommGroup E
inst✝¹ : Module k E
inst✝ : AddTorsor E PE
f : k → PE
a b : k
⊢ (b - a) • slope f a b +ᵥ f a = f b

Tactic:
rw [sub_smul_slope, vsub_vadd]

Result:
no goals
-- Mathlib/Data/Real/Basic.lean
theorem mk_mul {f g : CauSeq ℚ abs} : mk (f * g) = mk f * mk g

Proof state:
f g : CauSeq ℚ abs
⊢ mk (f * g) = mk f * mk g

Tactic:
simp [mk, ← ofCauchy_mul]

Result:
no goals
-- Mathlib/Algebra/Order/Floor.lean
theorem fract_zero : fract (0 : α) = 0

Proof state:
α : Type u_2
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
⊢ fract 0 = 0

Tactic:
rw [fract, floor_zero, cast_zero, sub_self]

Result:
no goals
-- Mathlib/RingTheory/Localization/Defs.lean
theorem ringEquivOfRingEquiv_eq {j : R ≃+* P} (H : M.map j.toMonoidHom = T) (x) :
    ringEquivOfRingEquiv S Q j H ((algebraMap R S) x) = algebraMap P Q (j x)

Proof state:
R : Type u_1
inst✝⁷ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝⁶ : CommSemiring S
inst✝⁵ : Algebra R S
P : Type u_3
inst✝⁴ : CommSemiring P
inst✝³ : IsLocalization M S
T : Submonoid P
Q : Type u_4
inst✝² : CommSemiring Q
inst✝¹ : Algebra P Q
inst✝ : IsLocalization T Q
j : R ≃+* P
H : Submonoid.map j.toMonoidHom M = T
x : R
⊢ (ringEquivOfRingEquiv S Q j H) ((algebraMap R S) x) = (algebraMap P Q) (j x)

Tactic:
simp

Result:
no goals
-- Mathlib/Data/Set/Function.lean
lemma apply_eq_of_range_eq_singleton {f : α → β} {b : β} (h : range f = {b}) (a : α) :
    f a = b

Proof state:
α : Type u_1
β : Type u_2
f : α → β
b : β
h : range f = {b}
a : α
⊢ f a = b

Tactic:
simpa only [h, mem_singleton_iff] using mem_range_self (f := f) a

Result:
no goals
-- Mathlib/Topology/MetricSpace/HausdorffDimension.lean
theorem dimH_univ_pi_fin (n : ℕ) : dimH (univ : Set (Fin n → ℝ)) = n

Proof state:
n : ℕ
⊢ dimH univ = ↑n

Tactic:
rw [dimH_univ_pi, Fintype.card_fin]

Result:
no goals
-- Mathlib/RingTheory/RootsOfUnity/PrimitiveRoots.lean
theorem card_rootsOfUnity {ζ : R} {n : ℕ} [NeZero n] (h : IsPrimitiveRoot ζ n) :
    Fintype.card (rootsOfUnity n R) = n

Proof state:
R : Type u_4
inst✝² : CommRing R
inst✝¹ : IsDomain R
ζ : R
n : ℕ
inst✝ : NeZero n
h : IsPrimitiveRoot ζ n
⊢ Fintype.card ↥(rootsOfUnity n R) = n

Tactic:
obtain ⟨ζ, hζ⟩ := h.isUnit <| NeZero.pos n

Result:
case intro
R : Type u_4
inst✝² : CommRing R
inst✝¹ : IsDomain R
ζ✝ : R
n : ℕ
inst✝ : NeZero n
h : IsPrimitiveRoot ζ✝ n
ζ : Rˣ
hζ : ↑ζ = ζ✝
⊢ Fintype.card ↥(rootsOfUnity n R) = n

Proof state:
case intro
R : Type u_4
inst✝² : CommRing R
inst✝¹ : IsDomain R
ζ✝ : R
n : ℕ
inst✝ : NeZero n
ζ : Rˣ
h : IsPrimitiveRoot ζ n
hζ : ↑ζ = ζ✝
⊢ Fintype.card ↥(rootsOfUnity n R) = n

Tactic:
exact h.card_rootsOfUnity'

Result:
no goals

Proof state:
case intro
R : Type u_4
inst✝² : CommRing R
inst✝¹ : IsDomain R
ζ✝ : R
n : ℕ
inst✝ : NeZero n
h : IsPrimitiveRoot ζ✝ n
ζ : Rˣ
hζ : ↑ζ = ζ✝
⊢ Fintype.card ↥(rootsOfUnity n R) = n

Tactic:
rw [← hζ, IsPrimitiveRoot.coe_units_iff] at h

Result:
case intro
R : Type u_4
inst✝² : CommRing R
inst✝¹ : IsDomain R
ζ✝ : R
n : ℕ
inst✝ : NeZero n
ζ : Rˣ
h : IsPrimitiveRoot ζ n
hζ : ↑ζ = ζ✝
⊢ Fintype.card ↥(rootsOfUnity n R) = n
-- Mathlib/LinearAlgebra/Matrix/Determinant/TotallyUnimodular.lean
lemma fromCols_one_isTotallyUnimodular_iff [DecidableEq m] (A : Matrix m n R) :
    (fromCols A (1 : Matrix m m R)).IsTotallyUnimodular ↔ A.IsTotallyUnimodular

Proof state:
m : Type u_1
n : Type u_3
R : Type u_5
inst✝¹ : CommRing R
inst✝ : DecidableEq m
A : Matrix m n R
⊢ (A.fromCols 1).IsTotallyUnimodular ↔ A.IsTotallyUnimodular

Tactic:
rw [←transpose_isTotallyUnimodular_iff, transpose_fromCols, transpose_one,
  fromRows_one_isTotallyUnimodular_iff, transpose_isTotallyUnimodular_iff]

Result:
no goals
-- Mathlib/Algebra/BigOperators/Ring/List.lean
@[simp]
lemma prod_map_neg (l : List M) :
    (l.map Neg.neg).prod = (-1) ^ l.length * l.prod

Proof state:
M : Type u_3
inst✝¹ : CommMonoid M
inst✝ : HasDistribNeg M
l : List M
⊢ (map Neg.neg l).prod = (-1) ^ l.length * l.prod

Tactic:
induction l <;> simp [*, pow_succ, ((Commute.neg_one_left _).pow_left _).left_comm]

Result:
no goals
-- Mathlib/Data/Seq/Seq.lean
theorem ofList_toList (s : Seq α) (h : s.Terminates) :
    ofList (toList s h) = s

Proof state:
case h.a
α : Type u
s : Seq α
h : s.Terminates
n : ℕ
a✝ : α
⊢ a✝ ∈ (↑(s.toList h)).get? n ↔ a✝ ∈ s.get? n

Tactic:
simp [ofList, List.get?_eq_getElem?]

Result:
no goals

Proof state:
α : Type u
s : Seq α
h : s.Terminates
⊢ ↑(s.toList h) = s

Tactic:
ext n

Result:
case h.a
α : Type u
s : Seq α
h : s.Terminates
n : ℕ
a✝ : α
⊢ a✝ ∈ (↑(s.toList h)).get? n ↔ a✝ ∈ s.get? n
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem toList_mapM [Monad m] [LawfulMonad m] (f : α → m β) (arr : Array α) :
    toList <$> arr.mapM f = arr.toList.mapM f

Proof state:
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : α → m β
arr : Array α
⊢ toList <$> mapM f arr = List.mapM f arr.toList

Tactic:
simp [mapM_eq_mapM_toList]

Result:
no goals
-- Mathlib/Analysis/Normed/Module/Convex.lean
theorem convexOn_dist (z : E) (hs : Convex ℝ s) : ConvexOn ℝ s fun z' => dist z' z

Proof state:
E : Type u_1
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
s : Set E
z : E
hs : Convex ℝ s
⊢ ConvexOn ℝ s fun z' => dist z' z

Tactic:
simpa [dist_eq_norm, preimage_preimage] using
  (convexOn_norm (hs.translate (-z))).comp_affineMap (AffineMap.id ℝ E - AffineMap.const ℝ E z)

Result:
no goals
-- Mathlib/Algebra/Polynomial/Degree/Definitions.lean
theorem natDegree_natCast (n : ℕ) : natDegree (n : R[X]) = 0

Proof state:
R : Type u
inst✝ : Semiring R
n : ℕ
⊢ (↑n).natDegree = 0

Tactic:
simp only [← C_eq_natCast, natDegree_C]

Result:
no goals
-- Mathlib/Analysis/InnerProductSpace/PiL2.lean
theorem inner_matrix_row_row [Fintype n] (A B : Matrix m n 𝕜) (i j : m) :
    ⟪A i, B j⟫ₑ = (B * Aᴴ) j i

Proof state:
𝕜 : Type u_3
inst✝¹ : RCLike 𝕜
m : Type u_7
n : Type u_8
inst✝ : Fintype n
A B : Matrix m n 𝕜
i j : m
⊢ inner ((WithLp.equiv 2 (n → 𝕜)).symm (A i)) ((WithLp.equiv 2 (n → 𝕜)).symm (B j)) = (B * Aᴴ) j i

Tactic:
simp_rw [EuclideanSpace.inner_piLp_equiv_symm, Matrix.mul_apply', dotProduct_comm,
  Matrix.conjTranspose_apply, Pi.star_def]

Result:
no goals
-- Mathlib/LinearAlgebra/CliffordAlgebra/Prod.lean
theorem map_mul_map_eq_neg_of_isOrtho_of_mem_evenOdd_one
    (hm₁ : m₁ ∈ evenOdd Q₁ 1) (hm₂ : m₂ ∈ evenOdd Q₂ 1) :
    map f₁ m₁ * map f₂ m₂ = - map f₂ m₂ * map f₁ m₁

Proof state:
R : Type u_1
M₁ : Type u_2
M₂ : Type u_3
N : Type u_4
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M₁
inst✝⁴ : AddCommGroup M₂
inst✝³ : AddCommGroup N
inst✝² : Module R M₁
inst✝¹ : Module R M₂
inst✝ : Module R N
Q₁ : QuadraticForm R M₁
Q₂ : QuadraticForm R M₂
Qₙ : QuadraticForm R N
f₁ : Q₁ →qᵢ Qₙ
f₂ : Q₂ →qᵢ Qₙ
hf : ∀ (x : M₁) (y : M₂), QuadraticMap.IsOrtho Qₙ (f₁ x) (f₂ y)
m₁ : CliffordAlgebra Q₁
m₂ : CliffordAlgebra Q₂
hm₁ : m₁ ∈ evenOdd Q₁ 1
hm₂ : m₂ ∈ evenOdd Q₂ 1
⊢ (map f₁) m₁ * (map f₂) m₂ = -(map f₂) m₂ * (map f₁) m₁

Tactic:
simp [map_mul_map_of_isOrtho_of_mem_evenOdd _ _ hf _ _ hm₁ hm₂]

Result:
no goals
-- Mathlib/Data/Real/Irrational.lean
theorem irrational_sqrt_intCast_iff {z : ℤ} :
    Irrational (√z) ↔ ¬IsSquare z ∧ 0 ≤ z

Proof state:
z : ℤ
⊢ Irrational √↑z ↔ ¬IsSquare z ∧ 0 ≤ z

Tactic:
rw [← Rat.cast_intCast, irrational_sqrt_ratCast_iff, Rat.isSquare_intCast_iff, Int.cast_nonneg]

Result:
no goals
-- Mathlib/Algebra/Order/SuccPred/WithBot.lean
@[simp] lemma succ_zero : succ (0 : WithBot α) = 1

Proof state:
α : Type u_1
inst✝³ : Preorder α
inst✝² : OrderBot α
inst✝¹ : AddMonoidWithOne α
inst✝ : SuccAddOrder α
⊢ succ 0 = 1

Tactic:
simpa using succ_natCast 0

Result:
no goals
-- Mathlib/Algebra/Order/Group/Pointwise/Interval.lean
@[to_additive (attr := simp)]
lemma inv_uIcc (a b : α) : [[a, b]]⁻¹ = [[a⁻¹, b⁻¹]]

Proof state:
α : Type u_1
inst✝ : LinearOrderedCommGroup α
a b : α
⊢ [[a, b]]⁻¹ = [[a⁻¹, b⁻¹]]

Tactic:
simp only [uIcc, inv_Icc, inv_sup, inv_inf]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Pow/Real.lean
lemma rpow_pow_comm {x : ℝ} (hx : 0 ≤ x) (y : ℝ) (n : ℕ) : (x ^ y) ^ n = (x ^ n) ^ y

Proof state:
x : ℝ
hx : 0 ≤ x
y : ℝ
n : ℕ
⊢ (x ^ y) ^ n = (x ^ n) ^ y

Tactic:
simp_rw [← rpow_natCast, ← rpow_mul hx, mul_comm y]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Zip.lean
theorem zip_mkVector {a : α} {b : β} {n : Nat} :
    zip (mkVector n a) (mkVector n b) = mkVector n (a, b)

Proof state:
α : Type u_1
β : Type u_2
a : α
b : β
n : Nat
⊢ (mkVector n a).zip (mkVector n b) = mkVector n (a, b)

Tactic:
ext <;> simp

Result:
no goals
-- Mathlib/Analysis/CStarAlgebra/GelfandDuality.lean
theorem gelfandStarTransform_naturality {A B : Type*} [CommCStarAlgebra A] [CommCStarAlgebra B]
    (φ : A →⋆ₐ[ℂ] B) :
    (gelfandStarTransform B : _ →⋆ₐ[ℂ] _).comp φ =
      (compContinuousMap φ |>.compStarAlgHom' ℂ ℂ).comp (gelfandStarTransform A : _ →⋆ₐ[ℂ] _)

Proof state:
A : Type u_1
B : Type u_2
inst✝¹ : CommCStarAlgebra A
inst✝ : CommCStarAlgebra B
φ : A →⋆ₐ[ℂ] B
⊢ (↑(gelfandStarTransform B)).comp φ =
    (ContinuousMap.compStarAlgHom' ℂ ℂ (compContinuousMap φ)).comp ↑(gelfandStarTransform A)

Tactic:
rfl

Result:
no goals
-- Mathlib/RingTheory/Idempotents.lean
lemma mem_corner_iff_mul_right (hc : IsMulCentral e) {r : R} : r ∈ corner e ↔ r * e = r

Proof state:
R : Type u_1
e : R
inst✝ : Semigroup R
idem : IsIdempotentElem e
hc : IsMulCentral e
r : R
⊢ r ∈ corner e ↔ r * e = r

Tactic:
rw [mem_corner_iff_mul_left idem hc, hc.comm]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Exp.lean
theorem map_exp_atBot : map exp atBot = 𝓝[>] 0

Proof state:
⊢ Filter.map rexp atBot = 𝓝[>] 0

Tactic:
rw [← coe_comp_expOrderIso, ← Filter.map_map, expOrderIso.map_atBot, ← map_coe_Ioi_atBot]

Result:
no goals