harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Topology/Category/Profinite/Nobeling.lean
theorem e_mem_of_eq_true {x : (π C (· ∈ s))} {a : I} (hx : x.val a = true) :
    e (π C (· ∈ s)) a ∈ factors C s x

Proof state:
case mk.intro.intro
I : Type u
C : Set (I → Bool)
inst✝ : LinearOrder I
s : Finset I
a : I
z : I → Bool
hz : z ∈ C
hx : ↑⟨Proj (fun x => x ∈ s) z, ⋯⟩ a = true
⊢ a ∈ s

Tactic:
aesop (add simp Proj)

Result:
no goals

Proof state:
case mk.intro.intro
I : Type u
C : Set (I → Bool)
inst✝ : LinearOrder I
s : Finset I
a : I
z : I → Bool
hz : z ∈ C
hx : ↑⟨Proj (fun x => x ∈ s) z, ⋯⟩ a = true
⊢ ∃ a_1 ∈ s,
    (if Proj (fun x => x ∈ s) z a_1 = true then e (π C fun x => x ∈ s) a_1 else 1 - e (π C fun x => x ∈ s) a_1) =
      e (π C fun x => x ∈ s) a

Tactic:
refine ⟨a, ?_, if_pos hx⟩

Result:
case mk.intro.intro
I : Type u
C : Set (I → Bool)
inst✝ : LinearOrder I
s : Finset I
a : I
z : I → Bool
hz : z ∈ C
hx : ↑⟨Proj (fun x => x ∈ s) z, ⋯⟩ a = true
⊢ a ∈ s

Proof state:
I : Type u
C : Set (I → Bool)
inst✝ : LinearOrder I
s : Finset I
x : ↑(π C fun x => x ∈ s)
a : I
hx : ↑x a = true
⊢ e (π C fun x => x ∈ s) a ∈ factors C s x

Tactic:
rcases x with ⟨_, z, hz, rfl⟩

Result:
case mk.intro.intro
I : Type u
C : Set (I → Bool)
inst✝ : LinearOrder I
s : Finset I
a : I
z : I → Bool
hz : z ∈ C
hx : ↑⟨Proj (fun x => x ∈ s) z, ⋯⟩ a = true
⊢ e (π C fun x => x ∈ s) a ∈ factors C s ⟨Proj (fun x => x ∈ s) z, ⋯⟩

Proof state:
case mk.intro.intro
I : Type u
C : Set (I → Bool)
inst✝ : LinearOrder I
s : Finset I
a : I
z : I → Bool
hz : z ∈ C
hx : ↑⟨Proj (fun x => x ∈ s) z, ⋯⟩ a = true
⊢ e (π C fun x => x ∈ s) a ∈ factors C s ⟨Proj (fun x => x ∈ s) z, ⋯⟩

Tactic:
simp only [factors, List.mem_map, Finset.mem_sort]

Result:
case mk.intro.intro
I : Type u
C : Set (I → Bool)
inst✝ : LinearOrder I
s : Finset I
a : I
z : I → Bool
hz : z ∈ C
hx : ↑⟨Proj (fun x => x ∈ s) z, ⋯⟩ a = true
⊢ ∃ a_1 ∈ s,
    (if Proj (fun x => x ∈ s) z a_1 = true then e (π C fun x => x ∈ s) a_1 else 1 - e (π C fun x => x ∈ s) a_1) =
      e (π C fun x => x ∈ s) a
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Int/Order.lean
theorem min_eq_left {a b : Int} (h : a ≤ b) : min a b = a

Proof state:
a b : Int
h : a ≤ b
⊢ min a b = a

Tactic:
simp [Int.min_def, h]

Result:
no goals
-- Mathlib/CategoryTheory/Limits/Shapes/End.lean
@[reassoc (attr := simp)]
lemma lift_ι (hc : IsLimit c) {X : C} (f : ∀ j, X ⟶ (F.obj (op j)).obj j)
    (hf : ∀ ⦃i j : J⦄ (g : i ⟶ j), f i ≫ (F.obj (op i)).map g = f j ≫ (F.map g.op).app j) (j : J) :
    lift hc f hf ≫ c.ι j = f j

Proof state:
J : Type u
inst✝¹ : Category.{v, u} J
C : Type u'
inst✝ : Category.{v', u'} C
F : Jᵒᵖ ⥤ J ⥤ C
c : Wedge F
hc : IsLimit c
X : C
f : (j : J) → X ⟶ (F.obj (op j)).obj j
hf : ∀ ⦃i j : J⦄ (g : i ⟶ j), f i ≫ (F.obj (op i)).map g = f j ≫ (F.map g.op).app j
j : J
⊢ lift hc f hf ≫ Multifork.ι c j = f j

Tactic:
apply IsLimit.fac

Result:
no goals
-- Mathlib/Geometry/Manifold/IsManifold/ExtChartAt.lean
theorem map_extend_symm_nhdsWithin_range {y : M} (hy : y ∈ f.source) :
    map (f.extend I).symm (𝓝[range I] f.extend I y) = 𝓝 y

Proof state:
𝕜 : Type u_1
E : Type u_2
M : Type u_3
H : Type u_4
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : TopologicalSpace H
inst✝ : TopologicalSpace M
f : PartialHomeomorph M H
I : ModelWithCorners 𝕜 E H
y : M
hy : y ∈ f.source
⊢ map (↑(f.extend I).symm) (𝓝[range ↑I] ↑(f.extend I) y) = 𝓝 y

Tactic:
rw [← nhdsWithin_univ, ← map_extend_symm_nhdsWithin f (I := I) hy, preimage_univ, univ_inter]

Result:
no goals
-- Mathlib/Algebra/Polynomial/Splits.lean
theorem degree_eq_one_of_irreducible_of_splits {p : K[X]} (hp : Irreducible p)
    (hp_splits : Splits (RingHom.id K) p) : p.degree = 1

Proof state:
K : Type v
inst✝ : Field K
p : K[X]
hp : Irreducible p
hp_splits : Splits (RingHom.id K) p
⊢ p.degree = 1

Tactic:
rcases hp_splits with ⟨⟩ | hp_splits

Result:
case inl
K : Type v
inst✝ : Field K
p : K[X]
hp : Irreducible p
h✝ : map (RingHom.id K) p = 0
⊢ p.degree = 1

case inr
K : Type v
inst✝ : Field K
p : K[X]
hp : Irreducible p
hp_splits : ∀ {g : K[X]}, Irreducible g → g ∣ map (RingHom.id K) p → g.degree = 1
⊢ p.degree = 1

Proof state:
case inl
K : Type v
inst✝ : Field K
p : K[X]
hp : Irreducible p
h✝ : map (RingHom.id K) p = 0
⊢ False

Tactic:
simp_all

Result:
no goals

Proof state:
case inr
K : Type v
inst✝ : Field K
p : K[X]
hp : Irreducible p
hp_splits : ∀ {g : K[X]}, Irreducible g → g ∣ map (RingHom.id K) p → g.degree = 1
⊢ p.degree = 1

Tactic:
apply hp_splits hp

Result:
case inr
K : Type v
inst✝ : Field K
p : K[X]
hp : Irreducible p
hp_splits : ∀ {g : K[X]}, Irreducible g → g ∣ map (RingHom.id K) p → g.degree = 1
⊢ p ∣ map (RingHom.id K) p

Proof state:
case inr
K : Type v
inst✝ : Field K
p : K[X]
hp : Irreducible p
hp_splits : ∀ {g : K[X]}, Irreducible g → g ∣ map (RingHom.id K) p → g.degree = 1
⊢ p ∣ map (RingHom.id K) p

Tactic:
simp

Result:
no goals

Proof state:
case inl
K : Type v
inst✝ : Field K
p : K[X]
hp : Irreducible p
h✝ : map (RingHom.id K) p = 0
⊢ p.degree = 1

Tactic:
exfalso

Result:
case inl
K : Type v
inst✝ : Field K
p : K[X]
hp : Irreducible p
h✝ : map (RingHom.id K) p = 0
⊢ False
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/MapIdx.lean
theorem mapIdx_eq_singleton_iff {l : Array α} {f : Nat → α → β} {b : β} :
    mapIdx f l = #[b] ↔ ∃ (a : α), l = #[a] ∧ f 0 a = b

Proof state:
α : Type u_1
β : Type u_2
l : Array α
f : Nat → α → β
b : β
⊢ mapIdx f l = #[b] ↔ ∃ a, l = #[a] ∧ f 0 a = b

Tactic:
rcases l with ⟨l⟩

Result:
case mk
α : Type u_1
β : Type u_2
f : Nat → α → β
b : β
l : List α
⊢ mapIdx f { toList := l } = #[b] ↔ ∃ a, { toList := l } = #[a] ∧ f 0 a = b

Proof state:
case mk
α : Type u_1
β : Type u_2
f : Nat → α → β
b : β
l : List α
⊢ mapIdx f { toList := l } = #[b] ↔ ∃ a, { toList := l } = #[a] ∧ f 0 a = b

Tactic:
simp [List.mapIdx_eq_singleton_iff]

Result:
no goals
-- Mathlib/Logic/Function/Iterate.lean
theorem iterate_pred_comp_of_pos {n : ℕ} (hn : 0 < n) : f^[n.pred] ∘ f = f^[n]

Proof state:
α : Type u
f : α → α
n : ℕ
hn : 0 < n
⊢ f^[n.pred] ∘ f = f^[n]

Tactic:
rw [← iterate_succ, Nat.succ_pred_eq_of_pos hn]

Result:
no goals
-- Mathlib/Topology/UniformSpace/UniformConvergenceTopology.lean
theorem uniformity_eq_of_basis {ι : Sort*} {p : ι → Prop} {V : ι → Set (β × β)}
    (h : (𝓤 β).HasBasis p V) :
    𝓤 (α →ᵤ[𝔖] β) = ⨅ s ∈ 𝔖, ⨅ (i) (_ : p i), 𝓟 (UniformOnFun.gen 𝔖 s (V i))

Proof state:
α : Type u_1
β : Type u_2
inst✝ : UniformSpace β
𝔖 : Set (Set α)
ι : Sort u_5
p : ι → Prop
V : ι → Set (β × β)
h : (𝓤 β).HasBasis p V
⊢ 𝓤 (α →ᵤ[𝔖] β) = ⨅ s ∈ 𝔖, ⨅ i, ⨅ (_ : p i), 𝓟 (UniformOnFun.gen 𝔖 s (V i))

Tactic:
simp_rw [iInf_uniformity, uniformity_comap,
  (UniformFun.hasBasis_uniformity_of_basis _ _ h).eq_biInf, comap_iInf, comap_principal,
  Function.comp_apply, UniformFun.gen, Subtype.forall, UniformOnFun.gen, preimage_setOf_eq,
  Prod.map_fst, Prod.map_snd, Function.comp_apply, UniformFun.toFun_ofFun, restrict_apply]

Result:
no goals
-- Mathlib/Topology/Instances/NNReal/Lemmas.lean
theorem hasSum_nat_add_iff {f : ℕ → ℝ≥0} (k : ℕ) {a : ℝ≥0} :
    HasSum (fun n => f (n + k)) a ↔ HasSum f (a + ∑ i ∈ range k, f i)

Proof state:
f : ℕ → ℝ≥0
k : ℕ
a : ℝ≥0
⊢ HasSum (fun n => f (n + k)) a ↔ HasSum f (a + ∑ i ∈ Finset.range k, f i)

Tactic:
rw [← hasSum_coe, hasSum_nat_add_iff (f := fun n => toReal (f n)) k]

Result:
f : ℕ → ℝ≥0
k : ℕ
a : ℝ≥0
⊢ HasSum (fun n => ↑(f n)) (↑a + ∑ i ∈ Finset.range k, ↑(f i)) ↔ HasSum f (a + ∑ i ∈ Finset.range k, f i)

Proof state:
f : ℕ → ℝ≥0
k : ℕ
a : ℝ≥0
⊢ HasSum (fun n => ↑(f n)) (↑a + ∑ i ∈ Finset.range k, ↑(f i)) ↔ HasSum f (a + ∑ i ∈ Finset.range k, f i)

Tactic:
norm_cast

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Lemmas.lean
theorem any_beq [BEq α] {l : List α} {a : α} : (l.any fun x => a == x) = l.contains a

Proof state:
α : Type u_1
inst✝ : BEq α
l : List α
a : α
⊢ (l.any fun x => a == x) = l.contains a

Tactic:
induction l <;> simp_all [contains_cons]

Result:
no goals
-- Mathlib/CategoryTheory/Sites/LocallyBijective.lean
lemma W_of_isLocallyBijective [Presheaf.IsLocallyInjective J f]
    [Presheaf.IsLocallySurjective J f] : J.W f

Proof state:
C : Type u
inst✝⁶ : Category.{v, u} C
J : GrothendieckTopology C
A : Type u'
inst✝⁵ : Category.{v', u'} A
FA : A → A → Type u_1
CA : A → Type w'
inst✝⁴ : (X Y : A) → FunLike (FA X Y) (CA X) (CA Y)
inst✝³ : ConcreteCategory A FA
inst✝² : J.WEqualsLocallyBijective A
X Y : Cᵒᵖ ⥤ A
f : X ⟶ Y
inst✝¹ : Presheaf.IsLocallyInjective J f
inst✝ : Presheaf.IsLocallySurjective J f
⊢ J.W f

Tactic:
rw [W_iff_isLocallyBijective]

Result:
C : Type u
inst✝⁶ : Category.{v, u} C
J : GrothendieckTopology C
A : Type u'
inst✝⁵ : Category.{v', u'} A
FA : A → A → Type u_1
CA : A → Type w'
inst✝⁴ : (X Y : A) → FunLike (FA X Y) (CA X) (CA Y)
inst✝³ : ConcreteCategory A FA
inst✝² : J.WEqualsLocallyBijective A
X Y : Cᵒᵖ ⥤ A
f : X ⟶ Y
inst✝¹ : Presheaf.IsLocallyInjective J f
inst✝ : Presheaf.IsLocallySurjective J f
⊢ Presheaf.IsLocallyInjective J f ∧ Presheaf.IsLocallySurjective J f

Proof state:
C : Type u
inst✝⁶ : Category.{v, u} C
J : GrothendieckTopology C
A : Type u'
inst✝⁵ : Category.{v', u'} A
FA : A → A → Type u_1
CA : A → Type w'
inst✝⁴ : (X Y : A) → FunLike (FA X Y) (CA X) (CA Y)
inst✝³ : ConcreteCategory A FA
inst✝² : J.WEqualsLocallyBijective A
X Y : Cᵒᵖ ⥤ A
f : X ⟶ Y
inst✝¹ : Presheaf.IsLocallyInjective J f
inst✝ : Presheaf.IsLocallySurjective J f
⊢ Presheaf.IsLocallyInjective J f ∧ Presheaf.IsLocallySurjective J f

Tactic:
constructor <;> infer_instance

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Pow/Real.lean
theorem rpow_sub' {x : ℝ} (hx : 0 ≤ x) {y z : ℝ} (h : y - z ≠ 0) : x ^ (y - z) = x ^ y / x ^ z

Proof state:
x : ℝ
hx : 0 ≤ x
y z : ℝ
h : y - z ≠ 0
⊢ x ^ (y - z) = x ^ y / x ^ z

Tactic:
simp only [sub_eq_add_neg] at h ⊢

Result:
x : ℝ
hx : 0 ≤ x
y z : ℝ
h : y + -z ≠ 0
⊢ x ^ (y + -z) = x ^ y / x ^ z

Proof state:
x : ℝ
hx : 0 ≤ x
y z : ℝ
h : y + -z ≠ 0
⊢ x ^ (y + -z) = x ^ y / x ^ z

Tactic:
simp only [rpow_add' hx h, rpow_neg hx, div_eq_mul_inv]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Lemmas.lean
theorem reverse_eq_concat {xs ys : List α} {a : α} :
    xs.reverse = ys ++ [a] ↔ xs = a :: ys.reverse

Proof state:
α : Type u_1
xs ys : List α
a : α
⊢ xs.reverse = ys ++ [a] ↔ xs = a :: ys.reverse

Tactic:
rw [reverse_eq_iff, reverse_concat]

Result:
no goals
-- Mathlib/Algebra/Star/Conjneg.lean
@[simp] lemma conjneg_neg (f : G → R) : conjneg (-f) = -conjneg f

Proof state:
case h
G : Type u_2
R : Type u_3
inst✝² : AddGroup G
inst✝¹ : CommRing R
inst✝ : StarRing R
f : G → R
x✝ : G
⊢ conjneg (-f) x✝ = (-conjneg f) x✝

Tactic:
simp

Result:
no goals

Proof state:
G : Type u_2
R : Type u_3
inst✝² : AddGroup G
inst✝¹ : CommRing R
inst✝ : StarRing R
f : G → R
⊢ conjneg (-f) = -conjneg f

Tactic:
ext

Result:
case h
G : Type u_2
R : Type u_3
inst✝² : AddGroup G
inst✝¹ : CommRing R
inst✝ : StarRing R
f : G → R
x✝ : G
⊢ conjneg (-f) x✝ = (-conjneg f) x✝
-- Mathlib/Analysis/SpecialFunctions/Pow/Real.lean
theorem rpow_one (x : ℝ) : x ^ (1 : ℝ) = x

Proof state:
x : ℝ
⊢ x ^ 1 = x

Tactic:
simp [rpow_def]

Result:
no goals
-- Mathlib/Order/Filter/Basic.lean
theorem frequently_true_iff_neBot (f : Filter α) : (∃ᶠ _ in f, True) ↔ NeBot f

Proof state:
α : Type u
f : Filter α
⊢ (∃ᶠ (x : α) in f, True) ↔ f.NeBot

Tactic:
simp [frequently_iff_neBot]

Result:
no goals
-- Mathlib/Analysis/InnerProductSpace/Calculus.lean
theorem DifferentiableAt.dist (hf : DifferentiableAt ℝ f x) (hg : DifferentiableAt ℝ g x)
    (hne : f x ≠ g x) : DifferentiableAt ℝ (fun y => dist (f y) (g y)) x

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝⁵ : RCLike 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace 𝕜 E
inst✝² : NormedSpace ℝ E
G : Type u_4
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
f g : G → E
x : G
hf : DifferentiableAt ℝ f x
hg : DifferentiableAt ℝ g x
hne : f x ≠ g x
⊢ DifferentiableAt ℝ (fun y => Dist.dist (f y) (g y)) x

Tactic:
simp only [dist_eq_norm]

Result:
𝕜 : Type u_1
E : Type u_2
inst✝⁵ : RCLike 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace 𝕜 E
inst✝² : NormedSpace ℝ E
G : Type u_4
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
f g : G → E
x : G
hf : DifferentiableAt ℝ f x
hg : DifferentiableAt ℝ g x
hne : f x ≠ g x
⊢ DifferentiableAt ℝ (fun y => ‖f y - g y‖) x

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝⁵ : RCLike 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace 𝕜 E
inst✝² : NormedSpace ℝ E
G : Type u_4
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
f g : G → E
x : G
hf : DifferentiableAt ℝ f x
hg : DifferentiableAt ℝ g x
hne : f x ≠ g x
⊢ DifferentiableAt ℝ (fun y => ‖f y - g y‖) x

Tactic:
exact (hf.sub hg).norm 𝕜 (sub_ne_zero.2 hne)

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem getElem_eq_iff {a : Array α} {i : Nat} {h : i < a.size} : a[i] = x ↔ a[i]? = some x

Proof state:
α : Type u_1
x : α
a : Array α
i : Nat
h : i < a.size
⊢ a[i] = x ↔ a[i]? = some x

Tactic:
simp only [getElem?_eq_some_iff]

Result:
α : Type u_1
x : α
a : Array α
i : Nat
h : i < a.size
⊢ a[i] = x ↔ ∃ h, a[i] = x

Proof state:
α : Type u_1
x : α
a : Array α
i : Nat
h : i < a.size
⊢ a[i] = x ↔ ∃ h, a[i] = x

Tactic:
exact ⟨fun w => ⟨h, w⟩, fun h => h.2⟩

Result:
no goals
-- Mathlib/Data/Ordmap/Ordset.lean
theorem eraseMax.valid {t} (h : @Valid α _ t) : Valid (eraseMax t)

Proof state:
α : Type u_1
inst✝ : Preorder α
t : Ordnode α
h : t.Valid
⊢ t.dual.eraseMin.Valid

Tactic:
exact eraseMin.valid h.dual

Result:
no goals

Proof state:
α : Type u_1
inst✝ : Preorder α
t : Ordnode α
h : t.Valid
⊢ t.eraseMax.Valid

Tactic:
rw [Valid.dual_iff, dual_eraseMax]

Result:
α : Type u_1
inst✝ : Preorder α
t : Ordnode α
h : t.Valid
⊢ t.dual.eraseMin.Valid
-- Mathlib/SetTheory/Cardinal/Finite.lean
theorem card_eq_of_equiv_fin {α : Type*} {n : ℕ} (f : α ≃ Fin n) : Nat.card α = n

Proof state:
α : Type u_3
n : ℕ
f : α ≃ Fin n
⊢ Nat.card α = n

Tactic:
simpa only [card_eq_fintype_card, Fintype.card_fin] using card_congr f

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/RawLemmas.lean
theorem getKeyD_alter_self [LawfulBEq α] [Inhabited α] {k : α} {fallback : α}
    {f : Option (β k) → Option (β k)} (h : m.WF) :
    (m.alter k f).getKeyD k fallback = if (f (m.get? k)).isSome then k else fallback

Proof state:
α : Type u
β : α → Type v
inst✝³ : BEq α
inst✝² : Hashable α
m : Raw α β
inst✝¹ : LawfulBEq α
inst✝ : Inhabited α
k fallback : α
f : Option (β k) → Option (β k)
h : m.WF
⊢ (m.alter k f).getKeyD k fallback = if (f (m.get? k)).isSome = true then k else fallback

Tactic:
simp [getKeyD_alter h]

Result:
no goals
-- Mathlib/Algebra/GroupWithZero/NonZeroDivisors.lean
lemma nmem_nonZeroDivisors_iff : r ∉ M₀⁰ ↔ {s | s * r = 0 ∧ s ≠ 0}.Nonempty

Proof state:
M₀ : Type u_2
inst✝ : MonoidWithZero M₀
r : M₀
⊢ r ∉ M₀⁰ ↔ {s | s * r = 0 ∧ s ≠ 0}.Nonempty

Tactic:
simpa [mem_nonZeroDivisors_iff] using Set.nonempty_def.symm

Result:
no goals
-- Mathlib/Algebra/Ring/Defs.lean
theorem mul_sub_one (a b : α) : a * (b - 1) = a * b - a

Proof state:
α : Type u
inst✝ : NonAssocRing α
a b : α
⊢ a * (b - 1) = a * b - a

Tactic:
rw [mul_sub, mul_one]

Result:
no goals
-- Mathlib/RingTheory/MvPolynomial.lean
theorem finrank_eq_one [IsEmpty σ] : Module.finrank K (MvPolynomial σ K) = 1 :=
  Module.rank_eq_one_iff_finrank_eq_one.mp <| by
    cases subsingleton_or_nontrivial K <;> simp [rank_eq_lift]

Proof state:
σ : Type u
K : Type v
inst✝¹ : CommRing K
inst✝ : IsEmpty σ
⊢ Module.rank K (MvPolynomial σ K) = 1

Tactic:
cases subsingleton_or_nontrivial K <;> simp [rank_eq_lift]

Result:
no goals
-- Mathlib/RingTheory/Binomial.lean
theorem choose_neg [NatPowAssoc R] (r : R) (n : ℕ) :
    choose (-r) n = Int.negOnePow n • choose (r + n - 1) n

Proof state:
R : Type u_1
inst✝³ : NonAssocRing R
inst✝² : Pow R ℕ
inst✝¹ : BinomialRing R
inst✝ : NatPowAssoc R
r : R
n : ℕ
⊢ n.factorial • choose (-r) n = n.factorial • (↑n).negOnePow • choose (r + ↑n - 1) n

Tactic:
rw [← descPochhammer_eq_factorial_smul_choose, smul_comm,
  ← descPochhammer_eq_factorial_smul_choose, descPochhammer_smeval_eq_ascPochhammer,
  show (-r - n + 1) = -(r + n - 1) by abel, ascPochhammer_smeval_neg_eq_descPochhammer]

Result:
no goals

Proof state:
R : Type u_1
inst✝³ : NonAssocRing R
inst✝² : Pow R ℕ
inst✝¹ : BinomialRing R
inst✝ : NatPowAssoc R
r : R
n : ℕ
⊢ choose (-r) n = (↑n).negOnePow • choose (r + ↑n - 1) n

Tactic:
apply (nsmul_right_inj (Nat.factorial_ne_zero n)).mp

Result:
R : Type u_1
inst✝³ : NonAssocRing R
inst✝² : Pow R ℕ
inst✝¹ : BinomialRing R
inst✝ : NatPowAssoc R
r : R
n : ℕ
⊢ n.factorial • choose (-r) n = n.factorial • (↑n).negOnePow • choose (r + ↑n - 1) n

Proof state:
R : Type u_1
inst✝³ : NonAssocRing R
inst✝² : Pow R ℕ
inst✝¹ : BinomialRing R
inst✝ : NatPowAssoc R
r : R
n : ℕ
⊢ -r - ↑n + 1 = -(r + ↑n - 1)

Tactic:
abel

Result:
no goals
-- Mathlib/MeasureTheory/Measure/Prod.lean
theorem prod_apply_symm {s : Set (α × β)} (hs : MeasurableSet s) :
    μ.prod ν s = ∫⁻ y, μ ((fun x => (x, y)) ⁻¹' s) ∂ν

Proof state:
α : Type u_1
β : Type u_2
inst✝³ : MeasurableSpace α
inst✝² : MeasurableSpace β
μ : Measure α
ν : Measure β
inst✝¹ : SFinite ν
inst✝ : SFinite μ
s : Set (α × β)
hs : MeasurableSet s
⊢ (μ.prod ν) s = ∫⁻ (y : β), μ ((fun x => (x, y)) ⁻¹' s) ∂ν

Tactic:
rw [← prod_swap, map_apply measurable_swap hs, prod_apply (measurable_swap hs)]

Result:
α : Type u_1
β : Type u_2
inst✝³ : MeasurableSpace α
inst✝² : MeasurableSpace β
μ : Measure α
ν : Measure β
inst✝¹ : SFinite ν
inst✝ : SFinite μ
s : Set (α × β)
hs : MeasurableSet s
⊢ ∫⁻ (x : β), μ (Prod.mk x ⁻¹' (Prod.swap ⁻¹' s)) ∂ν = ∫⁻ (y : β), μ ((fun x => (x, y)) ⁻¹' s) ∂ν

Proof state:
α : Type u_1
β : Type u_2
inst✝³ : MeasurableSpace α
inst✝² : MeasurableSpace β
μ : Measure α
ν : Measure β
inst✝¹ : SFinite ν
inst✝ : SFinite μ
s : Set (α × β)
hs : MeasurableSet s
⊢ ∫⁻ (x : β), μ (Prod.mk x ⁻¹' (Prod.swap ⁻¹' s)) ∂ν = ∫⁻ (y : β), μ ((fun x => (x, y)) ⁻¹' s) ∂ν

Tactic:
rfl

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Pow/NNReal.lean
theorem list_prod_map_rpow' {ι} (l : List ι) (f : ι → ℝ≥0) (r : ℝ) :
    (l.map (f · ^ r)).prod = (l.map f).prod ^ r

Proof state:
ι : Type u_1
l : List ι
f : ι → ℝ≥0
r : ℝ
⊢ (List.map (fun x => f x ^ r) l).prod = (List.map ((fun x => x ^ r) ∘ f) l).prod

Tactic:
rfl

Result:
no goals

Proof state:
ι : Type u_1
l : List ι
f : ι → ℝ≥0
r : ℝ
⊢ (List.map (fun x => f x ^ r) l).prod = (List.map f l).prod ^ r

Tactic:
rw [← list_prod_map_rpow, List.map_map]

Result:
ι : Type u_1
l : List ι
f : ι → ℝ≥0
r : ℝ
⊢ (List.map (fun x => f x ^ r) l).prod = (List.map ((fun x => x ^ r) ∘ f) l).prod
-- Mathlib/FieldTheory/Separable.lean
theorem nodup_of_separable_prod [Nontrivial R] {s : Multiset R}
    (hs : Separable (Multiset.map (fun a => X - C a) s).prod) : s.Nodup

Proof state:
R : Type u
inst✝¹ : CommRing R
inst✝ : Nontrivial R
a : R
t : Multiset R
hs : (Multiset.map (fun a => X - C a) (a ::ₘ a ::ₘ t)).prod.Separable
⊢ (X - C a) * (X - C a) ∣ (Multiset.map (fun a => X - C a) (a ::ₘ a ::ₘ t)).prod

Tactic:
simpa only [Multiset.map_cons, Multiset.prod_cons] using mul_dvd_mul_left _ (dvd_mul_right _ _)

Result:
no goals

Proof state:
R : Type u
inst✝¹ : CommRing R
inst✝ : Nontrivial R
s : Multiset R
hs : (Multiset.map (fun a => X - C a) s).prod.Separable
⊢ ∀ (a : R) (t : Multiset R), s ≠ a ::ₘ a ::ₘ t

Tactic:
rintro a t rfl

Result:
R : Type u
inst✝¹ : CommRing R
inst✝ : Nontrivial R
a : R
t : Multiset R
hs : (Multiset.map (fun a => X - C a) (a ::ₘ a ::ₘ t)).prod.Separable
⊢ False

Proof state:
R : Type u
inst✝¹ : CommRing R
inst✝ : Nontrivial R
a : R
t : Multiset R
hs : (Multiset.map (fun a => X - C a) (a ::ₘ a ::ₘ t)).prod.Separable
⊢ False

Tactic:
refine not_isUnit_X_sub_C a (isUnit_of_self_mul_dvd_separable hs ?_)

Result:
R : Type u
inst✝¹ : CommRing R
inst✝ : Nontrivial R
a : R
t : Multiset R
hs : (Multiset.map (fun a => X - C a) (a ::ₘ a ::ₘ t)).prod.Separable
⊢ (X - C a) * (X - C a) ∣ (Multiset.map (fun a => X - C a) (a ::ₘ a ::ₘ t)).prod

Proof state:
R : Type u
inst✝¹ : CommRing R
inst✝ : Nontrivial R
s : Multiset R
hs : (Multiset.map (fun a => X - C a) s).prod.Separable
⊢ s.Nodup

Tactic:
rw [Multiset.nodup_iff_ne_cons_cons]

Result:
R : Type u
inst✝¹ : CommRing R
inst✝ : Nontrivial R
s : Multiset R
hs : (Multiset.map (fun a => X - C a) s).prod.Separable
⊢ ∀ (a : R) (t : Multiset R), s ≠ a ::ₘ a ::ₘ t
-- Mathlib/Computability/ContextFreeGrammar.lean
lemma generates_reverse : g.reverse.Generates u.reverse ↔ g.Generates u

Proof state:
T : Type u_1
g : ContextFreeGrammar T
u : List (Symbol T g.NT)
⊢ g.reverse.Generates u.reverse ↔ g.Generates u

Tactic:
simp [Generates]

Result:
no goals
-- Mathlib/Algebra/Order/Group/Unbundled/Basic.lean
theorem inv_mul_le_iff_le_mul : b⁻¹ * a ≤ c ↔ a ≤ b * c

Proof state:
α : Type u
inst✝² : Group α
inst✝¹ : LE α
inst✝ : MulLeftMono α
a b c : α
⊢ b⁻¹ * a ≤ c ↔ a ≤ b * c

Tactic:
rw [← mul_le_mul_iff_left b, mul_inv_cancel_left]

Result:
no goals
-- Mathlib/Data/Rat/Defs.lean
lemma eq_num_of_isInt {q : ℚ} (h : q.isInt) : q = q.num

Proof state:
q : ℚ
h : q.den = 1
⊢ q = ↑q.num

Tactic:
exact (Rat.coe_int_num_of_den_eq_one h).symm

Result:
no goals

Proof state:
q : ℚ
h : q.isInt = true
⊢ q = ↑q.num

Tactic:
rw [Rat.isInt, Nat.beq_eq_true_eq] at h

Result:
q : ℚ
h : q.den = 1
⊢ q = ↑q.num
-- Mathlib/Algebra/CharP/Two.lean
theorem two_eq_zero [CharP R 2] : (2 : R) = 0

Proof state:
R : Type u_1
inst✝¹ : AddMonoidWithOne R
inst✝ : CharP R 2
⊢ 2 = 0

Tactic:
rw [← Nat.cast_two, CharP.cast_eq_zero]

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

Proof state:
α : Type u_1
s : Finset α
⊢ s.toList.isEmpty = true ↔ s = ∅

Tactic:
simp

Result:
no goals
-- Mathlib/ModelTheory/ElementaryMaps.lean
theorem theory_model_iff (f : M ↪ₑ[L] N) (T : L.Theory) : M ⊨ T ↔ N ⊨ T

Proof state:
L : Language
M : Type u_1
N : Type u_2
inst✝¹ : L.Structure M
inst✝ : L.Structure N
f : M ↪ₑ[L] N
T : L.Theory
⊢ M ⊨ T ↔ N ⊨ T

Tactic:
simp only [Theory.model_iff, f.map_sentence]

Result:
no goals
-- Mathlib/Data/Fin/Rev.lean
theorem rev_castPred {i : Fin (n + 1)}
    (h : i ≠ last n) (h' := rev_ne_iff.mpr ((rev_zero _).symm ▸ h)) :
    rev (castPred i h) = pred (rev i) h'

Proof state:
n : ℕ
i : Fin (n + 1)
h : i ≠ last n
h' : optParam (i.rev ≠ 0) ⋯
⊢ (i.castPred h).rev = i.rev.pred h'

Tactic:
rw [← succ_inj, succ_pred, ← rev_castSucc, castSucc_castPred]

Result:
no goals
-- Mathlib/Algebra/Group/Submonoid/Units.lean
@[to_additive]
lemma mem_units_iff_val_mem (H : Subgroup G) (x : Gˣ) : x ∈ H.units ↔ (x : G) ∈ H

Proof state:
G : Type u_2
inst✝ : Group G
H : Subgroup G
x : Gˣ
⊢ x ∈ H.units ↔ ↑x ∈ H

Tactic:
simp_rw [Submonoid.mem_units_iff, mem_toSubmonoid, val_inv_eq_inv_val, inv_mem_iff, and_self]

Result:
no goals
-- Mathlib/Data/TypeVec.lean
theorem snd_prod_mk {α α' β β' : TypeVec n} (f : α ⟹ β) (g : α' ⟹ β') :
    TypeVec.prod.snd ⊚ (f ⊗' g) = g ⊚ TypeVec.prod.snd

Proof state:
case h.fz
n n✝ : ℕ
α α' β β' : TypeVec.{u_1} (n✝ + 1)
f : α ⟹ β
g : α' ⟹ β'
⊢ (prod.snd ⊚ (f ⊗' g)) Fin2.fz = (g ⊚ prod.snd) Fin2.fz

Tactic:
rfl

Result:
no goals

Proof state:
case h
n : ℕ
α α' β β' : TypeVec.{u_1} n
f : α ⟹ β
g : α' ⟹ β'
i : Fin2 n
⊢ (prod.snd ⊚ (f ⊗' g)) i = (g ⊚ prod.snd) i

Tactic:
induction i with
| fz => rfl
| fs _ i_ih => apply i_ih

Result:
no goals

Proof state:
case h.fs
n n✝ : ℕ
a✝ : Fin2 n✝
i_ih : ∀ {α α' β β' : TypeVec.{u_1} n✝} (f : α ⟹ β) (g : α' ⟹ β'), (prod.snd ⊚ (f ⊗' g)) a✝ = (g ⊚ prod.snd) a✝
α α' β β' : TypeVec.{u_1} (n✝ + 1)
f : α ⟹ β
g : α' ⟹ β'
⊢ (prod.snd ⊚ (f ⊗' g)) a✝.fs = (g ⊚ prod.snd) a✝.fs

Tactic:
apply i_ih

Result:
no goals

Proof state:
n : ℕ
α α' β β' : TypeVec.{u_1} n
f : α ⟹ β
g : α' ⟹ β'
⊢ prod.snd ⊚ (f ⊗' g) = g ⊚ prod.snd

Tactic:
funext i

Result:
case h
n : ℕ
α α' β β' : TypeVec.{u_1} n
f : α ⟹ β
g : α' ⟹ β'
i : Fin2 n
⊢ (prod.snd ⊚ (f ⊗' g)) i = (g ⊚ prod.snd) i
-- Mathlib/SetTheory/Game/PGame.lean
/-- A small set of pre-games is bounded above. -/
lemma bddAbove_of_small (s : Set PGame.{u}) [Small.{u} s] : BddAbove s

Proof state:
s : Set PGame
inst✝ : Small.{u, u + 1} ↑s
⊢ BddAbove s

Tactic:
simpa using bddAbove_range_of_small (Subtype.val : s → PGame.{u})

Result:
no goals