harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Analysis/FunctionalSpaces/SobolevInequality.lean
theorem lintegral_pow_le_pow_lintegral_fderiv_aux [Fintype ι]
    {p : ℝ} (hp : Real.IsConjExponent #ι p)
    {u : (ι → ℝ) → F} (hu : ContDiff ℝ 1 u)
    (h2u : HasCompactSupport u) :
    ∫⁻ x, ‖u x‖ₑ ^ p ≤ (∫⁻ x, ‖fderiv ℝ u x‖ₑ) ^ p

Proof state:
ι : Type u_1
F : Type u_3
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : Fintype ι
p : ℝ
hp : (↑#ι).IsConjExponent p
u : (ι → ℝ) → F
hu : ContDiff ℝ 1 u
h2u : HasCompactSupport u
this : 1 ≤ ↑#ι - 1
⊢ ∫⁻ (x : ι → ℝ), ‖u x‖ₑ ^ p ≤ (∫⁻ (x : ι → ℝ), ‖fderiv ℝ u x‖ₑ) ^ p

Tactic:
calc ∫⁻ x, ‖u x‖ₑ ^ p
    = ∫⁻ x, (‖u x‖ₑ ^ (1 / (#ι - 1 : ℝ))) ^ (#ι : ℝ) := by
      congr! 2 with x
      rw [← ENNReal.rpow_mul, hp.conj_eq]
      field_simp
  _ = ∫⁻ x, ∏ _i : ι, ‖u x‖ₑ ^ (1 / (#ι - 1 : ℝ)) := by
      congr! 2 with x
      simp_rw [prod_const]
      norm_cast
  _ ≤ ∫⁻ x, ∏ i, (∫⁻ xᵢ, ‖fderiv ℝ u (update x i xᵢ)‖ₑ) ^ ((1 : ℝ) / (#ι - 1 : ℝ)) := ?_
  _ ≤ (∫⁻ x, ‖fderiv ℝ u x‖ₑ) ^ p := by
      apply lintegral_prod_lintegral_pow_le _ hp
      have : Continuous (fderiv ℝ u) := hu.continuous_fderiv le_rfl
      fun_prop

Result:
ι : Type u_1
F : Type u_3
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : Fintype ι
p : ℝ
hp : (↑#ι).IsConjExponent p
u : (ι → ℝ) → F
hu : ContDiff ℝ 1 u
h2u : HasCompactSupport u
this : 1 ≤ ↑#ι - 1
⊢ ∫⁻ (x : ι → ℝ), ∏ _i : ι, ‖u x‖ₑ ^ (1 / (↑#ι - 1)) ≤
    ∫⁻ (x : ι → ℝ), ∏ i : ι, (∫⁻ (xᵢ : ℝ), ‖fderiv ℝ u (update x i xᵢ)‖ₑ) ^ (1 / (↑#ι - 1))
-- Mathlib/RingTheory/Noetherian/Basic.lean
theorem isNoetherian_iff_submodule_quotient (S : Submodule R P) :
    IsNoetherian R P ↔ IsNoetherian R S ∧ IsNoetherian R (P ⧸ S)

Proof state:
R : Type u_1
P : Type u_4
inst✝² : Ring R
inst✝¹ : AddCommGroup P
inst✝ : Module R P
S : Submodule R P
x✝ : IsNoetherian R ↥S ∧ IsNoetherian R (P ⧸ S)
left✝ : IsNoetherian R ↥S
right✝ : IsNoetherian R (P ⧸ S)
⊢ IsNoetherian R P

Tactic:
apply isNoetherian_of_range_eq_ker S.subtype S.mkQ

Result:
R : Type u_1
P : Type u_4
inst✝² : Ring R
inst✝¹ : AddCommGroup P
inst✝ : Module R P
S : Submodule R P
x✝ : IsNoetherian R ↥S ∧ IsNoetherian R (P ⧸ S)
left✝ : IsNoetherian R ↥S
right✝ : IsNoetherian R (P ⧸ S)
⊢ LinearMap.range S.subtype = LinearMap.ker S.mkQ

Proof state:
R : Type u_1
P : Type u_4
inst✝² : Ring R
inst✝¹ : AddCommGroup P
inst✝ : Module R P
S : Submodule R P
⊢ IsNoetherian R P ↔ IsNoetherian R ↥S ∧ IsNoetherian R (P ⧸ S)

Tactic:
refine ⟨fun _ ↦ ⟨inferInstance, inferInstance⟩, fun ⟨_, _⟩ ↦ ?_⟩

Result:
R : Type u_1
P : Type u_4
inst✝² : Ring R
inst✝¹ : AddCommGroup P
inst✝ : Module R P
S : Submodule R P
x✝ : IsNoetherian R ↥S ∧ IsNoetherian R (P ⧸ S)
left✝ : IsNoetherian R ↥S
right✝ : IsNoetherian R (P ⧸ S)
⊢ IsNoetherian R P

Proof state:
R : Type u_1
P : Type u_4
inst✝² : Ring R
inst✝¹ : AddCommGroup P
inst✝ : Module R P
S : Submodule R P
x✝ : IsNoetherian R ↥S ∧ IsNoetherian R (P ⧸ S)
left✝ : IsNoetherian R ↥S
right✝ : IsNoetherian R (P ⧸ S)
⊢ LinearMap.range S.subtype = LinearMap.ker S.mkQ

Tactic:
rw [Submodule.ker_mkQ, Submodule.range_subtype]

Result:
no goals
-- Mathlib/ModelTheory/Satisfiability.lean
theorem empty_theory_categorical (T : Language.empty.Theory) : κ.Categorical T := fun M N hM hN =>
  by rw [empty.nonempty_equiv_iff, hM, hN]

Proof state:
κ : Cardinal.{w}
T : Language.empty.Theory
M N : T.ModelType
hM : #↑M = κ
hN : #↑N = κ
⊢ Nonempty (↑M ≃[Language.empty] ↑N)

Tactic:
rw [empty.nonempty_equiv_iff, hM, hN]

Result:
no goals
-- Mathlib/Data/Num/Lemmas.lean
theorem abs_to_nat : ∀ n, (abs n : ℕ) = Int.natAbs n
  | 0 => rfl
  | pos p => congr_arg Int.natAbs p.to_nat_to_int
  | neg p => show Int.natAbs ((p : ℕ) : ℤ) = Int.natAbs (-p) by rw [p.to_nat_to_int, Int.natAbs_neg]

Proof state:
p : PosNum
⊢ (↑↑p).natAbs = (-↑p).natAbs

Tactic:
rw [p.to_nat_to_int, Int.natAbs_neg]

Result:
no goals
-- Mathlib/Algebra/Ring/Ext.lean
theorem toRing_injective : Function.Injective (@toRing R)

Proof state:
R : Type u
⊢ Function.Injective (@toRing R)

Tactic:
rintro ⟨⟩ ⟨⟩ _

Result:
case mk.mk
R : Type u
toRing✝¹ : Ring R
mul_comm✝¹ : ∀ (a b : R), a * b = b * a
toRing✝ : Ring R
mul_comm✝ : ∀ (a b : R), a * b = b * a
a✝ : toRing = toRing
⊢ mk mul_comm✝¹ = mk mul_comm✝

Proof state:
case mk.mk
R : Type u
toRing✝¹ : Ring R
mul_comm✝¹ : ∀ (a b : R), a * b = b * a
toRing✝ : Ring R
mul_comm✝ : ∀ (a b : R), a * b = b * a
a✝ : toRing = toRing
⊢ mk mul_comm✝¹ = mk mul_comm✝

Tactic:
congr

Result:
no goals
-- Mathlib/RingTheory/PowerSeries/WellKnown.lean
theorem exp_mul_exp_eq_exp_add [Algebra ℚ A] (a b : A) :
    rescale a (exp A) * rescale b (exp A) = rescale (a + b) (exp A)

Proof state:
A : Type u_1
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
a b : A
n x : ℕ
hx : x ∈ Finset.range n.succ
this :
  a ^ x * b ^ (n - x) * ((algebraMap ℚ A) (1 / ↑x !) * (algebraMap ℚ A) (1 / ↑(n - x)!)) =
    a ^ x * b ^ (n - x) * (↑(n.choose x) * (algebraMap ℚ A) (1 / ↑n !))
⊢ a ^ x * (algebraMap ℚ A) (1 / ↑x !) * (b ^ (n - x) * (algebraMap ℚ A) (1 / ↑(n - x)!)) =
    a ^ x * b ^ (n - x) * ↑(n.choose x) * (algebraMap ℚ A) (1 / ↑n !)

Tactic:
convert this using 1 <;> ring

Result:
no goals

Proof state:
case h.e_a
A : Type u_1
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
a b : A
n x : ℕ
hx : x ∈ Finset.range n.succ
h : ↑n ! = 0
⊢ n ! = 0

Tactic:
rw [cast_eq_zero.1 h]

Result:
no goals

Proof state:
case h.e_a
A : Type u_1
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
a b : A
n x : ℕ
hx : x ∈ Finset.range n.succ
⊢ x ! * (n - x)! ∣ n !

Tactic:
apply factorial_mul_factorial_dvd_factorial (mem_range_succ_iff.1 hx)

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Internal/Order/Basic.lean
theorem fix_eq {f : α → α} (hf : monotone f) : fix f hf = f (fix f hf)

Proof state:
case a
α : Sort u
inst✝ : CCPO α
f : α → α
hf : monotone f
⊢ f (fix f hf) ⊑ fix f hf

Tactic:
apply le_csup (chain_iterates hf)

Result:
case a
α : Sort u
inst✝ : CCPO α
f : α → α
hf : monotone f
⊢ iterates f (f (fix f hf))

Proof state:
case a
α : Sort u
inst✝ : CCPO α
f : α → α
hf : monotone f
⊢ iterates f (fix f hf)

Tactic:
apply iterates.sup (chain_iterates hf)

Result:
case a
α : Sort u
inst✝ : CCPO α
f : α → α
hf : monotone f
⊢ ∀ (x : α), iterates f x → iterates f x

Proof state:
case a
α : Sort u
inst✝ : CCPO α
f : α → α
hf : monotone f
⊢ iterates f (f (fix f hf))

Tactic:
apply iterates.step

Result:
case a.a
α : Sort u
inst✝ : CCPO α
f : α → α
hf : monotone f
⊢ iterates f (fix f hf)

Proof state:
case a
α : Sort u
inst✝ : CCPO α
f : α → α
hf : monotone f
⊢ ∀ (x : α), iterates f x → iterates f x

Tactic:
exact fun _ h => h

Result:
no goals

Proof state:
case a.a
α : Sort u
inst✝ : CCPO α
f : α → α
hf : monotone f
⊢ iterates f (fix f hf)

Tactic:
apply iterates.sup (chain_iterates hf)

Result:
case a.a
α : Sort u
inst✝ : CCPO α
f : α → α
hf : monotone f
⊢ ∀ (x : α), iterates f x → iterates f x

Proof state:
case a.a
α : Sort u
inst✝ : CCPO α
f : α → α
hf : monotone f
y : α
hy : iterates f y
⊢ iterates f y

Tactic:
exact hy

Result:
no goals

Proof state:
case a
α : Sort u
inst✝ : CCPO α
f : α → α
hf : monotone f
⊢ fix f hf ⊑ f (fix f hf)

Tactic:
apply rel_f_of_iterates hf

Result:
case a
α : Sort u
inst✝ : CCPO α
f : α → α
hf : monotone f
⊢ iterates f (fix f hf)

Proof state:
case a.a
α : Sort u
inst✝ : CCPO α
f : α → α
hf : monotone f
⊢ ∀ (x : α), iterates f x → iterates f x

Tactic:
intro y hy

Result:
case a.a
α : Sort u
inst✝ : CCPO α
f : α → α
hf : monotone f
y : α
hy : iterates f y
⊢ iterates f y

Proof state:
α : Sort u
inst✝ : CCPO α
f : α → α
hf : monotone f
⊢ fix f hf = f (fix f hf)

Tactic:
apply rel_antisymm

Result:
case a
α : Sort u
inst✝ : CCPO α
f : α → α
hf : monotone f
⊢ fix f hf ⊑ f (fix f hf)

case a
α : Sort u
inst✝ : CCPO α
f : α → α
hf : monotone f
⊢ f (fix f hf) ⊑ fix f hf
-- Mathlib/Topology/Algebra/InfiniteSum/Nonarchimedean.lean
theorem HasSum.mul_of_nonarchimedean {f : α → R} {g : β → R} {a b : R} (hf : HasSum f a)
    (hg : HasSum g b) : HasSum (fun i : α × β ↦ f i.1 * g i.2) (a * b)

Proof state:
α : Type u_1
β : Type u_2
R : Type u_3
inst✝³ : Ring R
inst✝² : UniformSpace R
inst✝¹ : UniformAddGroup R
inst✝ : NonarchimedeanRing R
f : α → R
g : β → R
a b : R
hf : HasSum f a
hg : HasSum g b
⊢ HasSum (fun i => f i.1 * g i.2) (a * b)

Tactic:
rw [← hasSum_iff_hasSum_compl] at *

Result:
α : Type u_1
β : Type u_2
R : Type u_3
inst✝³ : Ring R
inst✝² : UniformSpace R
inst✝¹ : UniformAddGroup R
inst✝ : NonarchimedeanRing R
f : α → R
g : β → R
a b : R
hf : HasSum (⇑UniformSpace.Completion.toCompl ∘ f) ↑a
hg : HasSum (⇑UniformSpace.Completion.toCompl ∘ g) ↑b
⊢ HasSum (⇑UniformSpace.Completion.toCompl ∘ fun i => f i.1 * g i.2) ↑(a * b)

Proof state:
α : Type u_1
β : Type u_2
R : Type u_3
inst✝³ : Ring R
inst✝² : UniformSpace R
inst✝¹ : UniformAddGroup R
inst✝ : NonarchimedeanRing R
f : α → R
g : β → R
a b : R
hf : HasSum (⇑UniformSpace.Completion.toCompl ∘ f) ↑a
hg : HasSum (⇑UniformSpace.Completion.toCompl ∘ g) ↑b
⊢ HasSum (fun x => ↑(f x.1) * ↑(g x.2)) (↑a * ↑b)

Tactic:
exact (hf.mul hg) (hf.summable.mul_of_complete_nonarchimedean hg.summable :)

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
R : Type u_3
inst✝³ : Ring R
inst✝² : UniformSpace R
inst✝¹ : UniformAddGroup R
inst✝ : NonarchimedeanRing R
f : α → R
g : β → R
a b : R
hf : HasSum (⇑UniformSpace.Completion.toCompl ∘ f) ↑a
hg : HasSum (⇑UniformSpace.Completion.toCompl ∘ g) ↑b
⊢ HasSum (⇑UniformSpace.Completion.toCompl ∘ fun i => f i.1 * g i.2) ↑(a * b)

Tactic:
simp only [Function.comp_def, UniformSpace.Completion.toCompl_apply,
  UniformSpace.Completion.coe_mul]

Result:
α : Type u_1
β : Type u_2
R : Type u_3
inst✝³ : Ring R
inst✝² : UniformSpace R
inst✝¹ : UniformAddGroup R
inst✝ : NonarchimedeanRing R
f : α → R
g : β → R
a b : R
hf : HasSum (⇑UniformSpace.Completion.toCompl ∘ f) ↑a
hg : HasSum (⇑UniformSpace.Completion.toCompl ∘ g) ↑b
⊢ HasSum (fun x => ↑(f x.1) * ↑(g x.2)) (↑a * ↑b)
-- Mathlib/Order/Filter/Basic.lean
theorem eventuallyEq_univ {s : Set α} {l : Filter α} : s =ᶠ[l] univ ↔ s ∈ l

Proof state:
α : Type u
s : Set α
l : Filter α
⊢ s =ᶠ[l] univ ↔ s ∈ l

Tactic:
simp [eventuallyEq_set]

Result:
no goals
-- Mathlib/Data/Rat/Defs.lean
theorem add_mul : (a + b) * c = a * c + b * c :=
  numDenCasesOn' a fun n₁ d₁ h₁ ↦ numDenCasesOn' b fun n₂ d₂ h₂ ↦ numDenCasesOn' c fun n₃ d₃ h₃ ↦ by
    simp only [ne_eq, Int.natCast_eq_zero, h₁, not_false_eq_true, h₂, divInt_add_divInt,
      Int.mul_eq_zero, or_self, h₃, divInt_mul_divInt]
    rw [← divInt_mul_right (Int.natCast_ne_zero.2 h₃), Int.add_mul, Int.add_mul]
    ac_rfl

Proof state:
a b c : ℚ
n₁ : ℤ
d₁ : ℕ
h₁ : d₁ ≠ 0
n₂ : ℤ
d₂ : ℕ
h₂ : d₂ ≠ 0
n₃ : ℤ
d₃ : ℕ
h₃ : d₃ ≠ 0
⊢ (n₁ /. ↑d₁ + n₂ /. ↑d₂) * (n₃ /. ↑d₃) = n₁ /. ↑d₁ * (n₃ /. ↑d₃) + n₂ /. ↑d₂ * (n₃ /. ↑d₃)

Tactic:
simp only [ne_eq, Int.natCast_eq_zero, h₁, not_false_eq_true, h₂, divInt_add_divInt,
  Int.mul_eq_zero, or_self, h₃, divInt_mul_divInt]

Result:
a b c : ℚ
n₁ : ℤ
d₁ : ℕ
h₁ : d₁ ≠ 0
n₂ : ℤ
d₂ : ℕ
h₂ : d₂ ≠ 0
n₃ : ℤ
d₃ : ℕ
h₃ : d₃ ≠ 0
⊢ (n₁ * ↑d₂ + n₂ * ↑d₁) * n₃ /. (↑d₁ * ↑d₂ * ↑d₃) =
    (n₁ * n₃ * (↑d₂ * ↑d₃) + n₂ * n₃ * (↑d₁ * ↑d₃)) /. (↑d₁ * ↑d₃ * (↑d₂ * ↑d₃))

Proof state:
a b c : ℚ
n₁ : ℤ
d₁ : ℕ
h₁ : d₁ ≠ 0
n₂ : ℤ
d₂ : ℕ
h₂ : d₂ ≠ 0
n₃ : ℤ
d₃ : ℕ
h₃ : d₃ ≠ 0
⊢ (n₁ * ↑d₂ * n₃ * ↑d₃ + n₂ * ↑d₁ * n₃ * ↑d₃) /. (↑d₁ * ↑d₂ * ↑d₃ * ↑d₃) =
    (n₁ * n₃ * (↑d₂ * ↑d₃) + n₂ * n₃ * (↑d₁ * ↑d₃)) /. (↑d₁ * ↑d₃ * (↑d₂ * ↑d₃))

Tactic:
ac_rfl

Result:
no goals

Proof state:
a b c : ℚ
n₁ : ℤ
d₁ : ℕ
h₁ : d₁ ≠ 0
n₂ : ℤ
d₂ : ℕ
h₂ : d₂ ≠ 0
n₃ : ℤ
d₃ : ℕ
h₃ : d₃ ≠ 0
⊢ (n₁ * ↑d₂ + n₂ * ↑d₁) * n₃ /. (↑d₁ * ↑d₂ * ↑d₃) =
    (n₁ * n₃ * (↑d₂ * ↑d₃) + n₂ * n₃ * (↑d₁ * ↑d₃)) /. (↑d₁ * ↑d₃ * (↑d₂ * ↑d₃))

Tactic:
rw [← divInt_mul_right (Int.natCast_ne_zero.2 h₃), Int.add_mul, Int.add_mul]

Result:
a b c : ℚ
n₁ : ℤ
d₁ : ℕ
h₁ : d₁ ≠ 0
n₂ : ℤ
d₂ : ℕ
h₂ : d₂ ≠ 0
n₃ : ℤ
d₃ : ℕ
h₃ : d₃ ≠ 0
⊢ (n₁ * ↑d₂ * n₃ * ↑d₃ + n₂ * ↑d₁ * n₃ * ↑d₃) /. (↑d₁ * ↑d₂ * ↑d₃ * ↑d₃) =
    (n₁ * n₃ * (↑d₂ * ↑d₃) + n₂ * n₃ * (↑d₁ * ↑d₃)) /. (↑d₁ * ↑d₃ * (↑d₂ * ↑d₃))
-- Mathlib/Order/KrullDimension.lean
@[simp] lemma height_nat (n : ℕ) : height n = n

Proof state:
case ind.a
n : ℕ
ih : ∀ m < n, height m = ↑m
⊢ ∀ y < n, height y < ↑n

Tactic:
simp +contextual only [ih, Nat.cast_lt, implies_true]

Result:
no goals

Proof state:
case ind.a
n : ℕ
ih : ∀ m < n, height m = ↑m
⊢ ↑n ≤ height n

Tactic:
exact length_le_height_last (p := LTSeries.range n)

Result:
no goals

Proof state:
case ind
n : ℕ
ih : ∀ m < n, height m = ↑m
⊢ height n = ↑n

Tactic:
apply le_antisymm

Result:
case ind.a
n : ℕ
ih : ∀ m < n, height m = ↑m
⊢ height n ≤ ↑n

case ind.a
n : ℕ
ih : ∀ m < n, height m = ↑m
⊢ ↑n ≤ height n

Proof state:
case ind.a
n : ℕ
ih : ∀ m < n, height m = ↑m
⊢ height n ≤ ↑n

Tactic:
apply height_le_coe_iff.mpr

Result:
case ind.a
n : ℕ
ih : ∀ m < n, height m = ↑m
⊢ ∀ y < n, height y < ↑n
-- Mathlib/Combinatorics/SetFamily/LYM.lean
theorem card_div_choose_le_card_shadow_div_choose (hr : r ≠ 0)
    (h𝒜 : (𝒜 : Set (Finset α)).Sized r) : (#𝒜 : 𝕜) / (Fintype.card α).choose r
    ≤ #(∂ 𝒜) / (Fintype.card α).choose (r - 1)

Proof state:
𝕜 : Type u_1
α : Type u_2
inst✝² : LinearOrderedField 𝕜
inst✝¹ : DecidableEq α
inst✝ : Fintype α
𝒜 : Finset (Finset α)
r : ℕ
hr : r + 1 ≠ 0
hr' : r + 1 ≤ Fintype.card α
h𝒜 : #𝒜 * (r + 1) ≤ #(∂ 𝒜) * (Fintype.card α - r)
⊢ #𝒜 * (Fintype.card α).choose (r + 1 - 1) * (r + 1) ≤ #(∂ 𝒜) * (Fintype.card α).choose (r + 1) * (r + 1)

Tactic:
convert Nat.mul_le_mul_right ((Fintype.card α).choose r) h𝒜 using 1

Result:
case h.e'_3
𝕜 : Type u_1
α : Type u_2
inst✝² : LinearOrderedField 𝕜
inst✝¹ : DecidableEq α
inst✝ : Fintype α
𝒜 : Finset (Finset α)
r : ℕ
hr : r + 1 ≠ 0
hr' : r + 1 ≤ Fintype.card α
h𝒜 : #𝒜 * (r + 1) ≤ #(∂ 𝒜) * (Fintype.card α - r)
⊢ #𝒜 * (Fintype.card α).choose (r + 1 - 1) * (r + 1) = #𝒜 * (r + 1) * (Fintype.card α).choose r

case h.e'_4
𝕜 : Type u_1
α : Type u_2
inst✝² : LinearOrderedField 𝕜
inst✝¹ : DecidableEq α
inst✝ : Fintype α
𝒜 : Finset (Finset α)
r : ℕ
hr : r + 1 ≠ 0
hr' : r + 1 ≤ Fintype.card α
h𝒜 : #𝒜 * (r + 1) ≤ #(∂ 𝒜) * (Fintype.card α - r)
⊢ #(∂ 𝒜) * (Fintype.card α).choose (r + 1) * (r + 1) = #(∂ 𝒜) * (Fintype.card α - r) * (Fintype.card α).choose r

Proof state:
case inr.succ
𝕜 : Type u_1
α : Type u_2
inst✝² : LinearOrderedField 𝕜
inst✝¹ : DecidableEq α
inst✝ : Fintype α
𝒜 : Finset (Finset α)
r : ℕ
hr : r + 1 ≠ 0
hr' : r + 1 ≤ Fintype.card α
h𝒜 : #𝒜 * (r + 1) ≤ #(∂ 𝒜) * (Fintype.card α - r)
⊢ #𝒜 * (Fintype.card α).choose (r + 1 - 1) ≤ #(∂ 𝒜) * (Fintype.card α).choose (r + 1)

Tactic:
apply le_of_mul_le_mul_right _ (pos_iff_ne_zero.2 hr)

Result:
𝕜 : Type u_1
α : Type u_2
inst✝² : LinearOrderedField 𝕜
inst✝¹ : DecidableEq α
inst✝ : Fintype α
𝒜 : Finset (Finset α)
r : ℕ
hr : r + 1 ≠ 0
hr' : r + 1 ≤ Fintype.card α
h𝒜 : #𝒜 * (r + 1) ≤ #(∂ 𝒜) * (Fintype.card α - r)
⊢ #𝒜 * (Fintype.card α).choose (r + 1 - 1) * (r + 1) ≤ #(∂ 𝒜) * (Fintype.card α).choose (r + 1) * (r + 1)

Proof state:
case inl
𝕜 : Type u_1
α : Type u_2
inst✝² : LinearOrderedField 𝕜
inst✝¹ : DecidableEq α
inst✝ : Fintype α
𝒜 : Finset (Finset α)
r : ℕ
hr : r ≠ 0
h𝒜 : Set.Sized r ↑𝒜
hr' : Fintype.card α < r
⊢ 0 ≤ ↑(#(∂ 𝒜)) / ↑((Fintype.card α).choose (r - 1))

Tactic:
exact div_nonneg (cast_nonneg _) (cast_nonneg _)

Result:
no goals

Proof state:
case h.e'_4
𝕜 : Type u_1
α : Type u_2
inst✝² : LinearOrderedField 𝕜
inst✝¹ : DecidableEq α
inst✝ : Fintype α
𝒜 : Finset (Finset α)
r : ℕ
hr : r + 1 ≠ 0
hr' : r + 1 ≤ Fintype.card α
h𝒜 : #𝒜 * (r + 1) ≤ #(∂ 𝒜) * (Fintype.card α - r)
⊢ #(∂ 𝒜) * (Fintype.card α).choose (r + 1) * (r + 1) = #(∂ 𝒜) * (Fintype.card α - r) * (Fintype.card α).choose r

Tactic:
simp only [mul_assoc, choose_succ_right_eq, mul_eq_mul_left_iff]

Result:
case h.e'_4
𝕜 : Type u_1
α : Type u_2
inst✝² : LinearOrderedField 𝕜
inst✝¹ : DecidableEq α
inst✝ : Fintype α
𝒜 : Finset (Finset α)
r : ℕ
hr : r + 1 ≠ 0
hr' : r + 1 ≤ Fintype.card α
h𝒜 : #𝒜 * (r + 1) ≤ #(∂ 𝒜) * (Fintype.card α - r)
⊢ (Fintype.card α).choose r * (Fintype.card α - r) = (Fintype.card α - r) * (Fintype.card α).choose r ∨ #(∂ 𝒜) = 0
-- Mathlib/Algebra/MvPolynomial/Basic.lean
theorem constantCoeff_comp_C : constantCoeff.comp (C : R →+* MvPolynomial σ R) = RingHom.id R

Proof state:
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
⊢ constantCoeff.comp C = RingHom.id R

Tactic:
ext x

Result:
case a
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
x : R
⊢ (constantCoeff.comp C) x = (RingHom.id R) x

Proof state:
case a
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
x : R
⊢ (constantCoeff.comp C) x = (RingHom.id R) x

Tactic:
exact constantCoeff_C σ x

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Attach.lean
theorem pmap_pmap {p : α → Prop} {q : β → Prop} (g : ∀ a, p a → β) (f : ∀ b, q b → γ) (l : Vector α n) (H₁ H₂) :
    pmap f (pmap g l H₁) H₂ =
      pmap (α := { x // x ∈ l }) (fun a h => f (g a h) (H₂ (g a h) (mem_pmap_of_mem a.2))) l.attach
        (fun a _ => H₁ a a.2)

Proof state:
case mk
α : Type u_1
β : Type u_2
γ : Type u_3
p : α → Prop
q : β → Prop
g : (a : α) → p a → β
f : (b : β) → q b → γ
l : Array α
H₁ : ∀ (a : α), a ∈ { toArray := l, size_toArray := ⋯ } → p a
H₂ : ∀ (a : β), a ∈ pmap g { toArray := l, size_toArray := ⋯ } H₁ → q a
⊢ pmap f (pmap g { toArray := l, size_toArray := ⋯ } H₁) H₂ =
    pmap (fun a h => f (g a.val h) ⋯) { toArray := l, size_toArray := ⋯ }.attach ⋯

Tactic:
ext <;> simp

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
n : Nat
p : α → Prop
q : β → Prop
g : (a : α) → p a → β
f : (b : β) → q b → γ
l : Vector α n
H₁ : ∀ (a : α), a ∈ l → p a
H₂ : ∀ (a : β), a ∈ pmap g l H₁ → q a
⊢ pmap f (pmap g l H₁) H₂ = pmap (fun a h => f (g a.val h) ⋯) l.attach ⋯

Tactic:
rcases l with ⟨l, rfl⟩

Result:
case mk
α : Type u_1
β : Type u_2
γ : Type u_3
p : α → Prop
q : β → Prop
g : (a : α) → p a → β
f : (b : β) → q b → γ
l : Array α
H₁ : ∀ (a : α), a ∈ { toArray := l, size_toArray := ⋯ } → p a
H₂ : ∀ (a : β), a ∈ pmap g { toArray := l, size_toArray := ⋯ } H₁ → q a
⊢ pmap f (pmap g { toArray := l, size_toArray := ⋯ } H₁) H₂ =
    pmap (fun a h => f (g a.val h) ⋯) { toArray := l, size_toArray := ⋯ }.attach ⋯
-- Mathlib/RingTheory/RingHomProperties.lean
theorem IsStableUnderBaseChange.mk (h₁ : RespectsIso @P)
    (h₂ :
      ∀ ⦃R S T⦄ [CommRing R] [CommRing S] [CommRing T],
        ∀ [Algebra R S] [Algebra R T],
          P (algebraMap R T) →
            P (Algebra.TensorProduct.includeLeftRingHom : S →+* TensorProduct R S T)) :
    IsStableUnderBaseChange @P

Proof state:
case e_a.H
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
h₁ : RespectsIso P
h₂ :
  ∀ ⦃R S T : Type u⦄ [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : CommRing T] [inst_3 : Algebra R S]
    [inst_4 : Algebra R T], P (algebraMap R T) → P Algebra.TensorProduct.includeLeftRingHom
R S R' S' : Type u
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing S
inst✝⁸ : CommRing R'
inst✝⁷ : CommRing S'
inst✝⁶ : Algebra R S
inst✝⁵ : Algebra R R'
inst✝⁴ : Algebra R S'
inst✝³ : Algebra S S'
inst✝² : Algebra R' S'
inst✝¹ : IsScalarTower R S S'
inst✝ : IsScalarTower R R' S'
h : Algebra.IsPushout R S R' S'
H : P (algebraMap R S)
e : TensorProduct R R' S ≃ₛₗ[id R'] S' := ⋯.equiv
f' : TensorProduct R R' S →ₐ[R] S' :=
  Algebra.TensorProduct.productMap (IsScalarTower.toAlgHom R R' S') (IsScalarTower.toAlgHom R S S')
x✝ : TensorProduct R R' S
x : R'
y : S
⊢ (↑R ↑e) (x ⊗ₜ[R] y) = f'.toLinearMap (x ⊗ₜ[R] y)

Tactic:
simp [e, f', IsBaseChange.equiv_tmul, Algebra.smul_def]

Result:
no goals
-- Mathlib/Data/Finset/NoncommProd.lean
@[to_additive]
lemma noncommProd_induction (s : Finset α) (f : α → β) (comm)
    (p : β → Prop) (hom : ∀ a b, p a → p b → p (a * b)) (unit : p 1) (base : ∀ x ∈ s, p (f x)) :
    p (s.noncommProd f comm)

Proof state:
case intro.intro
α : Type u_3
β : Type u_4
inst✝ : Monoid β
s : Finset α
f : α → β
comm : (↑s).Pairwise (Commute on f)
p : β → Prop
hom : ∀ (a b : β), p a → p b → p (a * b)
unit : p 1
base : ∀ x ∈ s, p (f x)
a : α
ha : a ∈ s
hb : f a ∈ Multiset.map f s.val
⊢ p (f a)

Tactic:
exact base a ha

Result:
no goals

Proof state:
α : Type u_3
β : Type u_4
inst✝ : Monoid β
s : Finset α
f : α → β
comm : (↑s).Pairwise (Commute on f)
p : β → Prop
hom : ∀ (a b : β), p a → p b → p (a * b)
unit : p 1
base : ∀ x ∈ s, p (f x)
b : β
hb : b ∈ Multiset.map f s.val
⊢ p b

Tactic:
obtain (⟨a, ha : a ∈ s, rfl : f a = b⟩) := by simpa using hb

Result:
case intro.intro
α : Type u_3
β : Type u_4
inst✝ : Monoid β
s : Finset α
f : α → β
comm : (↑s).Pairwise (Commute on f)
p : β → Prop
hom : ∀ (a b : β), p a → p b → p (a * b)
unit : p 1
base : ∀ x ∈ s, p (f x)
a : α
ha : a ∈ s
hb : f a ∈ Multiset.map f s.val
⊢ p (f a)

Proof state:
α : Type u_3
β : Type u_4
inst✝ : Monoid β
s : Finset α
f : α → β
comm : (↑s).Pairwise (Commute on f)
p : β → Prop
hom : ∀ (a b : β), p a → p b → p (a * b)
unit : p 1
base : ∀ x ∈ s, p (f x)
⊢ p (s.noncommProd f comm)

Tactic:
refine Multiset.noncommProd_induction _ _ _ hom unit fun b hb ↦ ?_

Result:
α : Type u_3
β : Type u_4
inst✝ : Monoid β
s : Finset α
f : α → β
comm : (↑s).Pairwise (Commute on f)
p : β → Prop
hom : ∀ (a b : β), p a → p b → p (a * b)
unit : p 1
base : ∀ x ∈ s, p (f x)
b : β
hb : b ∈ Multiset.map f s.val
⊢ p b

Proof state:
α : Type u_3
β : Type u_4
inst✝ : Monoid β
s : Finset α
f : α → β
comm : (↑s).Pairwise (Commute on f)
p : β → Prop
hom : ∀ (a b : β), p a → p b → p (a * b)
unit : p 1
base : ∀ x ∈ s, p (f x)
b : β
hb : b ∈ Multiset.map f s.val
⊢ ?m.19078

Tactic:
simpa using hb

Result:
no goals
-- Mathlib/ModelTheory/Syntax.lean
theorem id_onBoundedFormula :
    ((LHom.id L).onBoundedFormula : L.BoundedFormula α n → L.BoundedFormula α n) = id

Proof state:
case h.equal
L : Language
α : Type u'
n n✝ : ℕ
t₁✝ t₂✝ : L.Term (α ⊕ Fin n✝)
⊢ (LHom.id L).onBoundedFormula (equal t₁✝ t₂✝) = id (equal t₁✝ t₂✝)

Tactic:
rw [onBoundedFormula, LHom.id_onTerm, id, id, id, Term.bdEqual]

Result:
no goals

Proof state:
case h.imp
L : Language
α : Type u'
n n✝ : ℕ
f₁✝ f₂✝ : L.BoundedFormula α n✝
ih1 : (LHom.id L).onBoundedFormula f₁✝ = id f₁✝
ih2 : (LHom.id L).onBoundedFormula f₂✝ = id f₂✝
⊢ (LHom.id L).onBoundedFormula (f₁✝.imp f₂✝) = id (f₁✝.imp f₂✝)

Tactic:
rw [onBoundedFormula, ih1, ih2, id, id, id]

Result:
no goals

Proof state:
case h
L : Language
α : Type u'
n : ℕ
f : L.BoundedFormula α n
⊢ (LHom.id L).onBoundedFormula f = id f

Tactic:
induction f with
| falsum => rfl
| equal => rw [onBoundedFormula, LHom.id_onTerm, id, id, id, Term.bdEqual]
| rel => rw [onBoundedFormula, LHom.id_onTerm]; rfl
| imp _ _ ih1 ih2 => rw [onBoundedFormula, ih1, ih2, id, id, id]
| all _ ih3 => rw [onBoundedFormula, ih3, id, id]

Result:
no goals

Proof state:
L : Language
α : Type u'
n : ℕ
⊢ (LHom.id L).onBoundedFormula = id

Tactic:
ext f

Result:
case h
L : Language
α : Type u'
n : ℕ
f : L.BoundedFormula α n
⊢ (LHom.id L).onBoundedFormula f = id f

Proof state:
case h.rel
L : Language
α : Type u'
n n✝ l✝ : ℕ
R✝ : L.Relations l✝
ts✝ : Fin l✝ → L.Term (α ⊕ Fin n✝)
⊢ (LHom.id L).onBoundedFormula (rel R✝ ts✝) = id (rel R✝ ts✝)

Tactic:
rw [onBoundedFormula, LHom.id_onTerm]

Result:
case h.rel
L : Language
α : Type u'
n n✝ l✝ : ℕ
R✝ : L.Relations l✝
ts✝ : Fin l✝ → L.Term (α ⊕ Fin n✝)
⊢ ((LHom.id L).onRelation R✝).boundedFormula (id ∘ ts✝) = id (rel R✝ ts✝)

Proof state:
case h.all
L : Language
α : Type u'
n n✝ : ℕ
f✝ : L.BoundedFormula α (n✝ + 1)
ih3 : (LHom.id L).onBoundedFormula f✝ = id f✝
⊢ (LHom.id L).onBoundedFormula f✝.all = id f✝.all

Tactic:
rw [onBoundedFormula, ih3, id, id]

Result:
no goals

Proof state:
case h.rel
L : Language
α : Type u'
n n✝ l✝ : ℕ
R✝ : L.Relations l✝
ts✝ : Fin l✝ → L.Term (α ⊕ Fin n✝)
⊢ ((LHom.id L).onRelation R✝).boundedFormula (id ∘ ts✝) = id (rel R✝ ts✝)

Tactic:
rfl

Result:
no goals

Proof state:
case h.falsum
L : Language
α : Type u'
n n✝ : ℕ
⊢ (LHom.id L).onBoundedFormula falsum = id falsum

Tactic:
rfl

Result:
no goals
-- Mathlib/Geometry/Euclidean/Sphere/Basic.lean
lemma IsDiameter.right_eq_of_isDiameter (h₁₂ : s.IsDiameter p₁ p₂) (h₁₃ : s.IsDiameter p₁ p₃) :
    p₂ = p₃

Proof state:
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : NormedSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
s : Sphere P
p₁ p₂ p₃ : P
h₁₂ : s.IsDiameter p₁ p₂
h₁₃ : s.IsDiameter p₁ p₃
⊢ p₂ = p₃

Tactic:
rw [← h₁₂.pointReflection_center_left, ← h₁₃.pointReflection_center_left]

Result:
no goals