harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/LinearAlgebra/Lagrange.lean
theorem degree_basisDivisor_self : (basisDivisor x x).degree = ⊥

Proof state:
F : Type u_1
inst✝ : Field F
x : F
⊢ (basisDivisor x x).degree = ⊥

Tactic:
rw [basisDivisor_self, degree_zero]

Result:
no goals
-- Mathlib/RingTheory/AlgebraicIndependent/Defs.lean
theorem mono {t s : Set A} (h : t ⊆ s)
    (hx : AlgebraicIndependent R ((↑) : s → A)) : AlgebraicIndependent R ((↑) : t → A)

Proof state:
R : Type u_3
A : Type u_5
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
t s : Set A
h : t ⊆ s
hx : AlgebraicIndependent R Subtype.val
⊢ AlgebraicIndependent R Subtype.val

Tactic:
simpa [Function.comp] using hx.comp (inclusion h) (inclusion_injective h)

Result:
no goals
-- Mathlib/Data/List/Basic.lean
theorem filter_eq_foldr (p : α → Bool) (l : List α) :
    filter p l = foldr (fun a out => bif p a then a :: out else out) [] l

Proof state:
case cons
α : Type u
p : α → Bool
head✝ : α
tail✝ : List α
tail_ih✝ : filter p tail✝ = foldr (fun a out => bif p a then a :: out else out) [] tail✝
⊢ (match p head✝ with
    | true => head✝ :: foldr (fun a out => bif p a then a :: out else out) [] tail✝
    | false => foldr (fun a out => bif p a then a :: out else out) [] tail✝) =
    bif p head✝ then head✝ :: foldr (fun a out => bif p a then a :: out else out) [] tail✝
    else foldr (fun a out => bif p a then a :: out else out) [] tail✝

Tactic:
rfl

Result:
no goals

Proof state:
α : Type u
p : α → Bool
l : List α
⊢ filter p l = foldr (fun a out => bif p a then a :: out else out) [] l

Tactic:
induction l <;> simp [*, filter]

Result:
case cons
α : Type u
p : α → Bool
head✝ : α
tail✝ : List α
tail_ih✝ : filter p tail✝ = foldr (fun a out => bif p a then a :: out else out) [] tail✝
⊢ (match p head✝ with
    | true => head✝ :: foldr (fun a out => bif p a then a :: out else out) [] tail✝
    | false => foldr (fun a out => bif p a then a :: out else out) [] tail✝) =
    bif p head✝ then head✝ :: foldr (fun a out => bif p a then a :: out else out) [] tail✝
    else foldr (fun a out => bif p a then a :: out else out) [] tail✝
-- Mathlib/GroupTheory/Order/Min.lean
@[to_additive (attr := simp)]
lemma le_minOrder {n : ℕ∞} :
    n ≤ minOrder α ↔ ∀ ⦃a : α⦄, a ≠ 1 → IsOfFinOrder a → n ≤ orderOf a

Proof state:
α : Type u_1
inst✝ : Monoid α
n : ℕ∞
⊢ n ≤ minOrder α ↔ ∀ ⦃a : α⦄, a ≠ 1 → IsOfFinOrder a → n ≤ ↑(orderOf a)

Tactic:
simp [minOrder]

Result:
no goals
-- Mathlib/Order/Filter/Extr.lean
theorem Filter.EventuallyLE.isMaxFilter {α β : Type*} [Preorder β] {f g : α → β} {a : α}
    {l : Filter α} (hle : g ≤ᶠ[l] f) (hfga : f a = g a) (h : IsMaxFilter f l a) :
    IsMaxFilter g l a

Proof state:
α : Type u_1
β : Type u_2
inst✝ : Preorder β
f g : α → β
a : α
l : Filter α
hle : g ≤ᶠ[l] f
hfga : f a = g a
h : IsMaxFilter f l a
⊢ IsMaxFilter g l a

Tactic:
refine hle.mp (h.mono fun x hf hgf => ?_)

Result:
α : Type u_1
β : Type u_2
inst✝ : Preorder β
f g : α → β
a : α
l : Filter α
hle : g ≤ᶠ[l] f
hfga : f a = g a
h : IsMaxFilter f l a
x : α
hf : f x ≤ f a
hgf : g x ≤ f x
⊢ g x ≤ g a

Proof state:
α : Type u_1
β : Type u_2
inst✝ : Preorder β
f g : α → β
a : α
l : Filter α
hle : g ≤ᶠ[l] f
hfga : f a = g a
h : IsMaxFilter f l a
x : α
hf : f x ≤ f a
hgf : g x ≤ f x
⊢ g x ≤ f a

Tactic:
exact le_trans hgf hf

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
inst✝ : Preorder β
f g : α → β
a : α
l : Filter α
hle : g ≤ᶠ[l] f
hfga : f a = g a
h : IsMaxFilter f l a
x : α
hf : f x ≤ f a
hgf : g x ≤ f x
⊢ g x ≤ g a

Tactic:
rw [← hfga]

Result:
α : Type u_1
β : Type u_2
inst✝ : Preorder β
f g : α → β
a : α
l : Filter α
hle : g ≤ᶠ[l] f
hfga : f a = g a
h : IsMaxFilter f l a
x : α
hf : f x ≤ f a
hgf : g x ≤ f x
⊢ g x ≤ f a
-- Mathlib/Data/Real/ConjExponents.lean
@[symm] protected lemma symm : q.IsConjExponent p where
  one_lt

Proof state:
p q : ℝ
h : p.IsConjExponent q
⊢ 1 < q

Tactic:
simpa only [h.conj_eq] using (one_lt_div h.sub_one_pos).mpr (sub_one_lt p)

Result:
no goals

Proof state:
p q : ℝ
h : p.IsConjExponent q
⊢ q⁻¹ + p⁻¹ = 1

Tactic:
simpa [add_comm] using h.inv_add_inv_conj

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Pow/Real.lean
theorem rpow_le_one {x z : ℝ} (hx1 : 0 ≤ x) (hx2 : x ≤ 1) (hz : 0 ≤ z) : x ^ z ≤ 1

Proof state:
x z : ℝ
hx1 : 0 ≤ x
hx2 : x ≤ 1
hz : 0 ≤ z
⊢ x ^ z ≤ 1

Tactic:
rw [← one_rpow z]

Result:
x z : ℝ
hx1 : 0 ≤ x
hx2 : x ≤ 1
hz : 0 ≤ z
⊢ x ^ z ≤ 1 ^ z

Proof state:
x z : ℝ
hx1 : 0 ≤ x
hx2 : x ≤ 1
hz : 0 ≤ z
⊢ x ^ z ≤ 1 ^ z

Tactic:
exact rpow_le_rpow hx1 hx2 hz

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Tactic/BVDecide/Reflect.lean
theorem udiv_congr (lhs rhs lhs' rhs' : BitVec w) (h1 : lhs' = lhs) (h2 : rhs' = rhs) :
    (lhs' / rhs') = (lhs / rhs)

Proof state:
w : Nat
lhs rhs lhs' rhs' : BitVec w
h1 : lhs' = lhs
h2 : rhs' = rhs
⊢ lhs' / rhs' = lhs / rhs

Tactic:
simp[*]

Result:
no goals
-- Mathlib/CategoryTheory/Bicategory/Basic.lean
theorem associator_inv_naturality_left {f f' : a ⟶ b} (η : f ⟶ f') (g : b ⟶ c) (h : c ⟶ d) :
    η ▷ (g ≫ h) ≫ (α_ f' g h).inv = (α_ f g h).inv ≫ η ▷ g ▷ h

Proof state:
B : Type u
inst✝ : Bicategory B
a b c d : B
f f' : a ⟶ b
η : f ⟶ f'
g : b ⟶ c
h : c ⟶ d
⊢ η ▷ (g ≫ h) ≫ (α_ f' g h).inv = (α_ f g h).inv ≫ η ▷ g ▷ h

Tactic:
simp

Result:
no goals
-- Mathlib/CategoryTheory/Adjunction/Unique.lean
theorem rightAdjointUniq_refl {F : C ⥤ D} {G : D ⥤ C} (adj1 : F ⊣ G) :
    (rightAdjointUniq adj1 adj1).hom = 𝟙 _

Proof state:
C : Type u_1
D : Type u_2
inst✝¹ : Category.{u_3, u_1} C
inst✝ : Category.{u_4, u_2} D
F : C ⥤ D
G : D ⥤ C
adj1 : F ⊣ G
⊢ ((conjugateIsoEquiv adj1 adj1) (Iso.refl F)).hom = 𝟙 G

Tactic:
simp

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
F : C ⥤ D
G : D ⥤ C
adj1 : F ⊣ G
⊢ (adj1.rightAdjointUniq adj1).hom = 𝟙 G

Tactic:
delta rightAdjointUniq

Result:
C : Type u_1
D : Type u_2
inst✝¹ : Category.{u_3, u_1} C
inst✝ : Category.{u_4, u_2} D
F : C ⥤ D
G : D ⥤ C
adj1 : F ⊣ G
⊢ ((conjugateIsoEquiv adj1 adj1) (Iso.refl F)).hom = 𝟙 G
-- Mathlib/Analysis/Normed/Group/Constructions.lean
lemma Pi.enorm_single [DecidableEq ι] [∀ i, NormedAddCommGroup (π i)] {i : ι} (y : π i) :
    ‖Pi.single i y‖ₑ = ‖y‖ₑ

Proof state:
ι : Type u_1
π : ι → Type u_4
inst✝² : Fintype ι
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → NormedAddCommGroup (π i)
i : ι
y : π i
⊢ ‖single i y‖ₑ = ‖y‖ₑ

Tactic:
simp [enorm, Pi.nnnorm_single]

Result:
no goals
-- Mathlib/Topology/Homeomorph.lean
theorem symm_map_nhds_eq (h : X ≃ₜ Y) (x : X) : map h.symm (𝓝 (h x)) = 𝓝 x

Proof state:
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
h : X ≃ₜ Y
x : X
⊢ map (⇑h.symm) (𝓝 (h x)) = 𝓝 x

Tactic:
rw [h.symm.map_nhds_eq, h.symm_apply_apply]

Result:
no goals
-- Mathlib/Algebra/Ring/Units.lean
theorem add_divp (a b : α) (u : αˣ) : a + b /ₚ u = (a * u + b) /ₚ u

Proof state:
α : Type u
inst✝ : Ring α
a b : α
u : αˣ
⊢ a + b /ₚ u = (a * ↑u + b) /ₚ u

Tactic:
simp only [divp, add_mul, Units.mul_inv_cancel_right]

Result:
no goals
-- Mathlib/NumberTheory/LegendreSymbol/GaussEisensteinLemmas.lean
theorem gauss_lemma {p : ℕ} [h : Fact p.Prime] {a : ℤ} (hp : p ≠ 2) (ha0 : (a : ZMod p) ≠ 0) :
    legendreSym p a = (-1) ^ #{x ∈ Ico 1 (p / 2).succ | p / 2 < (a * x.cast : ZMod p).val}

Proof state:
p : ℕ
h : Fact (Nat.Prime p)
a : ℤ
ha0 : ↑a ≠ 0
hp : Odd p
this : ↑(legendreSym p a) = ↑((-1) ^ #(filter (fun x => p / 2 < (↑a * ↑x).val) (Ico 1 (p / 2).succ)))
⊢ legendreSym p a = (-1) ^ #(filter (fun x => p / 2 < (↑a * ↑x).val) (Ico 1 (p / 2).succ))

Tactic:
cases legendreSym.eq_one_or_neg_one p ha0 <;>
cases neg_one_pow_eq_or ℤ #{x ∈ Ico 1 (p / 2).succ | p / 2 < (a * x.cast : ZMod p).val} <;>
simp_all [ne_neg_self hp one_ne_zero, (ne_neg_self hp one_ne_zero).symm]

Result:
no goals

Proof state:
p : ℕ
h : Fact (Nat.Prime p)
a : ℤ
ha0 : ↑a ≠ 0
hp : Odd p
⊢ ↑(legendreSym p a) = ↑((-1) ^ #(filter (fun x => p / 2 < (↑a * ↑x).val) (Ico 1 (p / 2).succ)))

Tactic:
rw [legendreSym.eq_pow, gauss_lemma_aux p ha0]

Result:
no goals

Proof state:
p : ℕ
h : Fact (Nat.Prime p)
a : ℤ
hp : p ≠ 2
ha0 : ↑a ≠ 0
⊢ legendreSym p a = (-1) ^ #(filter (fun x => p / 2 < (↑a * ↑x).val) (Ico 1 (p / 2).succ))

Tactic:
replace hp : Odd p := h.out.odd_of_ne_two hp

Result:
p : ℕ
h : Fact (Nat.Prime p)
a : ℤ
ha0 : ↑a ≠ 0
hp : Odd p
⊢ legendreSym p a = (-1) ^ #(filter (fun x => p / 2 < (↑a * ↑x).val) (Ico 1 (p / 2).succ))

Proof state:
p : ℕ
h : Fact (Nat.Prime p)
a : ℤ
ha0 : ↑a ≠ 0
hp : Odd p
⊢ legendreSym p a = (-1) ^ #(filter (fun x => p / 2 < (↑a * ↑x).val) (Ico 1 (p / 2).succ))

Tactic:
have : (legendreSym p a : ZMod p) =
    (((-1) ^ #{x ∈ Ico 1 (p / 2).succ | p / 2 < (a * x.cast : ZMod p).val} : ℤ) : ZMod p) := by
  rw [legendreSym.eq_pow, gauss_lemma_aux p ha0]

Result:
p : ℕ
h : Fact (Nat.Prime p)
a : ℤ
ha0 : ↑a ≠ 0
hp : Odd p
this : ↑(legendreSym p a) = ↑((-1) ^ #(filter (fun x => p / 2 < (↑a * ↑x).val) (Ico 1 (p / 2).succ)))
⊢ legendreSym p a = (-1) ^ #(filter (fun x => p / 2 < (↑a * ↑x).val) (Ico 1 (p / 2).succ))
-- Mathlib/LinearAlgebra/BilinearForm/Orthogonal.lean
theorem isOrtho_smul_left {x y : M₄} {a : R₄} (ha : a ≠ 0) :
    IsOrtho G (a • x) y ↔ IsOrtho G x y

Proof state:
R₄ : Type u_7
M₄ : Type u_8
inst✝³ : CommRing R₄
inst✝² : IsDomain R₄
inst✝¹ : AddCommGroup M₄
inst✝ : Module R₄ M₄
G : BilinForm R₄ M₄
x y : M₄
a : R₄
ha : a ≠ 0
⊢ (a • G x) y = 0 ↔ (G x) y = 0

Tactic:
simp only [LinearMap.smul_apply, smul_eq_mul, mul_eq_zero, or_iff_right_iff_imp]

Result:
R₄ : Type u_7
M₄ : Type u_8
inst✝³ : CommRing R₄
inst✝² : IsDomain R₄
inst✝¹ : AddCommGroup M₄
inst✝ : Module R₄ M₄
G : BilinForm R₄ M₄
x y : M₄
a : R₄
ha : a ≠ 0
⊢ a = 0 → (G x) y = 0

Proof state:
R₄ : Type u_7
M₄ : Type u_8
inst✝³ : CommRing R₄
inst✝² : IsDomain R₄
inst✝¹ : AddCommGroup M₄
inst✝ : Module R₄ M₄
G : BilinForm R₄ M₄
x y : M₄
a : R₄
ha : a ≠ 0
⊢ (G (a • x)) y = 0 ↔ (G x) y = 0

Tactic:
rw [map_smul]

Result:
R₄ : Type u_7
M₄ : Type u_8
inst✝³ : CommRing R₄
inst✝² : IsDomain R₄
inst✝¹ : AddCommGroup M₄
inst✝ : Module R₄ M₄
G : BilinForm R₄ M₄
x y : M₄
a : R₄
ha : a ≠ 0
⊢ (a • G x) y = 0 ↔ (G x) y = 0

Proof state:
R₄ : Type u_7
M₄ : Type u_8
inst✝³ : CommRing R₄
inst✝² : IsDomain R₄
inst✝¹ : AddCommGroup M₄
inst✝ : Module R₄ M₄
G : BilinForm R₄ M₄
x y : M₄
a : R₄
ha : a ≠ 0
⊢ a = 0 → (G x) y = 0

Tactic:
exact fun a ↦ (ha a).elim

Result:
no goals

Proof state:
R₄ : Type u_7
M₄ : Type u_8
inst✝³ : CommRing R₄
inst✝² : IsDomain R₄
inst✝¹ : AddCommGroup M₄
inst✝ : Module R₄ M₄
G : BilinForm R₄ M₄
x y : M₄
a : R₄
ha : a ≠ 0
⊢ G.IsOrtho (a • x) y ↔ G.IsOrtho x y

Tactic:
dsimp only [IsOrtho]

Result:
R₄ : Type u_7
M₄ : Type u_8
inst✝³ : CommRing R₄
inst✝² : IsDomain R₄
inst✝¹ : AddCommGroup M₄
inst✝ : Module R₄ M₄
G : BilinForm R₄ M₄
x y : M₄
a : R₄
ha : a ≠ 0
⊢ (G (a • x)) y = 0 ↔ (G x) y = 0
-- Mathlib/LinearAlgebra/AffineSpace/AffineSubspace/Basic.lean
theorem mem_affineSpan_singleton : p₁ ∈ affineSpan k ({p₂} : Set P) ↔ p₁ = p₂

Proof state:
k : Type u_1
V : Type u_2
P : Type u_3
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
S : AffineSpace V P
p₁ p₂ : P
⊢ p₁ ∈ affineSpan k {p₂} ↔ p₁ = p₂

Tactic:
simp [← mem_coe]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Log/Base.lean
theorem lt_logb_iff_rpow_lt_of_base_lt_one (hy : 0 < y) : x < logb b y ↔ y < b ^ x

Proof state:
b x y : ℝ
b_pos : 0 < b
b_lt_one : b < 1
hy : 0 < y
⊢ x < logb b y ↔ y < b ^ x

Tactic:
rw [← rpow_lt_rpow_left_iff_of_base_lt_one b_pos b_lt_one, rpow_logb b_pos (b_ne_one b_lt_one) hy]

Result:
no goals
-- Mathlib/CategoryTheory/Shift/Opposite.lean
lemma oppositeShiftFunctorAdd_hom_app :
    (shiftFunctorAdd (OppositeShift C A) a b).hom.app X =
      ((shiftFunctorAdd C a b).inv.app X.unop).op

Proof state:
C : Type u_1
inst✝² : Category.{u_3, u_1} C
A : Type u_2
inst✝¹ : AddMonoid A
inst✝ : HasShift C A
X : OppositeShift C A
a b : A
⊢ (shiftFunctorAdd (OppositeShift C A) a b).hom.app X = ((shiftFunctorAdd C a b).inv.app (Opposite.unop X)).op

Tactic:
rw [← cancel_mono ((shiftFunctorAdd (OppositeShift C A) a b).inv.app X),
  Iso.hom_inv_id_app, oppositeShiftFunctorAdd_inv_app, ← op_comp,
  Iso.hom_inv_id_app, op_id]

Result:
C : Type u_1
inst✝² : Category.{u_3, u_1} C
A : Type u_2
inst✝¹ : AddMonoid A
inst✝ : HasShift C A
X : OppositeShift C A
a b : A
⊢ 𝟙 ((shiftFunctor (OppositeShift C A) (a + b)).obj X) =
    𝟙 (Opposite.op ((shiftFunctor C (a + b)).obj (Opposite.unop X)))

Proof state:
C : Type u_1
inst✝² : Category.{u_3, u_1} C
A : Type u_2
inst✝¹ : AddMonoid A
inst✝ : HasShift C A
X : OppositeShift C A
a b : A
⊢ 𝟙 ((shiftFunctor (OppositeShift C A) (a + b)).obj X) =
    𝟙 (Opposite.op ((shiftFunctor C (a + b)).obj (Opposite.unop X)))

Tactic:
rfl

Result:
no goals
-- Mathlib/Algebra/Algebra/Operations.lean
theorem span_mul_span : span R S * span R T = span R (S * T)

Proof state:
R : Type u
inst✝² : CommSemiring R
A : Type v
inst✝¹ : Semiring A
inst✝ : Algebra R A
S T : Set A
⊢ map₂ (LinearMap.mul R A) (span R S) (span R T) = span R (S * T)

Tactic:
apply map₂_span_span

Result:
no goals

Proof state:
R : Type u
inst✝² : CommSemiring R
A : Type v
inst✝¹ : Semiring A
inst✝ : Algebra R A
S T : Set A
⊢ span R S * span R T = span R (S * T)

Tactic:
rw [mul_eq_map₂]

Result:
R : Type u
inst✝² : CommSemiring R
A : Type v
inst✝¹ : Semiring A
inst✝ : Algebra R A
S T : Set A
⊢ map₂ (LinearMap.mul R A) (span R S) (span R T) = span R (S * T)
-- Mathlib/Analysis/Analytic/Constructions.lean
theorem hasFPowerSeriesOnBall_const {c : F} {e : E} :
    HasFPowerSeriesOnBall (fun _ => c) (constFormalMultilinearSeries 𝕜 E c) e ⊤

Proof state:
𝕜 : Type u_2
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_3
F : Type u_4
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
c : F
e : E
⊢ ⊤ ≤ (constFormalMultilinearSeries 𝕜 E c).radius

Tactic:
simp

Result:
no goals

Proof state:
𝕜 : Type u_2
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_3
F : Type u_4
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
c : F
e : E
⊢ HasFPowerSeriesOnBall (fun x => c) (constFormalMultilinearSeries 𝕜 E c) e ⊤

Tactic:
refine ⟨by simp, WithTop.top_pos, fun _ => hasSum_single 0 fun n hn => ?_⟩

Result:
𝕜 : Type u_2
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_3
F : Type u_4
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
c : F
e y✝ : E
x✝ : y✝ ∈ EMetric.ball 0 ⊤
n : ℕ
hn : n ≠ 0
⊢ ((constFormalMultilinearSeries 𝕜 E c n) fun x => y✝) = 0

Proof state:
𝕜 : Type u_2
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_3
F : Type u_4
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
c : F
e y✝ : E
x✝ : y✝ ∈ EMetric.ball 0 ⊤
n : ℕ
hn : n ≠ 0
⊢ ((constFormalMultilinearSeries 𝕜 E c n) fun x => y✝) = 0

Tactic:
simp [constFormalMultilinearSeries_apply hn]

Result:
no goals
-- Mathlib/Order/Partition/Equipartition.lean
theorem IsEquipartition.average_le_card_part (hP : P.IsEquipartition) (ht : t ∈ P.parts) :
    #s / #P.parts ≤ #t

Proof state:
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
P : Finpartition s
hP : P.IsEquipartition
ht : t ∈ P.parts
⊢ (∑ i ∈ P.parts, #i) / #P.parts ≤ #t

Tactic:
exact Finset.EquitableOn.le hP ht

Result:
no goals

Proof state:
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
P : Finpartition s
hP : P.IsEquipartition
ht : t ∈ P.parts
⊢ #s / #P.parts ≤ #t

Tactic:
rw [← P.sum_card_parts]

Result:
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
P : Finpartition s
hP : P.IsEquipartition
ht : t ∈ P.parts
⊢ (∑ i ∈ P.parts, #i) / #P.parts ≤ #t
-- Mathlib/Probability/Kernel/Composition/MapComap.lean
@[simp]
lemma id_map {f : α → β} (hf : Measurable f) : Kernel.id.map f = deterministic f hf

Proof state:
case h.h
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
f : α → β
hf : Measurable f
a✝¹ : α
s✝ : Set β
a✝ : MeasurableSet s✝
⊢ ((Kernel.id.map f) a✝¹) s✝ = ((deterministic f hf) a✝¹) s✝

Tactic:
rw [Kernel.map_apply _ hf, Kernel.deterministic_apply, Kernel.id_apply, Measure.map_dirac hf]

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
f : α → β
hf : Measurable f
⊢ Kernel.id.map f = deterministic f hf

Tactic:
ext

Result:
case h.h
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
f : α → β
hf : Measurable f
a✝¹ : α
s✝ : Set β
a✝ : MeasurableSet s✝
⊢ ((Kernel.id.map f) a✝¹) s✝ = ((deterministic f hf) a✝¹) s✝
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Lemmas.lean
theorem isEmpty_eq_false_iff_exists_mem {xs : List α} :
    xs.isEmpty = false ↔ ∃ x, x ∈ xs

Proof state:
α : Type u_1
xs : List α
⊢ xs.isEmpty = false ↔ ∃ x, x ∈ xs

Tactic:
cases xs <;> simp

Result:
no goals
-- Mathlib/Topology/Basic.lean
theorem Filter.Tendsto.lift'_closure (hf : Continuous f) {l l'} (h : Tendsto f l l') :
    Tendsto f (l.lift' closure) (l'.lift' closure) :=
  tendsto_lift'.2 fun s hs ↦ by
    filter_upwards [mem_lift' (h hs)] using (mapsTo_preimage _ _).closure hf

Proof state:
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
hf : Continuous f
l : Filter X
l' : Filter Y
h : Tendsto f l l'
s : Set Y
hs : s ∈ l'
⊢ ∀ᶠ (a : X) in l.lift' closure, f a ∈ closure s

Tactic:
filter_upwards [mem_lift' (h hs)] using (mapsTo_preimage _ _).closure hf

Result:
no goals
-- Mathlib/Algebra/BigOperators/Group/Finset/Basic.lean
@[to_additive]
lemma mulSupport_prod (s : Finset ι) (f : ι → α → β) :
    mulSupport (fun x ↦ ∏ i ∈ s, f i x) ⊆ ⋃ i ∈ s, mulSupport (f i)

Proof state:
ι : Type u_1
α : Type u_3
β : Type u_4
inst✝ : CommMonoid β
s : Finset ι
f : ι → α → β
⊢ ∀ (x : α), (∀ x_1 ∈ s, f x_1 x = 1) → ∏ i ∈ s, f i x = 1

Tactic:
exact fun x ↦ prod_eq_one

Result:
no goals

Proof state:
ι : Type u_1
α : Type u_3
β : Type u_4
inst✝ : CommMonoid β
s : Finset ι
f : ι → α → β
⊢ (mulSupport fun x => ∏ i ∈ s, f i x) ⊆ ⋃ i ∈ s, mulSupport (f i)

Tactic:
simp only [mulSupport_subset_iff', Set.mem_iUnion, not_exists, nmem_mulSupport]

Result:
ι : Type u_1
α : Type u_3
β : Type u_4
inst✝ : CommMonoid β
s : Finset ι
f : ι → α → β
⊢ ∀ (x : α), (∀ x_1 ∈ s, f x_1 x = 1) → ∏ i ∈ s, f i x = 1
-- Mathlib/Logic/Equiv/Basic.lean
theorem swap_apply_self (i j a : α) : swap i j (swap i j a) = a

Proof state:
α : Sort u_1
inst✝ : DecidableEq α
i j a : α
⊢ (swap i j) ((swap i j) a) = a

Tactic:
rw [← Equiv.trans_apply, Equiv.swap_swap, Equiv.refl_apply]

Result:
no goals
-- Mathlib/ModelTheory/Semantics.lean
theorem realize_relabel_sumInr (φ : L.Formula (Fin n)) {v : Empty → M} {x : Fin n → M} :
    (BoundedFormula.relabel Sum.inr φ).Realize v x ↔ φ.Realize x

Proof state:
L : Language
M : Type w
inst✝ : L.Structure M
n : ℕ
φ : L.Formula (Fin n)
v : Empty → M
x : Fin n → M
⊢ (BoundedFormula.relabel Sum.inr φ).Realize v x ↔ φ.Realize x

Tactic:
rw [BoundedFormula.realize_relabel, Formula.Realize, Sum.elim_comp_inr, Fin.castAdd_zero,
  cast_refl, Function.comp_id,
  Subsingleton.elim (x ∘ (natAdd n : Fin 0 → Fin n)) default]

Result:
no goals
-- Mathlib/MeasureTheory/Constructions/Pi.lean
theorem measurePreserving_sumPiEquivProdPi_symm {π : ι ⊕ ι' → Type*}
    {m : ∀ i, MeasurableSpace (π i)} (μ : ∀ i, Measure (π i)) [∀ i, SigmaFinite (μ i)] :
    MeasurePreserving (MeasurableEquiv.sumPiEquivProdPi π).symm
      ((Measure.pi fun i => μ (.inl i)).prod (Measure.pi fun i => μ (.inr i))) (Measure.pi μ) where
  measurable := (MeasurableEquiv.sumPiEquivProdPi π).symm.measurable
  map_eq

Proof state:
ι : Type u_1
ι' : Type u_2
inst✝² : Fintype ι
inst✝¹ : Fintype ι'
π : ι ⊕ ι' → Type u_4
m : (i : ι ⊕ ι') → MeasurableSpace (π i)
μ : (i : ι ⊕ ι') → Measure (π i)
inst✝ : ∀ (i : ι ⊕ ι'), SigmaFinite (μ i)
⊢ Measure.map (⇑(MeasurableEquiv.sumPiEquivProdPi π).symm)
      ((Measure.pi fun i => μ (Sum.inl i)).prod (Measure.pi fun i => μ (Sum.inr i))) =
    Measure.pi μ

Tactic:
refine (pi_eq fun s _ => ?_).symm

Result:
ι : Type u_1
ι' : Type u_2
inst✝² : Fintype ι
inst✝¹ : Fintype ι'
π : ι ⊕ ι' → Type u_4
m : (i : ι ⊕ ι') → MeasurableSpace (π i)
μ : (i : ι ⊕ ι') → Measure (π i)
inst✝ : ∀ (i : ι ⊕ ι'), SigmaFinite (μ i)
s : (i : ι ⊕ ι') → Set (π i)
x✝ : ∀ (i : ι ⊕ ι'), MeasurableSet (s i)
⊢ (Measure.map (⇑(MeasurableEquiv.sumPiEquivProdPi π).symm)
        ((Measure.pi fun i => μ (Sum.inl i)).prod (Measure.pi fun i => μ (Sum.inr i))))
      (univ.pi s) =
    ∏ i : ι ⊕ ι', (μ i) (s i)

Proof state:
ι : Type u_1
ι' : Type u_2
inst✝² : Fintype ι
inst✝¹ : Fintype ι'
π : ι ⊕ ι' → Type u_4
m : (i : ι ⊕ ι') → MeasurableSpace (π i)
μ : (i : ι ⊕ ι') → Measure (π i)
inst✝ : ∀ (i : ι ⊕ ι'), SigmaFinite (μ i)
s : (i : ι ⊕ ι') → Set (π i)
x✝ : ∀ (i : ι ⊕ ι'), MeasurableSet (s i)
⊢ (Measure.map (⇑(MeasurableEquiv.sumPiEquivProdPi π).symm)
        ((Measure.pi fun i => μ (Sum.inl i)).prod (Measure.pi fun i => μ (Sum.inr i))))
      (univ.pi s) =
    ∏ i : ι ⊕ ι', (μ i) (s i)

Tactic:
simp_rw [MeasurableEquiv.map_apply, MeasurableEquiv.coe_sumPiEquivProdPi_symm,
  Equiv.sumPiEquivProdPi_symm_preimage_univ_pi, Measure.prod_prod, Measure.pi_pi,
  Fintype.prod_sum_type]

Result:
no goals
-- Mathlib/Data/List/Map2.lean
theorem zipLeft_nil_right : zipLeft as ([] : List β) = as.map fun a => (a, none)

Proof state:
α : Type u
β : Type v
as : List α
⊢ as.zipLeft [] = map (fun a => (a, none)) as

Tactic:
cases as <;> rfl

Result:
no goals
-- Mathlib/Data/Nat/Prime/Basic.lean
theorem not_prime_mul {a b : ℕ} (a1 : a ≠ 1) (b1 : b ≠ 1) : ¬Prime (a * b)

Proof state:
a b : ℕ
a1 : a ≠ 1
b1 : b ≠ 1
⊢ ¬Prime (a * b)

Tactic:
simp [prime_mul_iff, _root_.not_or, *]

Result:
no goals
-- Mathlib/GroupTheory/SchurZassenhaus.lean
theorem step0 : N ≠ ⊥

Proof state:
G : Type u
inst✝¹ : Group G
N : Subgroup G
inst✝ : N.Normal
h1 : (Nat.card ↥N).Coprime N.index
h3 : ∀ (H : Subgroup G), ¬N.IsComplement' H
⊢ N ≠ ⊥

Tactic:
rintro rfl

Result:
G : Type u
inst✝¹ : Group G
inst✝ : ⊥.Normal
h1 : (Nat.card ↥⊥).Coprime ⊥.index
h3 : ∀ (H : Subgroup G), ¬⊥.IsComplement' H
⊢ False

Proof state:
G : Type u
inst✝¹ : Group G
inst✝ : ⊥.Normal
h1 : (Nat.card ↥⊥).Coprime ⊥.index
h3 : ∀ (H : Subgroup G), ¬⊥.IsComplement' H
⊢ False

Tactic:
exact h3 ⊤ isComplement'_bot_top

Result:
no goals
-- Mathlib/Algebra/SkewMonoidAlgebra/Basic.lean
theorem coeff_single_apply {a a' : G} {b : k} [Decidable (a = a')] :
    coeff (single a b) a' = if a = a' then b else 0

Proof state:
k : Type u_1
G : Type u_2
inst✝¹ : AddCommMonoid k
a a' : G
b : k
inst✝ : Decidable (a = a')
⊢ (single a b).coeff a' = if a = a' then b else 0

Tactic:
simp [coeff, Finsupp.single_apply]

Result:
no goals
-- Mathlib/MeasureTheory/Constructions/Polish/Basic.lean
theorem Continuous.map_eq_borel {X Y : Type*} [TopologicalSpace X] [PolishSpace X]
    [MeasurableSpace X] [BorelSpace X] [TopologicalSpace Y] [T0Space Y] [SecondCountableTopology Y]
    {f : X → Y} (hf : Continuous f) (hsurj : Surjective f) :
    MeasurableSpace.map f ‹MeasurableSpace X› = borel Y

Proof state:
X : Type u_3
Y : Type u_4
inst✝⁶ : TopologicalSpace X
inst✝⁵ : PolishSpace X
inst✝⁴ : MeasurableSpace X
inst✝³ : BorelSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : T0Space Y
inst✝ : SecondCountableTopology Y
f : X → Y
hf : Continuous f
hsurj : Surjective f
⊢ MeasurableSpace.map f inst✝⁴ = borel Y

Tactic:
borelize Y

Result:
X : Type u_3
Y : Type u_4
inst✝⁶ : TopologicalSpace X
inst✝⁵ : PolishSpace X
inst✝⁴ : MeasurableSpace X
inst✝³ : BorelSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : T0Space Y
inst✝ : SecondCountableTopology Y
f : X → Y
hf : Continuous f
hsurj : Surjective f
this✝¹ : MeasurableSpace Y := borel Y
this✝ : BorelSpace Y
⊢ MeasurableSpace.map f inst✝⁴ = borel Y

Proof state:
X : Type u_3
Y : Type u_4
inst✝⁶ : TopologicalSpace X
inst✝⁵ : PolishSpace X
inst✝⁴ : MeasurableSpace X
inst✝³ : BorelSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : T0Space Y
inst✝ : SecondCountableTopology Y
f : X → Y
hf : Continuous f
hsurj : Surjective f
this✝¹ : MeasurableSpace Y := borel Y
this✝ : BorelSpace Y
⊢ MeasurableSpace.map f inst✝⁴ = borel Y

Tactic:
exact hf.measurable.map_measurableSpace_eq hsurj

Result:
no goals