harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Algebra/Order/Antidiag/Pi.lean
lemma map_nsmul_piAntidiag (s : Finset ι) (m : ℕ) {n : ℕ} (hn : n ≠ 0) :
    (piAntidiag s m).map
      ⟨(n • ·), fun _ _ h ↦ funext fun i ↦ mul_right_injective₀ hn (congr_fun h i)⟩ =
        (piAntidiag s (n * m)).filter fun f : ι → ℕ ↦ ∀ i ∈ s, n ∣ f i

Proof state:
ι : Type u_1
inst✝ : DecidableEq ι
s : Finset ι
m n : ℕ
hn : n ≠ 0
⊢ map { toFun := fun x => n • x, inj' := ⋯ } (s.piAntidiag m) =
    filter (fun f => ∀ i ∈ s, n ∣ f i) (s.piAntidiag (n * m))

Tactic:
classical rw [map_eq_image]; exact nsmul_piAntidiag _ _ hn

Result:
no goals

Proof state:
ι : Type u_1
inst✝ : DecidableEq ι
s : Finset ι
m n : ℕ
hn : n ≠ 0
⊢ map { toFun := fun x => n • x, inj' := ⋯ } (s.piAntidiag m) =
    filter (fun f => ∀ i ∈ s, n ∣ f i) (s.piAntidiag (n * m))

Tactic:
rw [map_eq_image]

Result:
ι : Type u_1
inst✝ : DecidableEq ι
s : Finset ι
m n : ℕ
hn : n ≠ 0
⊢ image (⇑{ toFun := fun x => n • x, inj' := ⋯ }) (s.piAntidiag m) =
    filter (fun f => ∀ i ∈ s, n ∣ f i) (s.piAntidiag (n * m))

Proof state:
ι : Type u_1
inst✝ : DecidableEq ι
s : Finset ι
m n : ℕ
hn : n ≠ 0
⊢ image (⇑{ toFun := fun x => n • x, inj' := ⋯ }) (s.piAntidiag m) =
    filter (fun f => ∀ i ∈ s, n ∣ f i) (s.piAntidiag (n * m))

Tactic:
exact nsmul_piAntidiag _ _ hn

Result:
no goals
-- Mathlib/Topology/Algebra/InfiniteSum/Real.lean
theorem summable_of_sum_range_le {f : ℕ → ℝ} {c : ℝ} (hf : ∀ n, 0 ≤ f n)
    (h : ∀ n, ∑ i ∈ Finset.range n, f i ≤ c) : Summable f

Proof state:
f : ℕ → ℝ
c : ℝ
hf : ∀ (n : ℕ), 0 ≤ f n
h : ∀ (n : ℕ), ∑ i ∈ range n, f i ≤ c
⊢ Summable f

Tactic:
refine (summable_iff_not_tendsto_nat_atTop_of_nonneg hf).2 fun H => ?_

Result:
f : ℕ → ℝ
c : ℝ
hf : ∀ (n : ℕ), 0 ≤ f n
h : ∀ (n : ℕ), ∑ i ∈ range n, f i ≤ c
H : Tendsto (fun n => ∑ i ∈ range n, f i) atTop atTop
⊢ False

Proof state:
f : ℕ → ℝ
c : ℝ
hf : ∀ (n : ℕ), 0 ≤ f n
h : ∀ (n : ℕ), ∑ i ∈ range n, f i ≤ c
H : Tendsto (fun n => ∑ i ∈ range n, f i) atTop atTop
⊢ False

Tactic:
rcases exists_lt_of_tendsto_atTop H 0 c with ⟨n, -, hn⟩

Result:
case intro.intro
f : ℕ → ℝ
c : ℝ
hf : ∀ (n : ℕ), 0 ≤ f n
h : ∀ (n : ℕ), ∑ i ∈ range n, f i ≤ c
H : Tendsto (fun n => ∑ i ∈ range n, f i) atTop atTop
n : ℕ
hn : c < ∑ i ∈ range n, f i
⊢ False

Proof state:
case intro.intro
f : ℕ → ℝ
c : ℝ
hf : ∀ (n : ℕ), 0 ≤ f n
h : ∀ (n : ℕ), ∑ i ∈ range n, f i ≤ c
H : Tendsto (fun n => ∑ i ∈ range n, f i) atTop atTop
n : ℕ
hn : c < ∑ i ∈ range n, f i
⊢ False

Tactic:
exact lt_irrefl _ (hn.trans_le (h n))

Result:
no goals
-- Mathlib/GroupTheory/Abelianization.lean
theorem rank_closureCommutatorRepresentatives_le [Finite (commutatorSet G)] :
    Group.rank (closureCommutatorRepresentatives G) ≤ 2 * Nat.card (commutatorSet G)

Proof state:
G : Type u
inst✝¹ : Group G
inst✝ : Finite ↑(commutatorSet G)
⊢ Group.rank ↥(closureCommutatorRepresentatives G) ≤ 2 * Nat.card ↑(commutatorSet G)

Tactic:
rw [two_mul]

Result:
G : Type u
inst✝¹ : Group G
inst✝ : Finite ↑(commutatorSet G)
⊢ Group.rank ↥(closureCommutatorRepresentatives G) ≤ Nat.card ↑(commutatorSet G) + Nat.card ↑(commutatorSet G)

Proof state:
G : Type u
inst✝¹ : Group G
inst✝ : Finite ↑(commutatorSet G)
⊢ Group.rank ↥(closureCommutatorRepresentatives G) ≤ Nat.card ↑(commutatorSet G) + Nat.card ↑(commutatorSet G)

Tactic:
exact
  (Subgroup.rank_closure_finite_le_nat_card _).trans
    ((Set.card_union_le _ _).trans
      (add_le_add ((Finite.card_image_le _).trans (Finite.card_range_le _))
        ((Finite.card_image_le _).trans (Finite.card_range_le _))))

Result:
no goals
-- Mathlib/Algebra/Lie/Subalgebra.lean
theorem subsingleton_bot : Subsingleton (⊥ : LieSubalgebra R L) :=
  show Subsingleton ((⊥ : LieSubalgebra R L) : Set L) by simp

Proof state:
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
⊢ Subsingleton ↑↑⊥

Tactic:
simp

Result:
no goals
-- Mathlib/MeasureTheory/Integral/Marginal.lean
theorem lmarginal_le_of_subset {f g : (∀ i, π i) → ℝ≥0∞} (hst : s ⊆ t)
    (hf : Measurable f) (hg : Measurable g) (hfg : ∫⋯∫⁻_s, f ∂μ ≤ ∫⋯∫⁻_s, g ∂μ) :
    ∫⋯∫⁻_t, f ∂μ ≤ ∫⋯∫⁻_t, g ∂μ

Proof state:
δ : Type u_1
π : δ → Type u_3
inst✝² : (x : δ) → MeasurableSpace (π x)
μ : (i : δ) → Measure (π i)
inst✝¹ : DecidableEq δ
s t : Finset δ
inst✝ : ∀ (i : δ), SigmaFinite (μ i)
f g : ((i : δ) → π i) → ℝ≥0∞
hst : s ⊆ t
hf : Measurable f
hg : Measurable g
hfg : ∫⋯∫⁻_s, f ∂μ ≤ ∫⋯∫⁻_s, g ∂μ
⊢ ∫⋯∫⁻_t \ s, ∫⋯∫⁻_s, f ∂μ ∂μ ≤ ∫⋯∫⁻_t \ s, ∫⋯∫⁻_s, g ∂μ ∂μ

Tactic:
exact lmarginal_mono hfg

Result:
no goals

Proof state:
δ : Type u_1
π : δ → Type u_3
inst✝² : (x : δ) → MeasurableSpace (π x)
μ : (i : δ) → Measure (π i)
inst✝¹ : DecidableEq δ
s t : Finset δ
inst✝ : ∀ (i : δ), SigmaFinite (μ i)
f g : ((i : δ) → π i) → ℝ≥0∞
hst : s ⊆ t
hf : Measurable f
hg : Measurable g
hfg : ∫⋯∫⁻_s, f ∂μ ≤ ∫⋯∫⁻_s, g ∂μ
⊢ ∫⋯∫⁻_t, f ∂μ ≤ ∫⋯∫⁻_t, g ∂μ

Tactic:
rw [← union_sdiff_of_subset hst, lmarginal_union' μ f hf disjoint_sdiff,
  lmarginal_union' μ g hg disjoint_sdiff]

Result:
δ : Type u_1
π : δ → Type u_3
inst✝² : (x : δ) → MeasurableSpace (π x)
μ : (i : δ) → Measure (π i)
inst✝¹ : DecidableEq δ
s t : Finset δ
inst✝ : ∀ (i : δ), SigmaFinite (μ i)
f g : ((i : δ) → π i) → ℝ≥0∞
hst : s ⊆ t
hf : Measurable f
hg : Measurable g
hfg : ∫⋯∫⁻_s, f ∂μ ≤ ∫⋯∫⁻_s, g ∂μ
⊢ ∫⋯∫⁻_t \ s, ∫⋯∫⁻_s, f ∂μ ∂μ ≤ ∫⋯∫⁻_t \ s, ∫⋯∫⁻_s, g ∂μ ∂μ
-- Mathlib/Algebra/Module/Defs.lean
theorem smul_add_one_sub_smul {R : Type*} [Ring R] [Module R M] {r : R} {m : M} :
    r • m + (1 - r) • m = m

Proof state:
M : Type u_3
inst✝² : AddCommMonoid M
R : Type u_5
inst✝¹ : Ring R
inst✝ : Module R M
r : R
m : M
⊢ r • m + (1 - r) • m = m

Tactic:
rw [← add_smul, add_sub_cancel, one_smul]

Result:
no goals
-- Mathlib/RingTheory/UniqueFactorizationDomain/FactorSet.lean
theorem map_subtype_coe_factors' {a : α} :
    (factors' a).map (↑) = (factors a).map Associates.mk

Proof state:
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
a : α
⊢ Multiset.map Subtype.val (factors' a) = Multiset.map Associates.mk (factors a)

Tactic:
simp [factors', Multiset.map_pmap, Multiset.pmap_eq_map]

Result:
no goals
-- Mathlib/LinearAlgebra/UnitaryGroup.lean
theorem mem_orthogonalGroup_iff' {A : Matrix n n β} :
    A ∈ Matrix.orthogonalGroup n β ↔ star A * A = 1

Proof state:
n : Type u
inst✝² : DecidableEq n
inst✝¹ : Fintype n
β : Type v
inst✝ : CommRing β
A : Matrix n n β
⊢ A ∈ orthogonalGroup n β ↔ star A * A = 1

Tactic:
refine ⟨And.left, fun hA => ⟨hA, ?_⟩⟩

Result:
n : Type u
inst✝² : DecidableEq n
inst✝¹ : Fintype n
β : Type v
inst✝ : CommRing β
A : Matrix n n β
hA : star A * A = 1
⊢ A * star A = 1

Proof state:
n : Type u
inst✝² : DecidableEq n
inst✝¹ : Fintype n
β : Type v
inst✝ : CommRing β
A : Matrix n n β
hA : star A * A = 1
⊢ A * star A = 1

Tactic:
rwa [mul_eq_one_comm] at hA

Result:
no goals
-- Mathlib/Data/ZMod/Basic.lean
theorem cast_cast_zmod_of_le {m n : ℕ} [hm : NeZero m] (h : m ≤ n) (a : ZMod m) :
    (cast (cast a : ZMod n) : ZMod m) = a

Proof state:
m n : ℕ
hm : NeZero m
h : m ≤ n
a : ZMod m
this : NeZero n
⊢ a.cast.cast = a

Tactic:
rw [cast_eq_val, val_cast_eq_val_of_lt (a.val_lt.trans_le h), natCast_zmod_val]

Result:
no goals

Proof state:
m n : ℕ
hm : NeZero m
h : m ≤ n
a : ZMod m
⊢ a.cast.cast = a

Tactic:
have : NeZero n := ⟨((Nat.zero_lt_of_ne_zero hm.out).trans_le h).ne'⟩

Result:
m n : ℕ
hm : NeZero m
h : m ≤ n
a : ZMod m
this : NeZero n
⊢ a.cast.cast = a
-- Mathlib/Data/Finset/MulAntidiagonal.lean
theorem IsWF.min_mul (hs : s.IsWF) (ht : t.IsWF) (hsn : s.Nonempty) (htn : t.Nonempty) :
    (hs.mul ht).min (hsn.mul htn) = hs.min hsn * ht.min htn

Proof state:
α : Type u_1
s t : Set α
inst✝ : LinearOrderedCancelCommMonoid α
hs : s.IsWF
ht : t.IsWF
hsn : s.Nonempty
htn : t.Nonempty
⊢ ∀ b ∈ s * t, hs.min hsn * ht.min htn ≤ b

Tactic:
rintro _ ⟨x, hx, y, hy, rfl⟩

Result:
case intro.intro.intro.intro
α : Type u_1
s t : Set α
inst✝ : LinearOrderedCancelCommMonoid α
hs : s.IsWF
ht : t.IsWF
hsn : s.Nonempty
htn : t.Nonempty
x : α
hx : x ∈ s
y : α
hy : y ∈ t
⊢ hs.min hsn * ht.min htn ≤ (fun x1 x2 => x1 * x2) x y

Proof state:
α : Type u_1
s t : Set α
inst✝ : LinearOrderedCancelCommMonoid α
hs : s.IsWF
ht : t.IsWF
hsn : s.Nonempty
htn : t.Nonempty
⊢ hs.min hsn * ht.min htn ≤ ⋯.min ⋯

Tactic:
rw [IsWF.le_min_iff]

Result:
α : Type u_1
s t : Set α
inst✝ : LinearOrderedCancelCommMonoid α
hs : s.IsWF
ht : t.IsWF
hsn : s.Nonempty
htn : t.Nonempty
⊢ ∀ b ∈ s * t, hs.min hsn * ht.min htn ≤ b

Proof state:
case intro.intro.intro.intro
α : Type u_1
s t : Set α
inst✝ : LinearOrderedCancelCommMonoid α
hs : s.IsWF
ht : t.IsWF
hsn : s.Nonempty
htn : t.Nonempty
x : α
hx : x ∈ s
y : α
hy : y ∈ t
⊢ hs.min hsn * ht.min htn ≤ (fun x1 x2 => x1 * x2) x y

Tactic:
exact mul_le_mul' (hs.min_le _ hx) (ht.min_le _ hy)

Result:
no goals

Proof state:
α : Type u_1
s t : Set α
inst✝ : LinearOrderedCancelCommMonoid α
hs : s.IsWF
ht : t.IsWF
hsn : s.Nonempty
htn : t.Nonempty
⊢ ⋯.min ⋯ = hs.min hsn * ht.min htn

Tactic:
refine le_antisymm (IsWF.min_le _ _ (mem_mul.2 ⟨_, hs.min_mem _, _, ht.min_mem _, rfl⟩)) ?_

Result:
α : Type u_1
s t : Set α
inst✝ : LinearOrderedCancelCommMonoid α
hs : s.IsWF
ht : t.IsWF
hsn : s.Nonempty
htn : t.Nonempty
⊢ hs.min hsn * ht.min htn ≤ ⋯.min ⋯
-- Mathlib/Data/Finset/Union.lean
lemma biUnion_inter (s : Finset α) (f : α → Finset β) (t : Finset β) :
    s.biUnion f ∩ t = s.biUnion fun x ↦ f x ∩ t

Proof state:
case h
α : Type u_1
β : Type u_2
inst✝ : DecidableEq β
s : Finset α
f : α → Finset β
t : Finset β
x : β
⊢ x ∈ s.biUnion f ∩ t ↔ x ∈ s.biUnion fun x => f x ∩ t

Tactic:
simp only [mem_biUnion, mem_inter]

Result:
case h
α : Type u_1
β : Type u_2
inst✝ : DecidableEq β
s : Finset α
f : α → Finset β
t : Finset β
x : β
⊢ (∃ a ∈ s, x ∈ f a) ∧ x ∈ t ↔ ∃ a ∈ s, x ∈ f a ∧ x ∈ t

Proof state:
α : Type u_1
β : Type u_2
inst✝ : DecidableEq β
s : Finset α
f : α → Finset β
t : Finset β
⊢ s.biUnion f ∩ t = s.biUnion fun x => f x ∩ t

Tactic:
ext x

Result:
case h
α : Type u_1
β : Type u_2
inst✝ : DecidableEq β
s : Finset α
f : α → Finset β
t : Finset β
x : β
⊢ x ∈ s.biUnion f ∩ t ↔ x ∈ s.biUnion fun x => f x ∩ t

Proof state:
case h
α : Type u_1
β : Type u_2
inst✝ : DecidableEq β
s : Finset α
f : α → Finset β
t : Finset β
x : β
⊢ (∃ a ∈ s, x ∈ f a) ∧ x ∈ t ↔ ∃ a ∈ s, x ∈ f a ∧ x ∈ t

Tactic:
tauto

Result:
no goals
-- Mathlib/FieldTheory/AlgebraicClosure.lean
theorem comap_eq_of_algHom (i : E →ₐ[F] K) :
    (algebraicClosure F K).comap i = algebraicClosure F E

Proof state:
F : Type u_1
E : Type u_2
inst✝⁴ : Field F
inst✝³ : Field E
inst✝² : Algebra F E
K : Type u_3
inst✝¹ : Field K
inst✝ : Algebra F K
i : E →ₐ[F] K
⊢ comap i (algebraicClosure F K) = algebraicClosure F E

Tactic:
ext x

Result:
case h
F : Type u_1
E : Type u_2
inst✝⁴ : Field F
inst✝³ : Field E
inst✝² : Algebra F E
K : Type u_3
inst✝¹ : Field K
inst✝ : Algebra F K
i : E →ₐ[F] K
x : E
⊢ x ∈ comap i (algebraicClosure F K) ↔ x ∈ algebraicClosure F E

Proof state:
case h
F : Type u_1
E : Type u_2
inst✝⁴ : Field F
inst✝³ : Field E
inst✝² : Algebra F E
K : Type u_3
inst✝¹ : Field K
inst✝ : Algebra F K
i : E →ₐ[F] K
x : E
⊢ x ∈ comap i (algebraicClosure F K) ↔ x ∈ algebraicClosure F E

Tactic:
exact map_mem_algebraicClosure_iff i

Result:
no goals
-- Mathlib/Algebra/MvPolynomial/PDeriv.lean
lemma X_mul_pderiv_monomial {i : σ} {m : σ →₀ ℕ} {r : R} :
    X i * pderiv i (monomial m r) = m i • monomial m r

Proof state:
case pos
R : Type u
σ : Type v
inst✝ : CommSemiring R
i : σ
m : σ →₀ ℕ
r : R
h : m i = 0
⊢ (monomial (single i 1 + (m - single i 1))) (1 * (r * ↑(m i))) = (monomial m) (m i • r)

Tactic:
simp_rw [h, Nat.cast_zero, mul_zero, zero_smul, monomial_zero]

Result:
no goals

Proof state:
R : Type u
σ : Type v
inst✝ : CommSemiring R
i : σ
m : σ →₀ ℕ
r : R
⊢ (monomial (single i 1 + (m - single i 1))) (1 * (r * ↑(m i))) = (monomial m) (m i • r)

Tactic:
by_cases h : m i = 0

Result:
case pos
R : Type u
σ : Type v
inst✝ : CommSemiring R
i : σ
m : σ →₀ ℕ
r : R
h : m i = 0
⊢ (monomial (single i 1 + (m - single i 1))) (1 * (r * ↑(m i))) = (monomial m) (m i • r)

case neg
R : Type u
σ : Type v
inst✝ : CommSemiring R
i : σ
m : σ →₀ ℕ
r : R
h : ¬m i = 0
⊢ (monomial (single i 1 + (m - single i 1))) (1 * (r * ↑(m i))) = (monomial m) (m i • r)

Proof state:
case neg
R : Type u
σ : Type v
inst✝ : CommSemiring R
i : σ
m : σ →₀ ℕ
r : R
h : ¬m i = 0
⊢ (monomial (single i 1 + (m - single i 1))) (1 * (r * ↑(m i))) = (monomial m) (m i • r)

Tactic:
rw [one_mul, mul_comm, nsmul_eq_mul, add_comm, sub_add_single_one_cancel h]

Result:
no goals

Proof state:
R : Type u
σ : Type v
inst✝ : CommSemiring R
i : σ
m : σ →₀ ℕ
r : R
⊢ X i * (pderiv i) ((monomial m) r) = m i • (monomial m) r

Tactic:
rw [pderiv_monomial, X, monomial_mul, smul_monomial]

Result:
R : Type u
σ : Type v
inst✝ : CommSemiring R
i : σ
m : σ →₀ ℕ
r : R
⊢ (monomial (single i 1 + (m - single i 1))) (1 * (r * ↑(m i))) = (monomial m) (m i • r)
-- Mathlib/LinearAlgebra/Matrix/Transvection.lean
theorem mul_transvection_apply_of_ne (a b : n) (hb : b ≠ j) (c : R) (M : Matrix n n R) :
    (M * transvection i j c) a b = M a b

Proof state:
n : Type u_1
R : Type u₂
inst✝² : DecidableEq n
inst✝¹ : CommRing R
i j : n
inst✝ : Fintype n
a b : n
hb : b ≠ j
c : R
M : Matrix n n R
⊢ (M * transvection i j c) a b = M a b

Tactic:
simp [transvection, Matrix.mul_add, hb]

Result:
no goals
-- Mathlib/SetTheory/Ordinal/Basic.lean
theorem lift_le {a b : Ordinal} : lift.{u, v} a ≤ lift.{u, v} b ↔ a ≤ b :=
  inductionOn₂ a b fun α r _ β s _ => by
    rw [← lift_umax]
    exact lift_type_le.{_,_,u}

Proof state:
a b : Ordinal.{v}
α : Type v
r : α → α → Prop
x✝¹ : IsWellOrder α r
β : Type v
s : β → β → Prop
x✝ : IsWellOrder β s
⊢ lift.{max v u, v} (type r) ≤ lift.{max v u, v} (type s) ↔ type r ≤ type s

Tactic:
exact lift_type_le.{_,_,u}

Result:
no goals

Proof state:
a b : Ordinal.{v}
α : Type v
r : α → α → Prop
x✝¹ : IsWellOrder α r
β : Type v
s : β → β → Prop
x✝ : IsWellOrder β s
⊢ lift.{u, v} (type r) ≤ lift.{u, v} (type s) ↔ type r ≤ type s

Tactic:
rw [← lift_umax]

Result:
a b : Ordinal.{v}
α : Type v
r : α → α → Prop
x✝¹ : IsWellOrder α r
β : Type v
s : β → β → Prop
x✝ : IsWellOrder β s
⊢ lift.{max v u, v} (type r) ≤ lift.{max v u, v} (type s) ↔ type r ≤ type s
-- Mathlib/Algebra/Polynomial/Smeval.lean
theorem smeval_comp : (p.comp q).smeval x  = p.smeval (q.smeval x)

Proof state:
case h_monomial
R : Type u_1
inst✝⁶ : Semiring R
p q : R[X]
S : Type u_2
inst✝⁵ : NonAssocSemiring S
inst✝⁴ : Module R S
inst✝³ : Pow S ℕ
x : S
inst✝² : NatPowAssoc S
inst✝¹ : IsScalarTower R S S
inst✝ : SMulCommClass R S S
n : ℕ
a : R
⊢ (((monomial n) a).comp q).smeval x = ((monomial n) a).smeval (q.smeval x)

Tactic:
simp [smeval_monomial, smeval_C_mul, smeval_pow]

Result:
no goals

Proof state:
case h_add
R : Type u_1
inst✝⁶ : Semiring R
p q : R[X]
S : Type u_2
inst✝⁵ : NonAssocSemiring S
inst✝⁴ : Module R S
inst✝³ : Pow S ℕ
x : S
inst✝² : NatPowAssoc S
inst✝¹ : IsScalarTower R S S
inst✝ : SMulCommClass R S S
r s : R[X]
hr : (r.comp q).smeval x = r.smeval (q.smeval x)
hs : (s.comp q).smeval x = s.smeval (q.smeval x)
⊢ ((r + s).comp q).smeval x = (r + s).smeval (q.smeval x)

Tactic:
simp [add_comp, hr, hs, smeval_add]

Result:
no goals

Proof state:
R : Type u_1
inst✝⁶ : Semiring R
p q : R[X]
S : Type u_2
inst✝⁵ : NonAssocSemiring S
inst✝⁴ : Module R S
inst✝³ : Pow S ℕ
x : S
inst✝² : NatPowAssoc S
inst✝¹ : IsScalarTower R S S
inst✝ : SMulCommClass R S S
⊢ (p.comp q).smeval x = p.smeval (q.smeval x)

Tactic:
induction p using Polynomial.induction_on' with
| h_add r s hr hs =>
  simp [add_comp, hr, hs, smeval_add]
| h_monomial n a =>
  simp [smeval_monomial, smeval_C_mul, smeval_pow]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Trigonometric/Deriv.lean
theorem Complex.LogDeriv_exp : logDeriv (Complex.exp) = 1

Proof state:
case h
x✝ : ℂ
⊢ logDeriv cexp x✝ = 1 x✝

Tactic:
rw [logDeriv, Complex.deriv_exp, Pi.div_apply, ← exp_sub, sub_self, exp_zero, Pi.one_apply]

Result:
no goals

Proof state:
⊢ logDeriv cexp = 1

Tactic:
ext

Result:
case h
x✝ : ℂ
⊢ logDeriv cexp x✝ = 1 x✝
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/RawLemmas.lean
theorem size_le_size_alter [LawfulBEq α] {k : α} {f : Option (β k) → Option (β k)} (h : m.WF) :
    m.size - 1 ≤ (m.alter k f).size

Proof state:
α : Type u
β : α → Type v
inst✝² : BEq α
inst✝¹ : Hashable α
m : Raw α β
inst✝ : LawfulBEq α
k : α
f : Option (β k) → Option (β k)
h : m.WF
⊢ m.size - 1 ≤ (m.alter k f).size

Tactic:
simp_to_raw using Raw₀.size_le_size_alter ⟨m, h.size_buckets_pos⟩

Result:
no goals
-- Mathlib/MeasureTheory/Measure/Prod.lean
/-- If `Prod.fst ⁻¹' s` is a null measurable set and `ν ≠ 0`, then `s` is a null measurable set. -/
lemma _root_.MeasureTheory.NullMeasurableSet.of_preimage_fst [NeZero ν] {s : Set α}
    (h : NullMeasurableSet (Prod.fst ⁻¹' s) (μ.prod ν)) : NullMeasurableSet s μ :=
  .left_of_prod (by rwa [prod_univ]) (NeZero.ne (ν univ))

Proof state:
α : Type u_1
β : Type u_2
inst✝⁴ : MeasurableSpace α
inst✝³ : MeasurableSpace β
μ : Measure α
ν : Measure β
inst✝² : SFinite ν
inst✝¹ : SFinite μ
inst✝ : NeZero ν
s : Set α
h : NullMeasurableSet (Prod.fst ⁻¹' s) (μ.prod ν)
⊢ NullMeasurableSet (s ×ˢ univ) (μ.prod ν)

Tactic:
rwa [prod_univ]

Result:
no goals
-- Mathlib/Order/Filter/Bases.lean
theorem hasBasis_iInf_principal {s : ι → Set α} (h : Directed (· ≥ ·) s) [Nonempty ι] :
    (⨅ i, 𝓟 (s i)).HasBasis (fun _ => True) s :=
  ⟨fun t => by
    simpa only [true_and] using mem_iInf_of_directed (h.mono_comp _ monotone_principal.dual) t⟩

Proof state:
α : Type u_1
ι : Sort u_4
s : ι → Set α
h : Directed (fun x1 x2 => x1 ≥ x2) s
inst✝ : Nonempty ι
t : Set α
⊢ t ∈ ⨅ i, 𝓟 (s i) ↔ ∃ i, True ∧ s i ⊆ t

Tactic:
simpa only [true_and] using mem_iInf_of_directed (h.mono_comp _ monotone_principal.dual) t

Result:
no goals
-- Mathlib/Algebra/Homology/ShortComplex/SnakeLemma.lean
lemma op_δ : S.op.δ = S.δ.op := Quiver.Hom.unop_inj (by
  rw [Quiver.Hom.unop_op, ← cancel_mono (pushout.inr _ _ : _ ⟶ S.P'),
    ← cancel_epi (pullback.snd _ _ : S.P ⟶ _), S.snd_δ_inr,
    ← cancel_mono S.P'IsoUnopOpP.hom, ← cancel_epi S.PIsoUnopOpP'.inv,
    P'IsoUnopOpP, PIsoUnopOpP', assoc, assoc, assoc, assoc,
    pushoutIsoUnopPullback_inr_hom, pullbackIsoUnopPushout_inv_snd_assoc,
    pushoutIsoUnopPullback_inl_hom, pullbackIsoUnopPushout_inv_fst_assoc]
  apply Quiver.Hom.op_inj
  simpa only [op_comp, Quiver.Hom.op_unop, assoc] using S.op.snd_δ_inr)

Proof state:
case a
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Abelian C
S : SnakeInput C
⊢ ((pushout.inr S.L₁.g.op S.v₀₁.τ₃.op).unop ≫ S.op.δ.unop ≫ (pullback.snd S.L₂.f.op S.v₂₃.τ₁.op).unop).op =
    ((pushout.inl S.L₁.g.op S.v₀₁.τ₃.op).unop ≫ S.v₁₂.τ₂ ≫ (pullback.fst S.L₂.f.op S.v₂₃.τ₁.op).unop).op

Tactic:
simpa only [op_comp, Quiver.Hom.op_unop, assoc] using S.op.snd_δ_inr

Result:
no goals

Proof state:
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Abelian C
S : SnakeInput C
⊢ (pushout.inr S.L₁.g.op S.v₀₁.τ₃.op).unop ≫ S.op.δ.unop ≫ (pullback.snd S.L₂.f.op S.v₂₃.τ₁.op).unop =
    (pushout.inl S.L₁.g.op S.v₀₁.τ₃.op).unop ≫ S.v₁₂.τ₂ ≫ (pullback.fst S.L₂.f.op S.v₂₃.τ₁.op).unop

Tactic:
apply Quiver.Hom.op_inj

Result:
case a
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Abelian C
S : SnakeInput C
⊢ ((pushout.inr S.L₁.g.op S.v₀₁.τ₃.op).unop ≫ S.op.δ.unop ≫ (pullback.snd S.L₂.f.op S.v₂₃.τ₁.op).unop).op =
    ((pushout.inl S.L₁.g.op S.v₀₁.τ₃.op).unop ≫ S.v₁₂.τ₂ ≫ (pullback.fst S.L₂.f.op S.v₂₃.τ₁.op).unop).op

Proof state:
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Abelian C
S : SnakeInput C
⊢ S.op.δ.unop = S.δ.op.unop

Tactic:
rw [Quiver.Hom.unop_op, ← cancel_mono (pushout.inr _ _ : _ ⟶ S.P'),
  ← cancel_epi (pullback.snd _ _ : S.P ⟶ _), S.snd_δ_inr,
  ← cancel_mono S.P'IsoUnopOpP.hom, ← cancel_epi S.PIsoUnopOpP'.inv,
  P'IsoUnopOpP, PIsoUnopOpP', assoc, assoc, assoc, assoc,
  pushoutIsoUnopPullback_inr_hom, pullbackIsoUnopPushout_inv_snd_assoc,
  pushoutIsoUnopPullback_inl_hom, pullbackIsoUnopPushout_inv_fst_assoc]

Result:
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Abelian C
S : SnakeInput C
⊢ (pushout.inr S.L₁.g.op S.v₀₁.τ₃.op).unop ≫ S.op.δ.unop ≫ (pullback.snd S.L₂.f.op S.v₂₃.τ₁.op).unop =
    (pushout.inl S.L₁.g.op S.v₀₁.τ₃.op).unop ≫ S.v₁₂.τ₂ ≫ (pullback.fst S.L₂.f.op S.v₂₃.τ₁.op).unop
-- Mathlib/NumberTheory/Dioph.lean
theorem ne_dioph : Dioph {v | f v ≠ g v} :=
  ext (df D< dg D∨ dg D< df) fun v => by dsimp; exact lt_or_lt_iff_ne (α := ℕ)

Proof state:
α : Type
f g : (α → ℕ) → ℕ
df : DiophFn f
dg : DiophFn g
v : α → ℕ
⊢ v ∈ {v | f v < g v} ∪ {v | g v < f v} ↔ ¬f v = g v

Tactic:
exact lt_or_lt_iff_ne (α := ℕ)

Result:
no goals

Proof state:
α : Type
f g : (α → ℕ) → ℕ
df : DiophFn f
dg : DiophFn g
v : α → ℕ
⊢ v ∈ {v | f v < g v} ∪ {v | g v < f v} ↔ v ∈ {v | f v ≠ g v}

Tactic:
dsimp

Result:
α : Type
f g : (α → ℕ) → ℕ
df : DiophFn f
dg : DiophFn g
v : α → ℕ
⊢ v ∈ {v | f v < g v} ∪ {v | g v < f v} ↔ ¬f v = g v
-- Mathlib/Data/Fintype/EquivFin.lean
theorem exists_of_card_le_finset [Fintype α] {s : Finset β} (h : Fintype.card α ≤ #s) :
    ∃ f : α ↪ β, Set.range f ⊆ s

Proof state:
α : Type u_1
β : Type u_2
inst✝ : Fintype α
s : Finset β
h : Fintype.card α ≤ Fintype.card { x // x ∈ s }
⊢ ∃ f, Set.range ⇑f ⊆ ↑s

Tactic:
rcases nonempty_of_card_le h with ⟨f⟩

Result:
case intro
α : Type u_1
β : Type u_2
inst✝ : Fintype α
s : Finset β
h : Fintype.card α ≤ Fintype.card { x // x ∈ s }
f : α ↪ { x // x ∈ s }
⊢ ∃ f, Set.range ⇑f ⊆ ↑s

Proof state:
α : Type u_1
β : Type u_2
inst✝ : Fintype α
s : Finset β
h : Fintype.card α ≤ #s
⊢ ∃ f, Set.range ⇑f ⊆ ↑s

Tactic:
rw [← Fintype.card_coe] at h

Result:
α : Type u_1
β : Type u_2
inst✝ : Fintype α
s : Finset β
h : Fintype.card α ≤ Fintype.card { x // x ∈ s }
⊢ ∃ f, Set.range ⇑f ⊆ ↑s

Proof state:
case intro
α : Type u_1
β : Type u_2
inst✝ : Fintype α
s : Finset β
h : Fintype.card α ≤ Fintype.card { x // x ∈ s }
f : α ↪ { x // x ∈ s }
⊢ ∃ f, Set.range ⇑f ⊆ ↑s

Tactic:
exact ⟨f.trans (Embedding.subtype _), by simp [Set.range_subset_iff]⟩

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
inst✝ : Fintype α
s : Finset β
h : Fintype.card α ≤ Fintype.card { x // x ∈ s }
f : α ↪ { x // x ∈ s }
⊢ Set.range ⇑(f.trans (subtype fun x => x ∈ s)) ⊆ ↑s

Tactic:
simp [Set.range_subset_iff]

Result:
no goals