harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Combinatorics/SetFamily/AhlswedeZhang.lean
lemma truncatedInf_of_isAntichain (hs : IsAntichain (· ≤ ·) (s : Set α)) (ha : a ∈ s) :
    truncatedInf s a = a

Proof state:
α : Type u_1
inst✝² : SemilatticeInf α
s : Finset α
a : α
inst✝¹ : DecidableRel fun x1 x2 => x1 ≤ x2
inst✝ : BoundedOrder α
hs : IsAntichain (fun x1 x2 => x1 ≤ x2) ↑s
ha : a ∈ s
⊢ s.truncatedInf a = a

Tactic:
refine le_antisymm truncatedInf_le ?_

Result:
α : Type u_1
inst✝² : SemilatticeInf α
s : Finset α
a : α
inst✝¹ : DecidableRel fun x1 x2 => x1 ≤ x2
inst✝ : BoundedOrder α
hs : IsAntichain (fun x1 x2 => x1 ≤ x2) ↑s
ha : a ∈ s
⊢ a ≤ s.truncatedInf a

Proof state:
case intro
α : Type u_1
inst✝² : SemilatticeInf α
s : Finset α
a : α
inst✝¹ : DecidableRel fun x1 x2 => x1 ≤ x2
inst✝ : BoundedOrder α
hs : IsAntichain (fun x1 x2 => x1 ≤ x2) ↑s
ha : a ∈ s
b : α
hb : b ∈ s
hba : b ≤ a
⊢ a ≤ id b

Tactic:
exact (hs.eq hb ha hba).ge

Result:
no goals

Proof state:
α : Type u_1
inst✝² : SemilatticeInf α
s : Finset α
a : α
inst✝¹ : DecidableRel fun x1 x2 => x1 ≤ x2
inst✝ : BoundedOrder α
hs : IsAntichain (fun x1 x2 => x1 ≤ x2) ↑s
ha : a ∈ s
⊢ ∀ (b : α), b ∈ s ∧ b ≤ a → a ≤ id b

Tactic:
rintro b ⟨hb, hba⟩

Result:
case intro
α : Type u_1
inst✝² : SemilatticeInf α
s : Finset α
a : α
inst✝¹ : DecidableRel fun x1 x2 => x1 ≤ x2
inst✝ : BoundedOrder α
hs : IsAntichain (fun x1 x2 => x1 ≤ x2) ↑s
ha : a ∈ s
b : α
hb : b ∈ s
hba : b ≤ a
⊢ a ≤ id b

Proof state:
α : Type u_1
inst✝² : SemilatticeInf α
s : Finset α
a : α
inst✝¹ : DecidableRel fun x1 x2 => x1 ≤ x2
inst✝ : BoundedOrder α
hs : IsAntichain (fun x1 x2 => x1 ≤ x2) ↑s
ha : a ∈ s
⊢ a ≤ s.truncatedInf a

Tactic:
simp_rw [truncatedInf_of_mem (subset_upperClosure ha), le_inf'_iff, mem_filter]

Result:
α : Type u_1
inst✝² : SemilatticeInf α
s : Finset α
a : α
inst✝¹ : DecidableRel fun x1 x2 => x1 ≤ x2
inst✝ : BoundedOrder α
hs : IsAntichain (fun x1 x2 => x1 ≤ x2) ↑s
ha : a ∈ s
⊢ ∀ (b : α), b ∈ s ∧ b ≤ a → a ≤ id b
-- Mathlib/Algebra/AddTorsor/Defs.lean
theorem vsub_self (p : P) : p -ᵥ p = (0 : G)

Proof state:
G : Type u_1
P : Type u_2
inst✝ : AddGroup G
T : AddTorsor G P
p : P
⊢ p -ᵥ p = 0

Tactic:
rw [← zero_add (p -ᵥ p), ← vadd_vsub_assoc, vadd_vsub]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem setWidth_zero (m n : Nat) : setWidth m 0#n = 0#m

Proof state:
case a
m n : Nat
⊢ (setWidth m 0#n).toNat = (0#m).toNat

Tactic:
simp [toNat_setWidth]

Result:
no goals

Proof state:
m n : Nat
⊢ setWidth m 0#n = 0#m

Tactic:
apply eq_of_toNat_eq

Result:
case a
m n : Nat
⊢ (setWidth m 0#n).toNat = (0#m).toNat
-- Mathlib/Dynamics/TopologicalEntropy/CoverEntropy.lean
lemma IsDynCoverOf.of_entourage_subset {T : X → X} {F : Set X} {U V : Set (X × X)} (U_V : U ⊆ V)
    {n : ℕ} {s : Set X} (h : IsDynCoverOf T F U n s) :
    IsDynCoverOf T F V n s

Proof state:
X : Type u_1
T : X → X
F : Set X
U V : Set (X × X)
U_V : U ⊆ V
n : ℕ
s : Set X
h : IsDynCoverOf T F U n s
⊢ IsDynCoverOf T F V n s

Tactic:
exact Subset.trans (c := ⋃ x ∈ s, ball x (dynEntourage T V n)) h
  (iUnion₂_mono fun x _ ↦ ball_mono (dynEntourage_monotone T n U_V) x)

Result:
no goals
-- Mathlib/LinearAlgebra/TensorProduct/Tower.lean
@[simp]
lemma baseChange_bot : (⊥ : Submodule R M).baseChange A = ⊥

Proof state:
R : Type u_1
M : Type u_2
A : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Algebra R A
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
⊢ baseChange A ⊥ = ⊥

Tactic:
simp [baseChange]

Result:
no goals
-- Mathlib/Order/Filter/Cocardinal.lean
theorem hasBasis_cocardinal : HasBasis (cocardinal α hreg) {s : Set α | #s < c} compl :=
  ⟨fun s =>
    ⟨fun h => ⟨sᶜ, h, (compl_compl s).subset⟩, fun ⟨_t, htf, hts⟩ => by
      have : #↑sᶜ < c

Proof state:
α : Type u
c : Cardinal.{u}
hreg : c.IsRegular
s : Set α
x✝ : ∃ i, {s | #↑s < c} i ∧ iᶜ ⊆ s
_t : Set α
htf : {s | #↑s < c} _t
hts : _tᶜ ⊆ s
⊢ #↑sᶜ < c

Tactic:
apply lt_of_le_of_lt _ htf

Result:
α : Type u
c : Cardinal.{u}
hreg : c.IsRegular
s : Set α
x✝ : ∃ i, {s | #↑s < c} i ∧ iᶜ ⊆ s
_t : Set α
htf : {s | #↑s < c} _t
hts : _tᶜ ⊆ s
⊢ #↑sᶜ ≤ #↑_t

Proof state:
α : Type u
c : Cardinal.{u}
hreg : c.IsRegular
s : Set α
x✝ : ∃ i, {s | #↑s < c} i ∧ iᶜ ⊆ s
_t : Set α
htf : {s | #↑s < c} _t
hts : _tᶜ ⊆ s
this : #↑sᶜ < c
⊢ s ∈ cocardinal α hreg

Tactic:
simp_all only [mem_cocardinal]

Result:
no goals

Proof state:
α : Type u
c : Cardinal.{u}
hreg : c.IsRegular
s : Set α
x✝ : ∃ i, {s | #↑s < c} i ∧ iᶜ ⊆ s
_t : Set α
htf : {s | #↑s < c} _t
hts : sᶜ ⊆ _t
⊢ #↑sᶜ ≤ #↑_t

Tactic:
apply Cardinal.mk_le_mk_of_subset hts

Result:
no goals

Proof state:
α : Type u
c : Cardinal.{u}
hreg : c.IsRegular
s : Set α
x✝ : ∃ i, {s | #↑s < c} i ∧ iᶜ ⊆ s
_t : Set α
htf : {s | #↑s < c} _t
hts : _tᶜ ⊆ s
⊢ #↑sᶜ ≤ #↑_t

Tactic:
rw [compl_subset_comm] at hts

Result:
α : Type u
c : Cardinal.{u}
hreg : c.IsRegular
s : Set α
x✝ : ∃ i, {s | #↑s < c} i ∧ iᶜ ⊆ s
_t : Set α
htf : {s | #↑s < c} _t
hts : sᶜ ⊆ _t
⊢ #↑sᶜ ≤ #↑_t

Proof state:
α : Type u
c : Cardinal.{u}
hreg : c.IsRegular
s : Set α
x✝ : ∃ i, {s | #↑s < c} i ∧ iᶜ ⊆ s
_t : Set α
htf : {s | #↑s < c} _t
hts : _tᶜ ⊆ s
⊢ s ∈ cocardinal α hreg

Tactic:
have : #↑sᶜ < c := by
  apply lt_of_le_of_lt _ htf
  rw [compl_subset_comm] at hts
  apply Cardinal.mk_le_mk_of_subset hts

Result:
α : Type u
c : Cardinal.{u}
hreg : c.IsRegular
s : Set α
x✝ : ∃ i, {s | #↑s < c} i ∧ iᶜ ⊆ s
_t : Set α
htf : {s | #↑s < c} _t
hts : _tᶜ ⊆ s
this : #↑sᶜ < c
⊢ s ∈ cocardinal α hreg
-- Mathlib/Topology/ContinuousOn.lean
theorem preimage_nhdsWithin_coinduced' {π : α → β} {s : Set β} {t : Set α} {a : α} (h : a ∈ t)
    (hs : s ∈ @nhds β (.coinduced (fun x : t => π x) inferInstance) (π a)) :
    π ⁻¹' s ∈ 𝓝[t] a

Proof state:
α : Type u_1
β : Type u_2
inst✝ : TopologicalSpace α
π : α → β
s : Set β
t : Set α
a : α
h : a ∈ t
hs : s ∈ 𝓝 (π a)
⊢ π ⁻¹' s ∈ 𝓝[t] a

Tactic:
lift a to t using h

Result:
case intro
α : Type u_1
β : Type u_2
inst✝ : TopologicalSpace α
π : α → β
s : Set β
t : Set α
a : { x // x ∈ t }
hs : s ∈ 𝓝 (π ↑a)
⊢ π ⁻¹' s ∈ 𝓝[t] ↑a

Proof state:
case intro
α : Type u_1
β : Type u_2
inst✝ : TopologicalSpace α
π : α → β
s : Set β
t : Set α
a : { x // x ∈ t }
hs : s ∈ 𝓝 (π ↑a)
⊢ π ⁻¹' s ∈ 𝓝[t] ↑a

Tactic:
replace hs : (fun x : t => π x) ⁻¹' s ∈ 𝓝 a := preimage_nhds_coinduced hs

Result:
case intro
α : Type u_1
β : Type u_2
inst✝ : TopologicalSpace α
π : α → β
s : Set β
t : Set α
a : { x // x ∈ t }
hs : (fun x => π ↑x) ⁻¹' s ∈ 𝓝 a
⊢ π ⁻¹' s ∈ 𝓝[t] ↑a

Proof state:
case intro
α : Type u_1
β : Type u_2
inst✝ : TopologicalSpace α
π : α → β
s : Set β
t : Set α
a : { x // x ∈ t }
hs : (fun x => π ↑x) ⁻¹' s ∈ 𝓝 a
⊢ π ⁻¹' s ∈ 𝓝[t] ↑a

Tactic:
rwa [← map_nhds_subtype_val, mem_map]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Raw.lean
theorem WF.Const.insertManyIfNewUnit [BEq α] [Hashable α] {ρ : Type w} [ForIn Id ρ α]
    {m : Raw α (fun _ => Unit)} {l : ρ} (h : m.WF) : (Const.insertManyIfNewUnit m l).WF

Proof state:
α : Type u
inst✝² : BEq α
inst✝¹ : Hashable α
ρ : Type w
inst✝ : ForIn Id ρ α
m : Raw α fun x => Unit
l : ρ
h : m.WF
⊢ (Raw.Const.insertManyIfNewUnit m l).WF

Tactic:
simpa [Raw.Const.insertManyIfNewUnit, h.size_buckets_pos] using
  (Raw₀.Const.insertManyIfNewUnit ⟨m, h.size_buckets_pos⟩ l).2 _ WF.insertIfNew₀ h

Result:
no goals
-- Mathlib/RingTheory/Localization/Integral.lean
theorem integerNormalization_aeval_eq_zero [Algebra R R'] [Algebra S R'] [IsScalarTower R S R']
    (p : S[X]) {x : R'} (hx : aeval x p = 0) : aeval x (integerNormalization M p) = 0

Proof state:
R : Type u_1
inst✝⁷ : CommRing R
M : Submonoid R
S : Type u_2
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
inst✝⁴ : IsLocalization M S
R' : Type u_3
inst✝³ : CommRing R'
inst✝² : Algebra R R'
inst✝¹ : Algebra S R'
inst✝ : IsScalarTower R S R'
p : S[X]
x : R'
hx : (aeval x) p = 0
⊢ (aeval x) (integerNormalization M p) = 0

Tactic:
rw [aeval_def, IsScalarTower.algebraMap_eq R S R',
  integerNormalization_eval₂_eq_zero _ (algebraMap _ _) _ hx]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Grind/Lemmas.lean
theorem eq_true_of_and_eq_true_right {a b : Prop} (h : (a ∧ b) = True) : b = True

Proof state:
a b : Prop
h : (a ∧ b) = True
⊢ b = True

Tactic:
simp_all

Result:
no goals
-- Mathlib/Order/WithBot.lean
@[simp]
lemma WithBot.ofDual_lt_ofDual_iff {x y : WithBot αᵒᵈ} :
    WithBot.ofDual x < WithBot.ofDual y ↔ y < x

Proof state:
α : Type u_1
inst✝ : LT α
x y : WithBot αᵒᵈ
⊢ WithBot.ofDual x < WithBot.ofDual y ↔ y < x

Tactic:
cases x <;> cases y <;> simp

Result:
no goals
-- Mathlib/Analysis/Asymptotics/Defs.lean
theorem isLittleO_norm_left : (fun x => ‖f' x‖) =o[l] g ↔ f' =o[l] g

Proof state:
α : Type u_1
F : Type u_4
E' : Type u_6
inst✝¹ : Norm F
inst✝ : SeminormedAddCommGroup E'
g : α → F
f' : α → E'
l : Filter α
⊢ (∀ ⦃c : ℝ⦄, 0 < c → IsBigOWith c l (fun x => ‖f' x‖) g) ↔ ∀ ⦃c : ℝ⦄, 0 < c → IsBigOWith c l f' g

Tactic:
exact forall₂_congr fun _ _ => isBigOWith_norm_left

Result:
no goals

Proof state:
α : Type u_1
F : Type u_4
E' : Type u_6
inst✝¹ : Norm F
inst✝ : SeminormedAddCommGroup E'
g : α → F
f' : α → E'
l : Filter α
⊢ (fun x => ‖f' x‖) =o[l] g ↔ f' =o[l] g

Tactic:
simp only [IsLittleO_def]

Result:
α : Type u_1
F : Type u_4
E' : Type u_6
inst✝¹ : Norm F
inst✝ : SeminormedAddCommGroup E'
g : α → F
f' : α → E'
l : Filter α
⊢ (∀ ⦃c : ℝ⦄, 0 < c → IsBigOWith c l (fun x => ‖f' x‖) g) ↔ ∀ ⦃c : ℝ⦄, 0 < c → IsBigOWith c l f' g
-- Mathlib/RingTheory/Ideal/Operations.lean
theorem mul_sup_eq_of_coprime_right (h : K ⊔ J = ⊤) : I * K ⊔ J = I ⊔ J

Proof state:
R : Type u
inst✝ : CommSemiring R
I J K : Ideal R
h : K ⊔ J = ⊤
⊢ I * K ⊔ J = I ⊔ J

Tactic:
rw [sup_comm] at h

Result:
R : Type u
inst✝ : CommSemiring R
I J K : Ideal R
h : J ⊔ K = ⊤
⊢ I * K ⊔ J = I ⊔ J

Proof state:
R : Type u
inst✝ : CommSemiring R
I J K : Ideal R
h : J ⊔ K = ⊤
⊢ I * K ⊔ J = I ⊔ J

Tactic:
rw [sup_comm, sup_mul_eq_of_coprime_right h, sup_comm]

Result:
no goals
-- Mathlib/MeasureTheory/Function/LpSeminorm/Basic.lean
theorem eLpNorm_eq_lintegral_rpow_enorm (hp_ne_zero : p ≠ 0) (hp_ne_top : p ≠ ∞) {f : α → ε} :
    eLpNorm f p μ = (∫⁻ x, ‖f x‖ₑ ^ p.toReal ∂μ) ^ (1 / p.toReal)

Proof state:
α : Type u_1
ε : Type u_2
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : ENorm ε
hp_ne_zero : p ≠ 0
hp_ne_top : p ≠ ⊤
f : α → ε
⊢ eLpNorm f p μ = (∫⁻ (x : α), ‖f x‖ₑ ^ p.toReal ∂μ) ^ (1 / p.toReal)

Tactic:
rw [eLpNorm_eq_eLpNorm' hp_ne_zero hp_ne_top, eLpNorm'_eq_lintegral_enorm]

Result:
no goals
-- Mathlib/CategoryTheory/Triangulated/Opposite/Basic.lean
lemma shiftFunctorZero_op_hom_app (X : Cᵒᵖ) :
    (shiftFunctorZero Cᵒᵖ ℤ).hom.app X = (shiftFunctorOpIso C 0 0 (zero_add 0)).hom.app X ≫
      ((shiftFunctorZero C ℤ).inv.app X.unop).op

Proof state:
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : HasShift C ℤ
X : Cᵒᵖ
⊢ (shiftFunctorZero Cᵒᵖ ℤ).hom.app X =
    (shiftFunctorOpIso C 0 0 ⋯).hom.app X ≫ ((shiftFunctorZero C ℤ).inv.app (Opposite.unop X)).op

Tactic:
erw [@pullbackShiftFunctorZero_hom_app (OppositeShift C ℤ), oppositeShiftFunctorZero_hom_app]

Result:
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : HasShift C ℤ
X : Cᵒᵖ
⊢ (pullbackShiftIso (OppositeShift C ℤ)
              (AddMonoidHom.mk' (fun n => -n) CategoryTheory.Pretriangulated.Opposite.OppositeShiftAux.proof_1) 0 0
              ⋯).hom.app
        X ≫
      ((shiftFunctorZero C ℤ).inv.app (Opposite.unop X)).op =
    (shiftFunctorOpIso C 0 0 ⋯).hom.app X ≫ ((shiftFunctorZero C ℤ).inv.app (Opposite.unop X)).op

Proof state:
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : HasShift C ℤ
X : Cᵒᵖ
⊢ (pullbackShiftIso (OppositeShift C ℤ)
              (AddMonoidHom.mk' (fun n => -n) CategoryTheory.Pretriangulated.Opposite.OppositeShiftAux.proof_1) 0 0
              ⋯).hom.app
        X ≫
      ((shiftFunctorZero C ℤ).inv.app (Opposite.unop X)).op =
    (shiftFunctorOpIso C 0 0 ⋯).hom.app X ≫ ((shiftFunctorZero C ℤ).inv.app (Opposite.unop X)).op

Tactic:
rfl

Result:
no goals
-- Mathlib/Algebra/Ring/Parity.lean
lemma iterate_eq_id (hf : Involutive f) (hne : f ≠ id) : f^[n] = id ↔ Even n :=
  ⟨fun H ↦ not_odd_iff_even.1 fun hn ↦ hne <| by rwa [hf.iterate_odd hn] at H, hf.iterate_even⟩

Proof state:
α : Type u_4
f : α → α
n : ℕ
hf : Involutive f
hne : f ≠ id
H : f^[n] = id
hn : Odd n
⊢ f = id

Tactic:
rwa [hf.iterate_odd hn] at H

Result:
no goals
-- Mathlib/SetTheory/Cardinal/Basic.lean
theorem power_le_max_power_one {a b c : Cardinal} (h : b ≤ c) : a ^ b ≤ max (a ^ c) 1

Proof state:
case neg
a b c : Cardinal.{u_1}
h : b ≤ c
ha : ¬a = 0
⊢ a ^ b ≤ a ^ c ⊔ 1

Tactic:
exact (power_le_power_left ha h).trans (le_max_left _ _)

Result:
no goals

Proof state:
a b c : Cardinal.{u_1}
h : b ≤ c
⊢ a ^ b ≤ a ^ c ⊔ 1

Tactic:
by_cases ha : a = 0

Result:
case pos
a b c : Cardinal.{u_1}
h : b ≤ c
ha : a = 0
⊢ a ^ b ≤ a ^ c ⊔ 1

case neg
a b c : Cardinal.{u_1}
h : b ≤ c
ha : ¬a = 0
⊢ a ^ b ≤ a ^ c ⊔ 1

Proof state:
case pos
a b c : Cardinal.{u_1}
h : b ≤ c
ha : a = 0
⊢ a ^ b ≤ a ^ c ⊔ 1

Tactic:
simp [ha, zero_power_le]

Result:
no goals
-- Mathlib/CategoryTheory/Category/Preorder.lean
lemma homOfLE_isIso_of_eq {x y : X} (h : x ≤ y) (heq : x = y) :
    IsIso (homOfLE h) :=
  ⟨homOfLE (le_of_eq heq.symm), by simp⟩

Proof state:
X : Type u
inst✝ : Preorder X
x y : X
h : x ≤ y
heq : x = y
⊢ homOfLE h ≫ homOfLE ⋯ = 𝟙 x ∧ homOfLE ⋯ ≫ homOfLE h = 𝟙 y

Tactic:
simp

Result:
no goals
-- Mathlib/MeasureTheory/Measure/Lebesgue/Basic.lean
theorem volume_emetric_ball (a : ℝ) (r : ℝ≥0∞) : volume (EMetric.ball a r) = 2 * r

Proof state:
a : ℝ
r : ℝ≥0∞
⊢ volume (EMetric.ball a r) = 2 * r

Tactic:
rcases eq_or_ne r ∞ with (rfl | hr)

Result:
case inl
a : ℝ
⊢ volume (EMetric.ball a ⊤) = 2 * ⊤

case inr
a : ℝ
r : ℝ≥0∞
hr : r ≠ ⊤
⊢ volume (EMetric.ball a r) = 2 * r

Proof state:
case inr.intro
a : ℝ
r : ℝ≥0
⊢ volume (EMetric.ball a ↑r) = 2 * ↑r

Tactic:
rw [Metric.emetric_ball_nnreal, volume_ball, two_mul, ← NNReal.coe_add,
  ENNReal.ofReal_coe_nnreal, ENNReal.coe_add, two_mul]

Result:
no goals

Proof state:
case inr
a : ℝ
r : ℝ≥0∞
hr : r ≠ ⊤
⊢ volume (EMetric.ball a r) = 2 * r

Tactic:
lift r to ℝ≥0 using hr

Result:
case inr.intro
a : ℝ
r : ℝ≥0
⊢ volume (EMetric.ball a ↑r) = 2 * ↑r

Proof state:
case inl
a : ℝ
⊢ volume (EMetric.ball a ⊤) = 2 * ⊤

Tactic:
rw [Metric.emetric_ball_top, volume_univ, two_mul, _root_.top_add]

Result:
no goals
-- Mathlib/GroupTheory/Perm/List.lean
theorem formPerm_pow_apply_get (l : List α) (h : Nodup l) (n : ℕ) (i : Fin l.length) :
    (formPerm l ^ n) (l.get i) =
      l.get ⟨((i.val + n) % l.length), (Nat.mod_lt _ (i.val.zero_le.trans_lt i.isLt))⟩

Proof state:
α : Type u_1
inst✝ : DecidableEq α
l : List α
h : l.Nodup
n : ℕ
i : Fin l.length
⊢ (l.formPerm ^ n) (l.get i) = l.get ⟨(↑i + n) % l.length, ⋯⟩

Tactic:
simp [formPerm_pow_apply_getElem, h]

Result:
no goals
-- Mathlib/SetTheory/Game/Nim.lean
theorem grundyValue_le_of_forall_moveRight {G : PGame} [G.Impartial] {o : Nimber}
    (h : ∀ i, grundyValue (G.moveRight i) ≠ o) : G.grundyValue ≤ o

Proof state:
G : PGame
inst✝ : G.Impartial
o : Nimber
h : o < G.grundyValue
⊢ ∃ i, (G.moveRight i).grundyValue = o

Tactic:
exact exists_grundyValue_moveRight_of_lt h

Result:
no goals

Proof state:
G : PGame
inst✝ : G.Impartial
o : Nimber
h : ∀ (i : G.RightMoves), (G.moveRight i).grundyValue ≠ o
⊢ G.grundyValue ≤ o

Tactic:
contrapose! h

Result:
G : PGame
inst✝ : G.Impartial
o : Nimber
h : o < G.grundyValue
⊢ ∃ i, (G.moveRight i).grundyValue = o
-- Mathlib/FieldTheory/PurelyInseparable/Basic.lean
theorem isPurelyInseparable_iff_natSepDegree_eq_one :
    IsPurelyInseparable F E ↔ ∀ x : E, (minpoly F x).natSepDegree = 1

Proof state:
case intro
F : Type u
E : Type v
inst✝² : Field F
inst✝¹ : Field E
inst✝ : Algebra F E
q : ℕ
h✝ : ExpChar F q
⊢ IsPurelyInseparable F E ↔ ∀ (x : E), (minpoly F x).natSepDegree = 1

Tactic:
simp_rw [isPurelyInseparable_iff_pow_mem F q, minpoly.natSepDegree_eq_one_iff_pow_mem q]

Result:
no goals

Proof state:
F : Type u
E : Type v
inst✝² : Field F
inst✝¹ : Field E
inst✝ : Algebra F E
⊢ IsPurelyInseparable F E ↔ ∀ (x : E), (minpoly F x).natSepDegree = 1

Tactic:
obtain ⟨q, _⟩ := ExpChar.exists F

Result:
case intro
F : Type u
E : Type v
inst✝² : Field F
inst✝¹ : Field E
inst✝ : Algebra F E
q : ℕ
h✝ : ExpChar F q
⊢ IsPurelyInseparable F E ↔ ∀ (x : E), (minpoly F x).natSepDegree = 1
-- Mathlib/Order/Filter/Lift.lean
theorem lift_iInf_of_map_univ {f : ι → Filter α} {g : Set α → Filter β}
    (hg : ∀ s t, g (s ∩ t) = g s ⊓ g t) (hg' : g univ = ⊤) :
    (iInf f).lift g = ⨅ i, (f i).lift g

Proof state:
α : Type u_1
β : Type u_2
ι : Sort u_4
f : ι → Filter α
g : Set α → Filter β
hg : ∀ (s t : Set α), g (s ∩ t) = g s ⊓ g t
hg' : g univ = ⊤
⊢ (iInf f).lift g = ⨅ i, (f i).lift g

Tactic:
cases isEmpty_or_nonempty ι

Result:
case inl
α : Type u_1
β : Type u_2
ι : Sort u_4
f : ι → Filter α
g : Set α → Filter β
hg : ∀ (s t : Set α), g (s ∩ t) = g s ⊓ g t
hg' : g univ = ⊤
h✝ : IsEmpty ι
⊢ (iInf f).lift g = ⨅ i, (f i).lift g

case inr
α : Type u_1
β : Type u_2
ι : Sort u_4
f : ι → Filter α
g : Set α → Filter β
hg : ∀ (s t : Set α), g (s ∩ t) = g s ⊓ g t
hg' : g univ = ⊤
h✝ : Nonempty ι
⊢ (iInf f).lift g = ⨅ i, (f i).lift g

Proof state:
case inl
α : Type u_1
β : Type u_2
ι : Sort u_4
f : ι → Filter α
g : Set α → Filter β
hg : ∀ (s t : Set α), g (s ∩ t) = g s ⊓ g t
hg' : g univ = ⊤
h✝ : IsEmpty ι
⊢ (iInf f).lift g = ⨅ i, (f i).lift g

Tactic:
simp [iInf_of_empty, hg']

Result:
no goals

Proof state:
case inr
α : Type u_1
β : Type u_2
ι : Sort u_4
f : ι → Filter α
g : Set α → Filter β
hg : ∀ (s t : Set α), g (s ∩ t) = g s ⊓ g t
hg' : g univ = ⊤
h✝ : Nonempty ι
⊢ (iInf f).lift g = ⨅ i, (f i).lift g

Tactic:
exact lift_iInf hg

Result:
no goals
-- Mathlib/Data/Nat/Bits.lean
lemma bodd_add_div2 : ∀ n, (bodd n).toNat + 2 * div2 n = n
  | 0 => rfl
  | succ n => by
    simp only [bodd_succ, Bool.cond_not, div2_succ, Nat.mul_comm]
    refine Eq.trans ?_ (congr_arg succ (bodd_add_div2 n))
    cases bodd n
    · simp
    · simp; omega

Proof state:
case false
n : ℕ
⊢ (!false).toNat + (bif false then n.div2.succ else n.div2) * 2 = (false.toNat + 2 * n.div2).succ

Tactic:
simp

Result:
no goals

Proof state:
n : ℕ
⊢ (!n.bodd).toNat + (bif n.bodd then n.div2.succ else n.div2) * 2 = n.succ

Tactic:
refine Eq.trans ?_ (congr_arg succ (bodd_add_div2 n))

Result:
n : ℕ
⊢ (!n.bodd).toNat + (bif n.bodd then n.div2.succ else n.div2) * 2 = (n.bodd.toNat + 2 * n.div2).succ

Proof state:
case true
n : ℕ
⊢ (!true).toNat + (bif true then n.div2.succ else n.div2) * 2 = (true.toNat + 2 * n.div2).succ

Tactic:
simp

Result:
case true
n : ℕ
⊢ (n.div2 + 1) * 2 = 1 + (1 + n.div2 * 2)

Proof state:
case true
n : ℕ
⊢ (n.div2 + 1) * 2 = 1 + (1 + n.div2 * 2)

Tactic:
omega

Result:
no goals

Proof state:
n : ℕ
⊢ n.succ.bodd.toNat + 2 * n.succ.div2 = n.succ

Tactic:
simp only [bodd_succ, Bool.cond_not, div2_succ, Nat.mul_comm]

Result:
n : ℕ
⊢ (!n.bodd).toNat + (bif n.bodd then n.div2.succ else n.div2) * 2 = n.succ

Proof state:
n : ℕ
⊢ (!n.bodd).toNat + (bif n.bodd then n.div2.succ else n.div2) * 2 = (n.bodd.toNat + 2 * n.div2).succ

Tactic:
cases bodd n

Result:
case false
n : ℕ
⊢ (!false).toNat + (bif false then n.div2.succ else n.div2) * 2 = (false.toNat + 2 * n.div2).succ

case true
n : ℕ
⊢ (!true).toNat + (bif true then n.div2.succ else n.div2) * 2 = (true.toNat + 2 * n.div2).succ
-- Mathlib/CategoryTheory/Limits/Shapes/StrongEpi.lean
theorem StrongMono.of_arrow_iso {A B A' B' : C} {f : A ⟶ B} {g : A' ⟶ B'}
    (e : Arrow.mk f ≅ Arrow.mk g) [h : StrongMono f] : StrongMono g :=
  { mono

Proof state:
C : Type u
inst✝ : Category.{v, u} C
A B A' B' : C
f : A ⟶ B
g : A' ⟶ B'
e : Arrow.mk f ≅ Arrow.mk g
h : StrongMono f
X Y : C
z : X ⟶ Y
⊢ ∀ [inst : Epi z], HasLiftingProperty z g

Tactic:
intro

Result:
C : Type u
inst✝¹ : Category.{v, u} C
A B A' B' : C
f : A ⟶ B
g : A' ⟶ B'
e : Arrow.mk f ≅ Arrow.mk g
h : StrongMono f
X Y : C
z : X ⟶ Y
inst✝ : Epi z
⊢ HasLiftingProperty z g

Proof state:
C : Type u
inst✝ : Category.{v, u} C
A B A' B' : C
f : A ⟶ B
g : A' ⟶ B'
e : Arrow.mk f ≅ Arrow.mk g
h : StrongMono f
⊢ Mono (e.inv.left ≫ f ≫ e.hom.right)

Tactic:
infer_instance

Result:
no goals

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
A B A' B' : C
f : A ⟶ B
g : A' ⟶ B'
e : Arrow.mk f ≅ Arrow.mk g
h : StrongMono f
X Y : C
z : X ⟶ Y
inst✝ : Epi z
⊢ HasLiftingProperty z g

Tactic:
apply HasLiftingProperty.of_arrow_iso_right z e

Result:
no goals

Proof state:
C : Type u
inst✝ : Category.{v, u} C
A B A' B' : C
f : A ⟶ B
g : A' ⟶ B'
e : Arrow.mk f ≅ Arrow.mk g
h : StrongMono f
⊢ Mono g

Tactic:
rw [Arrow.iso_w' e]

Result:
C : Type u
inst✝ : Category.{v, u} C
A B A' B' : C
f : A ⟶ B
g : A' ⟶ B'
e : Arrow.mk f ≅ Arrow.mk g
h : StrongMono f
⊢ Mono (e.inv.left ≫ f ≫ e.hom.right)
-- Mathlib/NumberTheory/LegendreSymbol/JacobiSymbol.lean
theorem nonsquare_iff_jacobiSym_eq_neg_one {a : ℤ} {p : ℕ} [Fact p.Prime] :
    J(a | p) = -1 ↔ ¬IsSquare (a : ZMod p)

Proof state:
a : ℤ
p : ℕ
inst✝ : Fact (Nat.Prime p)
⊢ J(a | p) = -1 ↔ ¬IsSquare ↑a

Tactic:
rw [← legendreSym.to_jacobiSym]

Result:
a : ℤ
p : ℕ
inst✝ : Fact (Nat.Prime p)
⊢ legendreSym p a = -1 ↔ ¬IsSquare ↑a

Proof state:
a : ℤ
p : ℕ
inst✝ : Fact (Nat.Prime p)
⊢ legendreSym p a = -1 ↔ ¬IsSquare ↑a

Tactic:
exact legendreSym.eq_neg_one_iff p

Result:
no goals
-- Mathlib/Analysis/Asymptotics/AsymptoticEquivalent.lean
theorem IsEquivalent.add_isLittleO (huv : u ~[l] v) (hwv : w =o[l] v) : u + w ~[l] v

Proof state:
α : Type u_1
β : Type u_2
inst✝ : NormedAddCommGroup β
u v w : α → β
l : Filter α
huv : u ~[l] v
hwv : w =o[l] v
⊢ u + w ~[l] v

Tactic:
simpa only [IsEquivalent, add_sub_right_comm] using huv.add hwv

Result:
no goals
-- Mathlib/Algebra/Homology/HomologySequence.lean
@[reassoc]
lemma pOpcycles_opcyclesToCycles_iCycles :
    K.pOpcycles i ≫ K.opcyclesToCycles i j ≫ K.iCycles j = K.d i j

Proof state:
C : Type u_1
ι : Type u_2
inst✝³ : Category.{u_3, u_1} C
inst✝² : HasZeroMorphisms C
c : ComplexShape ι
K : HomologicalComplex C c
i j : ι
inst✝¹ : K.HasHomology i
inst✝ : K.HasHomology j
⊢ K.pOpcycles i ≫ K.opcyclesToCycles i j ≫ K.iCycles j = K.d i j

Tactic:
simp [opcyclesToCycles]

Result:
no goals
-- Mathlib/GroupTheory/GroupAction/Basic.lean
theorem mem_fixedPoints_iff_card_orbit_eq_one {a : α} [Fintype (orbit M a)] :
    a ∈ fixedPoints M α ↔ Fintype.card (orbit M a) = 1

Proof state:
M : Type u
inst✝² : Monoid M
α : Type v
inst✝¹ : MulAction M α
a : α
inst✝ : Fintype ↑(orbit M a)
⊢ a ∈ fixedPoints M α ↔ Fintype.card ↑(orbit M a) = 1

Tactic:
simp only [← subsingleton_orbit_iff_mem_fixedPoints, le_antisymm_iff,
  Fintype.card_le_one_iff_subsingleton, Nat.add_one_le_iff, Fintype.card_pos_iff,
  Set.subsingleton_coe, iff_self_and, Set.nonempty_coe_sort, orbit_nonempty, implies_true]

Result:
no goals
-- Mathlib/Data/Fin/Basic.lean
theorem castSucc_pred_add_one_eq {a : Fin (n + 1)} (ha : a ≠ 0) :
    (a.pred ha).castSucc + 1 = a

Proof state:
n : ℕ
a : Fin (n + 1)
ha : a ≠ 0
⊢ (a.pred ha).castSucc + 1 = a

Tactic:
cases a using cases

Result:
case zero
n : ℕ
ha : 0 ≠ 0
⊢ (pred 0 ha).castSucc + 1 = 0

case succ
n : ℕ
i✝ : Fin n
ha : i✝.succ ≠ 0
⊢ (i✝.succ.pred ha).castSucc + 1 = i✝.succ

Proof state:
case succ
n : ℕ
i✝ : Fin n
ha : i✝.succ ≠ 0
⊢ (i✝.succ.pred ha).castSucc + 1 = i✝.succ

Tactic:
rw [pred_succ, coeSucc_eq_succ]

Result:
no goals

Proof state:
case zero
n : ℕ
ha : 0 ≠ 0
⊢ (pred 0 ha).castSucc + 1 = 0

Tactic:
exact (ha rfl).elim

Result:
no goals