harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/SetTheory/Ordinal/Basic.lean
theorem enum_zero_eq_bot {o : Ordinal} (ho : 0 < o) :
    enum (α := o.toType) (· < ·) ⟨0, by rwa [type_toType]⟩ =
      have H := toTypeOrderBot (o := o) (by rintro rfl; simp at ho)
      (⊥ : o.toType) :=
  rfl

Proof state:
α : Type u
β : Type v
γ : Type w
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
ho : 0 < 0
⊢ False

Tactic:
simp at ho

Result:
no goals

Proof state:
α : Type u
β : Type v
γ : Type w
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
o : Ordinal.{?u.78586}
ho : 0 < o
⊢ o ≠ 0

Tactic:
rintro rfl

Result:
α : Type u
β : Type v
γ : Type w
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
ho : 0 < 0
⊢ False

Proof state:
α : Type u
β : Type v
γ : Type w
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
o : Ordinal.{?u.78586}
ho : 0 < o
⊢ 0 ∈ Iio (type fun x1 x2 => x1 < x2)

Tactic:
rwa [type_toType]

Result:
no goals
-- Mathlib/RingTheory/Norm/Transitivity.lean
lemma mul_auxMat_toSquareBlock_eq :
    (M * auxMat M k).toSquareBlock (· = k) True = M k k • 1

Proof state:
case a.mk.mk
S : Type u_2
m : Type u_5
inst✝² : CommRing S
M : Matrix m m S
inst✝¹ : DecidableEq m
k : m
inst✝ : Fintype m
i : m
hi : (i = k) = True
j : m
hj : (j = k) = True
⊢ (M * auxMat M k).toSquareBlock (fun x => x = k) True ⟨i, hi⟩ ⟨j, hj⟩ = (M k k • 1) ⟨i, hi⟩ ⟨j, hj⟩

Tactic:
rw [eq_iff_iff, iff_true] at hi hj

Result:
case a.mk.mk
S : Type u_2
m : Type u_5
inst✝² : CommRing S
M : Matrix m m S
inst✝¹ : DecidableEq m
k : m
inst✝ : Fintype m
i : m
hi✝ : (i = k) = True
hi : i = k
j : m
hj✝ : (j = k) = True
hj : j = k
⊢ (M * auxMat M k).toSquareBlock (fun x => x = k) True ⟨i, hi✝⟩ ⟨j, hj✝⟩ = (M k k • 1) ⟨i, hi✝⟩ ⟨j, hj✝⟩

Proof state:
case a.mk.mk
S : Type u_2
m : Type u_5
inst✝² : CommRing S
M : Matrix m m S
inst✝¹ : DecidableEq m
k : m
inst✝ : Fintype m
i : m
hi✝ : (i = k) = True
hi : i = k
j : m
hj✝ : (j = k) = True
hj : j = k
⊢ (M * auxMat M k).toSquareBlock (fun x => x = k) True ⟨i, hi✝⟩ ⟨j, hj✝⟩ = (M k k • 1) ⟨i, hi✝⟩ ⟨j, hj✝⟩

Tactic:
simp [toSquareBlock_def, hi, hj, mul_auxMat_corner]

Result:
no goals

Proof state:
S : Type u_2
m : Type u_5
inst✝² : CommRing S
M : Matrix m m S
inst✝¹ : DecidableEq m
k : m
inst✝ : Fintype m
⊢ (M * auxMat M k).toSquareBlock (fun x => x = k) True = M k k • 1

Tactic:
ext ⟨i, hi⟩ ⟨j, hj⟩

Result:
case a.mk.mk
S : Type u_2
m : Type u_5
inst✝² : CommRing S
M : Matrix m m S
inst✝¹ : DecidableEq m
k : m
inst✝ : Fintype m
i : m
hi : (i = k) = True
j : m
hj : (j = k) = True
⊢ (M * auxMat M k).toSquareBlock (fun x => x = k) True ⟨i, hi⟩ ⟨j, hj⟩ = (M k k • 1) ⟨i, hi⟩ ⟨j, hj⟩
-- Mathlib/RingTheory/Localization/Defs.lean
theorem eq_mk'_of_mul_eq {x : R} {y : M} {z : R} (h : z * y = x) : (algebraMap R S) z = mk' S x y :=
  eq_mk'_iff_mul_eq.mpr (by rw [← h, map_mul])

Proof state:
R : Type u_1
inst✝³ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
x : R
y : ↥M
z : R
h : z * ↑y = x
⊢ (algebraMap R S) z * (algebraMap R S) ↑y = (algebraMap R S) x

Tactic:
rw [← h, map_mul]

Result:
no goals
-- Mathlib/MeasureTheory/Integral/Marginal.lean
theorem lmarginal_erase (f : (∀ i, π i) → ℝ≥0∞) (hf : Measurable f) {i : δ}
    (hi : i ∈ s) (x : ∀ i, π i) :
    (∫⋯∫⁻_s, f ∂μ) x = ∫⁻ xᵢ, (∫⋯∫⁻_(erase s i), f ∂μ) (Function.update x i xᵢ) ∂μ i

Proof state:
δ : Type u_1
π : δ → Type u_3
inst✝² : (x : δ) → MeasurableSpace (π x)
μ : (i : δ) → Measure (π i)
inst✝¹ : DecidableEq δ
s : Finset δ
inst✝ : ∀ (i : δ), SigmaFinite (μ i)
f : ((i : δ) → π i) → ℝ≥0∞
hf : Measurable f
i : δ
hi : i ∈ s
x : (i : δ) → π i
⊢ (∫⋯∫⁻_s, f ∂μ) x = ∫⁻ (xᵢ : π i), (∫⋯∫⁻_s.erase i, f ∂μ) (update x i xᵢ) ∂μ i

Tactic:
simpa [insert_erase hi] using lmarginal_insert _ hf (not_mem_erase i s) x

Result:
no goals
-- Mathlib/Data/Multiset/FinsetOps.lean
theorem Subset.ndinter_eq_left {s t : Multiset α} (h : s ⊆ t) : s.ndinter t = s

Proof state:
α : Type u_1
inst✝ : DecidableEq α
s t : Multiset α
h : s ⊆ t
⊢ s.ndinter t = s

Tactic:
induction s, t using Quot.induction_on₂

Result:
case h
α : Type u_1
inst✝ : DecidableEq α
a✝ b✝ : List α
h : Quot.mk (⇑(isSetoid α)) a✝ ⊆ Quot.mk (⇑(isSetoid α)) b✝
⊢ ndinter (Quot.mk (⇑(isSetoid α)) a✝) (Quot.mk (⇑(isSetoid α)) b✝) = Quot.mk (⇑(isSetoid α)) a✝

Proof state:
case h
α : Type u_1
inst✝ : DecidableEq α
a✝ b✝ : List α
h : Quot.mk (⇑(isSetoid α)) a✝ ⊆ Quot.mk (⇑(isSetoid α)) b✝
⊢ ndinter (Quot.mk (⇑(isSetoid α)) a✝) (Quot.mk (⇑(isSetoid α)) b✝) = Quot.mk (⇑(isSetoid α)) a✝

Tactic:
rw [quot_mk_to_coe'', quot_mk_to_coe'', coe_ndinter, List.Subset.inter_eq_left h]

Result:
no goals
-- Mathlib/Order/Bounds/Image.lean
lemma StrictMono.map_isLeast (hf : StrictMono f) : IsLeast (f '' s) (f a) ↔ IsLeast s a

Proof state:
α : Type u
β : Type v
inst✝¹ : LinearOrder α
inst✝ : Preorder β
f : α → β
a : α
s : Set α
hf : StrictMono f
⊢ IsLeast (f '' s) (f a) ↔ IsLeast s a

Tactic:
simp [IsLeast, hf.injective.eq_iff, hf.mem_lowerBounds_image]

Result:
no goals
-- Mathlib/Order/Filter/Basic.lean
@[simp] lemma eventuallyEq_top : f =ᶠ[⊤] g ↔ f = g

Proof state:
α : Type u
β : Type v
f g : α → β
⊢ f =ᶠ[⊤] g ↔ f = g

Tactic:
simp [EventuallyEq, funext_iff]

Result:
no goals
-- Mathlib/Algebra/Order/GroupWithZero/Canonical.lean
theorem inv_mul_lt_of_lt_mul₀ (h : a < b * c) : b⁻¹ * a < c

Proof state:
α : Type u_1
inst✝ : LinearOrderedCommGroupWithZero α
a b c : α
h : a < b * c
⊢ b⁻¹ * a < c

Tactic:
rw [mul_comm] at *

Result:
α : Type u_1
inst✝ : LinearOrderedCommGroupWithZero α
a b c : α
h : a < c * b
⊢ a * b⁻¹ < c

Proof state:
α : Type u_1
inst✝ : LinearOrderedCommGroupWithZero α
a b c : α
h : a < c * b
⊢ a * b⁻¹ < c

Tactic:
exact mul_inv_lt_of_lt_mul₀ h

Result:
no goals
-- Mathlib/RingTheory/IsAdjoinRoot.lean
theorem modByMonic_repr_map (h : IsAdjoinRootMonic S f) (g : R[X]) :
    h.repr (h.map g) %ₘ f = g %ₘ f :=
  modByMonic_eq_of_dvd_sub h.Monic <| by rw [← h.mem_ker_map, RingHom.sub_mem_ker_iff, map_repr]

Proof state:
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : Ring S
f : R[X]
inst✝ : Algebra R S
h : IsAdjoinRootMonic S f
g : R[X]
⊢ f ∣ h.repr (h.map g) - g

Tactic:
rw [← h.mem_ker_map, RingHom.sub_mem_ker_iff, map_repr]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Exp.lean
theorem exp_half (x : ℝ) : exp (x / 2) = √(exp x)

Proof state:
x : ℝ
⊢ rexp (x / 2) = √(rexp x)

Tactic:
rw [eq_comm, sqrt_eq_iff_eq_sq, sq, ← exp_add, add_halves] <;> exact (exp_pos _).le

Result:
no goals
-- Mathlib/RingTheory/TwoSidedIdeal/Basic.lean
lemma mul_mem_right (x y) (hx : x ∈ I) : x * y ∈ I

Proof state:
R : Type u_1
inst✝ : NonUnitalNonAssocRing R
I : TwoSidedIdeal R
x y : R
hx : x ∈ I
⊢ x * y ∈ I

Tactic:
simpa using I.ringCon.mul hx (I.ringCon.refl y)

Result:
no goals
-- Mathlib/Tactic/CategoryTheory/Monoidal/Normalize.lean
theorem evalHorizontalCompAux_of {f g h i : C} (η : f ⟶ g) (θ : h ⟶ i) :
    η ⊗ θ = (Iso.refl _).hom ≫ (η ⊗ θ) ≫ (Iso.refl _).hom

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : MonoidalCategory C
f g h i : C
η : f ⟶ g
θ : h ⟶ i
⊢ η ⊗ θ = (Iso.refl (f ⊗ h)).hom ≫ (η ⊗ θ) ≫ (Iso.refl (g ⊗ i)).hom

Tactic:
simp

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Fin/Lemmas.lean
theorem rev_last (n : Nat) : rev (last n) = 0 := Fin.ext <| by simp

Proof state:
n : Nat
⊢ ↑(last n).rev = ↑0

Tactic:
simp

Result:
no goals
-- Mathlib/Geometry/Manifold/VectorBundle/Basic.lean
theorem FiberBundle.extChartAt_target (x : TotalSpace F E) :
    (extChartAt (IB.prod 𝓘(𝕜, F)) x).target =
      ((extChartAt IB x.proj).target ∩
        (extChartAt IB x.proj).symm ⁻¹' (trivializationAt F E x.proj).baseSet) ×ˢ univ

Proof state:
𝕜 : Type u_1
B : Type u_2
F : Type u_4
E : B → Type u_6
inst✝¹⁰ : NontriviallyNormedField 𝕜
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace 𝕜 F
inst✝⁷ : TopologicalSpace (TotalSpace F E)
inst✝⁶ : (x : B) → TopologicalSpace (E x)
EB : Type u_7
inst✝⁵ : NormedAddCommGroup EB
inst✝⁴ : NormedSpace 𝕜 EB
HB : Type u_8
inst✝³ : TopologicalSpace HB
IB : ModelWithCorners 𝕜 EB HB
inst✝² : TopologicalSpace B
inst✝¹ : ChartedSpace HB B
inst✝ : FiberBundle F E
x : TotalSpace F E
⊢ (extChartAt (IB.prod 𝓘(𝕜, F)) x).target =
    ((extChartAt IB x.proj).target ∩ ↑(extChartAt IB x.proj).symm ⁻¹' (trivializationAt F E x.proj).baseSet) ×ˢ univ

Tactic:
rw [FiberBundle.extChartAt, PartialEquiv.trans_target, Trivialization.target_eq, inter_prod]

Result:
𝕜 : Type u_1
B : Type u_2
F : Type u_4
E : B → Type u_6
inst✝¹⁰ : NontriviallyNormedField 𝕜
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace 𝕜 F
inst✝⁷ : TopologicalSpace (TotalSpace F E)
inst✝⁶ : (x : B) → TopologicalSpace (E x)
EB : Type u_7
inst✝⁵ : NormedAddCommGroup EB
inst✝⁴ : NormedSpace 𝕜 EB
HB : Type u_8
inst✝³ : TopologicalSpace HB
IB : ModelWithCorners 𝕜 EB HB
inst✝² : TopologicalSpace B
inst✝¹ : ChartedSpace HB B
inst✝ : FiberBundle F E
x : TotalSpace F E
⊢ ((extChartAt IB x.proj).prod (PartialEquiv.refl F)).target ∩
      ↑((extChartAt IB x.proj).prod (PartialEquiv.refl F)).symm ⁻¹' (trivializationAt F E x.proj).baseSet ×ˢ univ =
    (extChartAt IB x.proj).target ×ˢ univ ∩
      (↑(extChartAt IB x.proj).symm ⁻¹' (trivializationAt F E x.proj).baseSet) ×ˢ univ

Proof state:
𝕜 : Type u_1
B : Type u_2
F : Type u_4
E : B → Type u_6
inst✝¹⁰ : NontriviallyNormedField 𝕜
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace 𝕜 F
inst✝⁷ : TopologicalSpace (TotalSpace F E)
inst✝⁶ : (x : B) → TopologicalSpace (E x)
EB : Type u_7
inst✝⁵ : NormedAddCommGroup EB
inst✝⁴ : NormedSpace 𝕜 EB
HB : Type u_8
inst✝³ : TopologicalSpace HB
IB : ModelWithCorners 𝕜 EB HB
inst✝² : TopologicalSpace B
inst✝¹ : ChartedSpace HB B
inst✝ : FiberBundle F E
x : TotalSpace F E
⊢ ((extChartAt IB x.proj).prod (PartialEquiv.refl F)).target ∩
      ↑((extChartAt IB x.proj).prod (PartialEquiv.refl F)).symm ⁻¹' (trivializationAt F E x.proj).baseSet ×ˢ univ =
    (extChartAt IB x.proj).target ×ˢ univ ∩
      (↑(extChartAt IB x.proj).symm ⁻¹' (trivializationAt F E x.proj).baseSet) ×ˢ univ

Tactic:
rfl

Result:
no goals
-- Mathlib/RingTheory/Ideal/Height.lean
lemma Ideal.primeHeight_add_one_le_of_lt {I J : Ideal R} [I.IsPrime] [J.IsPrime] (h : I < J) :
    I.primeHeight + 1 ≤ J.primeHeight

Proof state:
R : Type u_1
inst✝² : CommRing R
I J : Ideal R
inst✝¹ : I.IsPrime
inst✝ : J.IsPrime
h : I < J
⊢ I.primeHeight + 1 ≤ J.primeHeight

Tactic:
unfold primeHeight

Result:
R : Type u_1
inst✝² : CommRing R
I J : Ideal R
inst✝¹ : I.IsPrime
inst✝ : J.IsPrime
h : I < J
⊢ Order.height { asIdeal := I, isPrime := inst✝¹ } + 1 ≤ Order.height { asIdeal := J, isPrime := inst✝ }

Proof state:
R : Type u_1
inst✝² : CommRing R
I J : Ideal R
inst✝¹ : I.IsPrime
inst✝ : J.IsPrime
h : I < J
⊢ Order.height { asIdeal := I, isPrime := inst✝¹ } + 1 ≤ Order.height { asIdeal := J, isPrime := inst✝ }

Tactic:
exact Order.height_add_one_le h

Result:
no goals
-- Mathlib/Data/Num/Bitwise.lean
theorem bit_zero (b : Bool) : (b :: zero b) = zero b

Proof state:
b : Bool
⊢ (b::zero b) = zero b

Tactic:
cases b <;> rfl

Result:
no goals
-- Mathlib/Order/Category/BoolAlg.lean
lemma hom_inv_apply {X Y : BoolAlg} (e : X ≅ Y) (s : Y) : e.hom (e.inv s) = s

Proof state:
X Y : BoolAlg
e : X ≅ Y
s : ↑Y
⊢ (ConcreteCategory.hom e.hom) ((ConcreteCategory.hom e.inv) s) = s

Tactic:
simp

Result:
no goals
-- Mathlib/Analysis/InnerProductSpace/l2Space.lean
theorem inner_single_right [DecidableEq ι] (i : ι) (a : G i) (f : lp G 2) :
    ⟪f, lp.single 2 i a⟫ = ⟪f i, a⟫

Proof state:
ι : Type u_1
𝕜 : Type u_2
inst✝³ : RCLike 𝕜
G : ι → Type u_4
inst✝² : (i : ι) → NormedAddCommGroup (G i)
inst✝¹ : (i : ι) → InnerProductSpace 𝕜 (G i)
inst✝ : DecidableEq ι
i : ι
a : G i
f : ↥(lp G 2)
⊢ inner f (lp.single 2 i a) = inner (↑f i) a

Tactic:
simpa [inner_conj_symm] using congr_arg conj (inner_single_left (𝕜 := 𝕜) i a f)

Result:
no goals
-- Mathlib/Algebra/Ring/Idempotent.lean
@[simp] lemma zero_compl : (0 : {a : R // IsIdempotentElem a})ᶜ = 1

Proof state:
R : Type u_1
inst✝ : NonAssocRing R
⊢ 0ᶜ = 1

Tactic:
ext

Result:
case a
R : Type u_1
inst✝ : NonAssocRing R
⊢ ↑0ᶜ = ↑1

Proof state:
case a
R : Type u_1
inst✝ : NonAssocRing R
⊢ ↑0ᶜ = ↑1

Tactic:
simp

Result:
no goals
-- Mathlib/Data/NNReal/Defs.lean
@[simp, norm_cast] lemma coe_le_one : (r : ℝ) ≤ 1 ↔ r ≤ 1

Proof state:
r : ℝ≥0
⊢ ↑r ≤ 1 ↔ r ≤ 1

Tactic:
rw [← coe_le_coe, coe_one]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Bool.lean
theorem cond_prop {b : Bool} {p q : Prop} :
    (bif b then p else q) ↔ if b then p else q

Proof state:
b : Bool
p q : Prop
⊢ (bif b then p else q) ↔ if b = true then p else q

Tactic:
cases b <;> simp

Result:
no goals
-- Mathlib/Algebra/Polynomial/Degree/Definitions.lean
theorem natDegree_neg (p : R[X]) : natDegree (-p) = natDegree p

Proof state:
R : Type u
inst✝ : Ring R
p : R[X]
⊢ (-p).natDegree = p.natDegree

Tactic:
simp [natDegree]

Result:
no goals
-- Mathlib/MeasureTheory/Measure/Haar/NormedSpace.lean
theorem setIntegral_comp_smul_of_pos (f : E → F) {R : ℝ} (s : Set E) (hR : 0 < R) :
    ∫ x in s, f (R • x) ∂μ = (R ^ finrank ℝ E)⁻¹ • ∫ x in R • s, f x ∂μ

Proof state:
E : Type u_1
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : MeasurableSpace E
inst✝⁴ : BorelSpace E
inst✝³ : FiniteDimensional ℝ E
μ : Measure E
inst✝² : μ.IsAddHaarMeasure
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : E → F
R : ℝ
s : Set E
hR : 0 < R
⊢ ∫ (x : E) in s, f (R • x) ∂μ = (R ^ finrank ℝ E)⁻¹ • ∫ (x : E) in R • s, f x ∂μ

Tactic:
rw [setIntegral_comp_smul μ f s hR.ne', abs_of_nonneg (inv_nonneg.2 (pow_nonneg hR.le _))]

Result:
no goals
-- Mathlib/Order/Interval/Finset/Fin.lean
theorem card_Iio : #(Iio b) = b

Proof state:
n : ℕ
b : Fin n
⊢ #(Iio b) = ↑b

Tactic:
rw [← Nat.card_Iio b, ← map_valEmbedding_Iio, card_map]

Result:
no goals
-- Mathlib/Topology/NhdsSet.lean
theorem nhdsSet_diagonal (X) [TopologicalSpace (X × X)] :
    𝓝ˢ (diagonal X) = ⨆ (x : X), 𝓝 (x, x)

Proof state:
X : Type u_3
inst✝ : TopologicalSpace (X × X)
⊢ 𝓝ˢ (diagonal X) = ⨆ x, 𝓝 (x, x)

Tactic:
rw [nhdsSet, ← range_diag, ← range_comp]

Result:
X : Type u_3
inst✝ : TopologicalSpace (X × X)
⊢ sSup (range (𝓝 ∘ fun x => (x, x))) = ⨆ x, 𝓝 (x, x)

Proof state:
X : Type u_3
inst✝ : TopologicalSpace (X × X)
⊢ sSup (range (𝓝 ∘ fun x => (x, x))) = ⨆ x, 𝓝 (x, x)

Tactic:
rfl

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

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

Tactic:
rw [derivative_monomial, add_tsub_cancel_right, Nat.cast_add, Nat.cast_one]

Result:
no goals
-- Mathlib/Topology/FiberBundle/Trivialization.lean
/-- If the fiber is nonempty, then the projection also is. -/
lemma toPartialEquiv_injective [Nonempty F] :
    Injective (toPartialEquiv : Pretrivialization F proj → PartialEquiv Z (B × F))

Proof state:
B : Type u_1
F : Type u_2
Z : Type u_4
inst✝² : TopologicalSpace B
inst✝¹ : TopologicalSpace F
proj : Z → B
inst✝ : Nonempty F
⊢ Injective toPartialEquiv

Tactic:
refine fun e e' h ↦ ext' _ _ h ?_

Result:
B : Type u_1
F : Type u_2
Z : Type u_4
inst✝² : TopologicalSpace B
inst✝¹ : TopologicalSpace F
proj : Z → B
inst✝ : Nonempty F
e e' : Pretrivialization F proj
h : e.toPartialEquiv = e'.toPartialEquiv
⊢ e.baseSet = e'.baseSet
-- Mathlib/Data/Rel.lean
theorem preimage_univ : r.preimage Set.univ = r.dom

Proof state:
α : Type u_1
β : Type u_2
r : Rel α β
⊢ r.preimage Set.univ = r.dom

Tactic:
rw [preimage, image_univ, codom_inv]

Result:
no goals
-- Mathlib/Dynamics/PeriodicPts/Defs.lean
theorem zpow_mod_period_smul (j : ℤ) {g : G} {a : α} :
    g ^ (j % (period g a : ℤ)) • a = g ^ j • a

Proof state:
α : Type v
G : Type u
inst✝¹ : Group G
inst✝ : MulAction G α
j : ℤ
g : G
a : α
⊢ g ^ (j % ↑(period g a)) • a = g ^ j • a

Tactic:
conv_rhs => rw [← Int.emod_add_ediv j (period g a), zpow_add, mul_smul,
  zpow_smul_eq_iff_period_dvd.mpr (dvd_mul_right _ _)]

Result:
no goals
-- Mathlib/RingTheory/Regular/RegularSequence.lean
lemma top_eq_ofList_cons_smul_iff :
    (⊤ : Submodule R M) = Ideal.ofList (r :: rs) • ⊤ ↔
      (⊤ : Submodule R (QuotSMulTop r M)) = Ideal.ofList rs • ⊤

Proof state:
R : Type u_1
M : Type u_3
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
r : R
rs : List R
⊢ ⊤ = Ideal.ofList (r :: rs) • ⊤ ↔ ⊤ = Ideal.ofList rs • ⊤

Tactic:
conv => congr <;> rw [eq_comm, ← subsingleton_quotient_iff_eq_top]

Result:
R : Type u_1
M : Type u_3
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
r : R
rs : List R
⊢ Subsingleton (M ⧸ Ideal.ofList (r :: rs) • ⊤) ↔ Subsingleton (QuotSMulTop r M ⧸ Ideal.ofList rs • ⊤)

Proof state:
R : Type u_1
M : Type u_3
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
r : R
rs : List R
⊢ Subsingleton (M ⧸ Ideal.ofList (r :: rs) • ⊤) ↔ Subsingleton (QuotSMulTop r M ⧸ Ideal.ofList rs • ⊤)

Tactic:
exact (quotOfListConsSMulTopEquivQuotSMulTopInner M r rs).toEquiv.subsingleton_congr

Result:
no goals
-- Mathlib/RingTheory/OreLocalization/Ring.lean
theorem subsingleton_iff :
    Subsingleton R[S⁻¹] ↔ 0 ∈ S

Proof state:
R : Type u_1
inst✝¹ : Ring R
S : Submonoid R
inst✝ : OreSet S
⊢ (∃ u v, u • 1 = v • 0 ∧ ↑u * ↑1 = v * ↑1) ↔ 0 ∈ S

Tactic:
simp

Result:
no goals

Proof state:
R : Type u_1
inst✝¹ : Ring R
S : Submonoid R
inst✝ : OreSet S
⊢ Subsingleton (OreLocalization S R) ↔ 0 ∈ S

Tactic:
rw [← subsingleton_iff_zero_eq_one, OreLocalization.one_def,
  OreLocalization.zero_def, oreDiv_eq_iff]

Result:
R : Type u_1
inst✝¹ : Ring R
S : Submonoid R
inst✝ : OreSet S
⊢ (∃ u v, u • 1 = v • 0 ∧ ↑u * ↑1 = v * ↑1) ↔ 0 ∈ S
-- Mathlib/CategoryTheory/Enriched/Ordinary/Basic.lean
@[reassoc]
lemma eHom_whisker_exchange {X X' Y Y' : C} (f : X ⟶ X') (g : Y ⟶ Y') :
    eHomWhiskerLeft V X' g ≫ eHomWhiskerRight V f Y' =
      eHomWhiskerRight V f Y ≫ eHomWhiskerLeft V X g

Proof state:
V : Type u'
inst✝³ : Category.{v', u'} V
inst✝² : MonoidalCategory V
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : EnrichedOrdinaryCategory V C
X X' Y Y' : C
f : X ⟶ X'
g : Y ⟶ Y'
⊢ eHomWhiskerLeft V X' g ≫ eHomWhiskerRight V f Y' = eHomWhiskerRight V f Y ≫ eHomWhiskerLeft V X g

Tactic:
dsimp [eHomWhiskerLeft, eHomWhiskerRight]

Result:
V : Type u'
inst✝³ : Category.{v', u'} V
inst✝² : MonoidalCategory V
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : EnrichedOrdinaryCategory V C
X X' Y Y' : C
f : X ⟶ X'
g : Y ⟶ Y'
⊢ ((ρ_ (EnrichedCategory.Hom X' Y)).inv ≫ EnrichedCategory.Hom X' Y ◁ (eHomEquiv V) g ≫ eComp V X' Y Y') ≫
      (λ_ (EnrichedCategory.Hom X' Y')).inv ≫ (eHomEquiv V) f ▷ EnrichedCategory.Hom X' Y' ≫ eComp V X X' Y' =
    ((λ_ (EnrichedCategory.Hom X' Y)).inv ≫ (eHomEquiv V) f ▷ EnrichedCategory.Hom X' Y ≫ eComp V X X' Y) ≫
      (ρ_ (EnrichedCategory.Hom X Y)).inv ≫ EnrichedCategory.Hom X Y ◁ (eHomEquiv V) g ≫ eComp V X Y Y'

Proof state:
V : Type u'
inst✝³ : Category.{v', u'} V
inst✝² : MonoidalCategory V
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : EnrichedOrdinaryCategory V C
X X' Y Y' : C
f : X ⟶ X'
g : Y ⟶ Y'
⊢ ((ρ_ (EnrichedCategory.Hom X' Y)).inv ≫ EnrichedCategory.Hom X' Y ◁ (eHomEquiv V) g ≫ eComp V X' Y Y') ≫
      (λ_ (EnrichedCategory.Hom X' Y')).inv ≫ (eHomEquiv V) f ▷ EnrichedCategory.Hom X' Y' ≫ eComp V X X' Y' =
    ((λ_ (EnrichedCategory.Hom X' Y)).inv ≫ (eHomEquiv V) f ▷ EnrichedCategory.Hom X' Y ≫ eComp V X X' Y) ≫
      (ρ_ (EnrichedCategory.Hom X Y)).inv ≫ EnrichedCategory.Hom X Y ◁ (eHomEquiv V) g ≫ eComp V X Y Y'

Tactic:
rw [assoc, assoc, assoc, assoc, leftUnitor_inv_naturality_assoc,
  whisker_exchange_assoc, ← e_assoc, leftUnitor_tensor_inv_assoc,
  associator_inv_naturality_left_assoc, Iso.hom_inv_id_assoc,
  ← comp_whiskerRight_assoc, whisker_exchange_assoc,
  MonoidalCategory.whiskerRight_id_assoc, assoc, Iso.inv_hom_id_assoc,
  whisker_exchange_assoc, MonoidalCategory.whiskerRight_id_assoc, Iso.inv_hom_id_assoc]

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Regularity/Uniform.lean
theorem IsUniform.mono {ε' : 𝕜} (h : ε ≤ ε') (hε : IsUniform G ε s t) : IsUniform G ε' s t :=
  fun s' hs' t' ht' hs ht => by
  refine (hε hs' ht' (le_trans ?_ hs) (le_trans ?_ ht)).trans_le h <;> gcongr

Proof state:
α : Type u_1
𝕜 : Type u_2
inst✝¹ : LinearOrderedField 𝕜
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : 𝕜
s t : Finset α
ε' : 𝕜
h : ε ≤ ε'
hε : G.IsUniform ε s t
s' : Finset α
hs' : s' ⊆ s
t' : Finset α
ht' : t' ⊆ t
hs : ↑(#s) * ε' ≤ ↑(#s')
ht : ↑(#t) * ε' ≤ ↑(#t')
⊢ |↑(G.edgeDensity s' t') - ↑(G.edgeDensity s t)| < ε'

Tactic:
refine (hε hs' ht' (le_trans ?_ hs) (le_trans ?_ ht)).trans_le h <;> gcongr

Result:
no goals
-- Mathlib/Algebra/Homology/ShortComplex/SnakeLemma.lean
lemma snd_δ_inr : (pullback.snd _ _ : S.P ⟶ _) ≫ S.δ ≫ (pushout.inr _ _ : _ ⟶ S.P') =
    pullback.fst _ _ ≫ S.v₁₂.τ₂ ≫ pushout.inl _ _

Proof state:
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Abelian C
S : SnakeInput C
⊢ pullback.snd S.L₁.g S.v₀₁.τ₃ ≫ S.δ ≫ pushout.inr S.L₂.f S.v₂₃.τ₁ =
    pullback.fst S.L₁.g S.v₀₁.τ₃ ≫ S.v₁₂.τ₂ ≫ pushout.inl S.L₂.f S.v₂₃.τ₁

Tactic:
simp only [snd_δ_assoc, ← pushout.condition, φ₂, φ₁_L₂_f_assoc, assoc]

Result:
no goals
-- Mathlib/Data/Finsupp/Defs.lean
theorem support_zipWith [D : DecidableEq α] {f : M → N → P} {hf : f 0 0 = 0} {g₁ : α →₀ M}
    {g₂ : α →₀ N} : (zipWith f hf g₁ g₂).support ⊆ g₁.support ∪ g₂.support

Proof state:
α : Type u_1
M : Type u_5
N : Type u_7
P : Type u_8
inst✝² : Zero M
inst✝¹ : Zero N
inst✝ : Zero P
D : DecidableEq α
f : M → N → P
hf : f 0 0 = 0
g₁ : α →₀ M
g₂ : α →₀ N
⊢ (zipWith f hf g₁ g₂).support ⊆ g₁.support ∪ g₂.support

Tactic:
convert support_onFinset_subset

Result:
no goals
-- Mathlib/LinearAlgebra/Matrix/StdBasis.lean
theorem stdBasis_eq_stdBasisMatrix (i : m) (j : n) [DecidableEq m] [DecidableEq n] :
    stdBasis R m n (i, j) = stdBasisMatrix i j (1 : R)

Proof state:
R : Type u_1
m : Type u_2
n : Type u_3
inst✝⁴ : Fintype m
inst✝³ : Finite n
inst✝² : Semiring R
i : m
j : n
inst✝¹ : DecidableEq m
inst✝ : DecidableEq n
⊢ (stdBasis R m n) (i, j) = stdBasisMatrix i j 1

Tactic:
simp [stdBasis, stdBasisMatrix_eq_of_single_single]

Result:
no goals
-- Mathlib/Data/Fin/Basic.lean
theorem one_eq_mk {n a : Nat} {ha : a < n + 2} :
    1 = (⟨a, ha⟩ : Fin (n + 2)) ↔ a = 1

Proof state:
n a : ℕ
ha : a < n + 2
⊢ 1 = ⟨a, ha⟩ ↔ a = 1

Tactic:
simp [eq_comm]

Result:
no goals
-- Mathlib/MeasureTheory/OuterMeasure/Caratheodory.lean
lemma isCaratheodory_partialSups {ι : Type*} [PartialOrder ι] [LocallyFiniteOrderBot ι]
    {s : ι → Set α} (h : ∀ i, m.IsCaratheodory (s i)) (i : ι) :
    m.IsCaratheodory (partialSups s i)

Proof state:
α : Type u
m : OuterMeasure α
ι : Type u_1
inst✝¹ : PartialOrder ι
inst✝ : LocallyFiniteOrderBot ι
s : ι → Set α
h : ∀ (i : ι), m.IsCaratheodory (s i)
i : ι
⊢ m.IsCaratheodory ((partialSups s) i)

Tactic:
simpa only [partialSups_apply, Finset.sup'_eq_sup, Finset.sup_set_eq_biUnion, ← Finset.mem_coe,
  Finset.coe_Iic] using .biUnion_of_finite (finite_Iic _) (fun j _ ↦ h j)

Result:
no goals
-- Mathlib/Algebra/MonoidAlgebra/Basic.lean
theorem lift_apply (F : G →* A) (f : MonoidAlgebra k G) :
    lift k G A F f = f.sum fun a b => b • F a

Proof state:
k : Type u₁
G : Type u₂
inst✝³ : CommSemiring k
inst✝² : Monoid G
A : Type u₃
inst✝¹ : Semiring A
inst✝ : Algebra k A
F : G →* A
f : MonoidAlgebra k G
⊢ ((lift k G A) F) f = sum f fun a b => b • F a

Tactic:
simp only [lift_apply', Algebra.smul_def]

Result:
no goals