harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/AlgebraicGeometry/AffineSpace.lean
@[simp]
lemma homOfVector_appTop_coord (i) :
    (homOfVector f v).appTop (coord S i) = v i

Proof state:
n : Type v
S X : Scheme
f : X ⟶ S
v : n → ↑Γ(X, ⊤)
i : n
⊢ (ConcreteCategory.hom (Scheme.Hom.appTop (homOfVector f v))) (coord S i) = v i

Tactic:
rw [coord, ← toSpecMvPolyIntEquiv_comp, homOfVector_toSpecMvPoly,
  Equiv.apply_symm_apply]

Result:
no goals
-- Mathlib/FieldTheory/SplittingField/IsSplittingField.lean
theorem mul (f g : F[X]) (hf : f ≠ 0) (hg : g ≠ 0) [IsSplittingField F K f]
    [IsSplittingField K L (g.map <| algebraMap F K)] : IsSplittingField F L (f * g) :=
  ⟨(IsScalarTower.algebraMap_eq F K L).symm ▸
      splits_mul _ (splits_comp_of_splits _ _ (splits K f))
        ((splits_map_iff _ _).1 (splits L <| g.map <| algebraMap F K)), by
    classical
    rw [rootSet, aroots_mul (mul_ne_zero hf hg),
      Multiset.toFinset_add, Finset.coe_union, Algebra.adjoin_union_eq_adjoin_adjoin,
      aroots_def, aroots_def, IsScalarTower.algebraMap_eq F K L, ← map_map,
      roots_map (algebraMap K L) ((splits_id_iff_splits <| algebraMap F K).2 <| splits K f),
      Multiset.toFinset_map, Finset.coe_image, Algebra.adjoin_algebraMap, ← rootSet, adjoin_rootSet,
      Algebra.map_top, IsScalarTower.adjoin_range_toAlgHom, ← map_map, ← rootSet, adjoin_rootSet,
      Subalgebra.restrictScalars_top]⟩

Proof state:
F : Type u
K : Type v
L : Type w
inst✝⁸ : Field K
inst✝⁷ : Field L
inst✝⁶ : Field F
inst✝⁵ : Algebra K L
inst✝⁴ : Algebra F K
inst✝³ : Algebra F L
inst✝² : IsScalarTower F K L
f g : F[X]
hf : f ≠ 0
hg : g ≠ 0
inst✝¹ : IsSplittingField F K f
inst✝ : IsSplittingField K L (Polynomial.map (algebraMap F K) g)
⊢ Algebra.adjoin F ((f * g).rootSet L) = ⊤

Tactic:
classical
rw [rootSet, aroots_mul (mul_ne_zero hf hg),
  Multiset.toFinset_add, Finset.coe_union, Algebra.adjoin_union_eq_adjoin_adjoin,
  aroots_def, aroots_def, IsScalarTower.algebraMap_eq F K L, ← map_map,
  roots_map (algebraMap K L) ((splits_id_iff_splits <| algebraMap F K).2 <| splits K f),
  Multiset.toFinset_map, Finset.coe_image, Algebra.adjoin_algebraMap, ← rootSet, adjoin_rootSet,
  Algebra.map_top, IsScalarTower.adjoin_range_toAlgHom, ← map_map, ← rootSet, adjoin_rootSet,
  Subalgebra.restrictScalars_top]

Result:
no goals

Proof state:
F : Type u
K : Type v
L : Type w
inst✝⁸ : Field K
inst✝⁷ : Field L
inst✝⁶ : Field F
inst✝⁵ : Algebra K L
inst✝⁴ : Algebra F K
inst✝³ : Algebra F L
inst✝² : IsScalarTower F K L
f g : F[X]
hf : f ≠ 0
hg : g ≠ 0
inst✝¹ : IsSplittingField F K f
inst✝ : IsSplittingField K L (Polynomial.map (algebraMap F K) g)
⊢ Algebra.adjoin F ((f * g).rootSet L) = ⊤

Tactic:
rw [rootSet, aroots_mul (mul_ne_zero hf hg),
  Multiset.toFinset_add, Finset.coe_union, Algebra.adjoin_union_eq_adjoin_adjoin,
  aroots_def, aroots_def, IsScalarTower.algebraMap_eq F K L, ← map_map,
  roots_map (algebraMap K L) ((splits_id_iff_splits <| algebraMap F K).2 <| splits K f),
  Multiset.toFinset_map, Finset.coe_image, Algebra.adjoin_algebraMap, ← rootSet, adjoin_rootSet,
  Algebra.map_top, IsScalarTower.adjoin_range_toAlgHom, ← map_map, ← rootSet, adjoin_rootSet,
  Subalgebra.restrictScalars_top]

Result:
no goals
-- Mathlib/MeasureTheory/Measure/AddContent.lean
lemma addContent_union_le (hC : IsSetRing C) (hs : s ∈ C) (ht : t ∈ C) :
    m (s ∪ t) ≤ m s + m t

Proof state:
α : Type u_1
C : Set (Set α)
s t : Set α
m : AddContent C
hC : IsSetRing C
hs : s ∈ C
ht : t ∈ C
⊢ m s + m (t \ s) ≤ m s + m t

Tactic:
exact add_le_add le_rfl
  (addContent_mono hC.isSetSemiring (hC.diff_mem ht hs) ht diff_subset)

Result:
no goals

Proof state:
α : Type u_1
C : Set (Set α)
s t : Set α
m : AddContent C
hC : IsSetRing C
hs : s ∈ C
ht : t ∈ C
⊢ Disjoint s (t \ s)

Tactic:
rw [Set.disjoint_iff_inter_eq_empty, inter_diff_self]

Result:
no goals

Proof state:
α : Type u_1
C : Set (Set α)
s t : Set α
m : AddContent C
hC : IsSetRing C
hs : s ∈ C
ht : t ∈ C
⊢ m (s ∪ t) ≤ m s + m t

Tactic:
rw [← union_diff_self, addContent_union hC hs (hC.diff_mem ht hs)]

Result:
α : Type u_1
C : Set (Set α)
s t : Set α
m : AddContent C
hC : IsSetRing C
hs : s ∈ C
ht : t ∈ C
⊢ m s + m (t \ s) ≤ m s + m t

α : Type u_1
C : Set (Set α)
s t : Set α
m : AddContent C
hC : IsSetRing C
hs : s ∈ C
ht : t ∈ C
⊢ Disjoint s (t \ s)
-- Mathlib/CategoryTheory/Shift/ShiftSequence.lean
@[reassoc]
lemma shiftMap_comp' {X Y Z : C} {n : M} (f : X ⟶ Y) (g : Y ⟶ Z⟦n⟧) (a a' : M) (ha' : n + a = a') :
    F.shiftMap (f ≫ g) a a' ha' = (F.shift a).map f ≫ F.shiftMap g a a' ha'

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 Z : C
n : M
f : X ⟶ Y
g : Y ⟶ (shiftFunctor C n).obj Z
a a' : M
ha' : n + a = a'
⊢ F.shiftMap (f ≫ g) a a' ha' = (F.shift a).map f ≫ F.shiftMap g a a' ha'

Tactic:
simp [shiftMap]

Result:
no goals
-- Mathlib/Algebra/Order/BigOperators/Group/List.lean
@[to_additive exists_lt_of_sum_lt]
lemma exists_lt_of_prod_lt' [LinearOrder M] [MulRightMono M]
    [MulLeftMono M] {l : List ι} (f g : ι → M)
    (h : (l.map f).prod < (l.map g).prod) : ∃ i ∈ l, f i < g i

Proof state:
ι : Type u_1
M : Type u_3
inst✝³ : Monoid M
inst✝² : LinearOrder M
inst✝¹ : MulRightMono M
inst✝ : MulLeftMono M
l : List ι
f g : ι → M
h : (map f l).prod < (map g l).prod
⊢ ∃ i, i ∈ l ∧ f i < g i

Tactic:
contrapose! h

Result:
ι : Type u_1
M : Type u_3
inst✝³ : Monoid M
inst✝² : LinearOrder M
inst✝¹ : MulRightMono M
inst✝ : MulLeftMono M
l : List ι
f g : ι → M
h : ∀ (i : ι), i ∈ l → g i ≤ f i
⊢ (map g l).prod ≤ (map f l).prod

Proof state:
ι : Type u_1
M : Type u_3
inst✝³ : Monoid M
inst✝² : LinearOrder M
inst✝¹ : MulRightMono M
inst✝ : MulLeftMono M
l : List ι
f g : ι → M
h : ∀ (i : ι), i ∈ l → g i ≤ f i
⊢ (map g l).prod ≤ (map f l).prod

Tactic:
exact prod_le_prod' h

Result:
no goals
-- Mathlib/Topology/MetricSpace/Thickening.lean
theorem cthickening_closure : cthickening δ (closure s) = cthickening δ s

Proof state:
α : Type u
inst✝ : PseudoEMetricSpace α
δ : ℝ
s : Set α
⊢ cthickening δ (closure s) = cthickening δ s

Tactic:
simp_rw [cthickening, infEdist_closure]

Result:
no goals
-- Mathlib/Analysis/InnerProductSpace/LinearMap.lean
@[simp] lemma innerSL_real_flip : (innerSL ℝ (E := F)).flip = innerSL ℝ

Proof state:
F : Type u_3
inst✝¹ : SeminormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
⊢ (innerSL ℝ).flip = innerSL ℝ

Tactic:
ext v w

Result:
case h.h
F : Type u_3
inst✝¹ : SeminormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
v w : F
⊢ ((innerSL ℝ).flip v) w = ((innerSL ℝ) v) w

Proof state:
case h.h
F : Type u_3
inst✝¹ : SeminormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
v w : F
⊢ ((innerSL ℝ).flip v) w = ((innerSL ℝ) v) w

Tactic:
exact real_inner_comm _ _

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/RawLemmas.lean
theorem getKeyD_insertManyIfNewUnit_empty_list_of_contains_eq_false [EquivBEq α] [LawfulHashable α]
    {l : List α} {k fallback : α}
    (h' : l.contains k = false) :
    getKeyD (insertManyIfNewUnit (empty : Raw₀ α (fun _ => Unit)) l).1 k fallback = fallback

Proof state:
α : Type u
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
l : List α
k fallback : α
h' : l.contains k = false
⊢ (insertManyIfNewUnit empty l).val.getKeyD k fallback = fallback

Tactic:
exact getKeyD_insertManyIfNewUnit_list_of_contains_eq_false_of_contains_eq_false
  _ Raw.WF.empty₀ contains_empty h'

Result:
no goals
-- Mathlib/LinearAlgebra/Matrix/FixedDetMatrices.lean
@[simp]
lemma reduce_reduceStep {A : Δ m} (hc : (A.1 1 0) ≠ 0) :
    reduce (reduceStep A) = reduce A

Proof state:
m : ℤ
A : FixedDetMatrix (Fin 2) ℤ m
hc : ↑A 1 0 ≠ 0
⊢ reduce A = reduce (reduceStep A)

Tactic:
rw [reduce, if_neg hc]

Result:
no goals

Proof state:
m : ℤ
A : FixedDetMatrix (Fin 2) ℤ m
hc : ↑A 1 0 ≠ 0
⊢ reduce (reduceStep A) = reduce A

Tactic:
symm

Result:
m : ℤ
A : FixedDetMatrix (Fin 2) ℤ m
hc : ↑A 1 0 ≠ 0
⊢ reduce A = reduce (reduceStep A)
-- Mathlib/MeasureTheory/MeasurableSpace/Embedding.lean
theorem measurable_comp_iff {f : β → γ} (e : α ≃ᵐ β) :
    Measurable (f ∘ e) ↔ Measurable f :=
  Iff.intro
    (fun hfe => by
      have : Measurable (f ∘ (e.symm.trans e).toEquiv) := hfe.comp e.symm.measurable
      rwa [coe_toEquiv, symm_trans_self] at this)
    fun h => h.comp e.measurable

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
f : β → γ
e : α ≃ᵐ β
hfe : Measurable (f ∘ ⇑e)
this : Measurable (f ∘ ⇑(e.symm.trans e).toEquiv)
⊢ Measurable f

Tactic:
rwa [coe_toEquiv, symm_trans_self] at this

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
f : β → γ
e : α ≃ᵐ β
hfe : Measurable (f ∘ ⇑e)
⊢ Measurable f

Tactic:
have : Measurable (f ∘ (e.symm.trans e).toEquiv) := hfe.comp e.symm.measurable

Result:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
f : β → γ
e : α ≃ᵐ β
hfe : Measurable (f ∘ ⇑e)
this : Measurable (f ∘ ⇑(e.symm.trans e).toEquiv)
⊢ Measurable f
-- Mathlib/Topology/Exterior.lean
theorem exterior_sUnion (S : Set (Set X)) : exterior (⋃₀ S) = ⋃ s ∈ S, exterior s

Proof state:
X : Type u_2
inst✝ : TopologicalSpace X
S : Set (Set X)
⊢ exterior (⋃₀ S) = ⋃ s ∈ S, exterior s

Tactic:
simp only [sUnion_eq_biUnion, exterior_iUnion]

Result:
no goals
-- Mathlib/Combinatorics/Enumerative/Catalan.lean
theorem mem_treesOfNumNodesEq {x : Tree Unit} {n : ℕ} :
    x ∈ treesOfNumNodesEq n ↔ x.numNodes = n

Proof state:
x : Tree Unit
n : ℕ
⊢ x ∈ treesOfNumNodesEq n ↔ x.numNodes = n

Tactic:
induction x using Tree.unitRecOn generalizing n <;> cases n <;>
  simp [treesOfNumNodesEq_succ, *]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Lemmas.lean
theorem forall_getElem {l : Vector α n} {p : α → Prop} :
    (∀ (i : Nat) h, p (l[i]'h)) ↔ ∀ a, a ∈ l → p a

Proof state:
α : Type u_1
n : Nat
l : Vector α n
p : α → Prop
⊢ (∀ (i : Nat) (h : i < n), p l[i]) ↔ ∀ (a : α), a ∈ l → p a

Tactic:
rcases l with ⟨l, rfl⟩

Result:
case mk
α : Type u_1
p : α → Prop
l : Array α
⊢ (∀ (i : Nat) (h : i < l.size), p { toArray := l, size_toArray := ⋯ }[i]) ↔
    ∀ (a : α), a ∈ { toArray := l, size_toArray := ⋯ } → p a

Proof state:
case mk
α : Type u_1
p : α → Prop
l : Array α
⊢ (∀ (i : Nat) (h : i < l.size), p { toArray := l, size_toArray := ⋯ }[i]) ↔
    ∀ (a : α), a ∈ { toArray := l, size_toArray := ⋯ } → p a

Tactic:
simp [Array.forall_getElem]

Result:
no goals
-- Mathlib/RingTheory/MvPowerSeries/Order.lean
theorem nat_le_order {n : ℕ} (h : ∀ d, degree d < n → coeff R d f = 0) :
    n ≤ f.order

Proof state:
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
f : MvPowerSeries σ R
n : ℕ
h : ∀ (d : σ →₀ ℕ), d.degree < n → (coeff R d) f = 0
⊢ ↑n ≤ f.order

Tactic:
simp_rw [degree_eq_weight_one] at h

Result:
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
f : MvPowerSeries σ R
n : ℕ
h : ∀ (d : σ →₀ ℕ), (weight fun x => 1) d < n → (coeff R d) f = 0
⊢ ↑n ≤ f.order

Proof state:
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
f : MvPowerSeries σ R
n : ℕ
h : ∀ (d : σ →₀ ℕ), (weight fun x => 1) d < n → (coeff R d) f = 0
⊢ ↑n ≤ f.order

Tactic:
exact nat_le_weightedOrder _ h

Result:
no goals
-- Mathlib/Algebra/Homology/HomotopyCategory/ShortExact.lean
@[reassoc (attr := simp)]
lemma inr_descShortComplex : inr S.f ≫ descShortComplex S = S.g

Proof state:
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Abelian C
S : ShortComplex (CochainComplex C ℤ)
⊢ inr S.f ≫ descShortComplex S = S.g

Tactic:
simp [descShortComplex]

Result:
no goals
-- Mathlib/Data/Nat/Lattice.lean
theorem iSup_lt_succ' (u : ℕ → α) (n : ℕ) : ⨆ k < n + 1, u k = u 0 ⊔ ⨆ k < n, u (k + 1)

Proof state:
α : Type u_1
inst✝ : CompleteLattice α
u : ℕ → α
n : ℕ
⊢ ⨆ k, ⨆ (_ : k < n + 1), u k = u 0 ⊔ ⨆ k, ⨆ (_ : k < n), u (k + 1)

Tactic:
rw [← sup_iSup_nat_succ]

Result:
α : Type u_1
inst✝ : CompleteLattice α
u : ℕ → α
n : ℕ
⊢ (⨆ (_ : 0 < n + 1), u 0) ⊔ ⨆ i, ⨆ (_ : i + 1 < n + 1), u (i + 1) = u 0 ⊔ ⨆ k, ⨆ (_ : k < n), u (k + 1)

Proof state:
α : Type u_1
inst✝ : CompleteLattice α
u : ℕ → α
n : ℕ
⊢ (⨆ (_ : 0 < n + 1), u 0) ⊔ ⨆ i, ⨆ (_ : i + 1 < n + 1), u (i + 1) = u 0 ⊔ ⨆ k, ⨆ (_ : k < n), u (k + 1)

Tactic:
simp

Result:
no goals
-- Mathlib/MeasureTheory/Measure/AEDisjoint.lean
theorem exists_disjoint_diff (h : AEDisjoint μ s t) :
    ∃ u, MeasurableSet u ∧ μ u = 0 ∧ Disjoint (s \ u) t :=
  ⟨toMeasurable μ (s ∩ t), measurableSet_toMeasurable _ _, (measure_toMeasurable _).trans h,
    disjoint_sdiff_self_left.mono_left (b := s \ t) fun x hx => by
      simpa using ⟨hx.1, fun hxt => hx.2 <| subset_toMeasurable _ _ ⟨hx.1, hxt⟩⟩⟩

Proof state:
α : Type u_2
m : MeasurableSpace α
μ : Measure α
s t : Set α
h : AEDisjoint μ s t
x : α
hx : x ∈ s \ toMeasurable μ (s ∩ t)
⊢ x ∈ s \ t

Tactic:
simpa using ⟨hx.1, fun hxt => hx.2 <| subset_toMeasurable _ _ ⟨hx.1, hxt⟩⟩

Result:
no goals
-- Mathlib/Algebra/Homology/QuasiIso.lean
lemma quasiIso_iff_comp_right (φ : K ⟶ L) (φ' : L ⟶ M) [∀ i, K.HasHomology i]
    [∀ i, L.HasHomology i] [∀ i, M.HasHomology i]
    [hφ' : QuasiIso φ'] :
    QuasiIso (φ ≫ φ') ↔ QuasiIso φ

Proof state:
ι : Type u_1
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroMorphisms C
c : ComplexShape ι
K L M : HomologicalComplex C c
φ : K ⟶ L
φ' : L ⟶ M
inst✝² : ∀ (i : ι), K.HasHomology i
inst✝¹ : ∀ (i : ι), L.HasHomology i
inst✝ : ∀ (i : ι), M.HasHomology i
hφ' : QuasiIso φ'
⊢ QuasiIso (φ ≫ φ') ↔ QuasiIso φ

Tactic:
simp only [quasiIso_iff, quasiIsoAt_iff_comp_right φ φ']

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/HashMap/RawLemmas.lean
theorem getD_unitOfList
    {l : List α} {k : α} {fallback : Unit} :
    getD (unitOfList l) k fallback = ()

Proof state:
α : Type u
inst✝¹ : BEq α
inst✝ : Hashable α
l : List α
k : α
fallback : Unit
⊢ (unitOfList l).getD k fallback = ()

Tactic:
simp

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Nat/Modify.lean
theorem getElem?_modifyHead_zero {l : List α} {f : α → α} :
    (l.modifyHead f)[0]? = l[0]?.map f

Proof state:
α : Type u_1
l : List α
f : α → α
⊢ (modifyHead f l)[0]? = Option.map f l[0]?

Tactic:
simp [getElem?_modifyHead]

Result:
no goals
-- Mathlib/Order/CompleteLattice/SetLike.lean
@[simp] lemma not_mem_bot : ¬ x ∈ (⊥ : L)

Proof state:
X : Type u_1
L : CompleteSublattice (Set X)
x : X
⊢ x ∉ ⊥

Tactic:
simp [← mem_subtype]

Result:
no goals
-- Mathlib/Data/ENNReal/Order.lean
@[simp] lemma top_sub (ha : a ≠ ∞) : ∞ - a = ∞

Proof state:
case intro
a : ℝ≥0
⊢ ⊤ - ↑a = ⊤

Tactic:
exact top_sub_coe

Result:
no goals

Proof state:
a : ℝ≥0∞
ha : a ≠ ⊤
⊢ ⊤ - a = ⊤

Tactic:
lift a to ℝ≥0 using ha

Result:
case intro
a : ℝ≥0
⊢ ⊤ - ↑a = ⊤
-- Mathlib/Data/Nat/Init.lean
protected lemma sub_eq_of_eq_add' (h : a = b + c) : a - b = c

Proof state:
a b c : ℕ
h : a = b + c
⊢ a - b = c

Tactic:
omega

Result:
no goals
-- Mathlib/RingTheory/WittVector/WittPolynomial.lean
theorem wittPolynomial_one : wittPolynomial p R 1 = C (p : R) * X 1 + X 0 ^ p

Proof state:
p : ℕ
R : Type u_1
inst✝ : CommRing R
⊢ W_ R 1 = C ↑p * X 1 + X 0 ^ p

Tactic:
simp only [wittPolynomial_eq_sum_C_mul_X_pow, sum_range_succ_comm, range_one, sum_singleton,
  one_mul, pow_one, C_1, pow_zero, tsub_self, tsub_zero]

Result:
no goals
-- Mathlib/Algebra/Polynomial/FieldDivision.lean
theorem divByMonic_eq_div (p : R[X]) (hq : Monic q) : p /ₘ q = p / q :=
  show p /ₘ q = C (leadingCoeff q)⁻¹ * (p /ₘ (q * C (leadingCoeff q)⁻¹)) by
    simp only [Monic.def.1 hq, inv_one, C_1, one_mul, mul_one]

Proof state:
R : Type u
inst✝ : Field R
q p : R[X]
hq : q.Monic
⊢ p /ₘ q = C q.leadingCoeff⁻¹ * (p /ₘ (q * C q.leadingCoeff⁻¹))

Tactic:
simp only [Monic.def.1 hq, inv_one, C_1, one_mul, mul_one]

Result:
no goals
-- Mathlib/Algebra/Order/ToIntervalMod.lean
theorem modEq_iff_toIcoDiv_eq_toIocDiv_add_one :
    a ≡ b [PMOD p] ↔ toIcoDiv hp a b = toIocDiv hp a b + 1

Proof state:
α : Type u_1
inst✝ : LinearOrderedAddCommGroup α
hα : Archimedean α
p : α
hp : 0 < p
a b : α
⊢ a ≡ b [PMOD p] ↔ toIcoDiv hp a b = toIocDiv hp a b + 1

Tactic:
rw [modEq_iff_toIcoMod_add_period_eq_toIocMod hp, toIcoMod, toIocMod, ← eq_sub_iff_add_eq,
  sub_sub, sub_right_inj, ← add_one_zsmul, zsmul_left_inj hp]

Result:
no goals
-- Mathlib/GroupTheory/GroupAction/Defs.lean
@[to_additive]
nonrec lemma orbitRel.Quotient.orbit_nonempty (x : orbitRel.Quotient G α) :
    Set.Nonempty x.orbit

Proof state:
G : Type u_1
α : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
x : Quotient G α
⊢ (MulAction.orbit G (Quotient.out x)).Nonempty

Tactic:
exact orbit_nonempty _

Result:
no goals

Proof state:
G : Type u_1
α : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
x : Quotient G α
⊢ x.orbit.Nonempty

Tactic:
rw [orbitRel.Quotient.orbit_eq_orbit_out x Quotient.out_eq']

Result:
G : Type u_1
α : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
x : Quotient G α
⊢ (MulAction.orbit G (Quotient.out x)).Nonempty
-- Mathlib/Algebra/Star/SelfAdjoint.lean
theorem add_star_self (x : R) : IsSelfAdjoint (x + star x)

Proof state:
R : Type u_1
inst✝¹ : AddCommMonoid R
inst✝ : StarAddMonoid R
x : R
⊢ IsSelfAdjoint (x + star x)

Tactic:
simp only [isSelfAdjoint_iff, add_comm, star_add, star_star]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Trigonometric/Basic.lean
theorem continuous_cos : Continuous cos

Proof state:
⊢ Continuous cos

Tactic:
change Continuous fun z => (exp (z * I) + exp (-z * I)) / 2

Result:
⊢ Continuous fun z => (cexp (z * I) + cexp (-z * I)) / 2

Proof state:
⊢ Continuous fun z => (cexp (z * I) + cexp (-z * I)) / 2

Tactic:
continuity

Result:
no goals
-- Mathlib/FieldTheory/IntermediateField/Adjoin/Defs.lean
theorem iInf_toSubfield {ι : Sort*} (S : ι → IntermediateField F E) :
    (iInf S).toSubfield = ⨅ i, (S i).toSubfield :=
  SetLike.coe_injective <| by simp [iInf]

Proof state:
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
ι : Sort u_3
S : ι → IntermediateField F E
⊢ ↑(iInf S).toSubfield = ↑(⨅ i, (S i).toSubfield)

Tactic:
simp [iInf]

Result:
no goals
-- Mathlib/Geometry/Manifold/LocalDiffeomorph.lean
/-- A `C^n` diffeomorphism is a local diffeomorphism. -/
lemma Diffeomorph.isLocalDiffeomorph (Φ : M ≃ₘ^n⟮I, J⟯ N) : IsLocalDiffeomorph I J n Φ :=
  fun _x ↦ ⟨Φ.toPartialDiffeomorph, by trivial, eqOn_refl Φ _⟩

Proof state:
𝕜 : Type u_1
inst✝¹⁰ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace 𝕜 E
F : Type u_3
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace 𝕜 F
H : Type u_4
inst✝⁵ : TopologicalSpace H
G : Type u_5
inst✝⁴ : TopologicalSpace G
I : ModelWithCorners 𝕜 E H
J : ModelWithCorners 𝕜 F G
M : Type u_6
inst✝³ : TopologicalSpace M
inst✝² : ChartedSpace H M
N : Type u_7
inst✝¹ : TopologicalSpace N
inst✝ : ChartedSpace G N
n : WithTop ℕ∞
Φ : M ≃ₘ^n⟮I, J⟯ N
_x : M
⊢ _x ∈ Φ.toPartialDiffeomorph.source

Tactic:
trivial

Result:
no goals
-- Mathlib/Algebra/GCDMonoid/Multiset.lean
theorem gcd_ndinsert (a : α) (s : Multiset α) : (ndinsert a s).gcd = GCDMonoid.gcd a s.gcd

Proof state:
α : Type u_1
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : NormalizedGCDMonoid α
inst✝ : DecidableEq α
a : α
s : Multiset α
⊢ ∀ (a_1 : α), a_1 ∈ ndinsert a s ↔ a_1 ∈ a ::ₘ s

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : NormalizedGCDMonoid α
inst✝ : DecidableEq α
a : α
s : Multiset α
⊢ (ndinsert a s).gcd = GCDMonoid.gcd a s.gcd

Tactic:
rw [← gcd_dedup, dedup_ext.2, gcd_dedup, gcd_cons]

Result:
α : Type u_1
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : NormalizedGCDMonoid α
inst✝ : DecidableEq α
a : α
s : Multiset α
⊢ ∀ (a_1 : α), a_1 ∈ ndinsert a s ↔ a_1 ∈ a ::ₘ s
-- Mathlib/Topology/UniformSpace/UniformConvergence.lean
theorem Filter.Tendsto.tendstoUniformlyOnFilter_const {g : ι → β} {b : β} (hg : Tendsto g p (𝓝 b))
    (p' : Filter α) :
    TendstoUniformlyOnFilter (fun n : ι => fun _ : α => g n) (fun _ : α => b) p p'

Proof state:
α : Type u
β : Type v
ι : Type x
inst✝ : UniformSpace β
p : Filter ι
g : ι → β
b : β
hg : Tendsto g p (𝓝 b)
p' : Filter α
⊢ TendstoUniformlyOnFilter (fun n x => g n) (fun x => b) p p'

Tactic:
simpa only [nhds_eq_comap_uniformity, tendsto_comap_iff] using hg.comp (tendsto_fst (g := p'))

Result:
no goals
-- Mathlib/Analysis/Seminorm.lean
theorem sub_mem_ball (p : Seminorm 𝕜 E) (x₁ x₂ y : E) (r : ℝ) :
    x₁ - x₂ ∈ p.ball y r ↔ x₁ ∈ p.ball (x₂ + y) r

Proof state:
𝕜 : Type u_3
E : Type u_7
inst✝² : SeminormedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : SMul 𝕜 E
p : Seminorm 𝕜 E
x₁ x₂ y : E
r : ℝ
⊢ x₁ - x₂ ∈ p.ball y r ↔ x₁ ∈ p.ball (x₂ + y) r

Tactic:
simp_rw [mem_ball, sub_sub]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Nat/InsertIdx.lean
theorem length_insertIdx_of_length_lt (h : length as < n) : length (insertIdx n a as) = length as

Proof state:
α : Type u
a : α
as : List α
n : Nat
h : as.length < n
⊢ (insertIdx n a as).length = as.length

Tactic:
simp [length_insertIdx, h]

Result:
no goals
-- Mathlib/Analysis/Calculus/Gradient/Basic.lean
theorem Filter.EventuallyEq.hasGradientAtFilter_iff (h₀ : f₀ =ᶠ[L] f₁) (hx : f₀ x = f₁ x)
    (h₁ : f₀' = f₁') : HasGradientAtFilter f₀ f₀' x L ↔ HasGradientAtFilter f₁ f₁' x L :=
  h₀.hasFDerivAtFilter_iff hx (by simp [h₁])

Proof state:
𝕜 : Type u_1
F : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace 𝕜 F
inst✝ : CompleteSpace F
x : F
L : Filter F
f₀ f₁ : F → 𝕜
f₀' f₁' : F
h₀ : f₀ =ᶠ[L] f₁
hx : f₀ x = f₁ x
h₁ : f₀' = f₁'
⊢ ∀ (x : F), ((toDual 𝕜 F) f₀') x = ((toDual 𝕜 F) f₁') x

Tactic:
simp [h₁]

Result:
no goals
-- Mathlib/Algebra/Module/Basic.lean
lemma support_const_smul_of_ne_zero [Zero R] [Zero M] [SMulWithZero R M] [NoZeroSMulDivisors R M]
    (c : R) (g : α → M) (hc : c ≠ 0) : support (c • g) = support g :=
  ext fun x ↦ by simp only [hc, mem_support, Pi.smul_apply, Ne, smul_eq_zero, false_or]

Proof state:
α : Type u_1
R : Type u_2
M : Type u_3
inst✝³ : Zero R
inst✝² : Zero M
inst✝¹ : SMulWithZero R M
inst✝ : NoZeroSMulDivisors R M
c : R
g : α → M
hc : c ≠ 0
x : α
⊢ x ∈ support (c • g) ↔ x ∈ support g

Tactic:
simp only [hc, mem_support, Pi.smul_apply, Ne, smul_eq_zero, false_or]

Result:
no goals
-- Mathlib/Topology/ContinuousMap/Bounded/Basic.lean
theorem isometry_extend (f : α ↪ δ) (h : δ →ᵇ β) : Isometry fun g : α →ᵇ β => extend f g h :=
  Isometry.of_dist_eq fun g₁ g₂ => by simp [dist_nonneg]

Proof state:
α : Type u
β : Type v
inst✝³ : TopologicalSpace α
inst✝² : PseudoMetricSpace β
δ : Type u_2
inst✝¹ : TopologicalSpace δ
inst✝ : DiscreteTopology δ
f : α ↪ δ
h : δ →ᵇ β
g₁ g₂ : α →ᵇ β
⊢ dist (extend f g₁ h) (extend f g₂ h) = dist g₁ g₂

Tactic:
simp [dist_nonneg]

Result:
no goals
-- Mathlib/Algebra/Homology/Embedding/CochainComplex.lean
lemma isZero_of_isStrictlyGE (n i : ℤ) (hi : i < n) [K.IsStrictlyGE n] :
    IsZero (K.X i) :=
  isZero_X_of_isStrictlySupported K (embeddingUpIntGE n) i
    (by simpa only [not_mem_range_embeddingUpIntGE_iff] using hi)

Proof state:
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : HasZeroMorphisms C
K : CochainComplex C ℤ
n i : ℤ
hi : i < n
inst✝ : K.IsStrictlyGE n
⊢ ∀ (i_1 : ℕ), (embeddingUpIntGE n).f i_1 ≠ i

Tactic:
simpa only [not_mem_range_embeddingUpIntGE_iff] using hi

Result:
no goals
-- Mathlib/CategoryTheory/ConcreteCategory/Basic.lean
@[simp]
lemma NatTrans.naturality_apply {C D : Type*} [Category C] [Category D] {FD : D → D → Type*}
    {CD : D → Type*} [∀ X Y, FunLike (FD X Y) (CD X) (CD Y)] [ConcreteCategory D FD]
    {F G : C ⥤ D} (φ : F ⟶ G) {X Y : C} (f : X ⟶ Y) (x : ToType (F.obj X)) :
    φ.app Y (F.map f x) = G.map f (φ.app X x)

Proof state:
C : Type u_2
D : Type u_3
inst✝³ : Category.{u_6, u_2} C
inst✝² : Category.{u_7, u_3} D
FD : D → D → Type u_4
CD : D → Type u_5
inst✝¹ : (X Y : D) → FunLike (FD X Y) (CD X) (CD Y)
inst✝ : ConcreteCategory D FD
F G : C ⥤ D
φ : F ⟶ G
X Y : C
f : X ⟶ Y
x : ToType (F.obj X)
⊢ (ConcreteCategory.hom (φ.app Y)) ((ConcreteCategory.hom (F.map f)) x) =
    (ConcreteCategory.hom (G.map f)) ((ConcreteCategory.hom (φ.app X)) x)

Tactic:
simpa only [Functor.map_comp] using congr_fun ((forget D).congr_map (φ.naturality f)) x

Result:
no goals