harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Topology/Instances/AddCircle.lean
theorem liftIco_eq_lift_Icc {f : 𝕜 → B} (h : f a = f (a + p)) :
    liftIco p a f =
      Quot.lift (restrict (Icc a <| a + p) f)
          (by
            rintro _ _ ⟨_⟩
            exact h) ∘
        equivIccQuot p a :=
  rfl

Proof state:
𝕜 : Type u_1
B : Type u_2
inst✝¹ : LinearOrderedAddCommGroup 𝕜
p a : 𝕜
hp : Fact (0 < p)
inst✝ : Archimedean 𝕜
f : 𝕜 → B
h : f a = f (a + p)
⊢ ∀ (a_1 b : ↑(Icc a (a + p))), EndpointIdent p a a_1 b → (Icc a (a + p)).restrict f a_1 = (Icc a (a + p)).restrict f b

Tactic:
rintro _ _ ⟨_⟩

Result:
case mk
𝕜 : Type u_1
B : Type u_2
inst✝¹ : LinearOrderedAddCommGroup 𝕜
p a : 𝕜
hp : Fact (0 < p)
inst✝ : Archimedean 𝕜
f : 𝕜 → B
h : f a = f (a + p)
⊢ (Icc a (a + p)).restrict f ⟨a, ⋯⟩ = (Icc a (a + p)).restrict f ⟨a + p, ⋯⟩

Proof state:
case mk
𝕜 : Type u_1
B : Type u_2
inst✝¹ : LinearOrderedAddCommGroup 𝕜
p a : 𝕜
hp : Fact (0 < p)
inst✝ : Archimedean 𝕜
f : 𝕜 → B
h : f a = f (a + p)
⊢ (Icc a (a + p)).restrict f ⟨a, ⋯⟩ = (Icc a (a + p)).restrict f ⟨a + p, ⋯⟩

Tactic:
exact h

Result:
no goals
-- Mathlib/Algebra/Order/Group/Unbundled/Int.lean
theorem sign_eq_abs_ediv (a : ℤ) : sign a = |a| / a :=
  if az : a = 0 then by simp [az]
  else (Int.ediv_eq_of_eq_mul_left az (sign_mul_self_eq_abs _).symm).symm

Proof state:
a : ℤ
az : a = 0
⊢ a.sign = |a| / a

Tactic:
simp [az]

Result:
no goals
-- Mathlib/Algebra/Order/Floor.lean
theorem ceil_one : ⌈(1 : α)⌉₊ = 1

Proof state:
α : Type u_2
inst✝¹ : LinearOrderedSemiring α
inst✝ : FloorSemiring α
⊢ ⌈1⌉₊ = 1

Tactic:
rw [← Nat.cast_one, ceil_natCast]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem toInt_add (x y : BitVec w) :
  (x + y).toInt = (x.toInt + y.toInt).bmod (2^w)

Proof state:
w : Nat
x y : BitVec w
⊢ (x + y).toInt = (x.toInt + y.toInt).bmod (2 ^ w)

Tactic:
simp [toInt_eq_toNat_bmod]

Result:
no goals
-- Mathlib/LinearAlgebra/LinearIndependent/Defs.lean
theorem linearIndependent_iff_finset_linearIndependent :
    LinearIndependent R v ↔ ∀ (s : Finset ι), LinearIndependent R (v ∘ (Subtype.val : s → ι)) :=
  ⟨fun H _ ↦ H.comp _ Subtype.val_injective, fun H ↦ linearIndependent_iff'ₛ.2 fun s f g eq i hi ↦
    Fintype.linearIndependent_iffₛ.1 (H s) (f ∘ Subtype.val) (g ∘ Subtype.val)
      (by simpa only [← s.sum_coe_sort] using eq) ⟨i, hi⟩⟩

Proof state:
ι : Type u'
R : Type u_2
M : Type u_4
v : ι → M
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
H : ∀ (s : Finset ι), LinearIndependent R (v ∘ Subtype.val)
s : Finset ι
f g : ι → R
eq : ∑ i ∈ s, f i • v i = ∑ i ∈ s, g i • v i
i : ι
hi : i ∈ s
⊢ ∑ i : { x // x ∈ s }, (f ∘ Subtype.val) i • (v ∘ Subtype.val) i =
    ∑ i : { x // x ∈ s }, (g ∘ Subtype.val) i • (v ∘ Subtype.val) i

Tactic:
simpa only [← s.sum_coe_sort] using eq

Result:
no goals
-- Mathlib/Algebra/GroupWithZero/Associated.lean
theorem mul_mono {a b c d : Associates M} (h₁ : a ≤ b) (h₂ : c ≤ d) : a * c ≤ b * d :=
  let ⟨x, hx⟩ := h₁
  let ⟨y, hy⟩ := h₂
  ⟨x * y, by simp [hx, hy, mul_comm, mul_assoc, mul_left_comm]⟩

Proof state:
M : Type u_1
inst✝ : CommMonoid M
a b c d : Associates M
h₁ : a ≤ b
h₂ : c ≤ d
x : Associates M
hx : b = a * x
y : Associates M
hy : d = c * y
⊢ b * d = a * c * (x * y)

Tactic:
simp [hx, hy, mul_comm, mul_assoc, mul_left_comm]

Result:
no goals
-- Mathlib/Algebra/Group/Subgroup/Ker.lean
theorem map_eq_map_iff {f : G →* N} {H K : Subgroup G} :
    H.map f = K.map f ↔ H ⊔ f.ker = K ⊔ f.ker

Proof state:
G : Type u_1
inst✝¹ : Group G
N : Type u_5
inst✝ : Group N
f : G →* N
H K : Subgroup G
⊢ map f H = map f K ↔ H ⊔ f.ker = K ⊔ f.ker

Tactic:
simp only [le_antisymm_iff, map_le_map_iff']

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Nat/Lemmas.lean
theorem pos_of_mul_pos_right {a b : Nat} (h : 0 < a * b) : 0 < a

Proof state:
a b : Nat
h : 0 < a * b
⊢ 0 < a

Tactic:
apply Decidable.by_contra

Result:
case a
a b : Nat
h : 0 < a * b
⊢ ¬0 < a → False

Proof state:
case a
a b : Nat
h : 0 < a * b
a✝ : ¬0 < a
⊢ False

Tactic:
simp_all

Result:
no goals

Proof state:
case a
a b : Nat
h : 0 < a * b
⊢ ¬0 < a → False

Tactic:
intros

Result:
case a
a b : Nat
h : 0 < a * b
a✝ : ¬0 < a
⊢ False
-- Mathlib/CategoryTheory/Abelian/DiagramLemmas/KernelCokernelComp.lean
@[reassoc (attr := simp)]
lemma inl_φ : biprod.inl ≫ φ f g = f ≫ biprod.inl

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
⊢ biprod.inl ≫ φ f g = f ≫ biprod.inl

Tactic:
simp [φ]

Result:
no goals
-- Mathlib/LinearAlgebra/Matrix/PosDef.lean
theorem posSemidef_self_mul_conjTranspose [StarOrderedRing R] (A : Matrix m n R) :
    PosSemidef (A * Aᴴ)

Proof state:
m : Type u_1
n : Type u_2
R : Type u_3
inst✝⁵ : Fintype m
inst✝⁴ : Fintype n
inst✝³ : CommRing R
inst✝² : PartialOrder R
inst✝¹ : StarRing R
inst✝ : StarOrderedRing R
A : Matrix m n R
⊢ (A * Aᴴ).PosSemidef

Tactic:
simpa only [conjTranspose_conjTranspose] using posSemidef_conjTranspose_mul_self Aᴴ

Result:
no goals
-- Mathlib/Topology/MetricSpace/HolderNorm.lean
lemma HolderWith.nnholderNorm_le {C r : ℝ≥0} {f : X → Y} (hf : HolderWith C r f) :
    nnHolderNorm r f ≤ C

Proof state:
X : Type u_1
Y : Type u_2
inst✝¹ : MetricSpace X
inst✝ : EMetricSpace Y
C r : ℝ≥0
f : X → Y
hf : HolderWith C r f
⊢ nnHolderNorm r f ≤ C

Tactic:
rw [← ENNReal.coe_le_coe, hf.memHolder.coe_nnHolderNorm_eq_eHolderNorm]

Result:
X : Type u_1
Y : Type u_2
inst✝¹ : MetricSpace X
inst✝ : EMetricSpace Y
C r : ℝ≥0
f : X → Y
hf : HolderWith C r f
⊢ eHolderNorm r f ≤ ↑C

Proof state:
X : Type u_1
Y : Type u_2
inst✝¹ : MetricSpace X
inst✝ : EMetricSpace Y
C r : ℝ≥0
f : X → Y
hf : HolderWith C r f
⊢ eHolderNorm r f ≤ ↑C

Tactic:
exact hf.eHolderNorm_le

Result:
no goals
-- Mathlib/Algebra/Homology/QuasiIso.lean
lemma quasiIso_iff_of_arrow_mk_iso (φ : K ⟶ L) (φ' : K' ⟶ L') (e : Arrow.mk φ ≅ Arrow.mk φ')
    [∀ i, K.HasHomology i] [∀ i, L.HasHomology i]
    [∀ i, K'.HasHomology i] [∀ i, L'.HasHomology i] :
    QuasiIso φ ↔ QuasiIso φ'

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

Tactic:
simp [← quasiIso_iff_comp_left (show K' ⟶ K from e.inv.left) φ,
  ← quasiIso_iff_comp_right φ' (show L' ⟶ L from e.inv.right)]

Result:
no goals
-- Mathlib/Data/Fin/Basic.lean
@[simp] lemma natCast_eq_zero {a n : ℕ} [NeZero n] : (a : Fin n) = 0 ↔ n ∣ a

Proof state:
a n : ℕ
inst✝ : NeZero n
⊢ ↑a = 0 ↔ n ∣ a

Tactic:
simp [Fin.ext_iff, Nat.dvd_iff_mod_eq_zero]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Ord.lean
theorem eq_eq_of_isLE_of_isLE_swap {o : Ordering} : o.isLE → o.swap.isLE → o = .eq

Proof state:
o : Ordering
⊢ o.isLE = true → o.swap.isLE = true → o = eq

Tactic:
cases o <;> simp

Result:
no goals
-- Mathlib/Data/Set/Basic.lean
theorem mem_dite_univ_left (p : Prop) [Decidable p] (t : ¬p → Set α) (x : α) :
    (x ∈ if h : p then univ else t h) ↔ ∀ h : ¬p, x ∈ t h

Proof state:
α : Type u
p : Prop
inst✝ : Decidable p
t : ¬p → Set α
x : α
⊢ (x ∈ if h : p then univ else t h) ↔ ∀ (h : ¬p), x ∈ t h

Tactic:
split_ifs <;> simp_all

Result:
no goals
-- Mathlib/Data/Complex/Norm.lean
theorem range_normSq : range normSq = Ici 0 :=
  Subset.antisymm (range_subset_iff.2 normSq_nonneg) fun x hx =>
    ⟨Real.sqrt x, by rw [normSq_ofReal, Real.mul_self_sqrt hx]⟩

Proof state:
x : ℝ
hx : x ∈ Ici 0
⊢ normSq ↑√x = x

Tactic:
rw [normSq_ofReal, Real.mul_self_sqrt hx]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/RawLemmas.lean
theorem get!_eq_getD_default [LawfulBEq α] (h : m.1.WF) {a : α} [Inhabited (β a)] :
    m.get! a = m.getD a default

Proof state:
α : Type u
β : α → Type v
m : Raw₀ α β
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : LawfulBEq α
h : m.val.WF
a : α
inst✝ : Inhabited (β a)
⊢ m.get! a = m.getD a default

Tactic:
simp_to_model using List.getValueCast!_eq_getValueCastD_default

Result:
no goals
-- Mathlib/Analysis/Calculus/BumpFunction/FiniteDimension.lean
theorem w_compact_support {D : ℝ} (Dpos : 0 < D) : HasCompactSupport (w D : E → ℝ)

Proof state:
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : FiniteDimensional ℝ E
inst✝¹ : MeasurableSpace E
inst✝ : BorelSpace E
D : ℝ
Dpos : 0 < D
⊢ IsCompact (closedBall 0 D)

Tactic:
exact isCompact_closedBall _ _

Result:
no goals

Proof state:
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : FiniteDimensional ℝ E
inst✝¹ : MeasurableSpace E
inst✝ : BorelSpace E
D : ℝ
Dpos : 0 < D
⊢ HasCompactSupport (w D)

Tactic:
rw [hasCompactSupport_def, w_support E Dpos, closure_ball (0 : E) Dpos.ne']

Result:
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : FiniteDimensional ℝ E
inst✝¹ : MeasurableSpace E
inst✝ : BorelSpace E
D : ℝ
Dpos : 0 < D
⊢ IsCompact (closedBall 0 D)
-- Mathlib/Topology/Instances/ENNReal/Lemmas.lean
theorem edist_le_tsum_of_edist_le_of_tendsto₀ {f : ℕ → α} (d : ℕ → ℝ≥0∞)
    (hf : ∀ n, edist (f n) (f n.succ) ≤ d n) {a : α} (ha : Tendsto f atTop (𝓝 a)) :
    edist (f 0) a ≤ ∑' m, d m

Proof state:
α : Type u_1
inst✝ : PseudoEMetricSpace α
f : ℕ → α
d : ℕ → ℝ≥0∞
hf : ∀ (n : ℕ), edist (f n) (f n.succ) ≤ d n
a : α
ha : Tendsto f atTop (𝓝 a)
⊢ edist (f 0) a ≤ ∑' (m : ℕ), d m

Tactic:
simpa using edist_le_tsum_of_edist_le_of_tendsto d hf ha 0

Result:
no goals
-- Mathlib/LinearAlgebra/AffineSpace/Independent.lean
theorem reindex_symm_reindex {m n : ℕ} (s : Simplex k P m) (e : Fin (n + 1) ≃ Fin (m + 1)) :
    (s.reindex e.symm).reindex e = 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
m n : ℕ
s : Simplex k P m
e : Fin (n + 1) ≃ Fin (m + 1)
⊢ (s.reindex e.symm).reindex e = s

Tactic:
rw [← reindex_trans, Equiv.symm_trans_self, reindex_refl]

Result:
no goals
-- Mathlib/Analysis/Normed/Group/Basic.lean
theorem mem_ball_iff_norm''' : b ∈ ball a r ↔ ‖a / b‖ < r

Proof state:
E : Type u_5
inst✝ : SeminormedGroup E
a b : E
r : ℝ
⊢ b ∈ ball a r ↔ ‖a / b‖ < r

Tactic:
rw [mem_ball', dist_eq_norm_div]

Result:
no goals
-- Mathlib/Algebra/Order/Ring/Unbundled/Basic.lean
theorem lt_mul_of_lt_one_left [ExistsAddOfLE α] [MulPosStrictMono α]
    [AddRightStrictMono α] [AddRightReflectLT α]
    (hb : b < 0) (h : a < 1) : b < a * b

Proof state:
α : Type u
inst✝⁵ : Semiring α
inst✝⁴ : PartialOrder α
a b : α
inst✝³ : ExistsAddOfLE α
inst✝² : MulPosStrictMono α
inst✝¹ : AddRightStrictMono α
inst✝ : AddRightReflectLT α
hb : b < 0
h : a < 1
⊢ b < a * b

Tactic:
simpa only [one_mul] using mul_lt_mul_of_neg_right h hb

Result:
no goals
-- Mathlib/CategoryTheory/Functor/Derived/RightDerived.lean
lemma HasRightDerivedFunctor.hasLeftKanExtension [HasRightDerivedFunctor F W] :
    HasLeftKanExtension L F

Proof state:
C : Type u_1
D : Type u_5
H : Type u_2
inst✝⁴ : Category.{u_3, u_1} C
inst✝³ : Category.{u_6, u_5} D
inst✝² : Category.{u_4, u_2} H
F : C ⥤ H
L : C ⥤ D
W : MorphismProperty C
inst✝¹ : L.IsLocalization W
inst✝ : F.HasRightDerivedFunctor W
⊢ L.HasLeftKanExtension F

Tactic:
simpa only [← hasRightDerivedFunctor_iff F L W]

Result:
no goals
-- Mathlib/Data/List/Sigma.lean
theorem dlookup_eq_none {a : α} {l : List (Sigma β)} : dlookup a l = none ↔ a ∉ l.keys

Proof state:
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
l : List (Sigma β)
⊢ dlookup a l = none ↔ a ∉ l.keys

Tactic:
simp [← dlookup_isSome, Option.isNone_iff_eq_none]

Result:
no goals
-- Mathlib/Data/Set/Insert.lean
@[simp default+1]
lemma disjoint_singleton_left : Disjoint {a} s ↔ a ∉ s

Proof state:
α : Type u
s : Set α
a : α
⊢ Disjoint {a} s ↔ a ∉ s

Tactic:
simp [Set.disjoint_iff, subset_def]

Result:
no goals
-- Mathlib/Algebra/Ring/BooleanRing.lean
theorem sup_assoc (a b c : α) : a ⊔ b ⊔ c = a ⊔ (b ⊔ c)

Proof state:
α : Type u_1
inst✝ : BooleanRing α
a b c : α
⊢ a + b + a * b + c + (a + b + a * b) * c = a + (b + c + b * c) + a * (b + c + b * c)

Tactic:
ring

Result:
no goals
-- Mathlib/Algebra/Symmetrized.lean
theorem sym_mul_self [Semiring α] [Invertible (2 : α)] (a : α) : sym (a * a) = sym a * sym a

Proof state:
α : Type u_1
inst✝¹ : Semiring α
inst✝ : Invertible 2
a : α
⊢ sym (a * a) = sym a * sym a

Tactic:
rw [sym_mul_sym, ← two_mul, invOf_mul_cancel_left]

Result:
no goals
-- Mathlib/Dynamics/TopologicalEntropy/Semiconj.lean
lemma coverEntropy_restrict_subset [UniformSpace X] {T : X → X} {F G : Set X} (hF : F ⊆ G)
    (hG : MapsTo T G G) :
    coverEntropy (hG.restrict T G G) (val ⁻¹' F) = coverEntropy T F

Proof state:
X : Type u_1
inst✝ : UniformSpace X
T : X → X
F G : Set X
hF : F ⊆ G
hG : MapsTo T G G
⊢ coverEntropy (MapsTo.restrict T G G hG) (val ⁻¹' F) = coverEntropy T F

Tactic:
rw [← coverEntropy_image_of_comap _ hG.val_restrict_apply (val ⁻¹' F), image_preimage_coe G F,
  inter_eq_right.2 hF]

Result:
no goals
-- Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Unital.lean
lemma cfc_apply_of_not_continuousOn {f : R → R} (a : A) (hf : ¬ ContinuousOn f (spectrum R a)) :
    cfc f a = 0

Proof state:
R : Type u_1
A : Type u_2
p : A → Prop
inst✝⁸ : CommSemiring R
inst✝⁷ : StarRing R
inst✝⁶ : MetricSpace R
inst✝⁵ : IsTopologicalSemiring R
inst✝⁴ : ContinuousStar R
inst✝³ : TopologicalSpace A
inst✝² : Ring A
inst✝¹ : StarRing A
inst✝ : Algebra R A
instCFC : ContinuousFunctionalCalculus R p
f : R → R
a : A
hf : ¬ContinuousOn f (spectrum R a)
⊢ cfc f a = 0

Tactic:
rw [cfc_def, dif_neg (not_and_of_not_right _ hf)]

Result:
no goals
-- Mathlib/Algebra/GeomSum.lean
theorem geom_sum_Ico_mul [Ring α] (x : α) {m n : ℕ} (hmn : m ≤ n) :
    (∑ i ∈ Finset.Ico m n, x ^ i) * (x - 1) = x ^ n - x ^ m

Proof state:
α : Type u
inst✝ : Ring α
x : α
m n : ℕ
hmn : m ≤ n
⊢ (∑ i ∈ Ico m n, x ^ i) * (x - 1) = x ^ n - x ^ m

Tactic:
rw [sum_Ico_eq_sub _ hmn, sub_mul, geom_sum_mul, geom_sum_mul, sub_sub_sub_cancel_right]

Result:
no goals
-- Mathlib/Analysis/Normed/Group/SemiNormedGrp.lean
@[simp]
lemma hom_inv_apply {M N : SemiNormedGrp₁} (e : M ≅ N) (s : N) : e.hom (e.inv s) = s

Proof state:
M N : SemiNormedGrp₁
e : M ≅ N
s : N.carrier
⊢ ↑(Hom.hom (e.inv ≫ e.hom)) s = s

Tactic:
simp

Result:
no goals

Proof state:
M N : SemiNormedGrp₁
e : M ≅ N
s : N.carrier
⊢ ↑(Hom.hom e.hom) (↑(Hom.hom e.inv) s) = s

Tactic:
rw [← comp_apply]

Result:
M N : SemiNormedGrp₁
e : M ≅ N
s : N.carrier
⊢ ↑(Hom.hom (e.inv ≫ e.hom)) s = s
-- Mathlib/Probability/Kernel/Composition/CompMap.lean
lemma deterministic_comp_deterministic (hf : Measurable f) (hg : Measurable g) :
    (deterministic g hg) ∘ₖ (deterministic f hf) = deterministic (g ∘ f) (hg.comp hf)

Proof state:
case h.h
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
γ : Type u_4
mγ : MeasurableSpace γ
f : β → γ
g : γ → α
hf : Measurable f
hg : Measurable g
a✝¹ : β
s✝ : Set α
a✝ : MeasurableSet s✝
⊢ ((deterministic g hg ∘ₖ deterministic f hf) a✝¹) s✝ = ((deterministic (g ∘ f) ⋯) a✝¹) s✝

Tactic:
simp [comp_deterministic_eq_comap, comap_apply, deterministic_apply]

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
γ : Type u_4
mγ : MeasurableSpace γ
f : β → γ
g : γ → α
hf : Measurable f
hg : Measurable g
⊢ deterministic g hg ∘ₖ deterministic f hf = deterministic (g ∘ f) ⋯

Tactic:
ext

Result:
case h.h
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
γ : Type u_4
mγ : MeasurableSpace γ
f : β → γ
g : γ → α
hf : Measurable f
hg : Measurable g
a✝¹ : β
s✝ : Set α
a✝ : MeasurableSet s✝
⊢ ((deterministic g hg ∘ₖ deterministic f hf) a✝¹) s✝ = ((deterministic (g ∘ f) ⋯) a✝¹) s✝
-- Mathlib/NumberTheory/Padics/PadicIntegers.lean
theorem norm_lt_one_iff_dvd (x : ℤ_[p]) : ‖x‖ < 1 ↔ ↑p ∣ x

Proof state:
p : ℕ
hp : Fact (Nat.Prime p)
x : ℤ_[p]
this : ‖x‖ ≤ ↑p ^ (-↑1) ↔ x ∈ Ideal.span {↑p ^ 1}
⊢ ‖x‖ < 1 ↔ ↑p ∣ x

Tactic:
rw [Ideal.mem_span_singleton, pow_one] at this

Result:
p : ℕ
hp : Fact (Nat.Prime p)
x : ℤ_[p]
this : ‖x‖ ≤ ↑p ^ (-↑1) ↔ ↑p ∣ x
⊢ ‖x‖ < 1 ↔ ↑p ∣ x

Proof state:
p : ℕ
hp : Fact (Nat.Prime p)
x : ℤ_[p]
this : ‖x‖ ≤ ↑p ^ (-↑1) ↔ ↑p ∣ x
⊢ ‖x‖ < 1 ↔ ↑p ∣ x

Tactic:
rw [← this, norm_le_pow_iff_norm_lt_pow_add_one]

Result:
p : ℕ
hp : Fact (Nat.Prime p)
x : ℤ_[p]
this : ‖x‖ ≤ ↑p ^ (-↑1) ↔ ↑p ∣ x
⊢ ‖x‖ < 1 ↔ ‖x‖ < ↑p ^ (-↑1 + 1)

Proof state:
p : ℕ
hp : Fact (Nat.Prime p)
x : ℤ_[p]
this : ‖x‖ ≤ ↑p ^ (-↑1) ↔ ↑p ∣ x
⊢ ‖x‖ < 1 ↔ ‖x‖ < ↑p ^ (-↑1 + 1)

Tactic:
simp only [zpow_zero, Int.ofNat_zero, Int.ofNat_succ, neg_add_cancel, zero_add]

Result:
no goals

Proof state:
p : ℕ
hp : Fact (Nat.Prime p)
x : ℤ_[p]
⊢ ‖x‖ < 1 ↔ ↑p ∣ x

Tactic:
have := norm_le_pow_iff_mem_span_pow x 1

Result:
p : ℕ
hp : Fact (Nat.Prime p)
x : ℤ_[p]
this : ‖x‖ ≤ ↑p ^ (-↑1) ↔ x ∈ Ideal.span {↑p ^ 1}
⊢ ‖x‖ < 1 ↔ ↑p ∣ x
-- Mathlib/Data/Fintype/Card.lean
theorem Fintype.card_compl_eq_card_compl [Finite α] (p q : α → Prop) [Fintype { x // p x }]
    [Fintype { x // ¬p x }] [Fintype { x // q x }] [Fintype { x // ¬q x }]
    (h : Fintype.card { x // p x } = Fintype.card { x // q x }) :
    Fintype.card { x // ¬p x } = Fintype.card { x // ¬q x }

Proof state:
case intro
α : Type u_1
inst✝⁴ : Finite α
p q : α → Prop
inst✝³ : Fintype { x // p x }
inst✝² : Fintype { x // ¬p x }
inst✝¹ : Fintype { x // q x }
inst✝ : Fintype { x // ¬q x }
h : card { x // p x } = card { x // q x }
val✝ : Fintype α
⊢ card { x // ¬p x } = card { x // ¬q x }

Tactic:
simp only [Fintype.card_subtype_compl, h]

Result:
no goals

Proof state:
α : Type u_1
inst✝⁴ : Finite α
p q : α → Prop
inst✝³ : Fintype { x // p x }
inst✝² : Fintype { x // ¬p x }
inst✝¹ : Fintype { x // q x }
inst✝ : Fintype { x // ¬q x }
h : card { x // p x } = card { x // q x }
⊢ card { x // ¬p x } = card { x // ¬q x }

Tactic:
cases nonempty_fintype α

Result:
case intro
α : Type u_1
inst✝⁴ : Finite α
p q : α → Prop
inst✝³ : Fintype { x // p x }
inst✝² : Fintype { x // ¬p x }
inst✝¹ : Fintype { x // q x }
inst✝ : Fintype { x // ¬q x }
h : card { x // p x } = card { x // q x }
val✝ : Fintype α
⊢ card { x // ¬p x } = card { x // ¬q x }
-- Mathlib/MeasureTheory/Function/EssSup.lean
@[simp] lemma essInf_count [MeasurableSingletonClass α] (f : α → β) : essInf f .count = ⨅ i, f i :=
  essInf_eq_iInf (by simp) _

Proof state:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
inst✝¹ : CompleteLattice β
inst✝ : MeasurableSingletonClass α
f : α → β
⊢ ∀ (a : α), Measure.count {a} ≠ 0

Tactic:
simp

Result:
no goals
-- Mathlib/Geometry/Manifold/VectorField.lean
lemma mpullbackWithin_smul :
    mpullbackWithin I I' f (c • V) s = c • mpullbackWithin I I' f V s

Proof state:
𝕜 : Type u_1
inst✝¹⁰ : NontriviallyNormedField 𝕜
H : Type u_2
inst✝⁹ : TopologicalSpace H
E : Type u_3
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace 𝕜 E
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝⁶ : TopologicalSpace M
inst✝⁵ : ChartedSpace H M
H' : Type u_5
inst✝⁴ : TopologicalSpace H'
E' : Type u_6
inst✝³ : NormedAddCommGroup E'
inst✝² : NormedSpace 𝕜 E'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst✝¹ : TopologicalSpace M'
inst✝ : ChartedSpace H' M'
f : M → M'
s : Set M
V : (x : M') → TangentSpace I' x
c : 𝕜
⊢ mpullbackWithin I I' f (c • V) s = c • mpullbackWithin I I' f V s

Tactic:
ext x

Result:
case h
𝕜 : Type u_1
inst✝¹⁰ : NontriviallyNormedField 𝕜
H : Type u_2
inst✝⁹ : TopologicalSpace H
E : Type u_3
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace 𝕜 E
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝⁶ : TopologicalSpace M
inst✝⁵ : ChartedSpace H M
H' : Type u_5
inst✝⁴ : TopologicalSpace H'
E' : Type u_6
inst✝³ : NormedAddCommGroup E'
inst✝² : NormedSpace 𝕜 E'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst✝¹ : TopologicalSpace M'
inst✝ : ChartedSpace H' M'
f : M → M'
s : Set M
V : (x : M') → TangentSpace I' x
c : 𝕜
x : M
⊢ mpullbackWithin I I' f (c • V) s x = (c • mpullbackWithin I I' f V s) x

Proof state:
case h
𝕜 : Type u_1
inst✝¹⁰ : NontriviallyNormedField 𝕜
H : Type u_2
inst✝⁹ : TopologicalSpace H
E : Type u_3
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace 𝕜 E
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝⁶ : TopologicalSpace M
inst✝⁵ : ChartedSpace H M
H' : Type u_5
inst✝⁴ : TopologicalSpace H'
E' : Type u_6
inst✝³ : NormedAddCommGroup E'
inst✝² : NormedSpace 𝕜 E'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst✝¹ : TopologicalSpace M'
inst✝ : ChartedSpace H' M'
f : M → M'
s : Set M
V : (x : M') → TangentSpace I' x
c : 𝕜
x : M
⊢ mpullbackWithin I I' f (c • V) s x = (c • mpullbackWithin I I' f V s) x

Tactic:
simp [mpullbackWithin_apply]

Result:
no goals
-- Mathlib/CategoryTheory/Localization/DerivabilityStructure/Constructor.lean
/-- If a localizer morphism `Φ` is a localized equivalence, then it is a right
derivability structure if the categories of right resolutions are connected and the
categories of right resolutions of arrows are nonempty. -/
lemma mk' [Φ.IsLocalizedEquivalence] : Φ.IsRightDerivabilityStructure

Proof state:
C₁ : Type u_1
C₂ : Type u_2
inst✝⁶ : Category.{u_3, u_1} C₁
inst✝⁵ : Category.{u_4, u_2} C₂
W₁ : MorphismProperty C₁
W₂ : MorphismProperty C₂
Φ : LocalizerMorphism W₁ W₂
inst✝⁴ : W₁.IsMultiplicative
inst✝³ : ∀ (X₂ : C₂), IsConnected (Φ.RightResolution X₂)
inst✝² : Φ.arrow.HasRightResolutions
inst✝¹ : W₂.ContainsIdentities
inst✝ : Φ.IsLocalizedEquivalence
⊢ ∀ {X₂ : C₂} {X₃ : W₂.Localization} (g : W₂.Q.obj X₂ ⟶ (𝟭 W₂.Localization).obj X₃),
    IsConnected (TwoSquare.CostructuredArrowDownwards (Φ.functor ⋙ W₂.Q).rightUnitor.symm.hom g)

Tactic:
intro X₂ X₃ g

Result:
C₁ : Type u_1
C₂ : Type u_2
inst✝⁶ : Category.{u_3, u_1} C₁
inst✝⁵ : Category.{u_4, u_2} C₂
W₁ : MorphismProperty C₁
W₂ : MorphismProperty C₂
Φ : LocalizerMorphism W₁ W₂
inst✝⁴ : W₁.IsMultiplicative
inst✝³ : ∀ (X₂ : C₂), IsConnected (Φ.RightResolution X₂)
inst✝² : Φ.arrow.HasRightResolutions
inst✝¹ : W₂.ContainsIdentities
inst✝ : Φ.IsLocalizedEquivalence
X₂ : C₂
X₃ : W₂.Localization
g : W₂.Q.obj X₂ ⟶ (𝟭 W₂.Localization).obj X₃
⊢ IsConnected (TwoSquare.CostructuredArrowDownwards (Φ.functor ⋙ W₂.Q).rightUnitor.symm.hom g)

Proof state:
C₁ : Type u_1
C₂ : Type u_2
inst✝⁶ : Category.{u_3, u_1} C₁
inst✝⁵ : Category.{u_4, u_2} C₂
W₁ : MorphismProperty C₁
W₂ : MorphismProperty C₂
Φ : LocalizerMorphism W₁ W₂
inst✝⁴ : W₁.IsMultiplicative
inst✝³ : ∀ (X₂ : C₂), IsConnected (Φ.RightResolution X₂)
inst✝² : Φ.arrow.HasRightResolutions
inst✝¹ : W₂.ContainsIdentities
inst✝ : Φ.IsLocalizedEquivalence
⊢ Φ.IsRightDerivabilityStructure

Tactic:
rw [Φ.isRightDerivabilityStructure_iff (Φ.functor ⋙ W₂.Q) W₂.Q (𝟭 _)
  (Functor.rightUnitor _).symm, TwoSquare.guitartExact_iff_isConnected_downwards]

Result:
C₁ : Type u_1
C₂ : Type u_2
inst✝⁶ : Category.{u_3, u_1} C₁
inst✝⁵ : Category.{u_4, u_2} C₂
W₁ : MorphismProperty C₁
W₂ : MorphismProperty C₂
Φ : LocalizerMorphism W₁ W₂
inst✝⁴ : W₁.IsMultiplicative
inst✝³ : ∀ (X₂ : C₂), IsConnected (Φ.RightResolution X₂)
inst✝² : Φ.arrow.HasRightResolutions
inst✝¹ : W₂.ContainsIdentities
inst✝ : Φ.IsLocalizedEquivalence
⊢ ∀ {X₂ : C₂} {X₃ : W₂.Localization} (g : W₂.Q.obj X₂ ⟶ (𝟭 W₂.Localization).obj X₃),
    IsConnected (TwoSquare.CostructuredArrowDownwards (Φ.functor ⋙ W₂.Q).rightUnitor.symm.hom g)

Proof state:
C₁ : Type u_1
C₂ : Type u_2
inst✝⁶ : Category.{u_3, u_1} C₁
inst✝⁵ : Category.{u_4, u_2} C₂
W₁ : MorphismProperty C₁
W₂ : MorphismProperty C₂
Φ : LocalizerMorphism W₁ W₂
inst✝⁴ : W₁.IsMultiplicative
inst✝³ : ∀ (X₂ : C₂), IsConnected (Φ.RightResolution X₂)
inst✝² : Φ.arrow.HasRightResolutions
inst✝¹ : W₂.ContainsIdentities
inst✝ : Φ.IsLocalizedEquivalence
X₂ : C₂
X₃ : W₂.Localization
g : W₂.Q.obj X₂ ⟶ (𝟭 W₂.Localization).obj X₃
⊢ IsConnected (TwoSquare.CostructuredArrowDownwards (Φ.functor ⋙ W₂.Q).rightUnitor.symm.hom g)

Tactic:
apply Constructor.isConnected

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

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

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

Result:
no goals