harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/SetTheory/Cardinal/Basic.lean
theorem one_lt_iff_nontrivial {α : Type u} : 1 < #α ↔ Nontrivial α

Proof state:
α : Type u
⊢ 1 < #α ↔ Nontrivial α

Tactic:
rw [← not_le, le_one_iff_subsingleton, ← not_nontrivial_iff_subsingleton, Classical.not_not]

Result:
no goals
-- Mathlib/RingTheory/Flat/Basic.lean
theorem iff_rTensor_injective' :
    Flat R M ↔ ∀ I : Ideal R, Function.Injective (rTensor M I.subtype)

Proof state:
R : Type u
M : Type v
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
⊢ Flat R M ↔ ∀ (I : Ideal R), Function.Injective ⇑(rTensor M (Submodule.subtype I))

Tactic:
simp_rw [iff_characterModule_baer, Baer, rTensor_injective_iff_lcomp_surjective,
  Surjective, DFunLike.ext_iff, Subtype.forall]

Result:
R : Type u
M : Type v
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
⊢ (∀ (I : Ideal R) (g : ↥I →ₗ[R] CharacterModule M),
      ∃ g', ∀ (x : R) (mem : x ∈ I) (x_1 : M), (g' x) x_1 = (g ⟨x, mem⟩) x_1) ↔
    ∀ (I : Ideal R) (b : ↥I →ₗ[R] CharacterModule M),
      ∃ a,
        ∀ (a_1 : R) (b_1 : a_1 ∈ I) (x : M),
          (((lcomp R (CharacterModule M) (Submodule.subtype I)) a) ⟨a_1, b_1⟩) x = (b ⟨a_1, b_1⟩) x

Proof state:
R : Type u
M : Type v
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
⊢ (∀ (I : Ideal R) (g : ↥I →ₗ[R] CharacterModule M),
      ∃ g', ∀ (x : R) (mem : x ∈ I) (x_1 : M), (g' x) x_1 = (g ⟨x, mem⟩) x_1) ↔
    ∀ (I : Ideal R) (b : ↥I →ₗ[R] CharacterModule M),
      ∃ a,
        ∀ (a_1 : R) (b_1 : a_1 ∈ I) (x : M),
          (((lcomp R (CharacterModule M) (Submodule.subtype I)) a) ⟨a_1, b_1⟩) x = (b ⟨a_1, b_1⟩) x

Tactic:
rfl

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem reverse_eq_append_iff {xs ys zs : Array α} :
    xs.reverse = ys ++ zs ↔ xs = zs.reverse ++ ys.reverse

Proof state:
case mk
α : Type u_1
ys zs : Array α
toList✝ : List α
⊢ { toList := toList✝ }.reverse = ys ++ zs ↔ { toList := toList✝ } = zs.reverse ++ ys.reverse

Tactic:
cases ys

Result:
case mk.mk
α : Type u_1
zs : Array α
toList✝¹ toList✝ : List α
⊢ { toList := toList✝¹ }.reverse = { toList := toList✝ } ++ zs ↔
    { toList := toList✝¹ } = zs.reverse ++ { toList := toList✝ }.reverse

Proof state:
case mk.mk.mk
α : Type u_1
toList✝² toList✝¹ toList✝ : List α
⊢ { toList := toList✝² }.reverse = { toList := toList✝¹ } ++ { toList := toList✝ } ↔
    { toList := toList✝² } = { toList := toList✝ }.reverse ++ { toList := toList✝¹ }.reverse

Tactic:
simp

Result:
no goals

Proof state:
case mk.mk
α : Type u_1
zs : Array α
toList✝¹ toList✝ : List α
⊢ { toList := toList✝¹ }.reverse = { toList := toList✝ } ++ zs ↔
    { toList := toList✝¹ } = zs.reverse ++ { toList := toList✝ }.reverse

Tactic:
cases zs

Result:
case mk.mk.mk
α : Type u_1
toList✝² toList✝¹ toList✝ : List α
⊢ { toList := toList✝² }.reverse = { toList := toList✝¹ } ++ { toList := toList✝ } ↔
    { toList := toList✝² } = { toList := toList✝ }.reverse ++ { toList := toList✝¹ }.reverse

Proof state:
α : Type u_1
xs ys zs : Array α
⊢ xs.reverse = ys ++ zs ↔ xs = zs.reverse ++ ys.reverse

Tactic:
cases xs

Result:
case mk
α : Type u_1
ys zs : Array α
toList✝ : List α
⊢ { toList := toList✝ }.reverse = ys ++ zs ↔ { toList := toList✝ } = zs.reverse ++ ys.reverse
-- Mathlib/CategoryTheory/Monoidal/Functor.lean
@[reassoc (attr := simp)]
lemma whiskerRight_δ_μ (X Y : C) (T : D) : δ F X Y ▷ T ≫ μ F X Y ▷ T = 𝟙 _

Proof state:
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : MonoidalCategory D
F : C ⥤ D
inst✝ : F.Monoidal
X Y : C
T : D
⊢ δ F X Y ▷ T ≫ μ F X Y ▷ T = 𝟙 (F.obj (X ⊗ Y) ⊗ T)

Tactic:
rw [← MonoidalCategory.comp_whiskerRight, δ_μ, id_whiskerRight]

Result:
no goals
-- Mathlib/Algebra/Squarefree/Basic.lean
theorem Squarefree.isRadical {x : R} (hx : Squarefree x) : IsRadical x :=
  (isRadical_iff_pow_one_lt 2 one_lt_two).2 fun y hy ↦ by
    obtain ⟨a, b, ha, hb, rfl⟩ := exists_dvd_and_dvd_of_dvd_mul (sq y ▸ hy)
    exact (IsRelPrime.of_squarefree_mul hx).mul_dvd ha hb

Proof state:
case intro.intro.intro.intro
R : Type u_1
inst✝¹ : CommMonoidWithZero R
inst✝ : DecompositionMonoid R
y a b : R
ha : a ∣ y
hb : b ∣ y
hx : Squarefree (a * b)
hy : a * b ∣ y ^ 2
⊢ a * b ∣ y

Tactic:
exact (IsRelPrime.of_squarefree_mul hx).mul_dvd ha hb

Result:
no goals

Proof state:
R : Type u_1
inst✝¹ : CommMonoidWithZero R
inst✝ : DecompositionMonoid R
x : R
hx : Squarefree x
y : R
hy : x ∣ y ^ 2
⊢ x ∣ y

Tactic:
obtain ⟨a, b, ha, hb, rfl⟩ := exists_dvd_and_dvd_of_dvd_mul (sq y ▸ hy)

Result:
case intro.intro.intro.intro
R : Type u_1
inst✝¹ : CommMonoidWithZero R
inst✝ : DecompositionMonoid R
y a b : R
ha : a ∣ y
hb : b ∣ y
hx : Squarefree (a * b)
hy : a * b ∣ y ^ 2
⊢ a * b ∣ y
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem append_eq_mkArray_iff {l₁ l₂ : Array α} {a : α} :
    l₁ ++ l₂ = mkArray n a ↔
      l₁.size + l₂.size = n ∧ l₁ = mkArray l₁.size a ∧ l₂ = mkArray l₂.size a

Proof state:
α : Type u_1
n : Nat
l₁ l₂ : Array α
a : α
⊢ l₁ ++ l₂ = mkArray n a ↔ l₁.size + l₂.size = n ∧ l₁ = mkArray l₁.size a ∧ l₂ = mkArray l₂.size a

Tactic:
simp [← toList_inj, List.append_eq_replicate_iff]

Result:
no goals
-- Mathlib/LinearAlgebra/Lagrange.lean
theorem eq_of_degree_sub_lt_of_eval_finset_eq (degree_fg_lt : (f - g).degree < #s)
    (eval_fg : ∀ x ∈ s, f.eval x = g.eval x) : f = g

Proof state:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
f g : R[X]
s : Finset R
degree_fg_lt : (f - g).degree < ↑(#s)
eval_fg : ∀ x ∈ s, eval x f = eval x g
⊢ ∀ x ∈ s, eval x f = eval x g

Tactic:
exact eval_fg

Result:
no goals

Proof state:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
f g : R[X]
s : Finset R
degree_fg_lt : (f - g).degree < ↑(#s)
eval_fg : ∀ x ∈ s, eval x f = eval x g
⊢ f - g = 0

Tactic:
refine eq_zero_of_degree_lt_of_eval_finset_eq_zero _ degree_fg_lt ?_

Result:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
f g : R[X]
s : Finset R
degree_fg_lt : (f - g).degree < ↑(#s)
eval_fg : ∀ x ∈ s, eval x f = eval x g
⊢ ∀ x ∈ s, eval x (f - g) = 0

Proof state:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
f g : R[X]
s : Finset R
degree_fg_lt : (f - g).degree < ↑(#s)
eval_fg : ∀ x ∈ s, eval x f = eval x g
⊢ ∀ x ∈ s, eval x (f - g) = 0

Tactic:
simp_rw [eval_sub, sub_eq_zero]

Result:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
f g : R[X]
s : Finset R
degree_fg_lt : (f - g).degree < ↑(#s)
eval_fg : ∀ x ∈ s, eval x f = eval x g
⊢ ∀ x ∈ s, eval x f = eval x g

Proof state:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
f g : R[X]
s : Finset R
degree_fg_lt : (f - g).degree < ↑(#s)
eval_fg : ∀ x ∈ s, eval x f = eval x g
⊢ f = g

Tactic:
rw [← sub_eq_zero]

Result:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
f g : R[X]
s : Finset R
degree_fg_lt : (f - g).degree < ↑(#s)
eval_fg : ∀ x ∈ s, eval x f = eval x g
⊢ f - g = 0
-- Mathlib/Order/Hom/Basic.lean
theorem refl_trans (e : α ≃o β) : (refl α).trans e = e

Proof state:
α : Type u_2
β : Type u_3
inst✝¹ : LE α
inst✝ : LE β
e : α ≃o β
⊢ (refl α).trans e = e

Tactic:
ext x

Result:
case h.h
α : Type u_2
β : Type u_3
inst✝¹ : LE α
inst✝ : LE β
e : α ≃o β
x : α
⊢ ((refl α).trans e) x = e x

Proof state:
case h.h
α : Type u_2
β : Type u_3
inst✝¹ : LE α
inst✝ : LE β
e : α ≃o β
x : α
⊢ ((refl α).trans e) x = e x

Tactic:
rfl

Result:
no goals
-- Mathlib/Analysis/Calculus/Deriv/Add.lean
theorem derivWithin_const_add (c : F) :
    derivWithin (c + f ·) s x = derivWithin f s x

Proof state:
𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : 𝕜 → F
x : 𝕜
s : Set 𝕜
c : F
⊢ derivWithin (fun x => c + f x) s x = derivWithin f s x

Tactic:
simp only [derivWithin, fderivWithin_const_add]

Result:
no goals
-- Mathlib/GroupTheory/Congruence/Defs.lean
theorem induction_on_units {p : Units c.Quotient → Prop} (u : Units c.Quotient)
    (H : ∀ (x y : M) (hxy : c (x * y) 1) (hyx : c (y * x) 1), p ⟨x, y, c.eq.2 hxy, c.eq.2 hyx⟩) :
    p u

Proof state:
M : Type u_1
inst✝ : Monoid M
c : Con M
p : c.Quotientˣ → Prop
u : c.Quotientˣ
H : ∀ (x y : M) (hxy : c (x * y) 1) (hyx : c (y * x) 1), p { val := ↑x, inv := ↑y, val_inv := ⋯, inv_val := ⋯ }
⊢ p u

Tactic:
rcases u with ⟨⟨x⟩, ⟨y⟩, h₁, h₂⟩

Result:
case mk.mk.mk
M : Type u_1
inst✝ : Monoid M
c : Con M
p : c.Quotientˣ → Prop
H : ∀ (x y : M) (hxy : c (x * y) 1) (hyx : c (y * x) 1), p { val := ↑x, inv := ↑y, val_inv := ⋯, inv_val := ⋯ }
val✝ inv✝ : c.Quotient
x y : M
h₁ : Quot.mk (⇑c.toSetoid) x * Quot.mk (⇑c.toSetoid) y = 1
h₂ : Quot.mk (⇑c.toSetoid) y * Quot.mk (⇑c.toSetoid) x = 1
⊢ p { val := Quot.mk (⇑c.toSetoid) x, inv := Quot.mk (⇑c.toSetoid) y, val_inv := h₁, inv_val := h₂ }

Proof state:
case mk.mk.mk
M : Type u_1
inst✝ : Monoid M
c : Con M
p : c.Quotientˣ → Prop
H : ∀ (x y : M) (hxy : c (x * y) 1) (hyx : c (y * x) 1), p { val := ↑x, inv := ↑y, val_inv := ⋯, inv_val := ⋯ }
val✝ inv✝ : c.Quotient
x y : M
h₁ : Quot.mk (⇑c.toSetoid) x * Quot.mk (⇑c.toSetoid) y = 1
h₂ : Quot.mk (⇑c.toSetoid) y * Quot.mk (⇑c.toSetoid) x = 1
⊢ p { val := Quot.mk (⇑c.toSetoid) x, inv := Quot.mk (⇑c.toSetoid) y, val_inv := h₁, inv_val := h₂ }

Tactic:
exact H x y (c.eq.1 h₁) (c.eq.1 h₂)

Result:
no goals
-- Mathlib/Data/Fin/Parity.lean
lemma not_even_iff_odd_of_even {n : ℕ} [NeZero n] (hn : Even n) {k : Fin n} : ¬Even k ↔ Odd k

Proof state:
n : ℕ
inst✝ : NeZero n
hn : Even n
k : Fin n
⊢ ¬Even ↑k ↔ Odd ↑k

Tactic:
exact Nat.not_even_iff_odd

Result:
no goals

Proof state:
n : ℕ
inst✝ : NeZero n
hn : Even n
k : Fin n
⊢ ¬Even k ↔ Odd k

Tactic:
rw [even_iff_of_even hn, odd_iff_of_even hn]

Result:
n : ℕ
inst✝ : NeZero n
hn : Even n
k : Fin n
⊢ ¬Even ↑k ↔ Odd ↑k
-- Mathlib/Topology/Bornology/Basic.lean
theorem nonempty_of_not_isBounded (h : ¬IsBounded s) : s.Nonempty

Proof state:
α : Type u_2
x✝ : Bornology α
s : Set α
h : ¬IsBounded s
⊢ s ≠ ∅

Tactic:
rintro rfl

Result:
α : Type u_2
x✝ : Bornology α
h : ¬IsBounded ∅
⊢ False

Proof state:
α : Type u_2
x✝ : Bornology α
s : Set α
h : ¬IsBounded s
⊢ s.Nonempty

Tactic:
rw [nonempty_iff_ne_empty]

Result:
α : Type u_2
x✝ : Bornology α
s : Set α
h : ¬IsBounded s
⊢ s ≠ ∅

Proof state:
α : Type u_2
x✝ : Bornology α
h : ¬IsBounded ∅
⊢ False

Tactic:
exact h isBounded_empty

Result:
no goals
-- Mathlib/Order/Filter/AtTopBot/Field.lean
theorem tendsto_mul_const_atBot_iff_pos [NeBot l] (h : Tendsto f l atBot) :
    Tendsto (fun x => f x * r) l atBot ↔ 0 < r

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrderedField α
l : Filter β
f : β → α
r : α
inst✝ : l.NeBot
h : Tendsto f l atBot
⊢ Tendsto (fun x => f x * r) l atBot ↔ 0 < r

Tactic:
simp only [mul_comm _ r, tendsto_const_mul_atBot_iff_pos h]

Result:
no goals
-- Mathlib/Algebra/Category/Grp/Limits.lean
/-- A functor `F : J ⥤ Grp.{u}` has a limit iff `(F ⋙ forget Grp).sections` is
`u`-small. -/
@[to_additive "A functor `F : J ⥤ AddGrp.{u}` has a limit iff
`(F ⋙ forget AddGrp).sections` is `u`-small."]
lemma hasLimit_iff_small_sections :
    HasLimit F ↔ Small.{u} (F ⋙ forget Grp).sections

Proof state:
case mp
J : Type v
inst✝ : Category.{w, v} J
F : J ⥤ Grp
⊢ HasLimit F → Small.{u, max u v} ↑(F ⋙ forget Grp).sections

Tactic:
apply Concrete.small_sections_of_hasLimit

Result:
no goals

Proof state:
J : Type v
inst✝ : Category.{w, v} J
F : J ⥤ Grp
⊢ HasLimit F ↔ Small.{u, max u v} ↑(F ⋙ forget Grp).sections

Tactic:
constructor

Result:
case mp
J : Type v
inst✝ : Category.{w, v} J
F : J ⥤ Grp
⊢ HasLimit F → Small.{u, max u v} ↑(F ⋙ forget Grp).sections

case mpr
J : Type v
inst✝ : Category.{w, v} J
F : J ⥤ Grp
⊢ Small.{u, max u v} ↑(F ⋙ forget Grp).sections → HasLimit F

Proof state:
case mpr
J : Type v
inst✝ : Category.{w, v} J
F : J ⥤ Grp
⊢ Small.{u, max u v} ↑(F ⋙ forget Grp).sections → HasLimit F

Tactic:
intro

Result:
case mpr
J : Type v
inst✝ : Category.{w, v} J
F : J ⥤ Grp
a✝ : Small.{u, max u v} ↑(F ⋙ forget Grp).sections
⊢ HasLimit F

Proof state:
case mpr
J : Type v
inst✝ : Category.{w, v} J
F : J ⥤ Grp
a✝ : Small.{u, max u v} ↑(F ⋙ forget Grp).sections
⊢ HasLimit F

Tactic:
infer_instance

Result:
no goals
-- Mathlib/Data/Fintype/Basic.lean
theorem Fin.image_succ_univ (n : ℕ) : (univ : Finset (Fin n)).image Fin.succ = {0}ᶜ

Proof state:
n : ℕ
⊢ image succ univ = {0}ᶜ

Tactic:
rw [← Fin.succAbove_zero, Fin.image_succAbove_univ]

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Subgraph.lean
theorem verts_spanningCoe_injective :
    (fun G' : Subgraph G => (G'.verts, G'.spanningCoe)).Injective

Proof state:
V : Type u
G : SimpleGraph V
G₁ G₂ : G.Subgraph
h : (fun G' => (G'.verts, G'.spanningCoe)) G₁ = (fun G' => (G'.verts, G'.spanningCoe)) G₂
⊢ G₁ = G₂

Tactic:
rw [Prod.ext_iff] at h

Result:
V : Type u
G : SimpleGraph V
G₁ G₂ : G.Subgraph
h :
  ((fun G' => (G'.verts, G'.spanningCoe)) G₁).1 = ((fun G' => (G'.verts, G'.spanningCoe)) G₂).1 ∧
    ((fun G' => (G'.verts, G'.spanningCoe)) G₁).2 = ((fun G' => (G'.verts, G'.spanningCoe)) G₂).2
⊢ G₁ = G₂

Proof state:
V : Type u
G : SimpleGraph V
⊢ Function.Injective fun G' => (G'.verts, G'.spanningCoe)

Tactic:
intro G₁ G₂ h

Result:
V : Type u
G : SimpleGraph V
G₁ G₂ : G.Subgraph
h : (fun G' => (G'.verts, G'.spanningCoe)) G₁ = (fun G' => (G'.verts, G'.spanningCoe)) G₂
⊢ G₁ = G₂

Proof state:
V : Type u
G : SimpleGraph V
G₁ G₂ : G.Subgraph
h :
  ((fun G' => (G'.verts, G'.spanningCoe)) G₁).1 = ((fun G' => (G'.verts, G'.spanningCoe)) G₂).1 ∧
    ((fun G' => (G'.verts, G'.spanningCoe)) G₁).2 = ((fun G' => (G'.verts, G'.spanningCoe)) G₂).2
⊢ G₁ = G₂

Tactic:
exact Subgraph.ext h.1 (spanningCoe_inj.1 h.2)

Result:
no goals
-- Mathlib/Algebra/Polynomial/Smeval.lean
theorem eval_eq_smeval : p.eval r = p.smeval r

Proof state:
R : Type u_1
inst✝ : Semiring R
r : R
p : R[X]
⊢ (p.sum fun e a => a * r ^ e) = p.sum (smul_pow r)

Tactic:
rfl

Result:
no goals

Proof state:
R : Type u_1
inst✝ : Semiring R
r : R
p : R[X]
⊢ eval r p = p.smeval r

Tactic:
rw [eval_eq_sum, smeval_eq_sum]

Result:
R : Type u_1
inst✝ : Semiring R
r : R
p : R[X]
⊢ (p.sum fun e a => a * r ^ e) = p.sum (smul_pow r)
-- Mathlib/Analysis/RCLike/Inner.lean
lemma inner_eq_wInner_one (f g : PiLp 2 fun _i : ι ↦ 𝕜) :
    inner f g = ⟪WithLp.equiv 2 _ f, WithLp.equiv 2 _ g⟫_[𝕜, 1]

Proof state:
ι : Type u_1
𝕜 : Type u_3
inst✝¹ : Fintype ι
inst✝ : RCLike 𝕜
f g : PiLp 2 fun _i => 𝕜
⊢ inner f g = wInner 1 ((WithLp.equiv 2 (ι → 𝕜)) f) ((WithLp.equiv 2 (ι → 𝕜)) g)

Tactic:
simp [wInner]

Result:
no goals
-- Mathlib/Algebra/Group/Subgroup/Basic.lean
theorem conj_mem_conjugatesOfSet {x c : G} :
    x ∈ conjugatesOfSet s → c * x * c⁻¹ ∈ conjugatesOfSet s := fun H => by
  rcases mem_conjugatesOfSet_iff.1 H with ⟨a, h₁, h₂⟩
  exact mem_conjugatesOfSet_iff.2 ⟨a, h₁, h₂.trans (isConj_iff.2 ⟨c, rfl⟩)⟩

Proof state:
G : Type u_1
inst✝ : Group G
s : Set G
x c : G
H : x ∈ conjugatesOfSet s
⊢ c * x * c⁻¹ ∈ conjugatesOfSet s

Tactic:
rcases mem_conjugatesOfSet_iff.1 H with ⟨a, h₁, h₂⟩

Result:
case intro.intro
G : Type u_1
inst✝ : Group G
s : Set G
x c : G
H : x ∈ conjugatesOfSet s
a : G
h₁ : a ∈ s
h₂ : IsConj a x
⊢ c * x * c⁻¹ ∈ conjugatesOfSet s

Proof state:
case intro.intro
G : Type u_1
inst✝ : Group G
s : Set G
x c : G
H : x ∈ conjugatesOfSet s
a : G
h₁ : a ∈ s
h₂ : IsConj a x
⊢ c * x * c⁻¹ ∈ conjugatesOfSet s

Tactic:
exact mem_conjugatesOfSet_iff.2 ⟨a, h₁, h₂.trans (isConj_iff.2 ⟨c, rfl⟩)⟩

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Connectivity/Represents.lean
lemma ncard_inter (hrep : Represents s C) (h : c ∈ C) : (s ∩ c.supp).ncard = 1

Proof state:
V : Type u
G : SimpleGraph V
C : Set G.ConnectedComponent
s : Set V
c : G.ConnectedComponent
hrep : Represents s C
h : c ∈ C
⊢ (s ∩ c.supp).ncard = 1

Tactic:
rw [Set.ncard_eq_one]

Result:
V : Type u
G : SimpleGraph V
C : Set G.ConnectedComponent
s : Set V
c : G.ConnectedComponent
hrep : Represents s C
h : c ∈ C
⊢ ∃ a, s ∩ c.supp = {a}

Proof state:
V : Type u
G : SimpleGraph V
C : Set G.ConnectedComponent
s : Set V
c : G.ConnectedComponent
hrep : Represents s C
h : c ∈ C
⊢ ∃ a, s ∩ c.supp = {a}

Tactic:
exact exists_inter_eq_singleton hrep h

Result:
no goals
-- Mathlib/Data/ENNReal/Real.lean
@[simp]
lemma natCast_le_ofReal {n : ℕ} {p : ℝ} (hn : n ≠ 0) : n ≤ ENNReal.ofReal p ↔ n ≤ p

Proof state:
n : ℕ
p : ℝ
hn : n ≠ 0
⊢ ↑n ≤ ENNReal.ofReal p ↔ ↑n ≤ p

Tactic:
simp only [← not_lt, ofReal_lt_natCast hn]

Result:
no goals
-- Mathlib/Data/List/Sublists.lean
theorem mem_sublists {s t : List α} : s ∈ sublists t ↔ s <+ t

Proof state:
α : Type u
s t : List α
⊢ s ∈ t.sublists ↔ s <+ t

Tactic:
rw [← reverse_sublist, ← mem_sublists', sublists'_reverse,
  mem_map_of_injective reverse_injective]

Result:
no goals
-- Mathlib/Data/NNRat/Defs.lean
theorem ext_num_den (hn : p.num = q.num) (hd : p.den = q.den) : p = q

Proof state:
p q : ℚ≥0
hn : p.num = q.num
hd : p.den = q.den
⊢ (↑p).num = (↑q).num

Tactic:
simpa [num_coe]

Result:
no goals

Proof state:
p q : ℚ≥0
hn : p.num = q.num
hd : p.den = q.den
⊢ p = q

Tactic:
refine ext <| Rat.ext ?_ hd

Result:
p q : ℚ≥0
hn : p.num = q.num
hd : p.den = q.den
⊢ (↑p).num = (↑q).num
-- Mathlib/MeasureTheory/Integral/SetToL1.lean
theorem setToL1_smul (hT : DominatedFinMeasAdditive μ T C)
    (h_smul : ∀ c : 𝕜, ∀ s x, T s (c • x) = c • T s x) (c : 𝕜) (f : α →₁[μ] E) :
    setToL1 hT (c • f) = c • setToL1 hT f

Proof state:
α : Type u_1
E : Type u_2
F : Type u_3
𝕜 : Type u_6
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedSpace 𝕜 F
inst✝ : CompleteSpace F
T : Set α → E →L[ℝ] F
C : ℝ
hT : DominatedFinMeasAdditive μ T C
h_smul : ∀ (c : 𝕜) (s : Set α) (x : E), (T s) (c • x) = c • (T s) x
c : 𝕜
f : ↥(Lp E 1 μ)
⊢ (setToL1 hT) (c • f) = c • (setToL1 hT) f

Tactic:
rw [setToL1_eq_setToL1' hT h_smul, setToL1_eq_setToL1' hT h_smul]

Result:
α : Type u_1
E : Type u_2
F : Type u_3
𝕜 : Type u_6
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedSpace 𝕜 F
inst✝ : CompleteSpace F
T : Set α → E →L[ℝ] F
C : ℝ
hT : DominatedFinMeasAdditive μ T C
h_smul : ∀ (c : 𝕜) (s : Set α) (x : E), (T s) (c • x) = c • (T s) x
c : 𝕜
f : ↥(Lp E 1 μ)
⊢ (setToL1' 𝕜 hT h_smul) (c • f) = c • (setToL1' 𝕜 hT h_smul) f

Proof state:
α : Type u_1
E : Type u_2
F : Type u_3
𝕜 : Type u_6
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedSpace 𝕜 F
inst✝ : CompleteSpace F
T : Set α → E →L[ℝ] F
C : ℝ
hT : DominatedFinMeasAdditive μ T C
h_smul : ∀ (c : 𝕜) (s : Set α) (x : E), (T s) (c • x) = c • (T s) x
c : 𝕜
f : ↥(Lp E 1 μ)
⊢ (setToL1' 𝕜 hT h_smul) (c • f) = c • (setToL1' 𝕜 hT h_smul) f

Tactic:
exact ContinuousLinearMap.map_smul _ _ _

Result:
no goals
-- Mathlib/GroupTheory/DoubleCoset.lean
lemma doset_eq_image2 (a : α) (s t : Set α) : doset a s t = Set.image2 (· * a * ·) s t

Proof state:
α : Type u_2
inst✝ : Mul α
a : α
s t : Set α
⊢ doset a s t = Set.image2 (fun x1 x2 => x1 * a * x2) s t

Tactic:
simp_rw [doset, Set.mul_singleton, ← Set.image2_mul, Set.image2_image_left]

Result:
no goals
-- Mathlib/RingTheory/Jacobson/Semiprimary.lean
theorem IsSemisimpleModule.jacobson_le_ker [IsSemisimpleModule R₂ M₂] :
    Module.jacobson R M ≤ LinearMap.ker f :=
  (Module.le_comap_jacobson f).trans <| by simp_rw [jacobson_eq_bot, LinearMap.ker, le_rfl]

Proof state:
R : Type u_1
R₂ : Type u_2
M : Type u_3
M₂ : Type u_4
inst✝⁹ : Ring R
inst✝⁸ : Ring R₂
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : AddCommGroup M₂
inst✝⁴ : Module R₂ M₂
τ₁₂ : R →+* R₂
inst✝³ : RingHomSurjective τ₁₂
F : Type u_5
inst✝² : FunLike F M M₂
inst✝¹ : SemilinearMapClass F τ₁₂ M M₂
f : F
inst✝ : IsSemisimpleModule R₂ M₂
⊢ Submodule.comap f (Module.jacobson R₂ M₂) ≤ LinearMap.ker f

Tactic:
simp_rw [jacobson_eq_bot, LinearMap.ker, le_rfl]

Result:
no goals
-- Mathlib/Order/Hom/Lattice.lean
theorem withTopWithBot_id : (LatticeHom.id α).withTopWithBot = BoundedLatticeHom.id _ :=
  DFunLike.coe_injective <| by
    refine (congr_arg Option.map ?_).trans Option.map_id
    rw [withBot_id]
    rfl

Proof state:
α : Type u_3
inst✝ : Lattice α
⊢ ⇑(LatticeHom.id (WithBot α)).toSupHom = id

Tactic:
rfl

Result:
no goals

Proof state:
α : Type u_3
inst✝ : Lattice α
⊢ ⇑(LatticeHom.id α).withBot.toSupHom = id

Tactic:
rw [withBot_id]

Result:
α : Type u_3
inst✝ : Lattice α
⊢ ⇑(LatticeHom.id (WithBot α)).toSupHom = id

Proof state:
α : Type u_3
inst✝ : Lattice α
⊢ (fun f => ⇑f) (LatticeHom.id α).withTopWithBot = (fun f => ⇑f) (BoundedLatticeHom.id (WithTop (WithBot α)))

Tactic:
refine (congr_arg Option.map ?_).trans Option.map_id

Result:
α : Type u_3
inst✝ : Lattice α
⊢ ⇑(LatticeHom.id α).withBot.toSupHom = id
-- Mathlib/SetTheory/Ordinal/NaturalOps.lean
theorem nadd_zero (a : Ordinal) : a ♯ 0 = a

Proof state:
case h.e'_2.h.e'_4.h.h.e'_4.mk
a val✝ : Ordinal.{u_1}
property✝ : val✝ ∈ Iio a
⊢ ↑⟨val✝, property✝⟩ ♯ 0 = ↑⟨val✝, property✝⟩

Tactic:
exact nadd_zero _

Result:
no goals

Proof state:
case h.e'_2.h.e'_4.h.h.e'_4
a : Ordinal.{u_1}
x : ↑(Iio a)
⊢ ↑x ♯ 0 = ↑x

Tactic:
cases x

Result:
case h.e'_2.h.e'_4.h.h.e'_4.mk
a val✝ : Ordinal.{u_1}
property✝ : val✝ ∈ Iio a
⊢ ↑⟨val✝, property✝⟩ ♯ 0 = ↑⟨val✝, property✝⟩

Proof state:
case h.e'_2.h.e'_4.h.h.e'_4
a : Ordinal.{u_1}
x✝ : ↑(Iio a)
⊢ ↑x✝ ♯ 0 = ↑x✝

Tactic:
rename_i x

Result:
case h.e'_2.h.e'_4.h.h.e'_4
a : Ordinal.{u_1}
x : ↑(Iio a)
⊢ ↑x ♯ 0 = ↑x

Proof state:
a : Ordinal.{u_1}
⊢ a ♯ 0 = a

Tactic:
rw [nadd, ciSup_of_empty fun _ : Iio 0 ↦ _, sup_bot_eq]

Result:
a : Ordinal.{u_1}
⊢ ⨆ x, succ (↑x ♯ 0) = a

Proof state:
a : Ordinal.{u_1}
⊢ ⨆ x, succ (↑x ♯ 0) = a

Tactic:
convert iSup_succ a

Result:
case h.e'_2.h.e'_4.h.h.e'_4
a : Ordinal.{u_1}
x✝ : ↑(Iio a)
⊢ ↑x✝ ♯ 0 = ↑x✝
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/RawLemmas.lean
theorem getKey!_insertManyIfNewUnit_list_of_not_mem_of_contains_eq_false
    [EquivBEq α] [LawfulHashable α] [Inhabited α] (h : m.WF) {l : List α} {k : α} :
    ¬ k ∈ m → l.contains k = false → getKey! (insertManyIfNewUnit m l) k = default

Proof state:
α : Type u
inst✝⁴ : BEq α
inst✝³ : Hashable α
m : Raw α fun x => Unit
inst✝² : EquivBEq α
inst✝¹ : LawfulHashable α
inst✝ : Inhabited α
h : m.WF
l : List α
k : α
⊢ m.contains k = false → l.contains k = false → (insertManyIfNewUnit m l).getKey! k = default

Tactic:
simp_to_raw using
  Raw₀.Const.getKey!_insertManyIfNewUnit_list_of_contains_eq_false_of_contains_eq_false

Result:
no goals

Proof state:
α : Type u
inst✝⁴ : BEq α
inst✝³ : Hashable α
m : Raw α fun x => Unit
inst✝² : EquivBEq α
inst✝¹ : LawfulHashable α
inst✝ : Inhabited α
h : m.WF
l : List α
k : α
⊢ ¬k ∈ m → l.contains k = false → (insertManyIfNewUnit m l).getKey! k = default

Tactic:
simp only [mem_iff_contains, Bool.not_eq_true]

Result:
α : Type u
inst✝⁴ : BEq α
inst✝³ : Hashable α
m : Raw α fun x => Unit
inst✝² : EquivBEq α
inst✝¹ : LawfulHashable α
inst✝ : Inhabited α
h : m.WF
l : List α
k : α
⊢ m.contains k = false → l.contains k = false → (insertManyIfNewUnit m l).getKey! k = default
-- Mathlib/Algebra/Group/Indicator.lean
theorem mulIndicator_apply_ne_one {a : α} : s.mulIndicator f a ≠ 1 ↔ a ∈ s ∩ mulSupport f

Proof state:
α : Type u_1
M : Type u_3
inst✝ : One M
s : Set α
f : α → M
a : α
⊢ s.mulIndicator f a ≠ 1 ↔ a ∈ s ∩ mulSupport f

Tactic:
simp only [Ne, mulIndicator_apply_eq_one, Classical.not_imp, mem_inter_iff, mem_mulSupport]

Result:
no goals
-- Mathlib/Algebra/MvPolynomial/Equiv.lean
lemma optionEquivLeft_C (r : R) : optionEquivLeft R S₁ (C r) = Polynomial.C (C r)

Proof state:
R : Type u
S₁ : Type v
inst✝ : CommSemiring R
r : R
⊢ (optionEquivLeft R S₁) (C r) = Polynomial.C (C r)

Tactic:
simp only [optionEquivLeft_apply, aeval_C, Polynomial.algebraMap_apply, algebraMap_eq]

Result:
no goals