harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Data/Stream/Init.lean
theorem tail_iterate (f : α → α) (a : α) : tail (iterate f a) = iterate f (f a)

Proof state:
case a
α : Type u
f : α → α
a : α
n : ℕ
⊢ (iterate f a).tail.get n = (iterate f (f a)).get n

Tactic:
rw [get_tail]

Result:
case a
α : Type u
f : α → α
a : α
n : ℕ
⊢ (iterate f a).get (n + 1) = (iterate f (f a)).get n

Proof state:
case a.zero
α : Type u
f : α → α
a : α
⊢ (iterate f a).get (0 + 1) = (iterate f (f a)).get 0

Tactic:
rfl

Result:
no goals

Proof state:
case a.succ
α : Type u
f : α → α
a : α
n' : ℕ
ih : (iterate f a).get (n' + 1) = (iterate f (f a)).get n'
⊢ (iterate f a).get (n' + 1 + 1) = (iterate f (f a)).get (n' + 1)

Tactic:
rw [get_succ_iterate', ih, get_succ_iterate']

Result:
no goals

Proof state:
case a
α : Type u
f : α → α
a : α
n : ℕ
⊢ (iterate f a).get (n + 1) = (iterate f (f a)).get n

Tactic:
induction' n with n' ih

Result:
case a.zero
α : Type u
f : α → α
a : α
⊢ (iterate f a).get (0 + 1) = (iterate f (f a)).get 0

case a.succ
α : Type u
f : α → α
a : α
n' : ℕ
ih : (iterate f a).get (n' + 1) = (iterate f (f a)).get n'
⊢ (iterate f a).get (n' + 1 + 1) = (iterate f (f a)).get (n' + 1)

Proof state:
α : Type u
f : α → α
a : α
⊢ (iterate f a).tail = iterate f (f a)

Tactic:
ext n

Result:
case a
α : Type u
f : α → α
a : α
n : ℕ
⊢ (iterate f a).tail.get n = (iterate f (f a)).get n
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Find.lean
theorem find?_flatten_eq_none_iff {xs : List (List α)} {p : α → Bool} :
    xs.flatten.find? p = none ↔ ∀ ys ∈ xs, ∀ x ∈ ys, !p x

Proof state:
α : Type u_1
xs : List (List α)
p : α → Bool
⊢ find? p xs.flatten = none ↔ ∀ (ys : List α), ys ∈ xs → ∀ (x : α), x ∈ ys → (!p x) = true

Tactic:
simp

Result:
no goals
-- Mathlib/Data/Finset/Basic.lean
@[simp] lemma erase_nonempty (ha : a ∈ s) : (s.erase a).Nonempty ↔ s.Nontrivial

Proof state:
α : Type u_1
inst✝ : DecidableEq α
s : Finset α
a : α
ha : a ∈ s
⊢ (∃ x ∈ s, x ≠ a) → s.Nontrivial

Tactic:
rintro ⟨b, hb, hba⟩

Result:
case intro.intro
α : Type u_1
inst✝ : DecidableEq α
s : Finset α
a : α
ha : a ∈ s
b : α
hb : b ∈ s
hba : b ≠ a
⊢ s.Nontrivial

Proof state:
case intro.intro
α : Type u_1
inst✝ : DecidableEq α
s : Finset α
a : α
ha : a ∈ s
b : α
hb : b ∈ s
hba : b ≠ a
⊢ s.Nontrivial

Tactic:
exact ⟨_, hb, _, ha, hba⟩

Result:
no goals

Proof state:
α : Type u_1
inst✝ : DecidableEq α
s : Finset α
a : α
ha : a ∈ s
⊢ (s.erase a).Nonempty ↔ s.Nontrivial

Tactic:
simp only [Finset.Nonempty, mem_erase, and_comm (b := _ ∈ _)]

Result:
α : Type u_1
inst✝ : DecidableEq α
s : Finset α
a : α
ha : a ∈ s
⊢ (∃ x ∈ s, x ≠ a) ↔ s.Nontrivial

Proof state:
α : Type u_1
inst✝ : DecidableEq α
s : Finset α
a : α
ha : a ∈ s
⊢ (∃ x ∈ s, x ≠ a) ↔ s.Nontrivial

Tactic:
refine ⟨?_, fun hs ↦ hs.exists_ne a⟩

Result:
α : Type u_1
inst✝ : DecidableEq α
s : Finset α
a : α
ha : a ∈ s
⊢ (∃ x ∈ s, x ≠ a) → s.Nontrivial
-- Mathlib/Algebra/Polynomial/Monomial.lean
theorem monomial_one_eq_iff [Nontrivial R] {i j : ℕ} :
    (monomial i 1 : R[X]) = monomial j 1 ↔ i = j

Proof state:
R : Type u
inst✝¹ : Semiring R
inst✝ : Nontrivial R
i j : ℕ
⊢ Finsupp.single i 1 = Finsupp.single j 1 ↔ i = j

Tactic:
exact AddMonoidAlgebra.of_injective.eq_iff

Result:
no goals

Proof state:
R : Type u
inst✝¹ : Semiring R
inst✝ : Nontrivial R
i j : ℕ
⊢ (monomial i) 1 = (monomial j) 1 ↔ i = j

Tactic:
simp_rw [← ofFinsupp_single, ofFinsupp.injEq]

Result:
R : Type u
inst✝¹ : Semiring R
inst✝ : Nontrivial R
i j : ℕ
⊢ Finsupp.single i 1 = Finsupp.single j 1 ↔ i = j
-- Mathlib/Data/Multiset/Sections.lean
theorem coe_sections :
    ∀ l : List (List α),
      Sections (l.map fun l : List α => (l : Multiset α) : Multiset (Multiset α)) =
        (l.sections.map fun l : List α => (l : Multiset α) : Multiset (Multiset α))
  | [] => rfl
  | a :: l => by
    simp only [List.map_cons, List.sections]
    rw [← cons_coe, sections_cons, bind_map_comm, coe_sections l]
    simp [List.sections, Function.comp_def, List.flatMap]

Proof state:
α : Type u_1
a : List α
l : List (List α)
⊢ (↑(List.map (fun l => ↑l) (a :: l))).Sections = ↑(List.map (fun l => ↑l) (a :: l).sections)

Tactic:
simp only [List.map_cons, List.sections]

Result:
α : Type u_1
a : List α
l : List (List α)
⊢ (↑(↑a :: List.map (fun l => ↑l) l)).Sections =
    ↑(List.map (fun l => ↑l) (List.flatMap (fun s => List.map (fun a => a :: s) a) l.sections))

Proof state:
α : Type u_1
a : List α
l : List (List α)
⊢ ((↑(List.map (fun l => ↑l) l.sections)).bind fun b => map (fun a => a ::ₘ b) ↑a) =
    ↑(List.map (fun l => ↑l) (List.flatMap (fun s => List.map (fun a => a :: s) a) l.sections))

Tactic:
simp [List.sections, Function.comp_def, List.flatMap]

Result:
no goals

Proof state:
α : Type u_1
a : List α
l : List (List α)
⊢ (↑(↑a :: List.map (fun l => ↑l) l)).Sections =
    ↑(List.map (fun l => ↑l) (List.flatMap (fun s => List.map (fun a => a :: s) a) l.sections))

Tactic:
rw [← cons_coe, sections_cons, bind_map_comm, coe_sections l]

Result:
α : Type u_1
a : List α
l : List (List α)
⊢ ((↑(List.map (fun l => ↑l) l.sections)).bind fun b => map (fun a => a ::ₘ b) ↑a) =
    ↑(List.map (fun l => ↑l) (List.flatMap (fun s => List.map (fun a => a :: s) a) l.sections))
-- Mathlib/Analysis/SpecialFunctions/Log/Base.lean
theorem logb_le_logb_of_base_lt_one (h : 0 < x) (h₁ : 0 < y) : logb b x ≤ logb b y ↔ y ≤ x

Proof state:
b x y : ℝ
b_pos : 0 < b
b_lt_one : b < 1
h : 0 < x
h₁ : 0 < y
⊢ logb b x ≤ logb b y ↔ y ≤ x

Tactic:
rw [logb, logb, div_le_div_right_of_neg (log_neg b_pos b_lt_one), log_le_log_iff h₁ h]

Result:
no goals
-- Mathlib/LinearAlgebra/Projectivization/Cardinality.lean
/-- Cardinality formula for the points of `ℙ k V` if `k` and `V` are finite with less
natural subtraction. -/
lemma card' [Finite V] : Nat.card V = Nat.card (ℙ k V) * (Nat.card k - 1) + 1

Proof state:
k : Type u_1
V : Type u_2
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : Finite V
this : Nat.card V > 0
⊢ Nat.card V = Nat.card V - 1 + 1

Tactic:
omega

Result:
no goals

Proof state:
k : Type u_1
V : Type u_2
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : Finite V
⊢ Nat.card V = Nat.card (ℙ k V) * (Nat.card k - 1) + 1

Tactic:
rw [← card k V]

Result:
k : Type u_1
V : Type u_2
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : Finite V
⊢ Nat.card V = Nat.card V - 1 + 1

Proof state:
k : Type u_1
V : Type u_2
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : Finite V
⊢ Nat.card V = Nat.card V - 1 + 1

Tactic:
have : Nat.card V > 0 := Nat.card_pos

Result:
k : Type u_1
V : Type u_2
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : Finite V
this : Nat.card V > 0
⊢ Nat.card V = Nat.card V - 1 + 1
-- Mathlib/RingTheory/FractionalIdeal/Operations.lean
theorem _root_.Ideal.fg_of_isUnit (inj : Function.Injective (algebraMap R P)) (I : Ideal R)
    (h : IsUnit (I : FractionalIdeal S P)) : I.FG

Proof state:
R : Type u_1
inst✝² : CommRing R
S : Submonoid R
P : Type u_2
inst✝¹ : CommRing P
inst✝ : Algebra R P
inj : Function.Injective ⇑(algebraMap R P)
I : Ideal R
h : IsUnit ↑I
⊢ I.FG

Tactic:
rw [← coeIdeal_fg S inj I]

Result:
R : Type u_1
inst✝² : CommRing R
S : Submonoid R
P : Type u_2
inst✝¹ : CommRing P
inst✝ : Algebra R P
inj : Function.Injective ⇑(algebraMap R P)
I : Ideal R
h : IsUnit ↑I
⊢ (↑↑I).FG

Proof state:
R : Type u_1
inst✝² : CommRing R
S : Submonoid R
P : Type u_2
inst✝¹ : CommRing P
inst✝ : Algebra R P
inj : Function.Injective ⇑(algebraMap R P)
I : Ideal R
h : IsUnit ↑I
⊢ (↑↑I).FG

Tactic:
exact FractionalIdeal.fg_of_isUnit (R := R) I h

Result:
no goals
-- Mathlib/RingTheory/Localization/Ideal.lean
theorem map_comap (J : Ideal S) :
    Ideal.map (algebraMap R S) (Ideal.comap (algebraMap R S) J) = J :=
  le_antisymm (Ideal.map_le_iff_le_comap.2 le_rfl) fun x hJ => by
    obtain ⟨r, s, hx⟩ := mk'_surjective M x
    rw [← hx] at hJ ⊢
    exact
      Ideal.mul_mem_right _ _
        (Ideal.mem_map_of_mem _
          (show (algebraMap R S) r ∈ J from
            mk'_spec S r s ▸ J.mul_mem_right ((algebraMap R S) s) hJ))

Proof state:
case intro.intro
R : Type u_1
inst✝³ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
J : Ideal S
x : S
r : R
s : ↥M
hJ : mk' S r s ∈ J
hx : mk' S r s = x
⊢ mk' S r s ∈ Ideal.map (algebraMap R S) (Ideal.comap (algebraMap R S) J)

Tactic:
exact
  Ideal.mul_mem_right _ _
    (Ideal.mem_map_of_mem _
      (show (algebraMap R S) r ∈ J from
        mk'_spec S r s ▸ J.mul_mem_right ((algebraMap R S) s) hJ))

Result:
no goals

Proof state:
case intro.intro
R : Type u_1
inst✝³ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
J : Ideal S
x : S
hJ : x ∈ J
r : R
s : ↥M
hx : mk' S r s = x
⊢ x ∈ Ideal.map (algebraMap R S) (Ideal.comap (algebraMap R S) J)

Tactic:
rw [← hx] at hJ ⊢

Result:
case intro.intro
R : Type u_1
inst✝³ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
J : Ideal S
x : S
r : R
s : ↥M
hJ : mk' S r s ∈ J
hx : mk' S r s = x
⊢ mk' S r s ∈ Ideal.map (algebraMap R S) (Ideal.comap (algebraMap R S) J)

Proof state:
R : Type u_1
inst✝³ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
J : Ideal S
x : S
hJ : x ∈ J
⊢ x ∈ Ideal.map (algebraMap R S) (Ideal.comap (algebraMap R S) J)

Tactic:
obtain ⟨r, s, hx⟩ := mk'_surjective M x

Result:
case intro.intro
R : Type u_1
inst✝³ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
J : Ideal S
x : S
hJ : x ∈ J
r : R
s : ↥M
hx : mk' S r s = x
⊢ x ∈ Ideal.map (algebraMap R S) (Ideal.comap (algebraMap R S) J)
-- Mathlib/RingTheory/Jacobson/Radical.lean
theorem jacobson_quotient_of_le {N : Submodule R M} (le : N ≤ jacobson R M) :
    jacobson R (M ⧸ N) = map N.mkQ (jacobson R M) :=
  (map_jacobson_of_ker_le N.mkQ_surjective <| by rwa [ker_mkQ]).symm

Proof state:
R : Type u_1
M : Type u_3
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
N : Submodule R M
le : N ≤ jacobson R M
⊢ LinearMap.ker N.mkQ ≤ jacobson R M

Tactic:
rwa [ker_mkQ]

Result:
no goals
-- Mathlib/CategoryTheory/Abelian/NonPreadditive.lean
theorem lift_map {X Y : C} (f : X ⟶ Y) :
    prod.lift (𝟙 X) 0 ≫ Limits.prod.map f f = f ≫ prod.lift (𝟙 Y) 0

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : NonPreadditiveAbelian C
X Y : C
f : X ⟶ Y
⊢ prod.lift (𝟙 X) 0 ≫ prod.map f f = f ≫ prod.lift (𝟙 Y) 0

Tactic:
simp

Result:
no goals
-- Mathlib/RingTheory/LocalRing/ResidueField/Ideal.lean
lemma Ideal.injective_algebraMap_quotient_residueField :
    Function.Injective (algebraMap (R ⧸ I) I.ResidueField)

Proof state:
R : Type u_1
inst✝¹ : CommRing R
I : Ideal R
inst✝ : I.IsPrime
⊢ RingHom.ker (algebraMap (R ⧸ I) I.ResidueField) = ⊥

Tactic:
refine (Ideal.ker_quotient_lift _ _).trans ?_

Result:
R : Type u_1
inst✝¹ : CommRing R
I : Ideal R
inst✝ : I.IsPrime
⊢ map (Quotient.mk I) (RingHom.ker ↑(Algebra.ofId R I.ResidueField)) = ⊥

Proof state:
R : Type u_1
inst✝¹ : CommRing R
I : Ideal R
inst✝ : I.IsPrime
⊢ map (Quotient.mk I) (RingHom.ker (algebraMap R I.ResidueField)) = ⊥

Tactic:
rw [Ideal.ker_algebraMap_residueField, map_quotient_self]

Result:
no goals

Proof state:
R : Type u_1
inst✝¹ : CommRing R
I : Ideal R
inst✝ : I.IsPrime
⊢ Function.Injective ⇑(algebraMap (R ⧸ I) I.ResidueField)

Tactic:
rw [RingHom.injective_iff_ker_eq_bot]

Result:
R : Type u_1
inst✝¹ : CommRing R
I : Ideal R
inst✝ : I.IsPrime
⊢ RingHom.ker (algebraMap (R ⧸ I) I.ResidueField) = ⊥

Proof state:
R : Type u_1
inst✝¹ : CommRing R
I : Ideal R
inst✝ : I.IsPrime
⊢ map (Quotient.mk I) (RingHom.ker ↑(Algebra.ofId R I.ResidueField)) = ⊥

Tactic:
show map (Quotient.mk I) (RingHom.ker (algebraMap R I.ResidueField)) = ⊥

Result:
R : Type u_1
inst✝¹ : CommRing R
I : Ideal R
inst✝ : I.IsPrime
⊢ map (Quotient.mk I) (RingHom.ker (algebraMap R I.ResidueField)) = ⊥
-- Mathlib/Topology/UniformSpace/Basic.lean
theorem Filter.HasBasis.mem_uniformity_iff {p : β → Prop} {s : β → Set (α × α)}
    (h : (𝓤 α).HasBasis p s) {t : Set (α × α)} :
    t ∈ 𝓤 α ↔ ∃ i, p i ∧ ∀ a b, (a, b) ∈ s i → (a, b) ∈ t :=
  h.mem_iff.trans <| by simp only [Prod.forall, subset_def]

Proof state:
α : Type ua
β : Type ub
inst✝ : UniformSpace α
p : β → Prop
s : β → Set (α × α)
h : (𝓤 α).HasBasis p s
t : Set (α × α)
⊢ (∃ i, p i ∧ s i ⊆ t) ↔ ∃ i, p i ∧ ∀ (a b : α), (a, b) ∈ s i → (a, b) ∈ t

Tactic:
simp only [Prod.forall, subset_def]

Result:
no goals
-- Mathlib/Geometry/Manifold/MFDeriv/Basic.lean
theorem mfderiv_comp_apply_of_eq {y : M'} (hg : MDifferentiableAt I' I'' g y)
    (hf : MDifferentiableAt I I' f x)  (hy : f x = y) (v : TangentSpace I x) :
    mfderiv I I'' (g ∘ f) x v = (mfderiv I' I'' g y) ((mfderiv I I' f x) v)

Proof state:
𝕜 : Type u_1
inst✝¹⁵ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹⁴ : NormedAddCommGroup E
inst✝¹³ : NormedSpace 𝕜 E
H : Type u_3
inst✝¹² : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝¹¹ : TopologicalSpace M
inst✝¹⁰ : ChartedSpace H M
E' : Type u_5
inst✝⁹ : NormedAddCommGroup E'
inst✝⁸ : NormedSpace 𝕜 E'
H' : Type u_6
inst✝⁷ : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst✝⁶ : TopologicalSpace M'
inst✝⁵ : ChartedSpace H' M'
E'' : Type u_8
inst✝⁴ : NormedAddCommGroup E''
inst✝³ : NormedSpace 𝕜 E''
H'' : Type u_9
inst✝² : TopologicalSpace H''
I'' : ModelWithCorners 𝕜 E'' H''
M'' : Type u_10
inst✝¹ : TopologicalSpace M''
inst✝ : ChartedSpace H'' M''
f : M → M'
x : M
g : M' → M''
hf : MDifferentiableAt I I' f x
v : TangentSpace I x
hg : MDifferentiableAt I' I'' g (f x)
⊢ (mfderiv I I'' (g ∘ f) x) v = (mfderiv I' I'' g (f x)) ((mfderiv I I' f x) v)

Tactic:
exact mfderiv_comp_apply _ hg hf v

Result:
no goals

Proof state:
𝕜 : Type u_1
inst✝¹⁵ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹⁴ : NormedAddCommGroup E
inst✝¹³ : NormedSpace 𝕜 E
H : Type u_3
inst✝¹² : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝¹¹ : TopologicalSpace M
inst✝¹⁰ : ChartedSpace H M
E' : Type u_5
inst✝⁹ : NormedAddCommGroup E'
inst✝⁸ : NormedSpace 𝕜 E'
H' : Type u_6
inst✝⁷ : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst✝⁶ : TopologicalSpace M'
inst✝⁵ : ChartedSpace H' M'
E'' : Type u_8
inst✝⁴ : NormedAddCommGroup E''
inst✝³ : NormedSpace 𝕜 E''
H'' : Type u_9
inst✝² : TopologicalSpace H''
I'' : ModelWithCorners 𝕜 E'' H''
M'' : Type u_10
inst✝¹ : TopologicalSpace M''
inst✝ : ChartedSpace H'' M''
f : M → M'
x : M
g : M' → M''
y : M'
hg : MDifferentiableAt I' I'' g y
hf : MDifferentiableAt I I' f x
hy : f x = y
v : TangentSpace I x
⊢ (mfderiv I I'' (g ∘ f) x) v = (mfderiv I' I'' g y) ((mfderiv I I' f x) v)

Tactic:
subst hy

Result:
𝕜 : Type u_1
inst✝¹⁵ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹⁴ : NormedAddCommGroup E
inst✝¹³ : NormedSpace 𝕜 E
H : Type u_3
inst✝¹² : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝¹¹ : TopologicalSpace M
inst✝¹⁰ : ChartedSpace H M
E' : Type u_5
inst✝⁹ : NormedAddCommGroup E'
inst✝⁸ : NormedSpace 𝕜 E'
H' : Type u_6
inst✝⁷ : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst✝⁶ : TopologicalSpace M'
inst✝⁵ : ChartedSpace H' M'
E'' : Type u_8
inst✝⁴ : NormedAddCommGroup E''
inst✝³ : NormedSpace 𝕜 E''
H'' : Type u_9
inst✝² : TopologicalSpace H''
I'' : ModelWithCorners 𝕜 E'' H''
M'' : Type u_10
inst✝¹ : TopologicalSpace M''
inst✝ : ChartedSpace H'' M''
f : M → M'
x : M
g : M' → M''
hf : MDifferentiableAt I I' f x
v : TangentSpace I x
hg : MDifferentiableAt I' I'' g (f x)
⊢ (mfderiv I I'' (g ∘ f) x) v = (mfderiv I' I'' g (f x)) ((mfderiv I I' f x) v)
-- Mathlib/Algebra/SkewMonoidAlgebra/Basic.lean
theorem _root_.IsSMulRegular.skewMonoidAlgebra {S : Type*} [Monoid S] [DistribMulAction S k] {a : S}
    (ha : IsSMulRegular k a) : IsSMulRegular (SkewMonoidAlgebra k G) a
  | ⟨_⟩, ⟨_⟩, h => by
    simp only [← ofFinsupp_smul] at h
    exact congr_arg _ <| ha.finsupp (ofFinsupp.inj h)

Proof state:
k : Type u_1
G : Type u_2
inst✝² : AddCommMonoid k
S : Type u_3
inst✝¹ : Monoid S
inst✝ : DistribMulAction S k
a : S
ha : IsSMulRegular k a
toFinsupp✝¹ toFinsupp✝ : G →₀ k
h : { toFinsupp := a • toFinsupp✝¹ } = { toFinsupp := a • toFinsupp✝ }
⊢ { toFinsupp := toFinsupp✝¹ } = { toFinsupp := toFinsupp✝ }

Tactic:
exact congr_arg _ <| ha.finsupp (ofFinsupp.inj h)

Result:
no goals

Proof state:
k : Type u_1
G : Type u_2
inst✝² : AddCommMonoid k
S : Type u_3
inst✝¹ : Monoid S
inst✝ : DistribMulAction S k
a : S
ha : IsSMulRegular k a
toFinsupp✝¹ toFinsupp✝ : G →₀ k
h : (fun x => a • x) { toFinsupp := toFinsupp✝¹ } = (fun x => a • x) { toFinsupp := toFinsupp✝ }
⊢ { toFinsupp := toFinsupp✝¹ } = { toFinsupp := toFinsupp✝ }

Tactic:
simp only [← ofFinsupp_smul] at h

Result:
k : Type u_1
G : Type u_2
inst✝² : AddCommMonoid k
S : Type u_3
inst✝¹ : Monoid S
inst✝ : DistribMulAction S k
a : S
ha : IsSMulRegular k a
toFinsupp✝¹ toFinsupp✝ : G →₀ k
h : { toFinsupp := a • toFinsupp✝¹ } = { toFinsupp := a • toFinsupp✝ }
⊢ { toFinsupp := toFinsupp✝¹ } = { toFinsupp := toFinsupp✝ }
-- Mathlib/Data/Matroid/Circuit.lean
/-- A version of `cocircuit_iff_minimal_compl_nonspanning` with a support assumption
in the minimality -/
lemma isCocircuit_iff_minimal_compl_nonspanning' :
    M.IsCocircuit K ↔ Minimal (fun X ↦ ¬ M.Spanning (M.E \ X) ∧ X ⊆ M.E) K

Proof state:
α : Type u_1
M : Matroid α
K X : Set α
hX : ¬M.Spanning (M.E \ X)
⊢ ¬M.Spanning (M.E \ (X ∩ M.E))

Tactic:
rwa [diff_inter_self_eq_diff]

Result:
no goals

Proof state:
α : Type u_1
M : Matroid α
K : Set α
⊢ M.IsCocircuit K ↔ Minimal (fun X => ¬M.Spanning (M.E \ X) ∧ X ⊆ M.E) K

Tactic:
rw [isCocircuit_iff_minimal_compl_nonspanning]

Result:
α : Type u_1
M : Matroid α
K : Set α
⊢ Minimal (fun X => ¬M.Spanning (M.E \ X)) K ↔ Minimal (fun X => ¬M.Spanning (M.E \ X) ∧ X ⊆ M.E) K

Proof state:
α : Type u_1
M : Matroid α
K : Set α
⊢ Minimal (fun X => ¬M.Spanning (M.E \ X)) K ↔ Minimal (fun X => ¬M.Spanning (M.E \ X) ∧ X ⊆ M.E) K

Tactic:
exact minimal_iff_minimal_of_imp_of_forall (fun _ h ↦ h.1)
  (fun X hX ↦ ⟨X ∩ M.E, inter_subset_left, by rwa [diff_inter_self_eq_diff], inter_subset_right⟩)

Result:
no goals
-- Mathlib/Analysis/Normed/Module/FiniteDimension.lean
theorem exists_seq_norm_le_one_le_norm_sub (h : ¬FiniteDimensional 𝕜 E) :
    ∃ (R : ℝ) (f : ℕ → E), 1 < R ∧ (∀ n, ‖f n‖ ≤ R) ∧ Pairwise fun m n => 1 ≤ ‖f m - f n‖

Proof state:
case intro
𝕜 : Type u
inst✝³ : NontriviallyNormedField 𝕜
E : Type v
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : CompleteSpace 𝕜
h : ¬FiniteDimensional 𝕜 E
c : 𝕜
hc : 1 < ‖c‖
A : ‖c‖ < ‖c‖ + 1
⊢ ∃ R f, 1 < R ∧ (∀ (n : ℕ), ‖f n‖ ≤ R) ∧ Pairwise fun m n => 1 ≤ ‖f m - f n‖

Tactic:
rcases exists_seq_norm_le_one_le_norm_sub' hc A h with ⟨f, hf⟩

Result:
case intro.intro
𝕜 : Type u
inst✝³ : NontriviallyNormedField 𝕜
E : Type v
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : CompleteSpace 𝕜
h : ¬FiniteDimensional 𝕜 E
c : 𝕜
hc : 1 < ‖c‖
A : ‖c‖ < ‖c‖ + 1
f : ℕ → E
hf : (∀ (n : ℕ), ‖f n‖ ≤ ‖c‖ + 1) ∧ Pairwise fun m n => 1 ≤ ‖f m - f n‖
⊢ ∃ R f, 1 < R ∧ (∀ (n : ℕ), ‖f n‖ ≤ R) ∧ Pairwise fun m n => 1 ≤ ‖f m - f n‖

Proof state:
case intro
𝕜 : Type u
inst✝³ : NontriviallyNormedField 𝕜
E : Type v
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : CompleteSpace 𝕜
h : ¬FiniteDimensional 𝕜 E
c : 𝕜
hc : 1 < ‖c‖
⊢ ∃ R f, 1 < R ∧ (∀ (n : ℕ), ‖f n‖ ≤ R) ∧ Pairwise fun m n => 1 ≤ ‖f m - f n‖

Tactic:
have A : ‖c‖ < ‖c‖ + 1 := by linarith

Result:
case intro
𝕜 : Type u
inst✝³ : NontriviallyNormedField 𝕜
E : Type v
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : CompleteSpace 𝕜
h : ¬FiniteDimensional 𝕜 E
c : 𝕜
hc : 1 < ‖c‖
A : ‖c‖ < ‖c‖ + 1
⊢ ∃ R f, 1 < R ∧ (∀ (n : ℕ), ‖f n‖ ≤ R) ∧ Pairwise fun m n => 1 ≤ ‖f m - f n‖

Proof state:
𝕜 : Type u
inst✝³ : NontriviallyNormedField 𝕜
E : Type v
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : CompleteSpace 𝕜
h : ¬FiniteDimensional 𝕜 E
c : 𝕜
hc : 1 < ‖c‖
⊢ ‖c‖ < ‖c‖ + 1

Tactic:
linarith

Result:
no goals

Proof state:
𝕜 : Type u
inst✝³ : NontriviallyNormedField 𝕜
E : Type v
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : CompleteSpace 𝕜
h : ¬FiniteDimensional 𝕜 E
⊢ ∃ R f, 1 < R ∧ (∀ (n : ℕ), ‖f n‖ ≤ R) ∧ Pairwise fun m n => 1 ≤ ‖f m - f n‖

Tactic:
obtain ⟨c, hc⟩ : ∃ c : 𝕜, 1 < ‖c‖ := NormedField.exists_one_lt_norm 𝕜

Result:
case intro
𝕜 : Type u
inst✝³ : NontriviallyNormedField 𝕜
E : Type v
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : CompleteSpace 𝕜
h : ¬FiniteDimensional 𝕜 E
c : 𝕜
hc : 1 < ‖c‖
⊢ ∃ R f, 1 < R ∧ (∀ (n : ℕ), ‖f n‖ ≤ R) ∧ Pairwise fun m n => 1 ≤ ‖f m - f n‖

Proof state:
case intro.intro
𝕜 : Type u
inst✝³ : NontriviallyNormedField 𝕜
E : Type v
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : CompleteSpace 𝕜
h : ¬FiniteDimensional 𝕜 E
c : 𝕜
hc : 1 < ‖c‖
A : ‖c‖ < ‖c‖ + 1
f : ℕ → E
hf : (∀ (n : ℕ), ‖f n‖ ≤ ‖c‖ + 1) ∧ Pairwise fun m n => 1 ≤ ‖f m - f n‖
⊢ ∃ R f, 1 < R ∧ (∀ (n : ℕ), ‖f n‖ ≤ R) ∧ Pairwise fun m n => 1 ≤ ‖f m - f n‖

Tactic:
exact ⟨‖c‖ + 1, f, hc.trans A, hf.1, hf.2⟩

Result:
no goals
-- Mathlib/Algebra/Polynomial/Lifts.lean
theorem C'_mem_lifts {f : R →+* S} {s : S} (h : s ∈ Set.range f) : C s ∈ lifts f

Proof state:
case h
R : Type u
inst✝¹ : Semiring R
S : Type v
inst✝ : Semiring S
f : R →+* S
r : R
h : f r ∈ Set.range ⇑f
⊢ (mapRingHom f) (C r) = C (f r)

Tactic:
simp only [coe_mapRingHom, map_C, Set.mem_univ, Subsemiring.coe_top, eq_self_iff_true,
  and_self_iff]

Result:
no goals

Proof state:
case intro
R : Type u
inst✝¹ : Semiring R
S : Type v
inst✝ : Semiring S
f : R →+* S
r : R
h : f r ∈ Set.range ⇑f
⊢ C (f r) ∈ lifts f

Tactic:
use C r

Result:
case h
R : Type u
inst✝¹ : Semiring R
S : Type v
inst✝ : Semiring S
f : R →+* S
r : R
h : f r ∈ Set.range ⇑f
⊢ (mapRingHom f) (C r) = C (f r)

Proof state:
R : Type u
inst✝¹ : Semiring R
S : Type v
inst✝ : Semiring S
f : R →+* S
s : S
h : s ∈ Set.range ⇑f
⊢ C s ∈ lifts f

Tactic:
obtain ⟨r, rfl⟩ := Set.mem_range.1 h

Result:
case intro
R : Type u
inst✝¹ : Semiring R
S : Type v
inst✝ : Semiring S
f : R →+* S
r : R
h : f r ∈ Set.range ⇑f
⊢ C (f r) ∈ lifts f
-- Mathlib/Data/Nat/Bits.lean
theorem bit_cases_on_injective {motive : ℕ → Sort u} :
    Function.Injective fun H : ∀ b n, motive (bit b n) => fun n => bitCasesOn n H

Proof state:
motive : ℕ → Sort u
H₁ H₂ : (b : Bool) → (n : ℕ) → motive (bit b n)
h : (fun H n => bitCasesOn n H) H₁ = (fun H n => bitCasesOn n H) H₂
⊢ H₁ = H₂

Tactic:
ext b n

Result:
case h.h
motive : ℕ → Sort u
H₁ H₂ : (b : Bool) → (n : ℕ) → motive (bit b n)
h : (fun H n => bitCasesOn n H) H₁ = (fun H n => bitCasesOn n H) H₂
b : Bool
n : ℕ
⊢ H₁ b n = H₂ b n

Proof state:
motive : ℕ → Sort u
⊢ Function.Injective fun H n => bitCasesOn n H

Tactic:
intro H₁ H₂ h

Result:
motive : ℕ → Sort u
H₁ H₂ : (b : Bool) → (n : ℕ) → motive (bit b n)
h : (fun H n => bitCasesOn n H) H₁ = (fun H n => bitCasesOn n H) H₂
⊢ H₁ = H₂

Proof state:
case h.h
motive : ℕ → Sort u
H₁ H₂ : (b : Bool) → (n : ℕ) → motive (bit b n)
h : (fun H n => bitCasesOn n H) H₁ = (fun H n => bitCasesOn n H) H₂
b : Bool
n : ℕ
⊢ H₁ b n = H₂ b n

Tactic:
simpa only [bitCasesOn_bit] using congr_fun h (bit b n)

Result:
no goals