harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/CategoryTheory/MorphismProperty/Comma.lean
lemma inv_hom {X Y : P.Comma L R Q W} (f : X ⟶ Y) [IsIso f] : (inv f).hom = inv f.hom

Proof state:
case hom_inv_id
A : Type u_1
inst✝⁵ : Category.{u_4, u_1} A
B : Type u_2
inst✝⁴ : Category.{u_5, u_2} B
T : Type u_3
inst✝³ : Category.{u_6, u_3} T
L : A ⥤ T
R : B ⥤ T
P : MorphismProperty T
Q : MorphismProperty A
W : MorphismProperty B
inst✝² : Q.IsMultiplicative
inst✝¹ : W.IsMultiplicative
X Y : MorphismProperty.Comma L R P Q W
f : X ⟶ Y
inst✝ : IsIso f
⊢ Hom.hom f ≫ Hom.hom (inv f) = 𝟙 X.toComma

Tactic:
rw [← comp_hom, IsIso.hom_inv_id, id_hom]

Result:
no goals

Proof state:
A : Type u_1
inst✝⁵ : Category.{u_4, u_1} A
B : Type u_2
inst✝⁴ : Category.{u_5, u_2} B
T : Type u_3
inst✝³ : Category.{u_6, u_3} T
L : A ⥤ T
R : B ⥤ T
P : MorphismProperty T
Q : MorphismProperty A
W : MorphismProperty B
inst✝² : Q.IsMultiplicative
inst✝¹ : W.IsMultiplicative
X Y : MorphismProperty.Comma L R P Q W
f : X ⟶ Y
inst✝ : IsIso f
⊢ Hom.hom (inv f) = inv (Hom.hom f)

Tactic:
apply IsIso.eq_inv_of_hom_inv_id

Result:
case hom_inv_id
A : Type u_1
inst✝⁵ : Category.{u_4, u_1} A
B : Type u_2
inst✝⁴ : Category.{u_5, u_2} B
T : Type u_3
inst✝³ : Category.{u_6, u_3} T
L : A ⥤ T
R : B ⥤ T
P : MorphismProperty T
Q : MorphismProperty A
W : MorphismProperty B
inst✝² : Q.IsMultiplicative
inst✝¹ : W.IsMultiplicative
X Y : MorphismProperty.Comma L R P Q W
f : X ⟶ Y
inst✝ : IsIso f
⊢ Hom.hom f ≫ Hom.hom (inv f) = 𝟙 X.toComma
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Lemmas.lean
theorem mem_nil_iff (a : α) : a ∈ ([] : List α) ↔ False

Proof state:
α : Type u_1
a : α
⊢ a ∈ [] ↔ False

Tactic:
simp

Result:
no goals
-- Mathlib/Algebra/Star/Subalgebra.lean
theorem sInf_toSubalgebra (S : Set (StarSubalgebra R A)) :
    (sInf S).toSubalgebra = sInf (StarSubalgebra.toSubalgebra '' S) :=
  SetLike.coe_injective <| by simp

Proof state:
R : Type u_2
A : Type u_3
inst✝⁵ : CommSemiring R
inst✝⁴ : StarRing R
inst✝³ : Semiring A
inst✝² : Algebra R A
inst✝¹ : StarRing A
inst✝ : StarModule R A
S : Set (StarSubalgebra R A)
⊢ ↑(sInf S).toSubalgebra = ↑(sInf (toSubalgebra '' S))

Tactic:
simp

Result:
no goals
-- Mathlib/AlgebraicTopology/FundamentalGroupoid/Basic.lean
theorem transReflReparamAux_zero : transReflReparamAux 0 = 0

Proof state:
⊢ transReflReparamAux 0 = 0

Tactic:
norm_num [transReflReparamAux]

Result:
no goals
-- Mathlib/Data/Nat/Prime/Defs.lean
theorem le_minFac {m n : ℕ} : n = 1 ∨ m ≤ minFac n ↔ ∀ p, Prime p → p ∣ n → m ≤ p :=
  ⟨fun h p pp d =>
    h.elim (by rintro rfl; cases pp.not_dvd_one d) fun h =>
      le_trans h <| minFac_le_of_dvd pp.two_le d,
    fun H => or_iff_not_imp_left.2 fun n1 => H _ (minFac_prime n1) (minFac_dvd _)⟩

Proof state:
m p : ℕ
pp : Prime p
h : 1 = 1 ∨ m ≤ minFac 1
d : p ∣ 1
⊢ m ≤ p

Tactic:
cases pp.not_dvd_one d

Result:
no goals

Proof state:
m n : ℕ
h : n = 1 ∨ m ≤ n.minFac
p : ℕ
pp : Prime p
d : p ∣ n
⊢ n = 1 → m ≤ p

Tactic:
rintro rfl

Result:
m p : ℕ
pp : Prime p
h : 1 = 1 ∨ m ≤ minFac 1
d : p ∣ 1
⊢ m ≤ p
-- Mathlib/Dynamics/Ergodic/MeasurePreserving.lean
theorem add_measure {f μa' μb'} (hf : MeasurePreserving f μa μb)
    (hf' : MeasurePreserving f μa' μb') : MeasurePreserving f (μa + μa') (μb + μb') where
  measurable := hf.measurable
  map_eq

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
μa : Measure α
μb : Measure β
f : α → β
μa' : Measure α
μb' : Measure β
hf : MeasurePreserving f μa μb
hf' : MeasurePreserving f μa' μb'
⊢ map f (μa + μa') = μb + μb'

Tactic:
rw [Measure.map_add _ _ hf.measurable, hf.map_eq, hf'.map_eq]

Result:
no goals
-- Mathlib/Data/Matroid/Constructions.lean
theorem uniqueBaseOn_isBasis_iff (hX : X ⊆ E) : (uniqueBaseOn I E).IsBasis J X ↔ J = X ∩ I

Proof state:
α : Type u_1
E I X J : Set α
hX : X ⊆ E
⊢ (uniqueBaseOn I E).IsBasis J X ↔ J = X ∩ I

Tactic:
rw [isBasis_iff_maximal]

Result:
α : Type u_1
E I X J : Set α
hX : X ⊆ E
⊢ Maximal (fun I_1 => (uniqueBaseOn I E).Indep I_1 ∧ I_1 ⊆ X) J ↔ J = X ∩ I

Proof state:
α : Type u_1
E I X J : Set α
hX : X ⊆ E
⊢ (uniqueBaseOn I E).Indep (X ∩ I) ∧ X ∩ I ⊆ X

Tactic:
simp [inter_subset_left.trans hX]

Result:
no goals

Proof state:
α : Type u_1
E I X J : Set α
hX : X ⊆ E
⊢ Maximal (fun I_1 => (uniqueBaseOn I E).Indep I_1 ∧ I_1 ⊆ X) J ↔ J = X ∩ I

Tactic:
exact maximal_iff_eq (by simp [inter_subset_left.trans hX])
  (by simp (config := {contextual := true}))

Result:
no goals

Proof state:
α : Type u_1
E I X J : Set α
hX : X ⊆ E
⊢ ∀ ⦃x : Set α⦄, (uniqueBaseOn I E).Indep x ∧ x ⊆ X → x ≤ X ∩ I

Tactic:
simp (config := {contextual := true})

Result:
no goals
-- Mathlib/Data/Prod/Basic.lean
theorem eq_iff_fst_eq_snd_eq : ∀ {p q : α × β}, p = q ↔ p.1 = q.1 ∧ p.2 = q.2
  | ⟨p₁, p₂⟩, ⟨q₁, q₂⟩ => by simp

Proof state:
α : Type u_1
β : Type u_2
p₁ : α
p₂ : β
q₁ : α
q₂ : β
⊢ (p₁, p₂) = (q₁, q₂) ↔ (p₁, p₂).fst = (q₁, q₂).fst ∧ (p₁, p₂).snd = (q₁, q₂).snd

Tactic:
simp

Result:
no goals
-- Mathlib/SetTheory/Ordinal/Basic.lean
theorem card_eq_one {o} : card o = 1 ↔ o = 1

Proof state:
o : Ordinal.{u_1}
⊢ o.card = 1 ↔ o = 1

Tactic:
simpa using card_eq_nat (n := 1)

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/UInt/Lemmas.lean
theorem UInt32.toNat_le_of_le {n : UInt32} {m : Nat} (h : m < size) : n ≤ ofNat m → n.toNat ≤ m

Proof state:
n : UInt32
m : Nat
h : m < size
⊢ n ≤ ofNat m → n.toNat ≤ m

Tactic:
simp [le_def, BitVec.le_def, UInt32.toNat, toBitVec_eq_of_lt h]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/List/Associative.lean
theorem getValueCast!_insertEntry [BEq α] [LawfulBEq α] {l : List ((a : α) × β a)} {k a : α}
    [Inhabited (β a)] {v : β k} : getValueCast! a (insertEntry k v l) =
      if h : k == a then cast (congrArg β (eq_of_beq h)) v else getValueCast! a l

Proof state:
α : Type u
β : α → Type v
inst✝² : BEq α
inst✝¹ : LawfulBEq α
l : List ((a : α) × β a)
k a : α
inst✝ : Inhabited (β a)
v : β k
⊢ getValueCast! a (insertEntry k v l) = if h : (k == a) = true then cast ⋯ v else getValueCast! a l

Tactic:
simp [getValueCast!_eq_getValueCast?, getValueCast?_insertEntry, apply_dite Option.get!]

Result:
no goals
-- Mathlib/RingTheory/Multiplicity.lean
theorem multiplicity_eq_one_of_not_finiteMultiplicity (h : ¬FiniteMultiplicity a b) :
    multiplicity a b = 1

Proof state:
α : Type u_1
inst✝ : Monoid α
a b : α
h : ¬FiniteMultiplicity a b
⊢ multiplicity a b = 1

Tactic:
simp [multiplicity, emultiplicity_eq_top.2 h]

Result:
no goals
-- Mathlib/Analysis/Asymptotics/Theta.lean
theorem IsTheta.tendsto_norm_atTop_iff (h : f' =Θ[l] g') :
    Tendsto (norm ∘ f') l atTop ↔ Tendsto (norm ∘ g') l atTop

Proof state:
α : Type u_1
E' : Type u_6
F' : Type u_7
inst✝¹ : SeminormedAddCommGroup E'
inst✝ : SeminormedAddCommGroup F'
f' : α → E'
g' : α → F'
l : Filter α
h : f' =Θ[l] g'
⊢ Tendsto (norm ∘ f') l atTop ↔ Tendsto (norm ∘ g') l atTop

Tactic:
simp only [Function.comp_def, ← isLittleO_const_left_of_ne (one_ne_zero' ℝ),
  h.isLittleO_congr_right]

Result:
no goals
-- Mathlib/Algebra/BigOperators/Expect.lean
/-- Reorder an average.

The difference with `Finset.expect_bij'` is that the bijection is specified as a surjective
injection, rather than by an inverse function.

The difference with `Finset.expect_nbij` is that the bijection is allowed to use membership of the
domain of the average, rather than being a non-dependent function. -/
lemma expect_bij (i : ∀ a ∈ s, κ) (hi : ∀ a ha, i a ha ∈ t) (h : ∀ a ha, f a = g (i a ha))
    (i_inj : ∀ a₁ ha₁ a₂ ha₂, i a₁ ha₁ = i a₂ ha₂ → a₁ = a₂)
    (i_surj : ∀ b ∈ t, ∃ a ha, i a ha = b) : 𝔼 i ∈ s, f i = 𝔼 i ∈ t, g i

Proof state:
ι : Type u_1
κ : Type u_2
M : Type u_3
inst✝¹ : AddCommMonoid M
inst✝ : Module ℚ≥0 M
s : Finset ι
f : ι → M
t : Finset κ
g : κ → M
i : (a : ι) → a ∈ s → κ
hi : ∀ (a : ι) (ha : a ∈ s), i a ha ∈ t
h : ∀ (a : ι) (ha : a ∈ s), f a = g (i a ha)
i_inj : ∀ (a₁ : ι) (ha₁ : a₁ ∈ s) (a₂ : ι) (ha₂ : a₂ ∈ s), i a₁ ha₁ = i a₂ ha₂ → a₁ = a₂
i_surj : ∀ b ∈ t, ∃ a, ∃ (ha : a ∈ s), i a ha = b
⊢ 𝔼 i ∈ s, f i = 𝔼 i ∈ t, g i

Tactic:
simp_rw [expect, card_bij i hi i_inj i_surj, sum_bij i hi i_inj i_surj h]

Result:
no goals
-- Mathlib/Order/Filter/Map.lean
theorem comap_le_iff_le_kernMap : comap m g ≤ f ↔ g ≤ kernMap m f

Proof state:
α : Type u_1
β : Type u_2
g : Filter β
m : α → β
f : Filter α
⊢ comap m g ≤ f ↔ g ≤ kernMap m f

Tactic:
simp [Filter.le_def, mem_comap'', mem_kernMap, -mem_comap]

Result:
no goals
-- Mathlib/Probability/Kernel/Composition/CompMap.lean
lemma fst_comp (κ : Kernel α β) (η : Kernel β (γ × δ)) : (η ∘ₖ κ).fst = η.fst ∘ₖ κ

Proof state:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
γ : Type u_4
δ : Type u_5
mγ : MeasurableSpace γ
mδ : MeasurableSpace δ
κ : Kernel α β
η : Kernel β (γ × δ)
⊢ (η ∘ₖ κ).fst = η.fst ∘ₖ κ

Tactic:
simp [fst_eq, map_comp κ η _]

Result:
no goals
-- Mathlib/RingTheory/Localization/FractionRing.lean
@[simp]
lemma algEquivOfAlgEquiv_algebraMap
    (a : A) : algEquivOfAlgEquiv h (algebraMap A K a) = algebraMap B L (h a)

Proof state:
R : Type u_8
A : Type u_9
K : Type u_10
B : Type u_11
L : Type u_12
inst✝¹⁴ : CommSemiring R
inst✝¹³ : CommRing A
inst✝¹² : CommRing B
inst✝¹¹ : CommRing K
inst✝¹⁰ : CommRing L
inst✝⁹ : Algebra R A
inst✝⁸ : Algebra R K
inst✝⁷ : Algebra A K
inst✝⁶ : IsFractionRing A K
inst✝⁵ : IsScalarTower R A K
inst✝⁴ : Algebra R B
inst✝³ : Algebra R L
inst✝² : Algebra B L
inst✝¹ : IsFractionRing B L
inst✝ : IsScalarTower R B L
h : A ≃ₐ[R] B
a : A
⊢ (algEquivOfAlgEquiv h) ((algebraMap A K) a) = (algebraMap B L) (h a)

Tactic:
simp [algEquivOfAlgEquiv]

Result:
no goals
-- Mathlib/NumberTheory/ArithmeticFunction.lean
theorem natCoe_mul [Semiring R] {f g : ArithmeticFunction ℕ} :
    (↑(f * g) : ArithmeticFunction R) = f * g

Proof state:
case h
R : Type u_1
inst✝ : Semiring R
f g : ArithmeticFunction ℕ
n : ℕ
⊢ ↑(f * g) n = (↑f * ↑g) n

Tactic:
simp

Result:
no goals

Proof state:
R : Type u_1
inst✝ : Semiring R
f g : ArithmeticFunction ℕ
⊢ ↑(f * g) = ↑f * ↑g

Tactic:
ext n

Result:
case h
R : Type u_1
inst✝ : Semiring R
f g : ArithmeticFunction ℕ
n : ℕ
⊢ ↑(f * g) n = (↑f * ↑g) n
-- Mathlib/MeasureTheory/Integral/DominatedConvergence.lean
theorem continuous_parametric_intervalIntegral_of_continuous'
    (hf : Continuous f.uncurry) (a₀ b₀ : ℝ) :
    Continuous fun x ↦ ∫ t in a₀..b₀, f x t ∂μ

Proof state:
E : Type u_1
X : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : TopologicalSpace X
μ : Measure ℝ
inst✝¹ : NoAtoms μ
inst✝ : IsLocallyFiniteMeasure μ
f : X → ℝ → E
hf : Continuous (Function.uncurry f)
a₀ b₀ : ℝ
⊢ Continuous fun x => ∫ (t : ℝ) in a₀..b₀, f x t ∂μ

Tactic:
fun_prop

Result:
no goals
-- Mathlib/Algebra/Group/Graph.lean
/-- **Line test** for group isomorphisms.

Let `f : G → H × I` be a homomorphism to a product of groups. Assume that `f` is surjective on both
factors and that the image of `f` intersects every "vertical line" `{(h, i) | i : I}` and every
"horizontal line" `{(h, i) | h : H}` at most once. Then the image of `f` is the graph of some group
isomorphism `f' : H ≃ I`. -/
@[to_additive "**Line test** for monoid isomorphisms.

Let `f : G → H × I` be a homomorphism to a product of groups. Assume that `f` is surjective on both
factors and that the image of `f` intersects every \"vertical line\" `{(h, i) | i : I}` and every
\"horizontal line\" `{(h, i) | h : H}` at most once. Then the image of `f` is the graph of some
group isomorphism `f' : H ≃ I`."]
lemma exists_mulEquiv_range_eq_graph {f : G →* H × I} (hf₁ : Surjective (Prod.fst ∘ f))
    (hf₂ : Surjective (Prod.snd ∘ f)) (hf : ∀ g₁ g₂, (f g₁).1 = (f g₂).1 ↔ (f g₁).2 = (f g₂).2) :
    ∃ e : H ≃* I, range f = e.toMonoidHom.graph

Proof state:
G : Type u_1
H : Type u_2
I : Type u_3
inst✝² : Group G
inst✝¹ : Group H
inst✝ : Group I
f : G →* H × I
hf₁ : Surjective (Prod.fst ∘ ⇑f)
hf₂ : Surjective (Prod.snd ∘ ⇑f)
hf : ∀ (g₁ g₂ : G), (f g₁).1 = (f g₂).1 ↔ (f g₁).2 = (f g₂).2
⊢ ∃ e, f.range = e.toMonoidHom.graph

Tactic:
simpa [SetLike.ext_iff] using exists_mulEquiv_mrange_eq_mgraph hf₁ hf₂ hf

Result:
no goals
-- Mathlib/Data/Rel.lean
theorem preimage_top {s : Set β} (h : Set.Nonempty s) :
    (⊤ : Rel α β).preimage s = Set.univ

Proof state:
α : Type u_1
β : Type u_2
s : Set β
h : s.Nonempty
⊢ ⊤.preimage s = Set.univ

Tactic:
rwa [← inv_top, preimage, inv_inv, image_top]

Result:
no goals
-- Mathlib/NumberTheory/ArithmeticFunction.lean
theorem abs_moebius_eq_one_of_squarefree {l : ℕ} (hl : Squarefree l) : |μ l| = 1

Proof state:
l : ℕ
hl : Squarefree l
⊢ |μ l| = 1

Tactic:
simp only [moebius_apply_of_squarefree hl, abs_pow, abs_neg, abs_one, one_pow]

Result:
no goals
-- Mathlib/Algebra/Order/Sub/Basic.lean
theorem tsub_pos_iff_not_le : 0 < a - b ↔ ¬a ≤ b

Proof state:
α : Type u_1
inst✝⁴ : AddCommMonoid α
inst✝³ : PartialOrder α
inst✝² : CanonicallyOrderedAdd α
inst✝¹ : Sub α
inst✝ : OrderedSub α
a b : α
⊢ 0 < a - b ↔ ¬a ≤ b

Tactic:
rw [pos_iff_ne_zero, Ne, tsub_eq_zero_iff_le]

Result:
no goals
-- Mathlib/SetTheory/Ordinal/Notation.lean
theorem zero_lt_one : (0 : ONote) < 1

Proof state:
⊢ 0 < 1

Tactic:
simp only [lt_def, repr_zero, repr_one, Nat.cast_one, zero_lt_one]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Trigonometric/ArctanDeriv.lean
theorem hasDerivAt_tan {x : ℝ} (h : cos x ≠ 0) : HasDerivAt tan (1 / cos x ^ 2) x :=
  mod_cast (Complex.hasDerivAt_tan (by exact mod_cast h)).real_of_complex

Proof state:
x : ℝ
h : cos x ≠ 0
⊢ Complex.cos ↑x ≠ 0

Tactic:
exact mod_cast h

Result:
no goals
-- Mathlib/RingTheory/Valuation/Basic.lean
theorem isEquiv_iff_val_le_one [LinearOrderedCommGroupWithZero Γ₀]
    [LinearOrderedCommGroupWithZero Γ'₀] {v : Valuation K Γ₀} {v' : Valuation K Γ'₀} :
    v.IsEquiv v' ↔ ∀ {x : K}, v x ≤ 1 ↔ v' x ≤ 1 :=
  ⟨fun h x => by simpa using h x 1, isEquiv_of_val_le_one⟩

Proof state:
K : Type u_1
inst✝² : DivisionRing K
Γ₀ : Type u_4
Γ'₀ : Type u_5
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
inst✝ : LinearOrderedCommGroupWithZero Γ'₀
v : Valuation K Γ₀
v' : Valuation K Γ'₀
h : v.IsEquiv v'
x : K
⊢ v x ≤ 1 ↔ v' x ≤ 1

Tactic:
simpa using h x 1

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem _root_.List.filterMap_toArray (f : α → Option β) (l : List α) :
    l.toArray.filterMap f = (l.filterMap f).toArray

Proof state:
α : Type u_1
β : Type u_2
f : α → Option β
l : List α
⊢ filterMap f l.toArray = (List.filterMap f l).toArray

Tactic:
simp

Result:
no goals
-- Mathlib/CategoryTheory/Shift/ShiftSequence.lean
@[reassoc]
lemma shiftIso_inv_naturality {X Y : C} (n a a' : M) (ha' : n + a = a') (f : X ⟶ Y) :
    (shift F a').map f ≫ (shiftIso F n a a' ha').inv.app Y =
      (shiftIso F n a a' ha').inv.app X ≫ (shift F a).map (f⟦n⟧')

Proof state:
C : Type u_1
A : Type u_2
inst✝⁴ : Category.{u_5, u_1} C
inst✝³ : Category.{u_6, u_2} A
F : C ⥤ A
M : Type u_3
inst✝² : AddMonoid M
inst✝¹ : HasShift C M
inst✝ : F.ShiftSequence M
X Y : C
n a a' : M
ha' : n + a = a'
f : X ⟶ Y
⊢ (F.shift a').map f ≫ (F.shiftIso n a a' ha').inv.app Y =
    (F.shiftIso n a a' ha').inv.app X ≫ (F.shift a).map ((shiftFunctor C n).map f)

Tactic:
simp

Result:
no goals
-- Mathlib/LinearAlgebra/AffineSpace/AffineSubspace/Defs.lean
theorem vectorSpan_empty : vectorSpan k (∅ : Set P) = (⊥ : Submodule k V)

Proof state:
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
⊢ vectorSpan k ∅ = ⊥

Tactic:
rw [vectorSpan_def, vsub_empty, Submodule.span_empty]

Result:
no goals
-- Mathlib/ModelTheory/Algebra/Ring/Basic.lean
theorem realize_add (x y : ring.Term α) (v : α → R) :
    Term.realize v (x + y) = Term.realize v x + Term.realize v y

Proof state:
α : Type u_1
R : Type u_2
inst✝⁵ : Add R
inst✝⁴ : Mul R
inst✝³ : Neg R
inst✝² : One R
inst✝¹ : Zero R
inst✝ : CompatibleRing R
x y : ring.Term α
v : α → R
⊢ Term.realize v (x + y) = Term.realize v x + Term.realize v y

Tactic:
simp [add_def, funMap_add]

Result:
no goals
-- Mathlib/Analysis/Normed/Ring/SmoothingSeminorm.lean
theorem mu_le (n : ℕ) : mu μ hn n ≤ n

Proof state:
R : Type u_1
inst✝ : CommRing R
μ : RingSeminorm R
x y : R
hn : ∀ (n : ℕ), ∃ m < n + 1, μ ((x + y) ^ n) ^ (1 / ↑n) ≤ (μ (x ^ m) * μ (y ^ (n - m))) ^ (1 / ↑n)
n : ℕ
⊢ mu μ hn n ≤ n

Tactic:
simpa [mu, ← Nat.lt_succ_iff] using (Classical.choose_spec (hn n)).1

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Int/Lemmas.lean
theorem add_neg_cancel_right (a b : Int) : a + b + -b = a

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

Tactic:
rw [Int.add_assoc, Int.add_right_neg, Int.add_zero]

Result:
no goals
-- Mathlib/Algebra/Order/GroupWithZero/Unbundled.lean
/-- See `inv_mul_lt_iff₀'` for a version with multiplication on the other side. -/
lemma inv_mul_lt_iff₀ (hc : 0 < c) : c⁻¹ * b < a ↔ b < c * a where
  mp h

Proof state:
G₀ : Type u_2
inst✝⁴ : GroupWithZero G₀
inst✝³ : PartialOrder G₀
inst✝² : ZeroLEOneClass G₀
inst✝¹ : PosMulReflectLT G₀
a b c : G₀
inst✝ : PosMulStrictMono G₀
hc : 0 < c
h : c⁻¹ * b < a
⊢ b < c * a

Tactic:
simpa [hc.ne'] using mul_lt_mul_of_pos_left h hc

Result:
no goals

Proof state:
G₀ : Type u_2
inst✝⁴ : GroupWithZero G₀
inst✝³ : PartialOrder G₀
inst✝² : ZeroLEOneClass G₀
inst✝¹ : PosMulReflectLT G₀
a b c : G₀
inst✝ : PosMulStrictMono G₀
hc : 0 < c
h : b < c * a
⊢ c⁻¹ * b < a

Tactic:
simpa [hc.ne'] using mul_lt_mul_of_pos_left h (inv_pos.2 hc)

Result:
no goals
-- Mathlib/Order/Bounded.lean
theorem bounded_gt_Ici [Preorder α] [NoMinOrder α] (a : α) : Bounded (· > ·) (Ici a)

Proof state:
α : Type u_1
inst✝¹ : Preorder α
inst✝ : NoMinOrder α
a : α
⊢ Bounded (fun x1 x2 => x1 > x2) (Ici a)

Tactic:
simp only [← bounded_ge_iff_bounded_gt, bounded_ge_Ici]

Result:
no goals
-- Mathlib/Algebra/Group/Subgroup/ZPowers/Lemmas.lean
theorem intCast_mul_mem_zmultiples : ↑(k : ℤ) * r ∈ zmultiples r

Proof state:
R : Type u_4
inst✝ : Ring R
r : R
k : ℤ
⊢ ↑k * r ∈ zmultiples r

Tactic:
simpa only [← zsmul_eq_mul] using zsmul_mem_zmultiples r k

Result:
no goals
-- Mathlib/Algebra/Group/Basic.lean
theorem mul_inv_eq_one : a * b⁻¹ = 1 ↔ a = b

Proof state:
G : Type u_3
inst✝ : Group G
a b : G
⊢ a * b⁻¹ = 1 ↔ a = b

Tactic:
rw [mul_eq_one_iff_eq_inv, inv_inv]

Result:
no goals
-- Mathlib/RingTheory/Ideal/Operations.lean
theorem isCoprime_iff_exists : IsCoprime I J ↔ ∃ i ∈ I, ∃ j ∈ J, i + j = 1

Proof state:
R : Type u
inst✝ : CommSemiring R
I J : Ideal R
⊢ IsCoprime I J ↔ ∃ i ∈ I, ∃ j ∈ J, i + j = 1

Tactic:
rw [← add_eq_one_iff, isCoprime_iff_add]

Result:
no goals
-- Mathlib/Data/Sign.lean
theorem nonpos_iff_ne_one {a : SignType} : a ≤ 0 ↔ a ≠ 1

Proof state:
a : SignType
⊢ a ≤ 0 ↔ a ≠ 1

Tactic:
cases a <;> decide

Result:
no goals
-- Mathlib/LinearAlgebra/Span/Defs.lean
theorem mem_sup' : x ∈ p ⊔ p' ↔ ∃ (y : p) (z : p'), (y : M) + z = x :=
  mem_sup.trans <| by simp only [Subtype.exists, exists_prop]

Proof state:
R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
x : M
p p' : Submodule R M
⊢ (∃ y ∈ p, ∃ z ∈ p', y + z = x) ↔ ∃ y z, ↑y + ↑z = x

Tactic:
simp only [Subtype.exists, exists_prop]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Attach.lean
theorem toList_attachWith {l : Vector α n} {P : α → Prop} {H : ∀ x ∈ l, P x} :
   (l.attachWith P H).toList = l.toList.attachWith P (by simpa using H)

Proof state:
α : Type u_1
n : Nat
l : Vector α n
P : α → Prop
H : ∀ (x : α), x ∈ l → P x
⊢ (l.attachWith P H).toList = l.toList.attachWith P ⋯

Tactic:
simp [attachWith]

Result:
no goals

Proof state:
α : Type ?u.5118
n : Nat
l : Vector α n
P : α → Prop
H : ∀ (x : α), x ∈ l → P x
⊢ ∀ (x : α), x ∈ l.toList → P x

Tactic:
simpa using H

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Lemmas.lean
theorem ne_nil_of_tail_ne_nil {l : List α} : l.tail ≠ [] → l ≠ []

Proof state:
α : Type u_1
l : List α
⊢ l.tail ≠ [] → l ≠ []

Tactic:
cases l <;> simp

Result:
no goals
-- Mathlib/Data/Fintype/Sets.lean
theorem toFinset_nonempty {s : Set α} [Fintype s] : s.toFinset.Nonempty ↔ s.Nonempty

Proof state:
α : Type u_1
s : Set α
inst✝ : Fintype ↑s
⊢ s.toFinset.Nonempty ↔ s.Nonempty

Tactic:
rw [← Finset.coe_nonempty, coe_toFinset]

Result:
no goals
-- Mathlib/Order/Interval/Set/UnorderedInterval.lean
@[simp] lemma right_mem_uIoc : b ∈ Ι a b ↔ a < b

Proof state:
α : Type u_1
inst✝ : LinearOrder α
a b : α
⊢ b ∈ Ι a b ↔ a < b

Tactic:
simp [mem_uIoc]

Result:
no goals
-- Mathlib/GroupTheory/CommutingProbability.lean
lemma commProb_nil : commProb (Product []) = 1

Proof state:
⊢ commProb (Product []) = 1

Tactic:
simp [Product, commProb_pi]

Result:
no goals
-- Mathlib/Order/Filter/Map.lean
theorem neBot_inf_comap_iff_map' {f : α → β} {F : Filter α} {G : Filter β} :
    NeBot (comap f G ⊓ F) ↔ NeBot (G ⊓ map f F)

Proof state:
α : Type u_1
β : Type u_2
f : α → β
F : Filter α
G : Filter β
⊢ (comap f G ⊓ F).NeBot ↔ (G ⊓ map f F).NeBot

Tactic:
rw [← map_neBot_iff, Filter.push_pull']

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Complex/Arg.lean
theorem norm_mul_cos_add_sin_mul_I (x : ℂ) : (‖x‖ * (cos (arg x) + sin (arg x) * I) : ℂ) = x

Proof state:
x : ℂ
⊢ ↑‖x‖ * (cos ↑x.arg + sin ↑x.arg * I) = x

Tactic:
rw [← exp_mul_I, norm_mul_exp_arg_mul_I]

Result:
no goals
-- Mathlib/Combinatorics/Additive/Dissociation.lean
@[to_additive]
lemma prod_div_prod_mem_mulSpan (ht : t ⊆ s) (hu : u ⊆ s) :
    (∏ a ∈ t, a) / ∏ a ∈ u, a ∈ mulSpan s :=
  mem_mulSpan.2 ⟨Set.indicator t 1 - Set.indicator u 1, fun a ↦ by
    by_cases a ∈ t <;> by_cases a ∈ u <;> simp [*], by simp [prod_div_distrib, zpow_sub,
      ← div_eq_mul_inv, Set.indicator, pow_ite, inter_eq_right.2, *]⟩

Proof state:
α : Type u_1
inst✝² : CommGroup α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
s t u : Finset α
ht : t ⊆ s
hu : u ⊆ s
a : α
⊢ ((↑t).indicator 1 - (↑u).indicator 1) a = -1 ∨
    ((↑t).indicator 1 - (↑u).indicator 1) a = 0 ∨ ((↑t).indicator 1 - (↑u).indicator 1) a = 1

Tactic:
by_cases a ∈ t <;> by_cases a ∈ u <;> simp [*]

Result:
no goals

Proof state:
α : Type u_1
inst✝² : CommGroup α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
s t u : Finset α
ht : t ⊆ s
hu : u ⊆ s
⊢ ∏ a ∈ s, a ^ ((↑t).indicator 1 - (↑u).indicator 1) a = (∏ a ∈ t, a) / ∏ a ∈ u, a

Tactic:
simp [prod_div_distrib, zpow_sub,
← div_eq_mul_inv, Set.indicator, pow_ite, inter_eq_right.2, *]

Result:
no goals
-- Mathlib/Order/Filter/Prod.lean
theorem prod_pure_pure {a : α} {b : β} :
    (pure a : Filter α) ×ˢ (pure b : Filter β) = pure (a, b)

Proof state:
α : Type u_1
β : Type u_2
a : α
b : β
⊢ pure a ×ˢ pure b = pure (a, b)

Tactic:
simp

Result:
no goals
-- Mathlib/LinearAlgebra/AffineSpace/AffineSubspace/Basic.lean
theorem bot_parallel_iff_eq_bot {s : AffineSubspace k P} : ⊥ ∥ s ↔ s = ⊥

Proof state:
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : AffineSubspace k P
⊢ ⊥ ∥ s ↔ s = ⊥

Tactic:
rw [parallel_comm, parallel_bot_iff_eq_bot]

Result:
no goals
-- Mathlib/SetTheory/Ordinal/FixedPoint.lean
theorem nfp_zero : nfp 0 = id

Proof state:
case h
x✝ : Ordinal.{u_1}
⊢ nfp 0 x✝ = id x✝

Tactic:
exact nfp_zero_left _

Result:
no goals

Proof state:
⊢ nfp 0 = id

Tactic:
ext

Result:
case h
x✝ : Ordinal.{u_1}
⊢ nfp 0 x✝ = id x✝
-- Mathlib/Order/Height.lean
theorem wellFoundedLT_of_chainHeight_ne_top (s : Set α) (hs : s.chainHeight ≠ ⊤) :
    WellFoundedLT s :=
  wellFoundedGT_of_chainHeight_ne_top (ofDual ⁻¹' s) <| by rwa [chainHeight_dual]

Proof state:
α : Type u_1
inst✝ : Preorder α
s : Set α
hs : s.chainHeight ≠ ⊤
⊢ (⇑ofDual ⁻¹' s).chainHeight ≠ ⊤

Tactic:
rwa [chainHeight_dual]

Result:
no goals