harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Nat/Bitwise/Lemmas.lean
theorem testBit_mul_two_pow (x i n : Nat) :
    (x * 2 ^ n).testBit i = (decide (n ≤ i) && x.testBit (i - n))

Proof state:
x i n : Nat
⊢ (x * 2 ^ n).testBit i = (decide (n ≤ i) && x.testBit (i - n))

Tactic:
rw [← testBit_shiftLeft, shiftLeft_eq]

Result:
no goals
-- Mathlib/Algebra/Homology/ShortComplex/Exact.lean
lemma Exact.map_of_preservesLeftHomologyOf (h : S.Exact) (F : C ⥤ D)
    [F.PreservesZeroMorphisms] [F.PreservesLeftHomologyOf S]
    [(S.map F).HasHomology] : (S.map F).Exact

Proof state:
C : Type u_1
D : Type u_2
inst✝⁶ : Category.{u_3, u_1} C
inst✝⁵ : Category.{u_4, u_2} D
inst✝⁴ : HasZeroMorphisms C
inst✝³ : HasZeroMorphisms D
S : ShortComplex C
F : C ⥤ D
inst✝² : F.PreservesZeroMorphisms
inst✝¹ : F.PreservesLeftHomologyOf S
inst✝ : (S.map F).HasHomology
this : S.HasHomology
h : 𝟙 S.leftHomologyData.H = 0
⊢ (S.map F).Exact

Tactic:
rw [S.leftHomologyData.exact_map_iff F, IsZero.iff_id_eq_zero,
  ← F.map_id, h, F.map_zero]

Result:
no goals

Proof state:
C : Type u_1
D : Type u_2
inst✝⁶ : Category.{u_3, u_1} C
inst✝⁵ : Category.{u_4, u_2} D
inst✝⁴ : HasZeroMorphisms C
inst✝³ : HasZeroMorphisms D
S : ShortComplex C
h : S.Exact
F : C ⥤ D
inst✝² : F.PreservesZeroMorphisms
inst✝¹ : F.PreservesLeftHomologyOf S
inst✝ : (S.map F).HasHomology
this : S.HasHomology
⊢ (S.map F).Exact

Tactic:
rw [S.leftHomologyData.exact_iff, IsZero.iff_id_eq_zero] at h

Result:
C : Type u_1
D : Type u_2
inst✝⁶ : Category.{u_3, u_1} C
inst✝⁵ : Category.{u_4, u_2} D
inst✝⁴ : HasZeroMorphisms C
inst✝³ : HasZeroMorphisms D
S : ShortComplex C
F : C ⥤ D
inst✝² : F.PreservesZeroMorphisms
inst✝¹ : F.PreservesLeftHomologyOf S
inst✝ : (S.map F).HasHomology
this : S.HasHomology
h : 𝟙 S.leftHomologyData.H = 0
⊢ (S.map F).Exact

Proof state:
C : Type u_1
D : Type u_2
inst✝⁶ : Category.{u_3, u_1} C
inst✝⁵ : Category.{u_4, u_2} D
inst✝⁴ : HasZeroMorphisms C
inst✝³ : HasZeroMorphisms D
S : ShortComplex C
h : S.Exact
F : C ⥤ D
inst✝² : F.PreservesZeroMorphisms
inst✝¹ : F.PreservesLeftHomologyOf S
inst✝ : (S.map F).HasHomology
⊢ (S.map F).Exact

Tactic:
have := h.hasHomology

Result:
C : Type u_1
D : Type u_2
inst✝⁶ : Category.{u_3, u_1} C
inst✝⁵ : Category.{u_4, u_2} D
inst✝⁴ : HasZeroMorphisms C
inst✝³ : HasZeroMorphisms D
S : ShortComplex C
h : S.Exact
F : C ⥤ D
inst✝² : F.PreservesZeroMorphisms
inst✝¹ : F.PreservesLeftHomologyOf S
inst✝ : (S.map F).HasHomology
this : S.HasHomology
⊢ (S.map F).Exact
-- Mathlib/GroupTheory/Perm/Cycle/Basic.lean
theorem IsCycle.ne_one (h : IsCycle f) : f ≠ 1 := fun hf => by simp [hf, IsCycle] at h

Proof state:
α : Type u_2
f : Perm α
h : f.IsCycle
hf : f = 1
⊢ False

Tactic:
simp [hf, IsCycle] at h

Result:
no goals
-- Mathlib/Logic/Nontrivial/Defs.lean
theorem subsingleton_or_nontrivial (α : Type*) : Subsingleton α ∨ Nontrivial α

Proof state:
α : Type u_3
⊢ Nontrivial α ∨ ¬Nontrivial α

Tactic:
exact Classical.em _

Result:
no goals

Proof state:
α : Type u_3
⊢ Subsingleton α ∨ Nontrivial α

Tactic:
rw [← not_nontrivial_iff_subsingleton, or_comm]

Result:
α : Type u_3
⊢ Nontrivial α ∨ ¬Nontrivial α
-- Mathlib/Data/Finsupp/ToDFinsupp.lean
theorem DFinsupp.toFinsupp_single (i : ι) (m : M) :
    (DFinsupp.single i m : Π₀ _ : ι, M).toFinsupp = Finsupp.single i m

Proof state:
case h
ι : Type u_1
M : Type u_3
inst✝² : DecidableEq ι
inst✝¹ : Zero M
inst✝ : (m : M) → Decidable (m ≠ 0)
i : ι
m : M
a✝ : ι
⊢ (single i m).toFinsupp a✝ = (Finsupp.single i m) a✝

Tactic:
simp [Finsupp.single_apply, DFinsupp.single_apply]

Result:
no goals

Proof state:
ι : Type u_1
M : Type u_3
inst✝² : DecidableEq ι
inst✝¹ : Zero M
inst✝ : (m : M) → Decidable (m ≠ 0)
i : ι
m : M
⊢ (single i m).toFinsupp = Finsupp.single i m

Tactic:
ext

Result:
case h
ι : Type u_1
M : Type u_3
inst✝² : DecidableEq ι
inst✝¹ : Zero M
inst✝ : (m : M) → Decidable (m ≠ 0)
i : ι
m : M
a✝ : ι
⊢ (single i m).toFinsupp a✝ = (Finsupp.single i m) a✝
-- Mathlib/Probability/Kernel/MeasurableIntegral.lean
theorem ProbabilityTheory.measurableSet_integrable ⦃f : β → E⦄ (hf : StronglyMeasurable f) :
    MeasurableSet {a | Integrable f (κ a)}

Proof state:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
E : Type u_4
inst✝ : NormedAddCommGroup E
f : β → E
hf : StronglyMeasurable f
⊢ MeasurableSet {a | Integrable f (κ a)}

Tactic:
simp_rw [Integrable, hf.aestronglyMeasurable, true_and]

Result:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
E : Type u_4
inst✝ : NormedAddCommGroup E
f : β → E
hf : StronglyMeasurable f
⊢ MeasurableSet {a | HasFiniteIntegral f (κ a)}

Proof state:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
E : Type u_4
inst✝ : NormedAddCommGroup E
f : β → E
hf : StronglyMeasurable f
⊢ MeasurableSet {a | HasFiniteIntegral f (κ a)}

Tactic:
exact measurableSet_lt hf.enorm.lintegral_kernel measurable_const

Result:
no goals
-- Mathlib/Order/SuccPred/Archimedean.lean
lemma monotone_of_pred_le (hf : ∀ a, ¬ IsMin a → f (pred a) ≤ f a) : Monotone f

Proof state:
α : Type u_3
β : Type u_4
inst✝³ : PartialOrder α
inst✝² : Preorder β
inst✝¹ : PredOrder α
inst✝ : IsPredArchimedean α
f : α → β
hf : ∀ (a : α), ¬IsMin a → f (pred a) ≤ f a
⊢ Monotone f

Tactic:
simpa using monotoneOn_of_pred_le Set.ordConnected_univ (by simpa using hf)

Result:
no goals

Proof state:
α : Type u_3
β : Type u_4
inst✝³ : PartialOrder α
inst✝² : Preorder β
inst✝¹ : PredOrder α
inst✝ : IsPredArchimedean α
f : α → β
hf : ∀ (a : α), ¬IsMin a → f (pred a) ≤ f a
⊢ ∀ (a : α), ¬IsMin a → a ∈ Set.univ → pred a ∈ Set.univ → f (pred a) ≤ f a

Tactic:
simpa using hf

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/RawLemmas.lean
theorem getKey!_insertMany_list_of_contains_eq_false [EquivBEq α] [LawfulHashable α] [Inhabited α]
    (h : m.1.WF) {l : List (α × β)} {k : α}
    (h' : (l.map Prod.fst).contains k = false) :
    (insertMany m l).1.getKey! k = m.getKey! k

Proof state:
α : Type u
inst✝⁴ : BEq α
inst✝³ : Hashable α
β : Type v
m : Raw₀ α fun x => β
inst✝² : EquivBEq α
inst✝¹ : LawfulHashable α
inst✝ : Inhabited α
h : m.val.WF
l : List (α × β)
k : α
h' : (List.map Prod.fst l).contains k = false
⊢ (insertMany m l).val.getKey! k = m.getKey! k

Tactic:
simp_to_model [Const.insertMany] using List.getKey!_insertListConst_of_contains_eq_false

Result:
no goals
-- Mathlib/Algebra/Order/GroupWithZero/Unbundled.lean
lemma zpow_right_injective₀ (ha₀ : 0 < a) (ha₁ : a ≠ 1) : Injective fun n : ℤ ↦ a ^ n

Proof state:
case inl
G₀ : Type u_2
inst✝³ : GroupWithZero G₀
inst✝² : LinearOrder G₀
inst✝¹ : ZeroLEOneClass G₀
a : G₀
inst✝ : PosMulStrictMono G₀
ha₀ : 0 < a
ha₁✝ : a ≠ 1
ha₁ : a < 1
⊢ Injective fun n => a ^ n

Tactic:
exact (zpow_right_strictAnti₀ ha₀ ha₁).injective

Result:
no goals

Proof state:
case inr
G₀ : Type u_2
inst✝³ : GroupWithZero G₀
inst✝² : LinearOrder G₀
inst✝¹ : ZeroLEOneClass G₀
a : G₀
inst✝ : PosMulStrictMono G₀
ha₀ : 0 < a
ha₁✝ : a ≠ 1
ha₁ : 1 < a
⊢ Injective fun n => a ^ n

Tactic:
exact (zpow_right_strictMono₀ ha₁).injective

Result:
no goals

Proof state:
G₀ : Type u_2
inst✝³ : GroupWithZero G₀
inst✝² : LinearOrder G₀
inst✝¹ : ZeroLEOneClass G₀
a : G₀
inst✝ : PosMulStrictMono G₀
ha₀ : 0 < a
ha₁ : a ≠ 1
⊢ Injective fun n => a ^ n

Tactic:
obtain ha₁ | ha₁ := ha₁.lt_or_lt

Result:
case inl
G₀ : Type u_2
inst✝³ : GroupWithZero G₀
inst✝² : LinearOrder G₀
inst✝¹ : ZeroLEOneClass G₀
a : G₀
inst✝ : PosMulStrictMono G₀
ha₀ : 0 < a
ha₁✝ : a ≠ 1
ha₁ : a < 1
⊢ Injective fun n => a ^ n

case inr
G₀ : Type u_2
inst✝³ : GroupWithZero G₀
inst✝² : LinearOrder G₀
inst✝¹ : ZeroLEOneClass G₀
a : G₀
inst✝ : PosMulStrictMono G₀
ha₀ : 0 < a
ha₁✝ : a ≠ 1
ha₁ : 1 < a
⊢ Injective fun n => a ^ n
-- Mathlib/Analysis/Fourier/FiniteAbelian/PontryaginDuality.lean
@[simp] lemma zmod_intCast (x y : ℤ) : zmod n x y = exp (2 * π * (x * y / n))

Proof state:
n : ℕ
inst✝ : NeZero n
x y : ℤ
⊢ (zmod n ↑x) ↑y = exp (2 * π * (↑x * ↑y / ↑n))

Tactic:
simp [zmod, ← Int.cast_mul x y, -Int.cast_mul, ZMod.toAddCircle_intCast,
  AddCircle.toCircle_apply_mk]

Result:
no goals
-- Mathlib/Order/Basic.lean
protected lemma lt_of_le_of_lt (h₁ : x.1 ≤ y.1) (h₂ : x.2 < y.2) : x < y

Proof state:
α : Type u_2
β : Type u_3
inst✝¹ : Preorder α
inst✝ : Preorder β
x y : α × β
h₁ : x.fst ≤ y.fst
h₂ : x.snd < y.snd
⊢ x < y

Tactic:
simp [lt_iff, *]

Result:
no goals
-- Mathlib/Topology/Separation/Basic.lean
theorem SeparatedNhds.of_isCompact_isCompact_isClosed {K L : Set X} (hK : IsCompact K)
    (hL : IsCompact L) (h'L : IsClosed L) (hd : Disjoint K L) : SeparatedNhds K L

Proof state:
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : R1Space X
K L : Set X
hK : IsCompact K
hL : IsCompact L
h'L : IsClosed L
hd : Disjoint K L
⊢ SeparatedNhds K L

Tactic:
simp_rw [separatedNhds_iff_disjoint, hK.disjoint_nhdsSet_left, hL.disjoint_nhdsSet_right,
  disjoint_nhds_nhds_iff_not_inseparable]

Result:
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : R1Space X
K L : Set X
hK : IsCompact K
hL : IsCompact L
h'L : IsClosed L
hd : Disjoint K L
⊢ ∀ x ∈ K, ∀ x_1 ∈ L, ¬Inseparable x x_1

Proof state:
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : R1Space X
K L : Set X
hK : IsCompact K
hL : IsCompact L
h'L : IsClosed L
hd : Disjoint K L
⊢ ∀ x ∈ K, ∀ x_1 ∈ L, ¬Inseparable x x_1

Tactic:
intro x hx y hy h

Result:
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : R1Space X
K L : Set X
hK : IsCompact K
hL : IsCompact L
h'L : IsClosed L
hd : Disjoint K L
x : X
hx : x ∈ K
y : X
hy : y ∈ L
h : Inseparable x y
⊢ False

Proof state:
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : R1Space X
K L : Set X
hK : IsCompact K
hL : IsCompact L
h'L : IsClosed L
hd : Disjoint K L
x : X
hx : x ∈ K
y : X
hy : y ∈ L
h : Inseparable x y
⊢ False

Tactic:
exact absurd ((h.mem_closed_iff h'L).2 hy) <| disjoint_left.1 hd hx

Result:
no goals
-- Mathlib/CategoryTheory/MorphismProperty/Comma.lean
@[reassoc]
lemma Over.w {A B : P.Over Q X} (f : A ⟶ B) :
    f.left ≫ B.hom = A.hom

Proof state:
T : Type u_1
inst✝¹ : Category.{u_2, u_1} T
P Q : MorphismProperty T
X : T
inst✝ : Q.IsMultiplicative
A B : P.Over Q X
f : A ⟶ B
⊢ f.left ≫ B.hom = A.hom

Tactic:
simp

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/RawLemmas.lean
theorem isEmpty_insertManyIfNewUnit_list [EquivBEq α] [LawfulHashable α] (h : m.1.WF)
    {l : List α} :
    (insertManyIfNewUnit m l).1.1.isEmpty = (m.1.isEmpty && l.isEmpty)

Proof state:
α : Type u
inst✝³ : BEq α
inst✝² : Hashable α
m : Raw₀ α fun x => Unit
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
h : m.val.WF
l : List α
⊢ (insertManyIfNewUnit m l).val.val.isEmpty = (m.val.isEmpty && l.isEmpty)

Tactic:
simp_to_model [Const.insertManyIfNewUnit] using List.isEmpty_insertListIfNewUnit

Result:
no goals
-- Mathlib/FieldTheory/Finite/Basic.lean
theorem pow_card_sub_one_eq_one (a : K) (ha : a ≠ 0) : a ^ (q - 1) = 1

Proof state:
K : Type u_1
inst✝¹ : GroupWithZero K
inst✝ : Fintype K
a : K
ha : a ≠ 0
⊢ ↑1 = 1

Tactic:
rfl

Result:
no goals

Proof state:
K : Type u_1
inst✝¹ : GroupWithZero K
inst✝ : Fintype K
a : K
ha : a ≠ 0
⊢ a ^ (q - 1) = 1

Tactic:
calc
  a ^ (Fintype.card K - 1) = (Units.mk0 a ha ^ (Fintype.card K - 1) : Kˣ).1 := by
    rw [Units.val_pow_eq_pow_val, Units.val_mk0]
  _ = 1 := by
    classical
      rw [← Fintype.card_units, pow_card_eq_one]
      rfl

Result:
no goals

Proof state:
K : Type u_1
inst✝¹ : GroupWithZero K
inst✝ : Fintype K
a : K
ha : a ≠ 0
⊢ a ^ (q - 1) = ↑(Units.mk0 a ha ^ (q - 1))

Tactic:
rw [Units.val_pow_eq_pow_val, Units.val_mk0]

Result:
no goals

Proof state:
K : Type u_1
inst✝¹ : GroupWithZero K
inst✝ : Fintype K
a : K
ha : a ≠ 0
⊢ ↑(Units.mk0 a ha ^ (q - 1)) = 1

Tactic:
rw [← Fintype.card_units, pow_card_eq_one]

Result:
K : Type u_1
inst✝¹ : GroupWithZero K
inst✝ : Fintype K
a : K
ha : a ≠ 0
⊢ ↑1 = 1

Proof state:
K : Type u_1
inst✝¹ : GroupWithZero K
inst✝ : Fintype K
a : K
ha : a ≠ 0
⊢ ↑(Units.mk0 a ha ^ (q - 1)) = 1

Tactic:
classical
  rw [← Fintype.card_units, pow_card_eq_one]
  rfl

Result:
no goals
-- Mathlib/Geometry/Manifold/VectorField.lean
lemma mlieBracketWithin_eq_lieBracketWithin {V W : Π (x : E), TangentSpace 𝓘(𝕜, E) x} {s : Set E} :
    mlieBracketWithin 𝓘(𝕜, E) V W s = lieBracketWithin 𝕜 V W s

Proof state:
case h
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
V W : (x : E) → TangentSpace 𝓘(𝕜, E) x
s : Set E
x : E
⊢ mlieBracketWithin 𝓘(𝕜, E) V W s x = lieBracketWithin 𝕜 V W s x

Tactic:
simp [mlieBracketWithin_apply]

Result:
no goals

Proof state:
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
V W : (x : E) → TangentSpace 𝓘(𝕜, E) x
s : Set E
⊢ mlieBracketWithin 𝓘(𝕜, E) V W s = lieBracketWithin 𝕜 V W s

Tactic:
ext x

Result:
case h
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
V W : (x : E) → TangentSpace 𝓘(𝕜, E) x
s : Set E
x : E
⊢ mlieBracketWithin 𝓘(𝕜, E) V W s x = lieBracketWithin 𝕜 V W s x
-- Mathlib/RingTheory/MvPowerSeries/Order.lean
theorem min_weightedOrder_le_add :
    min (f.weightedOrder w) (g.weightedOrder w) ≤ (f + g).weightedOrder w

Proof state:
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
w : σ → ℕ
f g : MvPowerSeries σ R
⊢ weightedOrder w f ⊓ weightedOrder w g ≤ weightedOrder w (f + g)

Tactic:
apply le_weightedOrder w

Result:
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
w : σ → ℕ
f g : MvPowerSeries σ R
⊢ ∀ (d : σ →₀ ℕ), ↑((weight w) d) < weightedOrder w f ⊓ weightedOrder w g → (coeff R d) (f + g) = 0

Proof state:
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
w : σ → ℕ
f g : MvPowerSeries σ R
⊢ ∀ (d : σ →₀ ℕ), ↑((weight w) d) < weightedOrder w f ⊓ weightedOrder w g → (coeff R d) (f + g) = 0

Tactic:
simp (config := { contextual := true }) only
  [coeff_eq_zero_of_lt_weightedOrder w, lt_min_iff, map_add, add_zero,
    eq_self_iff_true, imp_true_iff]

Result:
no goals
-- Mathlib/Probability/Kernel/Basic.lean
@[simp]
lemma comapRight_id (κ : Kernel α β) : comapRight κ MeasurableEmbedding.id = κ

Proof state:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
⊢ κ.comapRight ⋯ = κ

Tactic:
ext _ _ hs

Result:
case h.h
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
a✝ : α
s✝ : Set β
hs : MeasurableSet s✝
⊢ ((κ.comapRight ⋯) a✝) s✝ = (κ a✝) s✝

Proof state:
case h.h
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
a✝ : α
s✝ : Set β
hs : MeasurableSet s✝
⊢ (κ a✝) (id '' s✝) = (κ a✝) s✝

Tactic:
simp

Result:
no goals

Proof state:
case h.h
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
a✝ : α
s✝ : Set β
hs : MeasurableSet s✝
⊢ ((κ.comapRight ⋯) a✝) s✝ = (κ a✝) s✝

Tactic:
rw [comapRight_apply' _ _ _ hs]

Result:
case h.h
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
a✝ : α
s✝ : Set β
hs : MeasurableSet s✝
⊢ (κ a✝) (id '' s✝) = (κ a✝) s✝
-- Mathlib/MeasureTheory/Measure/WithDensityFinite.lean
@[simp]
lemma ae_toFinite [SFinite μ] : ae μ.toFinite = ae μ

Proof state:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
inst✝ : SFinite μ
⊢ ae μ.toFinite = ae μ

Tactic:
simp [Measure.toFinite, ProbabilityTheory.cond]

Result:
no goals
-- Mathlib/Data/Finset/Basic.lean
theorem attach_eq_empty_iff {s : Finset α} : s.attach = ∅ ↔ s = ∅

Proof state:
α : Type u_1
s : Finset α
⊢ s.attach = ∅ ↔ s = ∅

Tactic:
simp [eq_empty_iff_forall_not_mem]

Result:
no goals
-- Mathlib/Data/Nat/Totient.lean
theorem card_units_zmod_lt_sub_one {p : ℕ} (hp : 1 < p) [Fintype (ZMod p)ˣ] :
    Fintype.card (ZMod p)ˣ ≤ p - 1

Proof state:
p : ℕ
hp : 1 < p
inst✝ : Fintype (ZMod p)ˣ
⊢ Fintype.card (ZMod p)ˣ ≤ p - 1

Tactic:
haveI : NeZero p := ⟨(pos_of_gt hp).ne'⟩

Result:
p : ℕ
hp : 1 < p
inst✝ : Fintype (ZMod p)ˣ
this : NeZero p
⊢ Fintype.card (ZMod p)ˣ ≤ p - 1

Proof state:
p : ℕ
hp : 1 < p
inst✝ : Fintype (ZMod p)ˣ
this : NeZero p
⊢ Fintype.card (ZMod p)ˣ ≤ p - 1

Tactic:
rw [ZMod.card_units_eq_totient p]

Result:
p : ℕ
hp : 1 < p
inst✝ : Fintype (ZMod p)ˣ
this : NeZero p
⊢ φ p ≤ p - 1

Proof state:
p : ℕ
hp : 1 < p
inst✝ : Fintype (ZMod p)ˣ
this : NeZero p
⊢ φ p ≤ p - 1

Tactic:
exact Nat.le_sub_one_of_lt (Nat.totient_lt p hp)

Result:
no goals
-- Mathlib/AlgebraicGeometry/Morphisms/FormallyUnramified.lean
theorem of_comp {X Y Z : Scheme} (f : X ⟶ Y) (g : Y ⟶ Z)
    [FormallyUnramified (f ≫ g)] : FormallyUnramified f :=
  HasRingHomProperty.of_comp (fun {R S T _ _ _} f g H ↦ by
    algebraize [f, g, g.comp f]
    exact Algebra.FormallyUnramified.of_comp R S T) ‹_›

Proof state:
X Y Z : Scheme
f✝ : X ⟶ Y
g✝ : Y ⟶ Z
inst✝ : FormallyUnramified (f✝ ≫ g✝)
R S T : Type u_1
x✝² : CommRing R
x✝¹ : CommRing S
x✝ : CommRing T
f : R →+* S
g : S →+* T
H : (g.comp f).FormallyUnramified
⊢ g.FormallyUnramified

Tactic:
algebraize [f, g, g.comp f]

Result:
X Y Z : Scheme
f✝ : X ⟶ Y
g✝ : Y ⟶ Z
inst✝ : FormallyUnramified (f✝ ≫ g✝)
R S T : Type u_1
x✝² : CommRing R
x✝¹ : CommRing S
x✝ : CommRing T
f : R →+* S
g : S →+* T
H : (g.comp f).FormallyUnramified
algInst✝² : Algebra R S := f.toAlgebra
algInst✝¹ : Algebra S T := g.toAlgebra
algInst✝ : Algebra R T := (g.comp f).toAlgebra
scalarTowerInst✝ : IsScalarTower R S T := IsScalarTower.of_algebraMap_eq' (Eq.refl (algebraMap R T))
algebraizeInst✝ : Algebra.FormallyUnramified R T
⊢ g.FormallyUnramified

Proof state:
X Y Z : Scheme
f✝ : X ⟶ Y
g✝ : Y ⟶ Z
inst✝ : FormallyUnramified (f✝ ≫ g✝)
R S T : Type u_1
x✝² : CommRing R
x✝¹ : CommRing S
x✝ : CommRing T
f : R →+* S
g : S →+* T
H : (g.comp f).FormallyUnramified
algInst✝² : Algebra R S := f.toAlgebra
algInst✝¹ : Algebra S T := g.toAlgebra
algInst✝ : Algebra R T := (g.comp f).toAlgebra
scalarTowerInst✝ : IsScalarTower R S T := IsScalarTower.of_algebraMap_eq' (Eq.refl (algebraMap R T))
algebraizeInst✝ : Algebra.FormallyUnramified R T
⊢ g.FormallyUnramified

Tactic:
exact Algebra.FormallyUnramified.of_comp R S T

Result:
no goals
-- Mathlib/Data/DFinsupp/NeLocus.lean
theorem mapRange_neLocus_eq [∀ a, DecidableEq (N a)] [∀ a, DecidableEq (M a)] (f g : Π₀ a, N a)
    {F : ∀ a, N a → M a} (F0 : ∀ a, F a 0 = 0) (hF : ∀ a, Function.Injective (F a)) :
    (f.mapRange F F0).neLocus (g.mapRange F F0) = f.neLocus g

Proof state:
case h
α : Type u_1
N : α → Type u_2
inst✝⁴ : DecidableEq α
M : α → Type u_3
inst✝³ : (a : α) → Zero (N a)
inst✝² : (a : α) → Zero (M a)
inst✝¹ : (a : α) → DecidableEq (N a)
inst✝ : (a : α) → DecidableEq (M a)
f g : Π₀ (a : α), N a
F : (a : α) → N a → M a
F0 : ∀ (a : α), F a 0 = 0
hF : ∀ (a : α), Function.Injective (F a)
a : α
⊢ a ∈ (mapRange F F0 f).neLocus (mapRange F F0 g) ↔ a ∈ f.neLocus g

Tactic:
simpa only [mem_neLocus] using (hF a).ne_iff

Result:
no goals

Proof state:
α : Type u_1
N : α → Type u_2
inst✝⁴ : DecidableEq α
M : α → Type u_3
inst✝³ : (a : α) → Zero (N a)
inst✝² : (a : α) → Zero (M a)
inst✝¹ : (a : α) → DecidableEq (N a)
inst✝ : (a : α) → DecidableEq (M a)
f g : Π₀ (a : α), N a
F : (a : α) → N a → M a
F0 : ∀ (a : α), F a 0 = 0
hF : ∀ (a : α), Function.Injective (F a)
⊢ (mapRange F F0 f).neLocus (mapRange F F0 g) = f.neLocus g

Tactic:
ext a

Result:
case h
α : Type u_1
N : α → Type u_2
inst✝⁴ : DecidableEq α
M : α → Type u_3
inst✝³ : (a : α) → Zero (N a)
inst✝² : (a : α) → Zero (M a)
inst✝¹ : (a : α) → DecidableEq (N a)
inst✝ : (a : α) → DecidableEq (M a)
f g : Π₀ (a : α), N a
F : (a : α) → N a → M a
F0 : ∀ (a : α), F a 0 = 0
hF : ∀ (a : α), Function.Injective (F a)
a : α
⊢ a ∈ (mapRange F F0 f).neLocus (mapRange F F0 g) ↔ a ∈ f.neLocus g
-- Mathlib/RingTheory/MvPolynomial/EulerIdentity.lean
protected lemma IsHomogeneous.pderiv {n : ℕ} {i : σ} (h : φ.IsHomogeneous n) :
    (pderiv i φ).IsHomogeneous (n - 1)

Proof state:
case succ
R : Type u_1
σ : Type u_2
inst✝ : CommSemiring R
φ : MvPolynomial σ R
i : σ
n : ℕ
h : φ.IsHomogeneous (n + 1)
⊢ ((pderiv i) φ).IsHomogeneous (n + 1 - 1)

Tactic:
exact IsWeightedHomogeneous.pderiv h rfl

Result:
no goals

Proof state:
R : Type u_1
σ : Type u_2
inst✝ : CommSemiring R
φ : MvPolynomial σ R
n : ℕ
i : σ
h : φ.IsHomogeneous n
⊢ ((pderiv i) φ).IsHomogeneous (n - 1)

Tactic:
obtain _ | n := n

Result:
case zero
R : Type u_1
σ : Type u_2
inst✝ : CommSemiring R
φ : MvPolynomial σ R
i : σ
h : φ.IsHomogeneous 0
⊢ ((pderiv i) φ).IsHomogeneous (0 - 1)

case succ
R : Type u_1
σ : Type u_2
inst✝ : CommSemiring R
φ : MvPolynomial σ R
i : σ
n : ℕ
h : φ.IsHomogeneous (n + 1)
⊢ ((pderiv i) φ).IsHomogeneous (n + 1 - 1)

Proof state:
case zero
R : Type u_1
σ : Type u_2
inst✝ : CommSemiring R
φ : MvPolynomial σ R
i : σ
h : φ.IsHomogeneous 0
⊢ ((pderiv i) φ).IsHomogeneous (0 - 1)

Tactic:
rw [← totalDegree_zero_iff_isHomogeneous, totalDegree_eq_zero_iff_eq_C] at h

Result:
case zero
R : Type u_1
σ : Type u_2
inst✝ : CommSemiring R
φ : MvPolynomial σ R
i : σ
h : φ = C (coeff 0 φ)
⊢ ((pderiv i) φ).IsHomogeneous (0 - 1)

Proof state:
case zero
R : Type u_1
σ : Type u_2
inst✝ : CommSemiring R
φ : MvPolynomial σ R
i : σ
h : φ = C (coeff 0 φ)
⊢ IsHomogeneous 0 (0 - 1)

Tactic:
apply isHomogeneous_zero

Result:
no goals

Proof state:
case zero
R : Type u_1
σ : Type u_2
inst✝ : CommSemiring R
φ : MvPolynomial σ R
i : σ
h : φ = C (coeff 0 φ)
⊢ ((pderiv i) φ).IsHomogeneous (0 - 1)

Tactic:
rw [h, pderiv_C]

Result:
case zero
R : Type u_1
σ : Type u_2
inst✝ : CommSemiring R
φ : MvPolynomial σ R
i : σ
h : φ = C (coeff 0 φ)
⊢ IsHomogeneous 0 (0 - 1)
-- Mathlib/Analysis/Calculus/Deriv/Polynomial.lean
theorem derivWithin (hxs : UniqueDiffWithinAt 𝕜 s x) :
    derivWithin (fun x => p.eval x) s x = p.derivative.eval x

Proof state:
𝕜 : Type u
inst✝ : NontriviallyNormedField 𝕜
x : 𝕜
s : Set 𝕜
p : 𝕜[X]
hxs : UniqueDiffWithinAt 𝕜 s x
⊢ derivWithin (fun x => eval x p) s x = eval x (derivative p)

Tactic:
rw [DifferentiableAt.derivWithin p.differentiableAt hxs]

Result:
𝕜 : Type u
inst✝ : NontriviallyNormedField 𝕜
x : 𝕜
s : Set 𝕜
p : 𝕜[X]
hxs : UniqueDiffWithinAt 𝕜 s x
⊢ deriv (fun x => eval x p) x = eval x (derivative p)

Proof state:
𝕜 : Type u
inst✝ : NontriviallyNormedField 𝕜
x : 𝕜
s : Set 𝕜
p : 𝕜[X]
hxs : UniqueDiffWithinAt 𝕜 s x
⊢ deriv (fun x => eval x p) x = eval x (derivative p)

Tactic:
exact p.deriv

Result:
no goals
-- Mathlib/RingTheory/TensorProduct/Basic.lean
theorem map_comp_includeLeft (f : A →ₐ[S] C) (g : B →ₐ[R] D) :
    (map f g).comp includeLeft = includeLeft.comp f :=
  AlgHom.ext <| by simp

Proof state:
R : Type uR
S : Type uS
A : Type uA
B : Type uB
C : Type uC
D : Type uD
inst✝¹⁴ : CommSemiring R
inst✝¹³ : CommSemiring S
inst✝¹² : Algebra R S
inst✝¹¹ : Semiring A
inst✝¹⁰ : Algebra R A
inst✝⁹ : Algebra S A
inst✝⁸ : IsScalarTower R S A
inst✝⁷ : Semiring B
inst✝⁶ : Algebra R B
inst✝⁵ : Semiring C
inst✝⁴ : Algebra R C
inst✝³ : Algebra S C
inst✝² : IsScalarTower R S C
inst✝¹ : Semiring D
inst✝ : Algebra R D
f : A →ₐ[S] C
g : B →ₐ[R] D
⊢ ∀ (x : A), ((map f g).comp includeLeft) x = (includeLeft.comp f) x

Tactic:
simp

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Option/Lemmas.lean
theorem getD_of_ne_none {x : Option α} (hx : x ≠ none) (y : α) : some (x.getD y) = x

Proof state:
α : Type u_1
x : Option α
hx : x ≠ none
y : α
⊢ some (x.getD y) = x

Tactic:
cases x

Result:
case none
α : Type u_1
y : α
hx : none ≠ none
⊢ some (none.getD y) = none

case some
α : Type u_1
y val✝ : α
hx : some val✝ ≠ none
⊢ some ((some val✝).getD y) = some val✝

Proof state:
case some
α : Type u_1
y val✝ : α
hx : some val✝ ≠ none
⊢ some ((some val✝).getD y) = some val✝

Tactic:
rw [getD_some]

Result:
no goals

Proof state:
case none
α : Type u_1
y : α
hx : none ≠ none
⊢ some (none.getD y) = none

Tactic:
contradiction

Result:
no goals

Proof state:
case none
α : Type u_1
y : α
hx : none ≠ none
⊢ some (none.getD y) = none

case some
α : Type u_1
y val✝ : α
hx : some val✝ ≠ none
⊢ some ((some val✝).getD y) = some val✝

Tactic:
{contradiction}

Result:
case some
α : Type u_1
y val✝ : α
hx : some val✝ ≠ none
⊢ some ((some val✝).getD y) = some val✝
-- Mathlib/Topology/Algebra/Order/Field.lean
@[simp]
lemma inv_nhdsLT_zero : (𝓝[<] (0 : 𝕜))⁻¹ = atBot

Proof state:
𝕜 : Type u_1
inst✝² : LinearOrderedField 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
⊢ (𝓝[<] 0)⁻¹ = atBot

Tactic:
rw [← inv_atBot₀, inv_inv]

Result:
no goals