harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/LinearAlgebra/Dual.lean
theorem coeffs_lc (l : ι →₀ R) : h.coeffs (DualBases.lc e l) = l

Proof state:
case h
R : Type u_1
M : Type u_2
ι : Type u_3
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
e : ι → M
ε : ι → Dual R M
h : DualBases e ε
l : ι →₀ R
i : ι
⊢ (h.coeffs (lc e l)) i = l i

Tactic:
rw [h.coeffs_apply, h.dual_lc]

Result:
no goals

Proof state:
R : Type u_1
M : Type u_2
ι : Type u_3
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
e : ι → M
ε : ι → Dual R M
h : DualBases e ε
l : ι →₀ R
⊢ h.coeffs (lc e l) = l

Tactic:
ext i

Result:
case h
R : Type u_1
M : Type u_2
ι : Type u_3
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
e : ι → M
ε : ι → Dual R M
h : DualBases e ε
l : ι →₀ R
i : ι
⊢ (h.coeffs (lc e l)) i = l i
-- Mathlib/Algebra/Polynomial/Coeff.lean
theorem coeff_mul_X (p : R[X]) (n : ℕ) : coeff (p * X) (n + 1) = coeff p n

Proof state:
R : Type u
inst✝ : Semiring R
p : R[X]
n : ℕ
⊢ (p * X).coeff (n + 1) = p.coeff n

Tactic:
simpa only [pow_one] using coeff_mul_X_pow p 1 n

Result:
no goals
-- Mathlib/Analysis/NormedSpace/Multilinear/Basic.lean
theorem norm_restr {k n : ℕ} (f : G[×n]→L[𝕜] G') (s : Finset (Fin n)) (hk : #s = k) (z : G) :
    ‖f.restr s hk z‖ ≤ ‖f‖ * ‖z‖ ^ (n - k)

Proof state:
𝕜 : Type u
G : Type wG
G' : Type wG'
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : SeminormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
inst✝¹ : SeminormedAddCommGroup G'
inst✝ : NormedSpace 𝕜 G'
k n : ℕ
f : ContinuousMultilinearMap 𝕜 (fun i => G) G'
s : Finset (Fin n)
hk : #s = k
z : G
⊢ ‖f.restr s hk z‖ ≤ ‖f‖ * ‖z‖ ^ (n - k)

Tactic:
apply MultilinearMap.mkContinuous_norm_le

Result:
case hC
𝕜 : Type u
G : Type wG
G' : Type wG'
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : SeminormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
inst✝¹ : SeminormedAddCommGroup G'
inst✝ : NormedSpace 𝕜 G'
k n : ℕ
f : ContinuousMultilinearMap 𝕜 (fun i => G) G'
s : Finset (Fin n)
hk : #s = k
z : G
⊢ 0 ≤ ‖f‖ * ‖z‖ ^ (n - k)

Proof state:
case hC
𝕜 : Type u
G : Type wG
G' : Type wG'
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : SeminormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
inst✝¹ : SeminormedAddCommGroup G'
inst✝ : NormedSpace 𝕜 G'
k n : ℕ
f : ContinuousMultilinearMap 𝕜 (fun i => G) G'
s : Finset (Fin n)
hk : #s = k
z : G
⊢ 0 ≤ ‖f‖ * ‖z‖ ^ (n - k)

Tactic:
exact mul_nonneg (norm_nonneg _) (pow_nonneg (norm_nonneg _) _)

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Nat/Bitwise/Lemmas.lean
theorem toNat_testBit (x i : Nat) :
    (x.testBit i).toNat = x / 2 ^ i % 2

Proof state:
x i : Nat
⊢ (decide (x / 2 ^ i % 2 = 1)).toNat = x / 2 ^ i % 2

Tactic:
rcases Nat.mod_two_eq_zero_or_one (x / 2^i) <;> simp_all

Result:
no goals

Proof state:
x i : Nat
⊢ (x.testBit i).toNat = x / 2 ^ i % 2

Tactic:
rw [Nat.testBit_to_div_mod]

Result:
x i : Nat
⊢ (decide (x / 2 ^ i % 2 = 1)).toNat = x / 2 ^ i % 2
-- Mathlib/CategoryTheory/Presentable/IsCardinalFiltered.lean
lemma hasCardinalLT_arrow_walkingParallelFamily {T : Type u}
    {κ : Cardinal.{w}} (hT : HasCardinalLT T κ) (hκ : Cardinal.aleph0 ≤ κ) :
    HasCardinalLT (Arrow (WalkingParallelFamily T)) κ

Proof state:
T : Type u
κ : Cardinal.{w}
hT : HasCardinalLT T κ
hκ : Cardinal.aleph0 ≤ κ
⊢ HasCardinalLT (Arrow (WalkingParallelFamily T)) κ

Tactic:
simpa only [hasCardinalLT_iff_of_equiv (WalkingParallelFamily.arrowEquiv T),
  hasCardinalLT_option_iff _ _ hκ] using hT

Result:
no goals
-- Mathlib/NumberTheory/DirichletCharacter/Basic.lean
lemma factorsThrough_one_iff : FactorsThrough χ 1 ↔ χ = 1

Proof state:
R : Type u_1
inst✝ : CommMonoidWithZero R
n : ℕ
χ : DirichletCharacter R n
h : χ = 1
⊢ χ = (changeLevel ⋯) 1

Tactic:
rw [h, changeLevel_one]

Result:
no goals

Proof state:
R : Type u_1
inst✝ : CommMonoidWithZero R
n : ℕ
χ : DirichletCharacter R n
⊢ χ.FactorsThrough 1 ↔ χ = 1

Tactic:
refine ⟨fun ⟨_, χ₀, hχ₀⟩ ↦ ?_,
        fun h ↦ ⟨one_dvd n, 1, by rw [h, changeLevel_one]⟩⟩

Result:
R : Type u_1
inst✝ : CommMonoidWithZero R
n : ℕ
χ : DirichletCharacter R n
x✝ : χ.FactorsThrough 1
w✝ : 1 ∣ n
χ₀ : DirichletCharacter R 1
hχ₀ : χ = (changeLevel w✝) χ₀
⊢ χ = 1

Proof state:
R : Type u_1
inst✝ : CommMonoidWithZero R
n : ℕ
χ : DirichletCharacter R n
x✝ : χ.FactorsThrough 1
w✝ : 1 ∣ n
χ₀ : DirichletCharacter R 1
hχ₀ : χ = (changeLevel w✝) χ₀
⊢ χ = 1

Tactic:
rwa [level_one χ₀, changeLevel_one] at hχ₀

Result:
no goals
-- Mathlib/Data/Int/Cast/Lemmas.lean
lemma MonoidHom.apply_mint (f : Multiplicative ℤ →* α) (n : Multiplicative ℤ) :
    f n = f (ofAdd 1) ^ n.toAdd

Proof state:
α : Type u_3
inst✝ : Group α
f : Multiplicative ℤ →* α
n : Multiplicative ℤ
⊢ f n = f (ofAdd 1) ^ toAdd n

Tactic:
rw [← zpowersHom_symm_apply, ← zpowersHom_apply, Equiv.apply_symm_apply]

Result:
no goals
-- Mathlib/NumberTheory/FactorisationProperties.lean
theorem deficient_three : Deficient 3

Proof state:
⊢ Deficient 3

Tactic:
norm_num [Deficient]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem anyM_stop_le_start [Monad m] (p : α → m Bool) (as : Array α) (start stop)
    (h : min stop as.size ≤ start) : anyM p as start stop = pure false

Proof state:
m : Type → Type u_1
α : Type u_2
inst✝ : Monad m
p : α → m Bool
as : Array α
start stop : Nat
h : min stop as.size ≤ start
⊢ anyM p as start stop = pure false

Tactic:
rw [anyM_eq_anyM_loop, anyM.loop, dif_neg (Nat.not_lt.2 h)]

Result:
no goals
-- Mathlib/Analysis/MeanInequalitiesPow.lean
theorem rpow_add_le_add_rpow {p : ℝ} (a b : ℝ≥0) (hp : 0 ≤ p) (hp1 : p ≤ 1) :
    (a + b) ^ p ≤ a ^ p + b ^ p

Proof state:
case inr
p : ℝ
a b : ℝ≥0
hp : 0 ≤ p
hp1 : p ≤ 1
hp_pos : 0 < p
h : (a ^ 1 + b ^ 1) ^ (1 / 1) ≤ (a ^ p + b ^ p) ^ (1 / p)
⊢ (a + b) ^ p ≤ a ^ p + b ^ p

Tactic:
rw [one_div_one, one_div] at h

Result:
case inr
p : ℝ
a b : ℝ≥0
hp : 0 ≤ p
hp1 : p ≤ 1
hp_pos : 0 < p
h : (a ^ 1 + b ^ 1) ^ 1 ≤ (a ^ p + b ^ p) ^ p⁻¹
⊢ (a + b) ^ p ≤ a ^ p + b ^ p

Proof state:
case inr
p : ℝ
a b : ℝ≥0
hp : 0 ≤ p
hp1 : p ≤ 1
hp_pos : 0 < p
h : (a ^ 1 + b ^ 1) ^ 1 ≤ (a ^ p + b ^ p) ^ p⁻¹
⊢ (a + b) ^ p ≤ a ^ p + b ^ p

Tactic:
repeat' rw [NNReal.rpow_one] at h

Result:
case inr
p : ℝ
a b : ℝ≥0
hp : 0 ≤ p
hp1 : p ≤ 1
hp_pos : 0 < p
h : a + b ≤ (a ^ p + b ^ p) ^ p⁻¹
⊢ (a + b) ^ p ≤ a ^ p + b ^ p

Proof state:
case inl
a b : ℝ≥0
hp : 0 ≤ 0
hp1 : 0 ≤ 1
⊢ (a + b) ^ 0 ≤ a ^ 0 + b ^ 0

Tactic:
simp

Result:
no goals

Proof state:
p : ℝ
a b : ℝ≥0
hp : 0 ≤ p
hp1 : p ≤ 1
⊢ (a + b) ^ p ≤ a ^ p + b ^ p

Tactic:
rcases hp.eq_or_lt with (rfl | hp_pos)

Result:
case inl
a b : ℝ≥0
hp : 0 ≤ 0
hp1 : 0 ≤ 1
⊢ (a + b) ^ 0 ≤ a ^ 0 + b ^ 0

case inr
p : ℝ
a b : ℝ≥0
hp : 0 ≤ p
hp1 : p ≤ 1
hp_pos : 0 < p
⊢ (a + b) ^ p ≤ a ^ p + b ^ p

Proof state:
case inr
p : ℝ
a b : ℝ≥0
hp : 0 ≤ p
hp1 : p ≤ 1
hp_pos : 0 < p
h : a + b ^ 1 ≤ (a ^ p + b ^ p) ^ p⁻¹
⊢ (a + b) ^ p ≤ a ^ p + b ^ p

Tactic:
rw [NNReal.rpow_one] at h

Result:
case inr
p : ℝ
a b : ℝ≥0
hp : 0 ≤ p
hp1 : p ≤ 1
hp_pos : 0 < p
h : a + b ≤ (a ^ p + b ^ p) ^ p⁻¹
⊢ (a + b) ^ p ≤ a ^ p + b ^ p

Proof state:
case inr
p : ℝ
a b : ℝ≥0
hp : 0 ≤ p
hp1 : p ≤ 1
hp_pos : 0 < p
h : a + b ≤ (a ^ p + b ^ p) ^ p⁻¹
⊢ (a + b) ^ p ≤ a ^ p + b ^ p

Tactic:
exact (NNReal.le_rpow_inv_iff hp_pos).mp h

Result:
no goals

Proof state:
case inr
p : ℝ
a b : ℝ≥0
hp : 0 ≤ p
hp1 : p ≤ 1
hp_pos : 0 < p
⊢ (a + b) ^ p ≤ a ^ p + b ^ p

Tactic:
have h := rpow_add_rpow_le a b hp_pos hp1

Result:
case inr
p : ℝ
a b : ℝ≥0
hp : 0 ≤ p
hp1 : p ≤ 1
hp_pos : 0 < p
h : (a ^ 1 + b ^ 1) ^ (1 / 1) ≤ (a ^ p + b ^ p) ^ (1 / p)
⊢ (a + b) ^ p ≤ a ^ p + b ^ p
-- Mathlib/LinearAlgebra/QuadraticForm/TensorProduct.lean
theorem polarBilin_tmul [Invertible (2 : A)] (Q₁ : QuadraticForm A M₁) (Q₂ : QuadraticForm R M₂) :
    polarBilin (Q₁.tmul Q₂) = ⅟(2 : A) • BilinForm.tmul (polarBilin Q₁) (polarBilin Q₂)

Proof state:
R : Type uR
A : Type uA
M₁ : Type uM₁
M₂ : Type uM₂
inst✝¹¹ : CommRing R
inst✝¹⁰ : CommRing A
inst✝⁹ : AddCommGroup M₁
inst✝⁸ : AddCommGroup M₂
inst✝⁷ : Algebra R A
inst✝⁶ : Module R M₁
inst✝⁵ : Module A M₁
inst✝⁴ : SMulCommClass R A M₁
inst✝³ : IsScalarTower R A M₁
inst✝² : Module R M₂
inst✝¹ : Invertible 2
inst✝ : Invertible 2
Q₁ : QuadraticForm A M₁
Q₂ : QuadraticForm R M₂
⊢ polarBilin (Q₁.tmul Q₂) = ⅟2 • BilinForm.tmul (polarBilin Q₁) (polarBilin Q₂)

Tactic:
simp_rw [← two_nsmul_associated A, ← two_nsmul_associated R, BilinForm.tmul, tmul_smul,
  ← smul_tmul', map_nsmul, associated_tmul]

Result:
R : Type uR
A : Type uA
M₁ : Type uM₁
M₂ : Type uM₂
inst✝¹¹ : CommRing R
inst✝¹⁰ : CommRing A
inst✝⁹ : AddCommGroup M₁
inst✝⁸ : AddCommGroup M₂
inst✝⁷ : Algebra R A
inst✝⁶ : Module R M₁
inst✝⁵ : Module A M₁
inst✝⁴ : SMulCommClass R A M₁
inst✝³ : IsScalarTower R A M₁
inst✝² : Module R M₂
inst✝¹ : Invertible 2
inst✝ : Invertible 2
Q₁ : QuadraticForm A M₁
Q₂ : QuadraticForm R M₂
⊢ 2 • BilinForm.tmul (associated Q₁) (associated Q₂) =
    ⅟2 • 2 • 2 • (BilinForm.tensorDistrib R A) ((associatedHom A) Q₁ ⊗ₜ[R] (associatedHom R) Q₂)

Proof state:
R : Type uR
A : Type uA
M₁ : Type uM₁
M₂ : Type uM₂
inst✝¹¹ : CommRing R
inst✝¹⁰ : CommRing A
inst✝⁹ : AddCommGroup M₁
inst✝⁸ : AddCommGroup M₂
inst✝⁷ : Algebra R A
inst✝⁶ : Module R M₁
inst✝⁵ : Module A M₁
inst✝⁴ : SMulCommClass R A M₁
inst✝³ : IsScalarTower R A M₁
inst✝² : Module R M₂
inst✝¹ : Invertible 2
inst✝ : Invertible 2
Q₁ : QuadraticForm A M₁
Q₂ : QuadraticForm R M₂
⊢ 2 • BilinForm.tmul (associated Q₁) (associated Q₂) =
    ⅟2 • 2 • 2 • (BilinForm.tensorDistrib R A) ((associatedHom A) Q₁ ⊗ₜ[R] (associatedHom R) Q₂)

Tactic:
rw [smul_comm (_ : A) (_ : ℕ), ← smul_assoc, two_smul _ (_ : A), invOf_two_add_invOf_two,
  one_smul]

Result:
no goals
-- Mathlib/FieldTheory/Separable.lean
theorem emultiplicity_le_one_of_separable {p q : R[X]} (hq : ¬IsUnit q) (hsep : Separable p) :
    emultiplicity q p ≤ 1

Proof state:
R : Type u
inst✝ : CommSemiring R
p q : R[X]
hq : ¬IsUnit q
hsep : p.Separable
⊢ emultiplicity q p ≤ 1

Tactic:
contrapose! hq

Result:
R : Type u
inst✝ : CommSemiring R
p q : R[X]
hsep : p.Separable
hq : 1 < emultiplicity q p
⊢ IsUnit q

Proof state:
R : Type u
inst✝ : CommSemiring R
p q : R[X]
hsep : p.Separable
hq : 1 < emultiplicity q p
⊢ q ^ 2 ∣ p

Tactic:
apply pow_dvd_of_le_emultiplicity

Result:
case hk
R : Type u
inst✝ : CommSemiring R
p q : R[X]
hsep : p.Separable
hq : 1 < emultiplicity q p
⊢ ↑2 ≤ emultiplicity q p

Proof state:
case hk
R : Type u
inst✝ : CommSemiring R
p q : R[X]
hsep : p.Separable
hq : 1 < emultiplicity q p
⊢ ↑2 ≤ emultiplicity q p

Tactic:
exact Order.add_one_le_of_lt hq

Result:
no goals

Proof state:
R : Type u
inst✝ : CommSemiring R
p q : R[X]
hsep : p.Separable
hq : 1 < emultiplicity q p
⊢ IsUnit q

Tactic:
apply isUnit_of_self_mul_dvd_separable hsep

Result:
R : Type u
inst✝ : CommSemiring R
p q : R[X]
hsep : p.Separable
hq : 1 < emultiplicity q p
⊢ q * q ∣ p

Proof state:
R : Type u
inst✝ : CommSemiring R
p q : R[X]
hsep : p.Separable
hq : 1 < emultiplicity q p
⊢ q * q ∣ p

Tactic:
rw [← sq]

Result:
R : Type u
inst✝ : CommSemiring R
p q : R[X]
hsep : p.Separable
hq : 1 < emultiplicity q p
⊢ q ^ 2 ∣ p
-- Mathlib/Data/Fin/Tuple/Sort.lean
theorem sort_eq_refl_iff_monotone : sort f = Equiv.refl _ ↔ Monotone f

Proof state:
n : ℕ
α : Type u_1
inst✝ : LinearOrder α
f : Fin n → α
⊢ sort f = Equiv.refl (Fin n) ↔ Monotone f

Tactic:
rw [eq_comm, eq_sort_iff, Equiv.coe_refl, Function.comp_id]

Result:
n : ℕ
α : Type u_1
inst✝ : LinearOrder α
f : Fin n → α
⊢ (Monotone f ∧ ∀ (i j : Fin n), i < j → f (id i) = f (id j) → id i < id j) ↔ Monotone f

Proof state:
n : ℕ
α : Type u_1
inst✝ : LinearOrder α
f : Fin n → α
⊢ (Monotone f ∧ ∀ (i j : Fin n), i < j → f (id i) = f (id j) → id i < id j) ↔ Monotone f

Tactic:
simp only [id, and_iff_left_iff_imp]

Result:
n : ℕ
α : Type u_1
inst✝ : LinearOrder α
f : Fin n → α
⊢ Monotone f → ∀ (i j : Fin n), i < j → f i = f j → i < j

Proof state:
n : ℕ
α : Type u_1
inst✝ : LinearOrder α
f : Fin n → α
⊢ Monotone f → ∀ (i j : Fin n), i < j → f i = f j → i < j

Tactic:
exact fun _ _ _ hij _ => hij

Result:
no goals
-- Mathlib/Probability/Moments/IntegrableExpMul.lean
/-- If `ω ↦ exp (u * X ω)` is integrable at `u ≥ 0`, then it is integrable on `[0, u]`. -/
lemma integrable_exp_mul_of_nonneg_of_le [IsFiniteMeasure μ]
    (hu : Integrable (fun ω ↦ exp (u * X ω)) μ) (h_nonneg : 0 ≤ t) (htu : t ≤ u) :
    Integrable (fun ω ↦ exp (t * X ω)) μ :=
  integrable_exp_mul_of_le_of_le (by simp) hu h_nonneg htu

Proof state:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t u : ℝ
inst✝ : IsFiniteMeasure μ
hu : Integrable (fun ω => rexp (u * X ω)) μ
h_nonneg : 0 ≤ t
htu : t ≤ u
⊢ Integrable (fun ω => rexp (0 * X ω)) μ

Tactic:
simp

Result:
no goals
-- Mathlib/Analysis/Analytic/Order.lean
/-- The order of an analytic function `f` at `z₀` is finite iff `f` can locally be written as
`f z = (z - z₀) ^ order • g z`, where `g` is analytic and does not vanish at `z₀`. -/
lemma order_ne_top_iff (hf : AnalyticAt 𝕜 f z₀) :
    hf.order ≠ ⊤ ↔ ∃ (g : 𝕜 → E), AnalyticAt 𝕜 g z₀ ∧ g z₀ ≠ 0
      ∧ f =ᶠ[𝓝 z₀] fun z ↦ (z - z₀) ^ (hf.order.toNat) • g z

Proof state:
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
z₀ : 𝕜
hf : AnalyticAt 𝕜 f z₀
⊢ hf.order ≠ ⊤ ↔ ∃ g, AnalyticAt 𝕜 g z₀ ∧ g z₀ ≠ 0 ∧ f =ᶠ[𝓝 z₀] fun z => (z - z₀) ^ hf.order.toNat • g z

Tactic:
simp only [← ENat.coe_toNat_eq_self, Eq.comm, EventuallyEq, ← hf.order_eq_nat_iff]

Result:
no goals
-- Mathlib/Data/Real/Archimedean.lean
theorem iInf_const_zero : ⨅ _ : ι, (0 : ℝ) = 0

Proof state:
case inr
ι : Sort u_1
h✝ : Nonempty ι
⊢ ⨅ x, 0 = 0

Tactic:
exact ciInf_const

Result:
no goals

Proof state:
ι : Sort u_1
⊢ ⨅ x, 0 = 0

Tactic:
cases isEmpty_or_nonempty ι

Result:
case inl
ι : Sort u_1
h✝ : IsEmpty ι
⊢ ⨅ x, 0 = 0

case inr
ι : Sort u_1
h✝ : Nonempty ι
⊢ ⨅ x, 0 = 0

Proof state:
case inl
ι : Sort u_1
h✝ : IsEmpty ι
⊢ ⨅ x, 0 = 0

Tactic:
exact Real.iInf_of_isEmpty _

Result:
no goals
-- Mathlib/Algebra/Module/Submodule/Ker.lean
theorem ker_sup_ker_le_ker_comp_of_commute {f g : M →ₗ[R] M} (h : Commute f g) :
    ker f ⊔ ker g ≤ ker (f ∘ₗ g)

Proof state:
R : Type u_1
M : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
f g : M →ₗ[R] M
h : Commute f g
⊢ ker f ⊔ ker g ≤ ker (f ∘ₗ g)

Tactic:
refine sup_le_iff.mpr ⟨?_, ker_le_ker_comp g f⟩

Result:
R : Type u_1
M : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
f g : M →ₗ[R] M
h : Commute f g
⊢ ker f ≤ ker (f ∘ₗ g)

Proof state:
R : Type u_1
M : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
f g : M →ₗ[R] M
h : Commute f g
⊢ ker f ≤ ker (g ∘ₗ f)

Tactic:
exact ker_le_ker_comp f g

Result:
no goals

Proof state:
R : Type u_1
M : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
f g : M →ₗ[R] M
h : Commute f g
⊢ ker f ≤ ker (f ∘ₗ g)

Tactic:
rw [← mul_eq_comp, h.eq, mul_eq_comp]

Result:
R : Type u_1
M : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
f g : M →ₗ[R] M
h : Commute f g
⊢ ker f ≤ ker (g ∘ₗ f)
-- Mathlib/FieldTheory/RatFunc/Degree.lean
theorem intDegree_X : intDegree (X : RatFunc K) = 1

Proof state:
K : Type u
inst✝ : Field K
⊢ X.intDegree = 1

Tactic:
rw [intDegree, num_X, Polynomial.natDegree_X, denom_X, Polynomial.natDegree_one,
  Int.ofNat_one, Int.ofNat_zero, sub_zero]

Result:
no goals
-- Mathlib/Order/CompleteBooleanAlgebra.lean
theorem sSup_inf_eq : sSup s ⊓ b = ⨆ a ∈ s, a ⊓ b

Proof state:
α : Type u
inst✝ : Frame α
s : Set α
b : α
⊢ sSup s ⊓ b = ⨆ a ∈ s, a ⊓ b

Tactic:
simpa only [inf_comm] using @inf_sSup_eq α _ s b

Result:
no goals
-- Mathlib/Data/Set/Finite/Basic.lean
/-- If a linear order does not contain any triple of elements `x < y < z`, then this type
is finite. -/
lemma Finite.of_forall_not_lt_lt (h : ∀ ⦃x y z : α⦄, x < y → y < z → False) : Finite α

Proof state:
α : Type u
inst✝ : LinearOrder α
h : ∀ ⦃x y z : α⦄, x < y → y < z → False
a✝ : Nontrivial α
⊢ Finite α

Tactic:
rcases exists_pair_ne α with ⟨x, y, hne⟩

Result:
case intro.intro
α : Type u
inst✝ : LinearOrder α
h : ∀ ⦃x y z : α⦄, x < y → y < z → False
a✝ : Nontrivial α
x y : α
hne : x ≠ y
⊢ Finite α

Proof state:
case intro.intro
α : Type u
inst✝ : LinearOrder α
h : ∀ ⦃x y z : α⦄, x < y → y < z → False
a✝ : Nontrivial α
x y : α
hne : x ≠ y
z : α
⊢ z ∈ {x, y}

Tactic:
simpa [hne] using eq_or_eq_or_eq_of_forall_not_lt_lt h z x y

Result:
no goals

Proof state:
case intro.intro
α : Type u
inst✝ : LinearOrder α
h : ∀ ⦃x y z : α⦄, x < y → y < z → False
a✝ : Nontrivial α
x y : α
hne : x ≠ y
⊢ Finite α

Tactic:
refine @Finite.of_fintype α ⟨{x, y}, fun z => ?_⟩

Result:
case intro.intro
α : Type u
inst✝ : LinearOrder α
h : ∀ ⦃x y z : α⦄, x < y → y < z → False
a✝ : Nontrivial α
x y : α
hne : x ≠ y
z : α
⊢ z ∈ {x, y}

Proof state:
α : Type u
inst✝ : LinearOrder α
h : ∀ ⦃x y z : α⦄, x < y → y < z → False
⊢ Finite α

Tactic:
nontriviality α

Result:
α : Type u
inst✝ : LinearOrder α
h : ∀ ⦃x y z : α⦄, x < y → y < z → False
a✝ : Nontrivial α
⊢ Finite α
-- Mathlib/ModelTheory/Satisfiability.lean
theorem exists_elementarilyEquivalent_card_eq (M : Type w') [L.Structure M] [Infinite M]
    (κ : Cardinal.{w}) (h1 : ℵ₀ ≤ κ) (h2 : lift.{w} L.card ≤ Cardinal.lift.{max u v} κ) :
    ∃ N : CategoryTheory.Bundled L.Structure, (M ≅[L] N) ∧ #N = κ

Proof state:
case intro.intro.inl
L : Language
M : Type w'
inst✝¹ : L.Structure M
inst✝ : Infinite M
κ : Cardinal.{w}
h1 : ℵ₀ ≤ κ
h2 : lift.{w, max u v} L.card ≤ lift.{max u v, w} κ
N : Bundled L.Structure
hNκ : #↑N = κ
NM : Nonempty (↑N ↪ₑ[L] M)
⊢ ∃ N, (M ≅[L] ↑N) ∧ #↑N = κ

Tactic:
exact ⟨N, NM.some.elementarilyEquivalent.symm, hNκ⟩

Result:
no goals

Proof state:
L : Language
M : Type w'
inst✝¹ : L.Structure M
inst✝ : Infinite M
κ : Cardinal.{w}
h1 : ℵ₀ ≤ κ
h2 : lift.{w, max u v} L.card ≤ lift.{max u v, w} κ
⊢ ∃ N, (M ≅[L] ↑N) ∧ #↑N = κ

Tactic:
obtain ⟨N, NM | MN, hNκ⟩ := exists_elementaryEmbedding_card_eq L M κ h1 h2

Result:
case intro.intro.inl
L : Language
M : Type w'
inst✝¹ : L.Structure M
inst✝ : Infinite M
κ : Cardinal.{w}
h1 : ℵ₀ ≤ κ
h2 : lift.{w, max u v} L.card ≤ lift.{max u v, w} κ
N : Bundled L.Structure
hNκ : #↑N = κ
NM : Nonempty (↑N ↪ₑ[L] M)
⊢ ∃ N, (M ≅[L] ↑N) ∧ #↑N = κ

case intro.intro.inr
L : Language
M : Type w'
inst✝¹ : L.Structure M
inst✝ : Infinite M
κ : Cardinal.{w}
h1 : ℵ₀ ≤ κ
h2 : lift.{w, max u v} L.card ≤ lift.{max u v, w} κ
N : Bundled L.Structure
hNκ : #↑N = κ
MN : Nonempty (M ↪ₑ[L] ↑N)
⊢ ∃ N, (M ≅[L] ↑N) ∧ #↑N = κ

Proof state:
case intro.intro.inr
L : Language
M : Type w'
inst✝¹ : L.Structure M
inst✝ : Infinite M
κ : Cardinal.{w}
h1 : ℵ₀ ≤ κ
h2 : lift.{w, max u v} L.card ≤ lift.{max u v, w} κ
N : Bundled L.Structure
hNκ : #↑N = κ
MN : Nonempty (M ↪ₑ[L] ↑N)
⊢ ∃ N, (M ≅[L] ↑N) ∧ #↑N = κ

Tactic:
exact ⟨N, MN.some.elementarilyEquivalent, hNκ⟩

Result:
no goals
-- Mathlib/RingTheory/Polynomial/Basic.lean
theorem disjoint_ker_aeval_of_isCoprime (f : M →ₗ[R] M) {p q : R[X]} (hpq : IsCoprime p q) :
    Disjoint (LinearMap.ker (aeval f p)) (LinearMap.ker (aeval f q))

Proof state:
case intro.intro
R : Type u
M : Type w
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : M →ₗ[R] M
p q : R[X]
v : M
hv : v ∈ LinearMap.ker ((aeval f) p) ⊓ LinearMap.ker ((aeval f) q)
p' q' : R[X]
hpq' : p' * p + q' * q = 1
⊢ v ∈ ⊥

Tactic:
simpa [LinearMap.mem_ker.1 (Submodule.mem_inf.1 hv).1,
  LinearMap.mem_ker.1 (Submodule.mem_inf.1 hv).2] using
  congr_arg (fun p : R[X] => aeval f p v) hpq'.symm

Result:
no goals

Proof state:
R : Type u
M : Type w
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : M →ₗ[R] M
p q : R[X]
hpq : IsCoprime p q
v : M
hv : v ∈ LinearMap.ker ((aeval f) p) ⊓ LinearMap.ker ((aeval f) q)
⊢ v ∈ ⊥

Tactic:
rcases hpq with ⟨p', q', hpq'⟩

Result:
case intro.intro
R : Type u
M : Type w
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : M →ₗ[R] M
p q : R[X]
v : M
hv : v ∈ LinearMap.ker ((aeval f) p) ⊓ LinearMap.ker ((aeval f) q)
p' q' : R[X]
hpq' : p' * p + q' * q = 1
⊢ v ∈ ⊥

Proof state:
R : Type u
M : Type w
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : M →ₗ[R] M
p q : R[X]
hpq : IsCoprime p q
⊢ Disjoint (LinearMap.ker ((aeval f) p)) (LinearMap.ker ((aeval f) q))

Tactic:
rw [disjoint_iff_inf_le]

Result:
R : Type u
M : Type w
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : M →ₗ[R] M
p q : R[X]
hpq : IsCoprime p q
⊢ LinearMap.ker ((aeval f) p) ⊓ LinearMap.ker ((aeval f) q) ≤ ⊥

Proof state:
R : Type u
M : Type w
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : M →ₗ[R] M
p q : R[X]
hpq : IsCoprime p q
⊢ LinearMap.ker ((aeval f) p) ⊓ LinearMap.ker ((aeval f) q) ≤ ⊥

Tactic:
intro v hv

Result:
R : Type u
M : Type w
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : M →ₗ[R] M
p q : R[X]
hpq : IsCoprime p q
v : M
hv : v ∈ LinearMap.ker ((aeval f) p) ⊓ LinearMap.ker ((aeval f) q)
⊢ v ∈ ⊥
-- Mathlib/Algebra/Category/Grp/Limits.lean
theorem kernelIsoKer_hom_comp_subtype {G H : AddCommGrp.{u}} (f : G ⟶ H) :
    (kernelIsoKer f).hom ≫ ofHom (AddSubgroup.subtype f.hom.ker) = kernel.ι f

Proof state:
case hf.h
G H : AddCommGrp
f : G ⟶ H
x✝ : ↑(kernel f)
⊢ (Hom.hom ((kernelIsoKer f).hom ≫ ofHom (Hom.hom f).ker.subtype)) x✝ = (Hom.hom (kernel.ι f)) x✝

Tactic:
rfl

Result:
no goals

Proof state:
G H : AddCommGrp
f : G ⟶ H
⊢ (kernelIsoKer f).hom ≫ ofHom (Hom.hom f).ker.subtype = kernel.ι f

Tactic:
ext

Result:
case hf.h
G H : AddCommGrp
f : G ⟶ H
x✝ : ↑(kernel f)
⊢ (Hom.hom ((kernelIsoKer f).hom ≫ ofHom (Hom.hom f).ker.subtype)) x✝ = (Hom.hom (kernel.ι f)) x✝
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem getElem?_push_lt (a : Array α) (x : α) (i : Nat) (h : i < a.size) :
    (a.push x)[i]? = some a[i]

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

Tactic:
rw [getElem?_pos, getElem_push_lt]

Result:
no goals
-- Mathlib/MeasureTheory/Integral/IntegralEqImproper.lean
theorem aecover_ball {x : α} {r : ι → ℝ} (hr : Tendsto r l atTop) :
    AECover μ l (fun i ↦ Metric.ball x (r i)) where
  measurableSet _ := Metric.isOpen_ball.measurableSet
  ae_eventually_mem

Proof state:
α : Type u_1
ι : Type u_2
inst✝² : MeasurableSpace α
μ : Measure α
l : Filter ι
inst✝¹ : PseudoMetricSpace α
inst✝ : OpensMeasurableSpace α
x : α
r : ι → ℝ
hr : Tendsto r l atTop
⊢ ∀ᵐ (x_1 : α) ∂μ, ∀ᶠ (i : ι) in l, x_1 ∈ Metric.ball x (r i)

Tactic:
filter_upwards with y

Result:
case h
α : Type u_1
ι : Type u_2
inst✝² : MeasurableSpace α
μ : Measure α
l : Filter ι
inst✝¹ : PseudoMetricSpace α
inst✝ : OpensMeasurableSpace α
x : α
r : ι → ℝ
hr : Tendsto r l atTop
y : α
⊢ ∀ᶠ (i : ι) in l, y ∈ Metric.ball x (r i)

Proof state:
α : Type u_1
ι : Type u_2
inst✝² : MeasurableSpace α
μ : Measure α
l : Filter ι
inst✝¹ : PseudoMetricSpace α
inst✝ : OpensMeasurableSpace α
x : α
r : ι → ℝ
hr : Tendsto r l atTop
y : α
a : ι
ha : a ∈ r ⁻¹' Ioi (dist x y)
⊢ y ∈ Metric.ball x (r a)

Tactic:
simpa [dist_comm] using ha

Result:
no goals

Proof state:
case h
α : Type u_1
ι : Type u_2
inst✝² : MeasurableSpace α
μ : Measure α
l : Filter ι
inst✝¹ : PseudoMetricSpace α
inst✝ : OpensMeasurableSpace α
x : α
r : ι → ℝ
hr : Tendsto r l atTop
y : α
⊢ ∀ᶠ (i : ι) in l, y ∈ Metric.ball x (r i)

Tactic:
filter_upwards [hr (Ioi_mem_atTop (dist x y))] with a ha using by simpa [dist_comm] using ha

Result:
no goals
-- Mathlib/CategoryTheory/Closed/Monoidal.lean
lemma curry'_comp {X Y Z : C} [Closed X] [Closed Y] (f : X ⟶ Y) (g : Y ⟶ Z) :
    curry' (f ≫ g) = (λ_ (𝟙_ C)).inv ≫ (curry' f ⊗ curry' g) ≫ comp X Y Z

Proof state:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : MonoidalCategory C
X Y Z : C
inst✝¹ : Closed X
inst✝ : Closed Y
f : X ⟶ Y
g : Y ⟶ Z
⊢ curry' (f ≫ g) = (λ_ (𝟙_ C)).inv ≫ (curry' f ⊗ curry' g) ≫ comp X Y Z

Tactic:
rw [tensorHom_def_assoc, whiskerLeft_curry'_comp, MonoidalCategory.whiskerRight_id,
  Category.assoc, Category.assoc, Iso.inv_hom_id_assoc, ← unitors_equal,
  Iso.inv_hom_id_assoc, curry'_ihom_map]

Result:
no goals