harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/ToArray.lean
theorem eraseIdxIfInBounds_toArray (l : List α) (i : Nat) :
    l.toArray.eraseIdxIfInBounds i = (l.eraseIdx i).toArray

Proof state:
α : Type u_1
l : List α
i : Nat
⊢ (if h : i < l.toArray.size then l.toArray.eraseIdx i h else l.toArray) = (l.eraseIdx i).toArray

Tactic:
split

Result:
case isTrue
α : Type u_1
l : List α
i : Nat
h✝ : i < l.toArray.size
⊢ l.toArray.eraseIdx i h✝ = (l.eraseIdx i).toArray

case isFalse
α : Type u_1
l : List α
i : Nat
h✝ : ¬i < l.toArray.size
⊢ l.toArray = (l.eraseIdx i).toArray

Proof state:
case isFalse
α : Type u_1
l : List α
i : Nat
h✝ : ¬i < l.toArray.size
⊢ l.toArray = (l.eraseIdx i).toArray

Tactic:
simp_all [eraseIdx_eq_self.2]

Result:
no goals

Proof state:
α : Type u_1
l : List α
i : Nat
⊢ l.toArray.eraseIdxIfInBounds i = (l.eraseIdx i).toArray

Tactic:
rw [Array.eraseIdxIfInBounds]

Result:
α : Type u_1
l : List α
i : Nat
⊢ (if h : i < l.toArray.size then l.toArray.eraseIdx i h else l.toArray) = (l.eraseIdx i).toArray

Proof state:
case isTrue
α : Type u_1
l : List α
i : Nat
h✝ : i < l.toArray.size
⊢ l.toArray.eraseIdx i h✝ = (l.eraseIdx i).toArray

Tactic:
simp

Result:
no goals
-- Mathlib/Data/Matrix/Mul.lean
theorem sub_vecMul [Fintype m] (A : Matrix m n α) (x y : m → α) :
    (x - y) ᵥ* A = x ᵥ* A - y ᵥ* A

Proof state:
m : Type u_2
n : Type u_3
α : Type v
inst✝¹ : NonUnitalNonAssocRing α
inst✝ : Fintype m
A : Matrix m n α
x y : m → α
⊢ (x - y) ᵥ* A = x ᵥ* A - y ᵥ* A

Tactic:
ext

Result:
case h
m : Type u_2
n : Type u_3
α : Type v
inst✝¹ : NonUnitalNonAssocRing α
inst✝ : Fintype m
A : Matrix m n α
x y : m → α
x✝ : n
⊢ ((x - y) ᵥ* A) x✝ = (x ᵥ* A - y ᵥ* A) x✝

Proof state:
case h
m : Type u_2
n : Type u_3
α : Type v
inst✝¹ : NonUnitalNonAssocRing α
inst✝ : Fintype m
A : Matrix m n α
x y : m → α
x✝ : n
⊢ ((x - y) ᵥ* A) x✝ = (x ᵥ* A - y ᵥ* A) x✝

Tactic:
apply sub_dotProduct

Result:
no goals
-- Mathlib/.lake/packages/batteries/Batteries/Data/Rat/Lemmas.lean
theorem neg_divInt (n d) : -(n /. d) = -n /. d

Proof state:
n d : Int
⊢ -(n /. d) = -n /. d

Tactic:
rcases Int.eq_nat_or_neg d with ⟨_, rfl | rfl⟩ <;> simp [divInt_neg', neg_mkRat]

Result:
no goals
-- Mathlib/CategoryTheory/Abelian/Projective/Resolution.lean
theorem liftFOne_zero_comm {Y Z : C} (f : Y ⟶ Z) (P : ProjectiveResolution Y)
    (Q : ProjectiveResolution Z) :
    liftFOne f P Q ≫ Q.complex.d 1 0 = P.complex.d 1 0 ≫ liftFZero f P Q

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
Y Z : C
f : Y ⟶ Z
P : ProjectiveResolution Y
Q : ProjectiveResolution Z
⊢ liftFOne f P Q ≫ Q.complex.d 1 0 = P.complex.d 1 0 ≫ liftFZero f P Q

Tactic:
apply Q.exact₀.liftFromProjective_comp

Result:
no goals
-- Mathlib/RingTheory/Ideal/Maps.lean
theorem smul_restrictScalars {R S M} [CommSemiring R] [CommSemiring S]
    [Algebra R S] [AddCommMonoid M] [Module R M] [Module S M]
    [IsScalarTower R S M] (I : Ideal R) (N : Submodule S M) :
    (I.map (algebraMap R S) • N).restrictScalars R = I • N.restrictScalars R

Proof state:
R : Type u_4
S : Type u_5
M : Type u_6
inst✝⁶ : CommSemiring R
inst✝⁵ : CommSemiring S
inst✝⁴ : Algebra R S
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : Module S M
inst✝ : IsScalarTower R S M
I : Ideal R
N : Submodule S M
⊢ Submodule.restrictScalars R (⨆ b ∈ ↑I, (algebraMap R S) b • N) =
    ⨆ a ∈ ↑I, Submodule.restrictScalars R ((algebraMap R S) a • N)

Tactic:
exact map_iSup₂ (Submodule.restrictScalarsLatticeHom R S M) _

Result:
no goals

Proof state:
R : Type u_4
S : Type u_5
M : Type u_6
inst✝⁶ : CommSemiring R
inst✝⁵ : CommSemiring S
inst✝⁴ : Algebra R S
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : Module S M
inst✝ : IsScalarTower R S M
I : Ideal R
N : Submodule S M
⊢ Submodule.restrictScalars R (map (algebraMap R S) I • N) = I • Submodule.restrictScalars R N

Tactic:
simp_rw [map, Submodule.span_smul_eq, ← Submodule.coe_set_smul,
  Submodule.set_smul_eq_iSup, ← element_smul_restrictScalars, iSup_image]

Result:
R : Type u_4
S : Type u_5
M : Type u_6
inst✝⁶ : CommSemiring R
inst✝⁵ : CommSemiring S
inst✝⁴ : Algebra R S
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : Module S M
inst✝ : IsScalarTower R S M
I : Ideal R
N : Submodule S M
⊢ Submodule.restrictScalars R (⨆ b ∈ ↑I, (algebraMap R S) b • N) =
    ⨆ a ∈ ↑I, Submodule.restrictScalars R ((algebraMap R S) a • N)
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Option/Lemmas.lean
theorem map_orElse {x y : Option α} : (x <|> y).map f = (x.map f <|> y.map f)

Proof state:
α : Type u_1
α✝ : Type u_2
f : α → α✝
x y : Option α
⊢ Option.map f (x <|> y) = (Option.map f x <|> Option.map f y)

Tactic:
cases x <;> simp

Result:
no goals
-- Mathlib/Data/Set/Card.lean
theorem encard_congr (e : s ≃ t) : s.encard = t.encard

Proof state:
α : Type u_1
β : Type u_2
s : Set α
t : Set β
e : ↑s ≃ ↑t
⊢ s.encard = t.encard

Tactic:
rw [← encard_univ_coe, ← encard_univ_coe t, encard_univ, encard_univ, ENat.card_congr e]

Result:
no goals
-- Mathlib/Data/Finset/NAry.lean
lemma sup_image₂_right (g : γ → δ) : sup (image₂ f s t) g = sup t fun y ↦ sup s (g <| f · y)

Proof state:
α : Type u_1
β : Type u_3
γ : Type u_5
δ : Type u_7
inst✝² : DecidableEq γ
f : α → β → γ
s : Finset α
t : Finset β
inst✝¹ : SemilatticeSup δ
inst✝ : OrderBot δ
g : γ → δ
⊢ (t.sup fun i' => s.sup fun i => (g ∘ uncurry f) (i, i')) = t.sup fun y => s.sup fun x => g (f x y)

Tactic:
rfl

Result:
no goals

Proof state:
α : Type u_1
β : Type u_3
γ : Type u_5
δ : Type u_7
inst✝² : DecidableEq γ
f : α → β → γ
s : Finset α
t : Finset β
inst✝¹ : SemilatticeSup δ
inst✝ : OrderBot δ
g : γ → δ
⊢ (image₂ f s t).sup g = t.sup fun y => s.sup fun x => g (f x y)

Tactic:
simp only [image₂, sup_image, sup_product_right]

Result:
α : Type u_1
β : Type u_3
γ : Type u_5
δ : Type u_7
inst✝² : DecidableEq γ
f : α → β → γ
s : Finset α
t : Finset β
inst✝¹ : SemilatticeSup δ
inst✝ : OrderBot δ
g : γ → δ
⊢ (t.sup fun i' => s.sup fun i => (g ∘ uncurry f) (i, i')) = t.sup fun y => s.sup fun x => g (f x y)
-- Mathlib/Data/Fin/Basic.lean
theorem le_pred_iff {j : Fin n} {i : Fin (n + 1)} (hi : i ≠ 0) : j ≤ pred i hi ↔ succ j ≤ i

Proof state:
n : ℕ
j : Fin n
i : Fin (n + 1)
hi : i ≠ 0
⊢ j ≤ i.pred hi ↔ j.succ ≤ i

Tactic:
rw [← succ_le_succ_iff, succ_pred]

Result:
no goals
-- Mathlib/CategoryTheory/Abelian/DiagramLemmas/Four.lean
theorem mono_of_epi_of_epi_of_mono (hR₂ : R₂.Exact) (hR₁' : Epi R₁.g)
    (h₀ : Epi φ.τ₁) (h₁ : Mono φ.τ₂) : Mono (φ.τ₃) :=
  Abelian.mono_of_epi_of_epi_mono' (ShortComplex.mapToComposableArrows φ)
    (by simp) hR₁' hR₂.exact_toComposableArrows h₀ h₁

Proof state:
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Abelian C
R₁ R₂ : ShortComplex C
φ : R₁ ⟶ R₂
hR₂ : R₂.Exact
hR₁' : Epi R₁.g
h₀ : Epi φ.τ₁
h₁ : Mono φ.τ₂
⊢ R₁.toComposableArrows.map' 0 2 ⋯ ⋯ = 0

Tactic:
simp

Result:
no goals
-- Mathlib/Data/Finset/Max.lean
theorem max_singleton {a : α} : Finset.max {a} = (a : WithBot α)

Proof state:
α : Type u_2
inst✝ : LinearOrder α
a : α
⊢ {a}.max = ↑a

Tactic:
rw [← insert_emptyc_eq]

Result:
α : Type u_2
inst✝ : LinearOrder α
a : α
⊢ (insert a ∅).max = ↑a

Proof state:
α : Type u_2
inst✝ : LinearOrder α
a : α
⊢ (insert a ∅).max = ↑a

Tactic:
exact max_insert

Result:
no goals
-- Mathlib/Algebra/BigOperators/Expect.lean
lemma expect_sum_comm (s : Finset ι) (t : Finset κ) (f : ι → κ → M) :
    𝔼 i ∈ s, ∑ j ∈ t, f i j = ∑ j ∈ t, 𝔼 i ∈ s, f i j

Proof state:
ι : Type u_1
κ : Type u_2
M : Type u_3
inst✝¹ : AddCommMonoid M
inst✝ : Module ℚ≥0 M
s : Finset ι
t : Finset κ
f : ι → κ → M
⊢ 𝔼 i ∈ s, ∑ j ∈ t, f i j = ∑ j ∈ t, 𝔼 i ∈ s, f i j

Tactic:
simpa only [expect, smul_sum] using sum_comm

Result:
no goals
-- Mathlib/AlgebraicGeometry/RationalMap.lean
@[simp]
lemma fromSpecStalkOfMem_compHom (f : X.PartialMap Y) (g : Y ⟶ Z) (x) (hx) :
    (f.compHom g).fromSpecStalkOfMem (x := x) hx = f.fromSpecStalkOfMem hx ≫ g

Proof state:
X Y Z : Scheme
f : X.PartialMap Y
g : Y ⟶ Z
x : ↑↑X.toPresheafedSpace
hx : x ∈ (f.compHom g).domain
⊢ (f.compHom g).fromSpecStalkOfMem hx = f.fromSpecStalkOfMem hx ≫ g

Tactic:
simp [fromSpecStalkOfMem]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem msb_zero_length (x : BitVec 0) : x.msb = false

Proof state:
x : BitVec 0
⊢ x.msb = false

Tactic:
simp [BitVec.msb, of_length_zero]

Result:
no goals
-- Mathlib/Data/Finsupp/Single.lean
theorem single_apply_eq_zero {a x : α} {b : M} : single a b x = 0 ↔ x = a → b = 0

Proof state:
α : Type u_1
M : Type u_5
inst✝ : Zero M
a x : α
b : M
⊢ (single a b) x = 0 ↔ x = a → b = 0

Tactic:
simp [single_eq_set_indicator]

Result:
no goals
-- Mathlib/Algebra/BigOperators/Group/Finset/Defs.lean
theorem prod_hom_rel [CommMonoid γ] {r : β → γ → Prop} {f : α → β} {g : α → γ} {s : Finset α}
    (h₁ : r 1 1) (h₂ : ∀ a b c, r b c → r (f a * b) (g a * c)) :
    r (∏ x ∈ s, f x) (∏ x ∈ s, g x)

Proof state:
α : Type u_3
β : Type u_4
γ : Type u_5
inst✝¹ : CommMonoid β
inst✝ : CommMonoid γ
r : β → γ → Prop
f : α → β
g : α → γ
s : Finset α
h₁ : r 1 1
h₂ : ∀ (a : α) (b : β) (c : γ), r b c → r (f a * b) (g a * c)
⊢ r (Multiset.map (fun x => f x) s.val).prod (Multiset.map (fun x => g x) s.val).prod

Tactic:
apply Multiset.prod_hom_rel <;> assumption

Result:
no goals

Proof state:
α : Type u_3
β : Type u_4
γ : Type u_5
inst✝¹ : CommMonoid β
inst✝ : CommMonoid γ
r : β → γ → Prop
f : α → β
g : α → γ
s : Finset α
h₁ : r 1 1
h₂ : ∀ (a : α) (b : β) (c : γ), r b c → r (f a * b) (g a * c)
⊢ r (∏ x ∈ s, f x) (∏ x ∈ s, g x)

Tactic:
delta Finset.prod

Result:
α : Type u_3
β : Type u_4
γ : Type u_5
inst✝¹ : CommMonoid β
inst✝ : CommMonoid γ
r : β → γ → Prop
f : α → β
g : α → γ
s : Finset α
h₁ : r 1 1
h₂ : ∀ (a : α) (b : β) (c : γ), r b c → r (f a * b) (g a * c)
⊢ r (Multiset.map (fun x => f x) s.val).prod (Multiset.map (fun x => g x) s.val).prod
-- Mathlib/Analysis/Meromorphic/Basic.lean
@[simp]
lemma inv_iff {f : 𝕜 → 𝕜} {x : 𝕜} :
    MeromorphicAt f⁻¹ x ↔ MeromorphicAt f x :=
  ⟨fun h ↦ by simpa only [inv_inv] using h.inv, MeromorphicAt.inv⟩

Proof state:
𝕜 : Type u_1
inst✝ : NontriviallyNormedField 𝕜
f : 𝕜 → 𝕜
x : 𝕜
h : MeromorphicAt f⁻¹ x
⊢ MeromorphicAt f x

Tactic:
simpa only [inv_inv] using h.inv

Result:
no goals
-- Mathlib/Analysis/Complex/UpperHalfPlane/Topology.lean
lemma ofComplex_apply_eq_of_im_nonpos {w w' : ℂ} (hw : w.im ≤ 0) (hw' : w'.im ≤ 0) :
    ofComplex w = ofComplex w'

Proof state:
w w' : ℂ
hw : w.im ≤ 0
hw' : w'.im ≤ 0
⊢ ↑ofComplex w = ↑ofComplex w'

Tactic:
simp [ofComplex_apply_of_im_nonpos, hw, hw']

Result:
no goals
-- Mathlib/MeasureTheory/Function/SimpleFunc.lean
theorem ennrealRatEmbed_encode (q : ℚ) :
    ennrealRatEmbed (Encodable.encode q) = Real.toNNReal q

Proof state:
q : ℚ
⊢ ENNReal.ofReal ↑((some q).getD 0) = ↑(↑q).toNNReal

Tactic:
rfl

Result:
no goals

Proof state:
q : ℚ
⊢ ennrealRatEmbed (Encodable.encode q) = ↑(↑q).toNNReal

Tactic:
rw [ennrealRatEmbed, Encodable.encodek]

Result:
q : ℚ
⊢ ENNReal.ofReal ↑((some q).getD 0) = ↑(↑q).toNNReal
-- Mathlib/.lake/packages/lean4/src/lean/Init/PropLemmas.lean
theorem dite_not [hn : Decidable (¬p)] [h : Decidable p]  (x : ¬p → α) (y : ¬¬p → α) :
    dite (¬p) x y = dite p (fun h => y (not_not_intro h)) x

Proof state:
case isTrue
p : Prop
α : Sort u_1
hn : Decidable ¬p
x : ¬p → α
y : ¬¬p → α
h✝ : p
⊢ dite (¬p) x y = dite p (fun h => y ⋯) x

Tactic:
rename_i g

Result:
case isTrue
p : Prop
α : Sort u_1
hn : Decidable ¬p
x : ¬p → α
y : ¬¬p → α
g : p
⊢ dite (¬p) x y = dite p (fun h => y ⋯) x

Proof state:
p : Prop
α : Sort u_1
hn : Decidable ¬p
h : Decidable p
x : ¬p → α
y : ¬¬p → α
⊢ dite (¬p) x y = dite p (fun h => y ⋯) x

Tactic:
cases h <;> (rename_i g; simp [g])

Result:
no goals

Proof state:
case isTrue
p : Prop
α : Sort u_1
hn : Decidable ¬p
x : ¬p → α
y : ¬¬p → α
g : p
⊢ dite (¬p) x y = dite p (fun h => y ⋯) x

Tactic:
simp [g]

Result:
no goals
-- Mathlib/RingTheory/Radical.lean
theorem radical_eq_of_associated {a b : M} (h : Associated a b) : radical a = radical b

Proof state:
M : Type u_1
inst✝² : CancelCommMonoidWithZero M
inst✝¹ : NormalizationMonoid M
inst✝ : UniqueFactorizationMonoid M
a b : M
h : Associated a b
⊢ (primeFactors a).prod id = (primeFactors b).prod id

Tactic:
rw [h.primeFactors_eq]

Result:
no goals

Proof state:
M : Type u_1
inst✝² : CancelCommMonoidWithZero M
inst✝¹ : NormalizationMonoid M
inst✝ : UniqueFactorizationMonoid M
a b : M
h : Associated a b
⊢ radical a = radical b

Tactic:
unfold radical

Result:
M : Type u_1
inst✝² : CancelCommMonoidWithZero M
inst✝¹ : NormalizationMonoid M
inst✝ : UniqueFactorizationMonoid M
a b : M
h : Associated a b
⊢ (primeFactors a).prod id = (primeFactors b).prod id
-- Mathlib/Data/DFinsupp/NeLocus.lean
theorem neLocus_eq_empty {f g : Π₀ a, N a} : f.neLocus g = ∅ ↔ f = g :=
  ⟨fun h ↦
    ext fun a ↦ not_not.mp (mem_neLocus.not.mp (Finset.eq_empty_iff_forall_not_mem.mp h a)),
    fun h ↦ h ▸ by simp only [neLocus, Ne, eq_self_iff_true, not_true, Finset.filter_False]⟩

Proof state:
α : Type u_1
N : α → Type u_2
inst✝² : DecidableEq α
inst✝¹ : (a : α) → DecidableEq (N a)
inst✝ : (a : α) → Zero (N a)
f g : Π₀ (a : α), N a
h : f = g
⊢ f.neLocus f = ∅

Tactic:
simp only [neLocus, Ne, eq_self_iff_true, not_true, Finset.filter_False]

Result:
no goals
-- Mathlib/.lake/packages/batteries/Batteries/Data/Nat/Gcd.lean
theorem Coprime.eq_one_of_dvd {k m : Nat} (H : Coprime k m) (d : k ∣ m) : k = 1

Proof state:
k m : Nat
H : k.Coprime m
d : k ∣ m
⊢ k = 1

Tactic:
rw [← H.gcd_eq_one, gcd_eq_left d]

Result:
no goals
-- Mathlib/RingTheory/Adjoin/Field.lean
theorem IsIntegral.mem_range_algHom_of_minpoly_splits
    (int : IsIntegral R x) (h : Splits (algebraMap R K) (minpoly R x))(f : K →ₐ[R] L) :
    x ∈ f.range :=
  show x ∈ Set.range f from Set.image_subset_range _ ((minpoly R x).rootSet K) <| by
    rw [image_rootSet h f, mem_rootSet']
    exact ⟨((minpoly.monic int).map _).ne_zero, minpoly.aeval R x⟩

Proof state:
R : Type u_1
K : Type u_2
L : Type u_3
inst✝⁴ : CommRing R
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra R K
x : L
inst✝ : Algebra R L
int : IsIntegral R x
h : Splits (algebraMap R K) (minpoly R x)
f : K →ₐ[R] L
⊢ x ∈ ⇑f '' (minpoly R x).rootSet K

Tactic:
rw [image_rootSet h f, mem_rootSet']

Result:
R : Type u_1
K : Type u_2
L : Type u_3
inst✝⁴ : CommRing R
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra R K
x : L
inst✝ : Algebra R L
int : IsIntegral R x
h : Splits (algebraMap R K) (minpoly R x)
f : K →ₐ[R] L
⊢ Polynomial.map (algebraMap R L) (minpoly R x) ≠ 0 ∧ (aeval x) (minpoly R x) = 0

Proof state:
R : Type u_1
K : Type u_2
L : Type u_3
inst✝⁴ : CommRing R
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra R K
x : L
inst✝ : Algebra R L
int : IsIntegral R x
h : Splits (algebraMap R K) (minpoly R x)
f : K →ₐ[R] L
⊢ Polynomial.map (algebraMap R L) (minpoly R x) ≠ 0 ∧ (aeval x) (minpoly R x) = 0

Tactic:
exact ⟨((minpoly.monic int).map _).ne_zero, minpoly.aeval R x⟩

Result:
no goals
-- Mathlib/RingTheory/Generators.lean
@[simp]
lemma Hom.id_comp [Algebra S S'] (f : Hom P P') : (Hom.id P').comp f = f

Proof state:
R : Type u
S : Type v
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
P : Generators R S
R' : Type u_2
S' : Type u_1
inst✝³ : CommRing R'
inst✝² : CommRing S'
inst✝¹ : Algebra R' S'
P' : Generators R' S'
inst✝ : Algebra S S'
f : P.Hom P'
⊢ (Hom.id P').comp f = f

Tactic:
ext

Result:
case val.h.a
R : Type u
S : Type v
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
P : Generators R S
R' : Type u_2
S' : Type u_1
inst✝³ : CommRing R'
inst✝² : CommRing S'
inst✝¹ : Algebra R' S'
P' : Generators R' S'
inst✝ : Algebra S S'
f : P.Hom P'
x✝ : P.vars
m✝ : P'.vars →₀ ℕ
⊢ coeff m✝ (((Hom.id P').comp f).val x✝) = coeff m✝ (f.val x✝)

Proof state:
case val.h.a
R : Type u
S : Type v
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
P : Generators R S
R' : Type u_2
S' : Type u_1
inst✝³ : CommRing R'
inst✝² : CommRing S'
inst✝¹ : Algebra R' S'
P' : Generators R' S'
inst✝ : Algebra S S'
f : P.Hom P'
x✝ : P.vars
m✝ : P'.vars →₀ ℕ
⊢ coeff m✝ (((Hom.id P').comp f).val x✝) = coeff m✝ (f.val x✝)

Tactic:
simp [Hom.id, aeval_X_left]

Result:
no goals
-- Mathlib/RingTheory/Ideal/Maps.lean
theorem ker_isPrime {F : Type*} [Semiring R] [Semiring S] [IsDomain S]
    [FunLike F R S] [RingHomClass F R S] (f : F) :
    (ker f).IsPrime :=
  ⟨by
    rw [Ne, Ideal.eq_top_iff_one]
    exact not_one_mem_ker f,
   fun {x y} => by
    simpa only [mem_ker, map_mul] using @eq_zero_or_eq_zero_of_mul_eq_zero S _ _ _ _ _⟩

Proof state:
R : Type u
S : Type v
F : Type u_1
inst✝⁴ : Semiring R
inst✝³ : Semiring S
inst✝² : IsDomain S
inst✝¹ : FunLike F R S
inst✝ : RingHomClass F R S
f : F
⊢ 1 ∉ ker f

Tactic:
exact not_one_mem_ker f

Result:
no goals

Proof state:
R : Type u
S : Type v
F : Type u_1
inst✝⁴ : Semiring R
inst✝³ : Semiring S
inst✝² : IsDomain S
inst✝¹ : FunLike F R S
inst✝ : RingHomClass F R S
f : F
⊢ ker f ≠ ⊤

Tactic:
rw [Ne, Ideal.eq_top_iff_one]

Result:
R : Type u
S : Type v
F : Type u_1
inst✝⁴ : Semiring R
inst✝³ : Semiring S
inst✝² : IsDomain S
inst✝¹ : FunLike F R S
inst✝ : RingHomClass F R S
f : F
⊢ 1 ∉ ker f

Proof state:
R : Type u
S : Type v
F : Type u_1
inst✝⁴ : Semiring R
inst✝³ : Semiring S
inst✝² : IsDomain S
inst✝¹ : FunLike F R S
inst✝ : RingHomClass F R S
f : F
x y : R
⊢ x * y ∈ ker f → x ∈ ker f ∨ y ∈ ker f

Tactic:
simpa only [mem_ker, map_mul] using @eq_zero_or_eq_zero_of_mul_eq_zero S _ _ _ _ _

Result:
no goals
-- Mathlib/LinearAlgebra/SesquilinearForm.lean
theorem IsAdjointPair.sub (h : IsAdjointPair B B' f g) (h' : IsAdjointPair B B' f' g') :
    IsAdjointPair B B' (f - f') (g - g') := fun x _ ↦ by
  rw [Pi.sub_apply, Pi.sub_apply, B'.map_sub₂, (B x).map_sub, h, h']

Proof state:
R : Type u_1
M : Type u_5
M₁ : Type u_6
M₂ : Type u_7
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : AddCommGroup M₁
inst✝² : Module R M₁
inst✝¹ : AddCommGroup M₂
inst✝ : Module R M₂
B : M →ₗ[R] M →ₗ[R] M₂
B' : M₁ →ₗ[R] M₁ →ₗ[R] M₂
f f' : M → M₁
g g' : M₁ → M
h : B.IsAdjointPair B' f g
h' : B.IsAdjointPair B' f' g'
x : M
x✝ : M₁
⊢ (B' ((f - f') x)) x✝ = (B x) ((g - g') x✝)

Tactic:
rw [Pi.sub_apply, Pi.sub_apply, B'.map_sub₂, (B x).map_sub, h, h']

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Attach.lean
theorem foldr_pmap (l : Array α) {P : α → Prop} (f : (a : α) → P a → β)
  (H : ∀ (a : α), a ∈ l → P a) (g : β → γ → γ) (x : γ) :
    (l.pmap f H).foldr g x = l.attach.foldr (fun a acc => g (f a.1 (H _ a.2)) acc) x

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
l : Array α
P : α → Prop
f : (a : α) → P a → β
H : ∀ (a : α), a ∈ l → P a
g : β → γ → γ
x : γ
⊢ foldr g x (pmap f l H) = foldr (fun a acc => g (f a.val ⋯) acc) x l.attach

Tactic:
rw [pmap_eq_map_attach, foldr_map]

Result:
no goals
-- Mathlib/Data/Nat/ModEq.lean
theorem add_mod_of_add_mod_lt {a b c : ℕ} (hc : a % c + b % c < c) :
    (a + b) % c = a % c + b % c

Proof state:
a b c : ℕ
hc : a % c + b % c < c
⊢ (a + b) % c = a % c + b % c

Tactic:
rw [← add_mod_add_ite, if_neg (not_le_of_lt hc), add_zero]

Result:
no goals
-- Mathlib/Topology/MetricSpace/HausdorffDistance.lean
theorem infDist_zero_of_mem_closure (hx : x ∈ closure s) : infDist x s = 0

Proof state:
α : Type u
inst✝ : PseudoMetricSpace α
s : Set α
x : α
hx : x ∈ closure s
⊢ infDist x s = 0

Tactic:
rw [← infDist_closure]

Result:
α : Type u
inst✝ : PseudoMetricSpace α
s : Set α
x : α
hx : x ∈ closure s
⊢ infDist x (closure s) = 0

Proof state:
α : Type u
inst✝ : PseudoMetricSpace α
s : Set α
x : α
hx : x ∈ closure s
⊢ infDist x (closure s) = 0

Tactic:
exact infDist_zero_of_mem hx

Result:
no goals
-- Mathlib/Analysis/BoxIntegral/Partition/Basic.lean
theorem iUnion_restrict : (π.restrict J).iUnion = (J : Set (ι → ℝ)) ∩ (π.iUnion)

Proof state:
ι : Type u_1
I J : Box ι
π : Prepartition I
⊢ (π.restrict J).iUnion = ↑J ∩ π.iUnion

Tactic:
simp [restrict, ← inter_iUnion, ← iUnion_def]

Result:
no goals
-- Mathlib/Order/Interval/Finset/Fin.lean
theorem card_fintypeIic : Fintype.card (Set.Iic b) = b + 1

Proof state:
n : ℕ
b : Fin n
⊢ Fintype.card ↑(Set.Iic b) = ↑b + 1

Tactic:
rw [Fintype.card_ofFinset, card_Iic]

Result:
no goals
-- Mathlib/Algebra/MonoidAlgebra/Defs.lean
theorem mul_single_zero_apply [AddZeroClass G] (f : k[G]) (r : k) (x : G) :
    (f * single (0 : G) r) x = f x * r :=
  f.mul_single_apply_aux r _ _ _ fun a _ => by rw [add_zero]

Proof state:
k : Type u₁
G : Type u₂
inst✝¹ : Semiring k
inst✝ : AddZeroClass G
f : k[G]
r : k
x a : G
x✝ : a ∈ f.support
⊢ a + 0 = x ↔ a = x

Tactic:
rw [add_zero]

Result:
no goals
-- Mathlib/Algebra/CharP/Lemmas.lean
lemma prime_ringChar : Nat.Prime (ringChar R)

Proof state:
R : Type u_1
inst✝³ : Ring R
inst✝² : NoZeroDivisors R
inst✝¹ : Nontrivial R
inst✝ : Finite R
⊢ Nat.Prime (ringChar R)

Tactic:
apply CharP.char_prime_of_ne_zero R

Result:
R : Type u_1
inst✝³ : Ring R
inst✝² : NoZeroDivisors R
inst✝¹ : Nontrivial R
inst✝ : Finite R
⊢ ringChar R ≠ 0

Proof state:
R : Type u_1
inst✝³ : Ring R
inst✝² : NoZeroDivisors R
inst✝¹ : Nontrivial R
inst✝ : Finite R
⊢ ringChar R ≠ 0

Tactic:
exact CharP.ringChar_ne_zero_of_finite R

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem filter_eq_empty_iff {p : α → Bool} {l : Array α} :
    filter p l = #[] ↔ ∀ a, a ∈ l → ¬p a

Proof state:
α : Type u_1
p : α → Bool
l : Array α
⊢ filter p l = #[] ↔ ∀ (a : α), a ∈ l → ¬p a = true

Tactic:
rcases l with ⟨l⟩

Result:
case mk
α : Type u_1
p : α → Bool
l : List α
⊢ filter p { toList := l } = #[] ↔ ∀ (a : α), a ∈ { toList := l } → ¬p a = true

Proof state:
case mk
α : Type u_1
p : α → Bool
l : List α
⊢ filter p { toList := l } = #[] ↔ ∀ (a : α), a ∈ { toList := l } → ¬p a = true

Tactic:
simp

Result:
no goals
-- Mathlib/Algebra/Lie/Weights/Basic.lean
theorem mem_genWeightSpace (χ : L → R) (m : M) :
    m ∈ genWeightSpace M χ ↔ ∀ x, ∃ k : ℕ, ((toEnd R L M x - χ x • ↑1) ^ k) m = 0

Proof state:
R : Type u_2
L : Type u_3
M : Type u_4
inst✝⁷ : CommRing R
inst✝⁶ : LieRing L
inst✝⁵ : LieAlgebra R L
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : LieRingModule L M
inst✝¹ : LieModule R L M
inst✝ : LieRing.IsNilpotent L
χ : L → R
m : M
⊢ m ∈ genWeightSpace M χ ↔ ∀ (x : L), ∃ k, (((toEnd R L M) x - χ x • 1) ^ k) m = 0

Tactic:
simp [genWeightSpace, mem_genWeightSpaceOf]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/RawLemmas.lean
theorem get?_empty [LawfulBEq α] {a : α} {c} : (empty c : Raw₀ α β).get? a = none

Proof state:
α : Type u
β : α → Type v
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : LawfulBEq α
a : α
c : Nat
⊢ (empty c).get? a = none

Tactic:
simp [get?]

Result:
no goals
-- Mathlib/MeasureTheory/MeasurableSpace/Basic.lean
theorem measurableSet_range_inl [MeasurableSpace α] :
    MeasurableSet (range Sum.inl : Set (α ⊕ β))

Proof state:
α : Type u_1
β : Type u_2
mβ : MeasurableSpace β
inst✝ : MeasurableSpace α
⊢ MeasurableSet (Sum.inl '' univ)

Tactic:
exact MeasurableSet.univ.inl_image

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
mβ : MeasurableSpace β
inst✝ : MeasurableSpace α
⊢ MeasurableSet (range Sum.inl)

Tactic:
rw [← image_univ]

Result:
α : Type u_1
β : Type u_2
mβ : MeasurableSpace β
inst✝ : MeasurableSpace α
⊢ MeasurableSet (Sum.inl '' univ)