harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/NumberTheory/NumberField/Discriminant/Defs.lean
theorem discr_eq_discr {ι : Type*} [Fintype ι] [DecidableEq ι] (b : Basis ι ℤ (𝓞 K)) :
    Algebra.discr ℤ b = discr K

Proof state:
K : Type u_1
inst✝³ : Field K
inst✝² : NumberField K
ι : Type u_2
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
b : Basis ι ℤ (𝓞 K)
b₀ : Basis ι ℤ (𝓞 K) := (RingOfIntegers.basis K).reindex ((RingOfIntegers.basis K).indexEquiv b)
⊢ Algebra.discr ℤ ⇑b = discr K

Tactic:
rw [Algebra.discr_eq_discr (𝓞 K) b b₀, Basis.coe_reindex, Algebra.discr_reindex]

Result:
no goals

Proof state:
K : Type u_1
inst✝³ : Field K
inst✝² : NumberField K
ι : Type u_2
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
b : Basis ι ℤ (𝓞 K)
⊢ Algebra.discr ℤ ⇑b = discr K

Tactic:
let b₀ := Basis.reindex (RingOfIntegers.basis K) (Basis.indexEquiv (RingOfIntegers.basis K) b)

Result:
K : Type u_1
inst✝³ : Field K
inst✝² : NumberField K
ι : Type u_2
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
b : Basis ι ℤ (𝓞 K)
b₀ : Basis ι ℤ (𝓞 K) := (RingOfIntegers.basis K).reindex ((RingOfIntegers.basis K).indexEquiv b)
⊢ Algebra.discr ℤ ⇑b = discr K
-- Mathlib/MeasureTheory/Measure/FiniteMeasureProd.lean
lemma prod_apply (s : Set (α × β)) (s_mble : MeasurableSet s) :
    μ.prod ν s = ENNReal.toNNReal (∫⁻ x, ν.toMeasure (Prod.mk x ⁻¹' s) ∂μ)

Proof state:
α : Type u_1
inst✝¹ : MeasurableSpace α
β : Type u_2
inst✝ : MeasurableSpace β
μ : FiniteMeasure α
ν : FiniteMeasure β
s : Set (α × β)
s_mble : MeasurableSet s
⊢ (μ.prod ν) s = (∫⁻ (x : α), ↑ν (Prod.mk x ⁻¹' s) ∂↑μ).toNNReal

Tactic:
simp [coeFn_def, Measure.prod_apply s_mble]

Result:
no goals
-- Mathlib/MeasureTheory/Integral/SetIntegral.lean
theorem integral_Icc_eq_integral_Ioo : ∫ t in Icc x y, f t ∂μ = ∫ t in Ioo x y, f t ∂μ

Proof state:
X : Type u_1
E : Type u_3
mX : MeasurableSpace X
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
f : X → E
μ : Measure X
inst✝¹ : PartialOrder X
x y : X
inst✝ : NoAtoms μ
⊢ ∫ (t : X) in Icc x y, f t ∂μ = ∫ (t : X) in Ioo x y, f t ∂μ

Tactic:
rw [integral_Icc_eq_integral_Ico, integral_Ico_eq_integral_Ioo]

Result:
no goals
-- Mathlib/Algebra/Group/Hom/Defs.lean
theorem ne_one_of_map {R S F : Type*} [One R] [One S] [FunLike F R S] [OneHomClass F R S]
    {f : F} {x : R} (hx : f x ≠ 1) : x ≠ 1 := ne_of_apply_ne f <| (by rwa [(map_one f)])

Proof state:
R : Type u_10
S : Type u_11
F : Type u_12
inst✝³ : One R
inst✝² : One S
inst✝¹ : FunLike F R S
inst✝ : OneHomClass F R S
f : F
x : R
hx : f x ≠ 1
⊢ f x ≠ f 1

Tactic:
rwa [(map_one f)]

Result:
no goals
-- Mathlib/SetTheory/Cardinal/Aleph.lean
theorem preOmega_zero : preOmega 0 = 0

Proof state:
⊢ sInf {x | x.IsInitial} = 0

Tactic:
exact csInf_eq_bot_of_bot_mem isInitial_zero

Result:
no goals

Proof state:
⊢ preOmega 0 = 0

Tactic:
rw [coe_preOmega, enumOrd_zero]

Result:
⊢ sInf {x | x.IsInitial} = 0
-- Mathlib/RingTheory/HahnSeries/Addition.lean
@[simp]
lemma addOppositeEquiv_symm_support (x : (HahnSeries Γ R)ᵃᵒᵖ) :
    (addOppositeEquiv.symm x).support = x.unop.support

Proof state:
Γ : Type u_1
R : Type u_3
inst✝¹ : PartialOrder Γ
inst✝ : AddMonoid R
x : (HahnSeries Γ R)ᵃᵒᵖ
⊢ (addOppositeEquiv.symm x).support = (AddOpposite.unop x).support

Tactic:
rw [← addOppositeEquiv_support, AddEquiv.apply_symm_apply]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem zero_ushiftRight {n : Nat} : 0#w >>> n = 0#w

Proof state:
w n : Nat
⊢ 0#w >>> n = 0#w

Tactic:
simp [bv_toNat]

Result:
no goals
-- Mathlib/Data/Real/ConjExponents.lean
theorem div_conj_eq_sub_one : p / q = p - 1

Proof state:
p q : ℝ
h : p.IsConjExponent q
⊢ p / q = p - 1

Tactic:
field_simp [h.symm.ne_zero]

Result:
p q : ℝ
h : p.IsConjExponent q
⊢ p = (p - 1) * q

Proof state:
p q : ℝ
h : p.IsConjExponent q
⊢ p = (p - 1) * q

Tactic:
rw [h.sub_one_mul_conj]

Result:
no goals
-- Mathlib/Algebra/Module/CharacterModule.lean
lemma exists_character_apply_ne_zero_of_ne_zero {a : A} (ne_zero : a ≠ 0) :
    ∃ (c : CharacterModule A), c a ≠ 0 :=
  have ⟨c, hc⟩ := dual_surjective_of_injective _ (Submodule.injective_subtype _) (ofSpanSingleton a)
  ⟨c, fun h ↦ ne_zero <| eq_zero_of_ofSpanSingleton_apply_self a <| by rwa [← hc]⟩

Proof state:
A : Type uA
inst✝ : AddCommGroup A
a : A
ne_zero : a ≠ 0
c : CharacterModule A
hc : (dual (Submodule.span ℤ {a}).subtype) c = ofSpanSingleton a
h : c a = 0
⊢ (ofSpanSingleton a) ⟨a, ⋯⟩ = 0

Tactic:
rwa [← hc]

Result:
no goals
-- Mathlib/Order/Heyting/Regular.lean
theorem IsRegular.disjoint_compl_left_iff (ha : IsRegular a) :
    Disjoint aᶜ b ↔ b ≤ a

Proof state:
α : Type u_1
inst✝ : HeytingAlgebra α
a b : α
ha : IsRegular a
⊢ Disjoint aᶜ b ↔ b ≤ a

Tactic:
rw [← le_compl_iff_disjoint_left, ha.eq]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Lemmas.lean
theorem get?_alter_self [LawfulBEq α] {k : α} {f : Option (β k) → Option (β k)} :
    (m.alter k f).get? k = f (m.get? k)

Proof state:
α : Type u
β : α → Type v
x✝¹ : BEq α
x✝ : Hashable α
m : DHashMap α β
inst✝ : LawfulBEq α
k : α
f : Option (β k) → Option (β k)
⊢ (m.alter k f).get? k = f (m.get? k)

Tactic:
simp only [get?_alter, beq_self_eq_true, reduceDIte, Function.comp_apply, cast_eq]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Nat/Bitwise/Lemmas.lean
theorem two_pow_succ_sub_succ_div_two : (2 ^ (n+1) - (x + 1)) / 2 = 2^n - (x/2 + 1)

Proof state:
n x : Nat
⊢ (2 ^ (n + 1) - (x + 1)) / 2 = 2 ^ n - (x / 2 + 1)

Tactic:
omega

Result:
no goals
-- Mathlib/Algebra/SkewMonoidAlgebra/Basic.lean
theorem single_eq_zero {a : G} {b : k} : single a b = 0 ↔ b = 0

Proof state:
k : Type u_1
G : Type u_2
inst✝ : AddCommMonoid k
a : G
b : k
⊢ single a b = 0 ↔ b = 0

Tactic:
rw [ofFinsupp_eq_zero, single, Finsupp.single_eq_zero]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Gamma/Basic.lean
theorem Gamma_one : Gamma 1 = 1

Proof state:
⊢ Gamma 1 = 1

Tactic:
rw [Gamma, Complex.ofReal_one, Complex.Gamma_one, Complex.one_re]

Result:
no goals
-- Mathlib/Algebra/Group/Subgroup/Ker.lean
theorem comap_injective {f : G →* N} (h : Function.Surjective f) : Function.Injective (comap f) :=
  fun K L => by simp only [le_antisymm_iff, comap_le_comap_of_surjective h, imp_self]

Proof state:
G : Type u_1
inst✝¹ : Group G
N : Type u_5
inst✝ : Group N
f : G →* N
h : Surjective ⇑f
K L : Subgroup N
⊢ comap f K = comap f L → K = L

Tactic:
simp only [le_antisymm_iff, comap_le_comap_of_surjective h, imp_self]

Result:
no goals
-- Mathlib/Order/Filter/Basic.lean
theorem Eventually.and_frequently {p q : α → Prop} {f : Filter α} (hp : ∀ᶠ x in f, p x)
    (hq : ∃ᶠ x in f, q x) : ∃ᶠ x in f, p x ∧ q x

Proof state:
α : Type u
p q : α → Prop
f : Filter α
hp : ∀ᶠ (x : α) in f, p x
hq : ∃ᶠ (x : α) in f, q x
⊢ ∃ᶠ (x : α) in f, p x ∧ q x

Tactic:
simpa only [and_comm] using hq.and_eventually hp

Result:
no goals
-- Mathlib/Data/ENNReal/Inv.lean
private lemma exists_lt_mul_right {a b c : ℝ≥0∞} (hc : c < a * b) : ∃ b' < b, c < a * b'

Proof state:
a b c : ℝ≥0∞
hc : c < b * a
⊢ ∃ b' < b, c < b' * a

Tactic:
exact exists_lt_mul_left hc

Result:
no goals

Proof state:
a b c : ℝ≥0∞
hc : c < a * b
⊢ ∃ b' < b, c < a * b'

Tactic:
simp_rw [mul_comm a] at hc ⊢

Result:
a b c : ℝ≥0∞
hc : c < b * a
⊢ ∃ b' < b, c < b' * a
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem toFin_cast (h : w = v) (x : BitVec w) :
    (x.cast h).toFin = x.toFin.cast (by rw [h]) :=
  rfl

Proof state:
w v : Nat
h : w = v
x : BitVec w
⊢ 2 ^ w = 2 ^ v

Tactic:
rw [h]

Result:
no goals
-- Mathlib/Algebra/Order/Floor/Div.lean
lemma support_floorDiv_subset : (f ⌊/⌋ a).support ⊆ f.support

Proof state:
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝³ : OrderedAddCommMonoid α
inst✝² : OrderedAddCommMonoid β
inst✝¹ : SMulZeroClass α β
inst✝ : FloorDiv α β
f : ι →₀ β
a : α
⊢ (f ⌊/⌋ a).support ⊆ f.support

Tactic:
simp +contextual [Finset.subset_iff, not_imp_not]

Result:
no goals
-- Mathlib/NumberTheory/LSeries/RiemannZeta.lean
lemma HurwitzZeta.hurwitzZeta_zero : hurwitzZeta 0 = riemannZeta

Proof state:
case h
s : ℂ
⊢ hurwitzZeta 0 s = riemannZeta s

Tactic:
simpa [hurwitzZeta, hurwitzZetaEven_zero] using hurwitzZetaOdd_neg 0 s

Result:
no goals

Proof state:
⊢ hurwitzZeta 0 = riemannZeta

Tactic:
ext1 s

Result:
case h
s : ℂ
⊢ hurwitzZeta 0 s = riemannZeta s
-- Mathlib/Order/Interval/Set/Pi.lean
theorem image_update_uIcc (f : ∀ i, α i) (i : ι) (a b : α i) :
    update f i '' uIcc a b = uIcc (update f i a) (update f i b) :=
  (image_update_Icc _ _ _ _).trans <| by simp_rw [uIcc, update_sup, update_inf]

Proof state:
ι : Type u_1
α : ι → Type u_2
inst✝¹ : (i : ι) → Lattice (α i)
inst✝ : DecidableEq ι
f : (i : ι) → α i
i : ι
a b : α i
⊢ Icc (update f i (a ⊓ b)) (update f i (a ⊔ b)) = uIcc (update f i a) (update f i b)

Tactic:
simp_rw [uIcc, update_sup, update_inf]

Result:
no goals
-- Mathlib/Analysis/NormedSpace/MStructure.lean
theorem mul_compl_self {P : { P : M // IsLprojection X P }} : (↑P : M) * ↑Pᶜ = 0

Proof state:
X : Type u_1
inst✝² : NormedAddCommGroup X
M : Type u_2
inst✝¹ : Ring M
inst✝ : Module M X
P : { P // IsLprojection X P }
⊢ ↑P * ↑Pᶜ = 0

Tactic:
rw [coe_compl, P.prop.proj.mul_one_sub_self]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/ToArray.lean
theorem findRevM?_toArray [Monad m] [LawfulMonad m] (f : α → m Bool) (l : List α) :
    l.toArray.findRevM? f = l.reverse.findM? f

Proof state:
m : Type → Type u_1
α : Type
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : α → m Bool
l : List α
⊢ findRevM? f l.toArray = findM? f l.reverse

Tactic:
rw [Array.findRevM?, findSomeRevM?_toArray, findM?_eq_findSomeM?]

Result:
no goals
-- Mathlib/Data/Set/Card.lean
theorem encard_pos : 0 < s.encard ↔ s.Nonempty

Proof state:
α : Type u_1
s : Set α
⊢ 0 < s.encard ↔ s.Nonempty

Tactic:
rw [pos_iff_ne_zero, encard_ne_zero]

Result:
no goals
-- Mathlib/Order/BooleanAlgebra.lean
theorem compl_sdiff : (x \ y)ᶜ = x ⇨ y

Proof state:
α : Type u
x y : α
inst✝ : BooleanAlgebra α
⊢ (x \ y)ᶜ = x ⇨ y

Tactic:
rw [sdiff_eq, himp_eq, compl_inf, compl_compl, sup_comm]

Result:
no goals
-- Mathlib/Computability/Primrec.lean
theorem option_some : Primrec (@some α) :=
  ((casesOn1 0 (Nat.Primrec.succ.comp .succ)).comp (@Primcodable.prim α _)).of_eq fun n => by
    cases @decode α _ n <;> simp

Proof state:
α : Type u_1
inst✝ : Primcodable α
n : ℕ
⊢ (Nat.casesOn (encode (decode n)) 0 fun n => n.succ.succ) = encode (Option.map some (decode n))

Tactic:
cases @decode α _ n <;> simp

Result:
no goals
-- Mathlib/Data/Finset/Card.lean
theorem card_filter_eq_iff {p : α → Prop} [DecidablePred p] :
    #(s.filter p) = #s ↔ ∀ x ∈ s, p x

Proof state:
α : Type u_1
s : Finset α
p : α → Prop
inst✝ : DecidablePred p
⊢ #(filter p s) = #s ↔ ∀ x ∈ s, p x

Tactic:
rw [(card_filter_le s p).eq_iff_not_lt, not_lt, eq_iff_card_le_of_subset (filter_subset p s),
  filter_eq_self]

Result:
no goals
-- Mathlib/Algebra/Group/Basic.lean
theorem mul_div_right_comm : a * b / c = a / c * b

Proof state:
α : Type u_1
inst✝ : DivisionCommMonoid α
a b c : α
⊢ a * b / c = a / c * b

Tactic:
simp

Result:
no goals
-- Mathlib/RingTheory/Algebraic/Basic.lean
theorem Subalgebra.isField_of_algebraic [Algebra.IsAlgebraic K L] : IsField A :=
  { show Nontrivial A by infer_instance, Subalgebra.toCommRing A with
    mul_inv_cancel := fun {a} ha =>
      ⟨⟨a⁻¹, A.inv_mem_of_algebraic (Algebra.IsAlgebraic.isAlgebraic (a : L))⟩,
        Subtype.ext (mul_inv_cancel₀ (mt (Subalgebra.coe_eq_zero _).mp ha))⟩ }

Proof state:
K : Type u_1
L : Type u_2
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
A : Subalgebra K L
inst✝ : Algebra.IsAlgebraic K L
⊢ Nontrivial ↥A

Tactic:
infer_instance

Result:
no goals
-- Mathlib/Probability/Kernel/Composition/Prod.lean
theorem lintegral_prod_symm (κ : Kernel α β) [IsSFiniteKernel κ] (η : Kernel α γ)
    [IsSFiniteKernel η] (a : α) {g : β × γ → ℝ≥0∞} (hg : Measurable g) :
    ∫⁻ c, g c ∂(κ ×ₖ η) a = ∫⁻ c, ∫⁻ b, g (b, c) ∂κ a ∂η a

Proof state:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
γ : Type u_4
mγ : MeasurableSpace γ
κ : Kernel α β
inst✝¹ : IsSFiniteKernel κ
η : Kernel α γ
inst✝ : IsSFiniteKernel η
a : α
g : β × γ → ℝ≥0∞
hg : Measurable g
⊢ ∫⁻ (c : β × γ), g c ∂(κ ×ₖ η) a = ∫⁻ (c : γ), ∫⁻ (b : β), g (b, c) ∂κ a ∂η a

Tactic:
rw [prod_apply, MeasureTheory.lintegral_prod_symm _ hg.aemeasurable]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Pow/NNReal.lean
theorem rpow_zero {x : ℝ≥0∞} : x ^ (0 : ℝ) = 1

Proof state:
case coe
x✝ : ℝ≥0
⊢ (if x✝ = 0 ∧ 0 < 0 then ⊤ else ↑(x✝.rpow 0)) = 1

Tactic:
simp [lt_irrefl]

Result:
no goals
-- Mathlib/Algebra/Ring/Periodic.lean
theorem Periodic.sub_const [AddCommGroup α] (h : Periodic f c) (a : α) :
    Periodic (fun x => f (x - a)) c

Proof state:
α : Type u_1
β : Type u_2
f : α → β
c : α
inst✝ : AddCommGroup α
h : Periodic f c
a : α
⊢ Periodic (fun x => f (x - a)) c

Tactic:
simpa only [sub_eq_add_neg] using h.add_const (-a)

Result:
no goals
-- Mathlib/Data/Real/Sqrt.lean
theorem sqrt_ne_zero' : √x ≠ 0 ↔ 0 < x

Proof state:
x : ℝ
⊢ √x ≠ 0 ↔ 0 < x

Tactic:
rw [← not_le, not_iff_not, sqrt_eq_zero']

Result:
no goals
-- Mathlib/CategoryTheory/Generator/Basic.lean
theorem isCodetector_op_iff (G : C) : IsCodetector (op G) ↔ IsDetector G

Proof state:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
G : C
⊢ IsCodetector (op G) ↔ IsDetector G

Tactic:
rw [IsDetector, IsCodetector, ← isCodetecting_op_iff, Set.singleton_op]

Result:
no goals
-- Mathlib/MeasureTheory/Integral/Lebesgue.lean
theorem lintegral_inter_add_diff {B : Set α} (f : α → ℝ≥0∞) (A : Set α) (hB : MeasurableSet B) :
    ∫⁻ x in A ∩ B, f x ∂μ + ∫⁻ x in A \ B, f x ∂μ = ∫⁻ x in A, f x ∂μ

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
B : Set α
f : α → ℝ≥0∞
A : Set α
hB : MeasurableSet B
⊢ ∫⁻ (x : α) in A ∩ B, f x ∂μ + ∫⁻ (x : α) in A \ B, f x ∂μ = ∫⁻ (x : α) in A, f x ∂μ

Tactic:
rw [← lintegral_add_measure, restrict_inter_add_diff _ hB]

Result:
no goals
-- Mathlib/LinearAlgebra/AffineSpace/Basis.lean
theorem nonempty : Nonempty ι :=
  not_isEmpty_iff.mp fun hι => by
    simpa only [@range_eq_empty _ _ hι, AffineSubspace.span_empty, bot_ne_top] using b.tot

Proof state:
ι : Type u_1
k : Type u_5
V : Type u_6
P : Type u_7
inst✝³ : AddCommGroup V
inst✝² : AffineSpace V P
inst✝¹ : Ring k
inst✝ : Module k V
b : AffineBasis ι k P
hι : IsEmpty ι
⊢ False

Tactic:
simpa only [@range_eq_empty _ _ hι, AffineSubspace.span_empty, bot_ne_top] using b.tot

Result:
no goals
-- Mathlib/Data/Matroid/Basic.lean
theorem IsBasis.isBasis_iUnion {ι : Type _} [Nonempty ι] (X : ι → Set α)
    (hI : ∀ i, M.IsBasis I (X i)) : M.IsBasis I (⋃ i, X i)

Proof state:
α : Type u_1
M : Matroid α
I : Set α
ι : Type u_2
inst✝ : Nonempty ι
X : ι → Set α
hI : ∀ (i : ι), M.IsBasis I (X i)
⊢ M.IsBasis I (⋃ i, X i)

Tactic:
convert IsBasis.iUnion_isBasis_iUnion X (fun _ ↦ I) (fun i ↦ hI i) _ <;> rw [iUnion_const]

Result:
α : Type u_1
M : Matroid α
I : Set α
ι : Type u_2
inst✝ : Nonempty ι
X : ι → Set α
hI : ∀ (i : ι), M.IsBasis I (X i)
⊢ M.Indep I

Proof state:
α : Type u_1
M : Matroid α
I : Set α
ι : Type u_2
inst✝ : Nonempty ι
X : ι → Set α
hI : ∀ (i : ι), M.IsBasis I (X i)
⊢ M.Indep I

Tactic:
exact (hI (Classical.arbitrary ι)).indep

Result:
no goals
-- Mathlib/RingTheory/Ideal/Maps.lean
theorem map_eq_bot_iff_of_injective {I : Ideal R} {f : F} (hf : Function.Injective f) :
    I.map f = ⊥ ↔ I = ⊥

Proof state:
R : Type u_1
S : Type u_2
F : Type u_3
inst✝² : Semiring R
inst✝¹ : Semiring S
inst✝ : FunLike F R S
rc : RingHomClass F R S
I : Ideal R
f : F
hf : Function.Injective ⇑f
⊢ map f I = ⊥ ↔ I = ⊥

Tactic:
simp [map, span_eq_bot, ← map_zero f, -map_zero, hf.eq_iff, I.eq_bot_iff]

Result:
no goals
-- Mathlib/Algebra/Order/Floor.lean
theorem floor_add_one (ha : 0 ≤ a) : ⌊a + 1⌋₊ = ⌊a⌋₊ + 1

Proof state:
α : Type u_2
inst✝¹ : LinearOrderedSemiring α
inst✝ : FloorSemiring α
a : α
ha : 0 ≤ a
⊢ ⌊a + 1⌋₊ = ⌊a⌋₊ + 1

Tactic:
rw [← cast_one, floor_add_nat ha 1]

Result:
no goals
-- Mathlib/NumberTheory/FLT/Three.lean
private lemma X_ne_zero : S.X ≠ 0 :=
  fun h ↦ lambda_not_dvd_x S <| by simp [← X_u₁_spec, h]

Proof state:
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑3
S : Solution hζ
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
h : FermatLastTheoremForThreeGen.Solution.X S = 0
⊢ λ ∣ FermatLastTheoremForThreeGen.Solution.x S

Tactic:
simp [← X_u₁_spec, h]

Result:
no goals
-- Mathlib/Data/NNRat/Defs.lean
theorem le_toNNRat_iff_coe_le {q : ℚ≥0} (hp : 0 ≤ p) : q ≤ toNNRat p ↔ ↑q ≤ p

Proof state:
p : ℚ
q : ℚ≥0
hp : 0 ≤ p
⊢ q ≤ p.toNNRat ↔ ↑q ≤ p

Tactic:
rw [← coe_le_coe, Rat.coe_toNNRat p hp]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/BinaryEntropy.lean
@[simp] lemma binEntropy_one : binEntropy 1 = 0

Proof state:
⊢ binEntropy 1 = 0

Tactic:
simp [binEntropy]

Result:
no goals
-- Mathlib/Algebra/Ring/Parity.lean
lemma Even.pow_of_ne_zero (ha : Even a) : ∀ {n : ℕ}, n ≠ 0 → Even (a ^ n)
  | n + 1, _ => by rw [pow_succ]; exact ha.mul_left _

Proof state:
α : Type u_2
inst✝ : Semiring α
a : α
ha : Even a
n : ℕ
x✝ : n + 1 ≠ 0
⊢ Even (a ^ n * a)

Tactic:
exact ha.mul_left _

Result:
no goals

Proof state:
α : Type u_2
inst✝ : Semiring α
a : α
ha : Even a
n : ℕ
x✝ : n + 1 ≠ 0
⊢ Even (a ^ (n + 1))

Tactic:
rw [pow_succ]

Result:
α : Type u_2
inst✝ : Semiring α
a : α
ha : Even a
n : ℕ
x✝ : n + 1 ≠ 0
⊢ Even (a ^ n * a)
-- Mathlib/Algebra/MonoidAlgebra/Degree.lean
theorem supDegree_single (a : A) (r : R) :
    (single a r).supDegree D = if r = 0 then ⊥ else D a

Proof state:
R : Type u_1
A : Type u_3
B : Type u_5
inst✝² : Semiring R
inst✝¹ : SemilatticeSup B
inst✝ : OrderBot B
D : A → B
a : A
r : R
⊢ supDegree D (single a r) = if r = 0 then ⊥ else D a

Tactic:
split_ifs with hr <;> simp [supDegree_single_ne_zero, hr]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Int/DivModLemmas.lean
theorem fdiv_eq_ediv : ∀ (a : Int) {b : Int}, 0 ≤ b → fdiv a b = a / b
  | 0, _, _ | -[_+1], 0, _ => by simp
  | succ _, ofNat _, _ | -[_+1], succ _, _ => rfl

Proof state:
a✝ : Nat
x✝ : 0 ≤ 0
⊢ -[a✝+1].fdiv 0 = -[a✝+1] / 0

Tactic:
simp

Result:
no goals
-- Mathlib/Algebra/Algebra/Basic.lean
theorem injective_algebraMap_of_linearMap (hb : Injective b) :
    Injective (algebraMap F E) := fun x y e ↦ hb <| by
  rw [← mul_one x, ← mul_one y, ← smul_eq_mul, ← smul_eq_mul,
    map_smul, map_smul, Algebra.smul_def, Algebra.smul_def, e]

Proof state:
F : Type u_1
E : Type u_2
inst✝² : CommSemiring F
inst✝¹ : Semiring E
inst✝ : Algebra F E
b : F →ₗ[F] E
hb : Injective ⇑b
x y : F
e : (algebraMap F E) x = (algebraMap F E) y
⊢ b x = b y

Tactic:
rw [← mul_one x, ← mul_one y, ← smul_eq_mul, ← smul_eq_mul,
  map_smul, map_smul, Algebra.smul_def, Algebra.smul_def, e]

Result:
no goals
-- Mathlib/Analysis/PSeries.lean
theorem not_summable_one_div_natCast : ¬Summable (fun n => 1 / n : ℕ → ℝ)

Proof state:
⊢ ¬Summable fun n => 1 / ↑n

Tactic:
simpa only [inv_eq_one_div] using not_summable_natCast_inv

Result:
no goals
-- Mathlib/ModelTheory/Substructures.lean
theorem mem_closure_iff_exists_term {x : M} :
    x ∈ closure L s ↔ ∃ t : L.Term s, t.realize ((↑) : s → M) = x

Proof state:
L : Language
M : Type w
inst✝ : L.Structure M
s : Set M
x : M
⊢ x ∈ (closure L).toFun s ↔ ∃ t, Term.realize Subtype.val t = x

Tactic:
rw [← SetLike.mem_coe, coe_closure_eq_range_term_realize, mem_range]

Result:
no goals
-- Mathlib/Algebra/Polynomial/AlgebraMap.lean
lemma dvd_comp_X_add_C_iff (p q : R[X]) (a : R) :
    p ∣ q.comp (X + C a) ↔ p.comp (X - C a) ∣ q

Proof state:
R : Type u
inst✝ : CommRing R
p q : R[X]
a : R
⊢ p ∣ q.comp (X + C a) ↔ p.comp (X - C a) ∣ q

Tactic:
simpa using dvd_comp_X_sub_C_iff p q (-a)

Result:
no goals
-- Mathlib/LinearAlgebra/Basis/Defs.lean
theorem reindexRange_apply (x : range b) : b.reindexRange x = x

Proof state:
case mk.intro
ι : Type u_1
R : Type u_3
M : Type u_6
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
b : Basis ι R M
i : ι
⊢ b.reindexRange ⟨b i, ⋯⟩ = ↑⟨b i, ⋯⟩

Tactic:
exact b.reindexRange_self i

Result:
no goals

Proof state:
ι : Type u_1
R : Type u_3
M : Type u_6
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
b : Basis ι R M
x : ↑(range ⇑b)
⊢ b.reindexRange x = ↑x

Tactic:
rcases x with ⟨bi, ⟨i, rfl⟩⟩

Result:
case mk.intro
ι : Type u_1
R : Type u_3
M : Type u_6
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
b : Basis ι R M
i : ι
⊢ b.reindexRange ⟨b i, ⋯⟩ = ↑⟨b i, ⋯⟩
-- Mathlib/Algebra/Group/Basic.lean
theorem eq_inv_mul_of_mul_eq (h : b * a = c) : a = b⁻¹ * c

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

Tactic:
simp [h.symm]

Result:
no goals
-- Mathlib/Topology/ContinuousMap/CompactlySupported.lean
lemma compLeft_apply {g : C(β, γ)} (hg : g 0 = 0) (f : C_c(α, β)) (a : α) :
    f.compLeft g a = g (f a)

Proof state:
α : Type u_2
β : Type u_3
inst✝⁴ : TopologicalSpace α
inst✝³ : TopologicalSpace β
inst✝² : Zero β
γ : Type u_5
inst✝¹ : TopologicalSpace γ
inst✝ : Zero γ
g : C(β, γ)
hg : g 0 = 0
f : α →C_c β
a : α
⊢ (compLeft g f) a = g (f a)

Tactic:
simp [coe_compLeft hg f]

Result:
no goals
-- Mathlib/Probability/Kernel/Composition/MeasureComp.lean
lemma ae_ae_of_ae_comp {p : β → Prop} (h : ∀ᵐ ω ∂(κ ∘ₘ μ), p ω) :
    ∀ᵐ ω' ∂μ, ∀ᵐ ω ∂(κ ω'), p ω

Proof state:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
κ : Kernel α β
p : β → Prop
h : ∀ᵐ (ω : β) ∂⇑κ ∘ₘ μ, p ω
⊢ ∀ᵐ (ω' : α) ∂μ, ∀ᵐ (ω : β) ∂κ ω', p ω

Tactic:
rw [comp_eq_comp_const_apply] at h

Result:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
κ : Kernel α β
p : β → Prop
h : ∀ᵐ (ω : β) ∂(κ ∘ₖ Kernel.const Unit μ) (), p ω
⊢ ∀ᵐ (ω' : α) ∂μ, ∀ᵐ (ω : β) ∂κ ω', p ω

Proof state:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
κ : Kernel α β
p : β → Prop
h : ∀ᵐ (ω : β) ∂(κ ∘ₖ Kernel.const Unit μ) (), p ω
⊢ ∀ᵐ (ω' : α) ∂μ, ∀ᵐ (ω : β) ∂κ ω', p ω

Tactic:
exact Kernel.ae_ae_of_ae_comp h

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Lemmas.lean
theorem cast_mk (a : Array α) (h : a.size = n) (h' : n = m) :
    (Vector.mk a h).cast h' = Vector.mk a (by simp [h, h']) := rfl

Proof state:
α : Type ?u.8300
n m : Nat
a : Array α
h : a.size = n
h' : n = m
⊢ a.size = m

Tactic:
simp [h, h']

Result:
no goals
-- Mathlib/Algebra/BigOperators/Expect.lean
@[simp] lemma expect_ite_mem (s : Finset ι) (f : ι → M) :
    𝔼 i, (if i ∈ s then f i else 0) = s.dens • 𝔼 i ∈ s, f i

Proof state:
ι : Type u_1
M : Type u_3
inst✝³ : Fintype ι
inst✝² : AddCommMonoid M
inst✝¹ : Module ℚ≥0 M
inst✝ : DecidableEq ι
s : Finset ι
f : ι → M
⊢ (𝔼 i : ι, if i ∈ s then f i else 0) = s.dens • 𝔼 i ∈ s, f i

Tactic:
simp [Finset.expect_ite_mem, dens]

Result:
no goals
-- Mathlib/Algebra/ContinuedFractions/Translations.lean
theorem first_cont_eq {gp : Pair K} (zeroth_s_eq : g.s.get? 0 = some gp) :
    g.conts 1 = ⟨gp.b * g.h + gp.a, gp.b⟩

Proof state:
K : Type u_1
g : GenContFract K
inst✝ : DivisionRing K
gp : Pair K
zeroth_s_eq : g.s.get? 0 = some gp
⊢ g.conts 1 = { a := gp.b * g.h + gp.a, b := gp.b }

Tactic:
simp [nth_cont_eq_succ_nth_contAux, second_contAux_eq zeroth_s_eq]

Result:
no goals
-- Mathlib/Algebra/Order/Group/Unbundled/Basic.lean
theorem div_lt_div_iff' : a / b < c / d ↔ a * d < c * b

Proof state:
α : Type u
inst✝² : CommGroup α
inst✝¹ : LT α
inst✝ : MulLeftStrictMono α
a b c d : α
⊢ a / b < c / d ↔ a * d < c * b

Tactic:
simpa only [div_eq_mul_inv] using mul_inv_lt_mul_inv_iff'

Result:
no goals
-- Mathlib/Logic/Basic.lean
theorem xor_iff_iff_not : Xor' a b ↔ (a ↔ ¬b)

Proof state:
a b : Prop
⊢ Xor' a b ↔ (a ↔ ¬b)

Tactic:
simp only [← @xor_not_right a, not_not]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Erase.lean
theorem eraseP_ne_nil_iff {xs : List α} {p : α → Bool} : xs.eraseP p ≠ [] ↔ xs ≠ [] ∧ ∀ x, p x → xs ≠ [x]

Proof state:
α : Type u_1
xs : List α
p : α → Bool
⊢ eraseP p xs ≠ [] ↔ xs ≠ [] ∧ ∀ (x : α), p x = true → xs ≠ [x]

Tactic:
simp

Result:
no goals
-- Mathlib/Topology/PartialHomeomorph.lean
theorem interior (h : e.IsImage s t) : e.IsImage (interior s) (interior t)

Proof state:
X : Type u_1
Y : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
e : PartialHomeomorph X Y
s : Set X
t : Set Y
h : e.IsImage s t
⊢ e.IsImage (interior s) (interior t)

Tactic:
simpa only [closure_compl, compl_compl] using h.compl.closure.compl

Result:
no goals