harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/LinearAlgebra/LinearIndependent/Defs.lean
theorem LinearMap.linearIndependent_iff_of_injOn (f : M →ₗ[R] M')
    (hf_inj : Set.InjOn f (span R (Set.range v))) :
    LinearIndependent R (f ∘ v) ↔ LinearIndependent R v

Proof state:
ι : Type u'
R : Type u_2
M : Type u_4
M' : Type u_5
v : ι → M
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M'
inst✝¹ : Module R M
inst✝ : Module R M'
f : M →ₗ[R] M'
hf_inj : InjOn ⇑f ↑(span R (Set.range v))
⊢ LinearIndependent R (⇑f ∘ v) ↔ LinearIndependent R v

Tactic:
simp_rw [LinearIndependent, Finsupp.linearCombination_linear_comp, coe_comp]

Result:
ι : Type u'
R : Type u_2
M : Type u_4
M' : Type u_5
v : ι → M
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M'
inst✝¹ : Module R M
inst✝ : Module R M'
f : M →ₗ[R] M'
hf_inj : InjOn ⇑f ↑(span R (Set.range v))
⊢ Injective (⇑f ∘ ⇑(Finsupp.linearCombination R v)) ↔ Injective ⇑(Finsupp.linearCombination R v)

Proof state:
ι : Type u'
R : Type u_2
M : Type u_4
M' : Type u_5
v : ι → M
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M'
inst✝¹ : Module R M
inst✝ : Module R M'
f : M →ₗ[R] M'
hf_inj : InjOn ⇑f ↑(span R (Set.range v))
⊢ Set.range ⇑(Finsupp.linearCombination R v) ⊆ ↑(span R (Set.range v))

Tactic:
rw [← Finsupp.range_linearCombination, LinearMap.range_coe]

Result:
no goals

Proof state:
ι : Type u'
R : Type u_2
M : Type u_4
M' : Type u_5
v : ι → M
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M'
inst✝¹ : Module R M
inst✝ : Module R M'
f : M →ₗ[R] M'
hf_inj : InjOn ⇑f ↑(span R (Set.range v))
⊢ Injective (⇑f ∘ ⇑(Finsupp.linearCombination R v)) ↔ Injective ⇑(Finsupp.linearCombination R v)

Tactic:
rw [hf_inj.injective_iff]

Result:
ι : Type u'
R : Type u_2
M : Type u_4
M' : Type u_5
v : ι → M
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M'
inst✝¹ : Module R M
inst✝ : Module R M'
f : M →ₗ[R] M'
hf_inj : InjOn ⇑f ↑(span R (Set.range v))
⊢ Set.range ⇑(Finsupp.linearCombination R v) ⊆ ↑(span R (Set.range v))
-- Mathlib/Data/Finset/Basic.lean
theorem filter_erase (a : α) (s : Finset α) : filter p (erase s a) = erase (filter p s) a

Proof state:
α : Type u_1
p : α → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidableEq α
a : α
s : Finset α
⊢ filter p (s.erase a) = (filter p s).erase a

Tactic:
ext x

Result:
case h
α : Type u_1
p : α → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidableEq α
a : α
s : Finset α
x : α
⊢ x ∈ filter p (s.erase a) ↔ x ∈ (filter p s).erase a

Proof state:
case h
α : Type u_1
p : α → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidableEq α
a : α
s : Finset α
x : α
⊢ x ∈ filter p (s.erase a) ↔ x ∈ (filter p s).erase a

Tactic:
simp only [and_assoc, mem_filter, iff_self, mem_erase]

Result:
no goals
-- Mathlib/SetTheory/Ordinal/Exponential.lean
theorem lt_opow_succ_log_self {b : Ordinal} (hb : 1 < b) (x : Ordinal) :
    x < b ^ succ (log b x)

Proof state:
case inr
b : Ordinal.{u_1}
hb : 1 < b
x : Ordinal.{u_1}
hx : x ≠ 0
⊢ x < b ^ sInf {o | x < b ^ o}

Tactic:
exact csInf_mem (log_nonempty hb)

Result:
no goals

Proof state:
b : Ordinal.{u_1}
hb : 1 < b
x : Ordinal.{u_1}
⊢ x < b ^ succ (log b x)

Tactic:
rcases eq_or_ne x 0 with (rfl | hx)

Result:
case inl
b : Ordinal.{u_1}
hb : 1 < b
⊢ 0 < b ^ succ (log b 0)

case inr
b : Ordinal.{u_1}
hb : 1 < b
x : Ordinal.{u_1}
hx : x ≠ 0
⊢ x < b ^ succ (log b x)

Proof state:
case inl
b : Ordinal.{u_1}
hb : 1 < b
⊢ 0 < b ^ succ (log b 0)

Tactic:
apply opow_pos _ (zero_lt_one.trans hb)

Result:
no goals

Proof state:
case inr
b : Ordinal.{u_1}
hb : 1 < b
x : Ordinal.{u_1}
hx : x ≠ 0
⊢ x < b ^ succ (log b x)

Tactic:
rw [succ_log_def hb hx]

Result:
case inr
b : Ordinal.{u_1}
hb : 1 < b
x : Ordinal.{u_1}
hx : x ≠ 0
⊢ x < b ^ sInf {o | x < b ^ o}
-- Mathlib/Logic/Equiv/Option.lean
theorem optionSubtype_apply_symm_apply
    [DecidableEq β] (x : β)
    (e : { e : Option α ≃ β // e none = x })
    (b : { y : β // y ≠ x }) : ↑((optionSubtype x e).symm b) = (e : Option α ≃ β).symm b

Proof state:
α : Type u_1
β : Type u_2
inst✝ : DecidableEq β
x : β
e : { e // e none = x }
b : { y // y ≠ x }
⊢ some (((optionSubtype x) e).symm b) = (↑e).symm ↑b

Tactic:
dsimp only [optionSubtype]

Result:
α : Type u_1
β : Type u_2
inst✝ : DecidableEq β
x : β
e : { e // e none = x }
b : { y // y ≠ x }
⊢ some
      (({
              toFun := fun e =>
                { toFun := fun a => ⟨↑e (some a), ⋯⟩, invFun := fun b => ((↑e).symm ↑b).get ⋯, left_inv := ⋯,
                  right_inv := ⋯ },
              invFun := fun e =>
                ⟨{ toFun := fun a => a.casesOn' x (Subtype.val ∘ ⇑e),
                    invFun := fun b => if h : b = x then none else some (e.symm ⟨b, h⟩), left_inv := ⋯,
                    right_inv := ⋯ },
                  ⋯⟩,
              left_inv := ⋯, right_inv := ⋯ }
            e).symm
        b) =
    (↑e).symm ↑b

Proof state:
α : Type u_1
β : Type u_2
inst✝ : DecidableEq β
x : β
e : { e // e none = x }
b : { y // y ≠ x }
⊢ some
      (({
              toFun := fun e =>
                { toFun := fun a => ⟨↑e (some a), ⋯⟩, invFun := fun b => ((↑e).symm ↑b).get ⋯, left_inv := ⋯,
                  right_inv := ⋯ },
              invFun := fun e =>
                ⟨{ toFun := fun a => a.casesOn' x (Subtype.val ∘ ⇑e),
                    invFun := fun b => if h : b = x then none else some (e.symm ⟨b, h⟩), left_inv := ⋯,
                    right_inv := ⋯ },
                  ⋯⟩,
              left_inv := ⋯, right_inv := ⋯ }
            e).symm
        b) =
    (↑e).symm ↑b

Tactic:
simp

Result:
no goals
-- Mathlib/CategoryTheory/Generator/Basic.lean
theorem IsCoseparator.of_equivalence {G : C} (h : IsCoseparator G) (α : C ≌ D) :
    IsCoseparator (α.functor.obj G)

Proof state:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
G : C
h : IsCoseparator G
α : C ≌ D
⊢ IsCoseparator (α.functor.obj G)

Tactic:
simpa using IsCoseparating.of_equivalence h α

Result:
no goals
-- Mathlib/Data/List/Cycle.lean
theorem coe_cons_eq_coe_append (l : List α) (a : α) :
    (↑(a :: l) : Cycle α) = (↑(l ++ [a]) : Cycle α) :=
  Quot.sound ⟨1, by rw [rotate_cons_succ, rotate_zero]⟩

Proof state:
α : Type u_1
l : List α
a : α
⊢ (a :: l).rotate 1 = l ++ [a]

Tactic:
rw [rotate_cons_succ, rotate_zero]

Result:
no goals
-- Mathlib/Data/ZMod/Basic.lean
theorem natAbs_mod_two (a : ℤ) : (a.natAbs : ZMod 2) = a

Proof state:
case negSucc
a✝ : ℕ
⊢ ↑(Int.negSucc a✝).natAbs = ↑(Int.negSucc a✝)

Tactic:
simp only [neg_eq_self_mod_two, Nat.cast_succ, Int.natAbs, Int.cast_negSucc]

Result:
no goals

Proof state:
case ofNat
a✝ : ℕ
⊢ ↑(Int.ofNat a✝).natAbs = ↑(Int.ofNat a✝)

Tactic:
simp only [Int.natAbs_ofNat, Int.cast_natCast, Int.ofNat_eq_coe]

Result:
no goals

Proof state:
a : ℤ
⊢ ↑a.natAbs = ↑a

Tactic:
cases a

Result:
case ofNat
a✝ : ℕ
⊢ ↑(Int.ofNat a✝).natAbs = ↑(Int.ofNat a✝)

case negSucc
a✝ : ℕ
⊢ ↑(Int.negSucc a✝).natAbs = ↑(Int.negSucc a✝)
-- Mathlib/Algebra/MvPolynomial/Basic.lean
theorem coeff_X' [DecidableEq σ] (i : σ) (m) :
    coeff m (X i : MvPolynomial σ R) = if Finsupp.single i 1 = m then 1 else 0

Proof state:
R : Type u
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : DecidableEq σ
i : σ
m : σ →₀ ℕ
⊢ coeff m (X i) = if Finsupp.single i 1 = m then 1 else 0

Tactic:
rw [← coeff_X_pow, pow_one]

Result:
no goals
-- Mathlib/Order/Filter/Bases.lean
theorem hasBasis_principal (t : Set α) : (𝓟 t).HasBasis (fun _ : Unit => True) fun _ => t :=
  ⟨fun U => by simp⟩

Proof state:
α : Type u_1
t U : Set α
⊢ U ∈ 𝓟 t ↔ ∃ i, True ∧ t ⊆ U

Tactic:
simp

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Subgraph.lean
theorem deleteEdges_le : G'.deleteEdges s ≤ G'

Proof state:
V : Type u
G : SimpleGraph V
G' : G.Subgraph
s : Set (Sym2 V)
⊢ G'.deleteEdges s ≤ G'

Tactic:
constructor <;> simp +contextual [subset_rfl]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Find.lean
theorem find?_mkVector :
    find? p (mkVector n a) = if n = 0 then none else if p a then some a else none

Proof state:
α✝ : Type
p : α✝ → Bool
n : Nat
a : α✝
⊢ find? p (mkVector n a) = if n = 0 then none else if p a = true then some a else none

Tactic:
rw [mkVector_eq_mk_mkArray, find?_mk, Array.find?_mkArray]

Result:
no goals
-- Mathlib/MeasureTheory/Constructions/BorelSpace/Order.lean
theorem measurable_of_Ici {f : δ → α} (hf : ∀ x, MeasurableSet (f ⁻¹' Ici x)) : Measurable f

Proof state:
α : Type u_1
δ : Type u_4
inst✝⁴ : TopologicalSpace α
mα : MeasurableSpace α
inst✝³ : BorelSpace α
mδ : MeasurableSpace δ
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : SecondCountableTopology α
f : δ → α
hf : ∀ (x : α), MeasurableSet (f ⁻¹' Ici x)
⊢ Measurable f

Tactic:
apply measurable_of_Iio

Result:
case hf
α : Type u_1
δ : Type u_4
inst✝⁴ : TopologicalSpace α
mα : MeasurableSpace α
inst✝³ : BorelSpace α
mδ : MeasurableSpace δ
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : SecondCountableTopology α
f : δ → α
hf : ∀ (x : α), MeasurableSet (f ⁻¹' Ici x)
⊢ ∀ (x : α), MeasurableSet (f ⁻¹' Iio x)

Proof state:
case hf
α : Type u_1
δ : Type u_4
inst✝⁴ : TopologicalSpace α
mα : MeasurableSpace α
inst✝³ : BorelSpace α
mδ : MeasurableSpace δ
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : SecondCountableTopology α
f : δ → α
hf : ∀ (x : α), MeasurableSet (f ⁻¹' Ici x)
⊢ ∀ (x : α), MeasurableSet (f ⁻¹' Ici x)

Tactic:
assumption

Result:
no goals

Proof state:
case hf
α : Type u_1
δ : Type u_4
inst✝⁴ : TopologicalSpace α
mα : MeasurableSpace α
inst✝³ : BorelSpace α
mδ : MeasurableSpace δ
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : SecondCountableTopology α
f : δ → α
hf : ∀ (x : α), MeasurableSet (f ⁻¹' Ici x)
⊢ ∀ (x : α), MeasurableSet (f ⁻¹' Iio x)

Tactic:
simp_rw [← compl_Ici, preimage_compl, MeasurableSet.compl_iff]

Result:
case hf
α : Type u_1
δ : Type u_4
inst✝⁴ : TopologicalSpace α
mα : MeasurableSpace α
inst✝³ : BorelSpace α
mδ : MeasurableSpace δ
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : SecondCountableTopology α
f : δ → α
hf : ∀ (x : α), MeasurableSet (f ⁻¹' Ici x)
⊢ ∀ (x : α), MeasurableSet (f ⁻¹' Ici x)
-- Mathlib/Geometry/Euclidean/Angle/Oriented/RightAngle.lean
theorem oangle_add_left_eq_arccos_of_oangle_eq_pi_div_two {x y : V} (h : o.oangle x y = ↑(π / 2)) :
    o.oangle (x + y) y = Real.arccos (‖y‖ / ‖x + y‖)

Proof state:
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
hd2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
h : (-o).oangle y x = ↑(π / 2)
⊢ (-o).oangle y (x + y) = ↑(Real.arccos (‖y‖ / ‖x + y‖))

Tactic:
rw [add_comm]

Result:
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
hd2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
h : (-o).oangle y x = ↑(π / 2)
⊢ (-o).oangle y (y + x) = ↑(Real.arccos (‖y‖ / ‖y + x‖))

Proof state:
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
hd2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
h : (-o).oangle y x = ↑(π / 2)
⊢ (-o).oangle y (y + x) = ↑(Real.arccos (‖y‖ / ‖y + x‖))

Tactic:
exact (-o).oangle_add_right_eq_arccos_of_oangle_eq_pi_div_two h

Result:
no goals

Proof state:
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
hd2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
h : o.oangle x y = ↑(π / 2)
⊢ o.oangle (x + y) y = ↑(Real.arccos (‖y‖ / ‖x + y‖))

Tactic:
rw [← neg_inj, oangle_rev, ← oangle_neg_orientation_eq_neg, neg_inj] at h ⊢

Result:
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
hd2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
h : (-o).oangle y x = ↑(π / 2)
⊢ (-o).oangle y (x + y) = ↑(Real.arccos (‖y‖ / ‖x + y‖))
-- Mathlib/Topology/ContinuousOn.lean
theorem nhdsWithin_eq_nhdsWithin {a : α} {s t u : Set α} (h₀ : a ∈ s) (h₁ : IsOpen s)
    (h₂ : t ∩ s = u ∩ s) : 𝓝[t] a = 𝓝[u] a

Proof state:
α : Type u_1
inst✝ : TopologicalSpace α
a : α
s t u : Set α
h₀ : a ∈ s
h₁ : IsOpen s
h₂ : t ∩ s = u ∩ s
⊢ 𝓝[t] a = 𝓝[u] a

Tactic:
rw [nhdsWithin_restrict t h₀ h₁, nhdsWithin_restrict u h₀ h₁, h₂]

Result:
no goals
-- Mathlib/Algebra/MvPolynomial/Degrees.lean
theorem degrees_sum_le {ι : Type*} [DecidableEq σ] (s : Finset ι) (f : ι → MvPolynomial σ R) :
    (∑ i ∈ s, f i).degrees ≤ s.sup fun i => (f i).degrees

Proof state:
R : Type u
σ : Type u_1
inst✝¹ : CommSemiring R
ι : Type u_3
inst✝ : DecidableEq σ
s : Finset ι
f : ι → MvPolynomial σ R
⊢ (∑ i ∈ s, f i).degrees ≤ s.sup fun i => (f i).degrees

Tactic:
simp_rw [degrees_def]

Result:
R : Type u
σ : Type u_1
inst✝¹ : CommSemiring R
ι : Type u_3
inst✝ : DecidableEq σ
s : Finset ι
f : ι → MvPolynomial σ R
⊢ ((∑ i ∈ s, f i).support.sup fun s => toMultiset s) ≤ s.sup fun i => (f i).support.sup fun s => toMultiset s

Proof state:
R : Type u
σ : Type u_1
inst✝¹ : CommSemiring R
ι : Type u_3
inst✝ : DecidableEq σ
s : Finset ι
f : ι → MvPolynomial σ R
⊢ ((∑ i ∈ s, f i).support.sup fun s => toMultiset s) ≤ s.sup fun i => (f i).support.sup fun s => toMultiset s

Tactic:
exact supDegree_sum_le

Result:
no goals
-- Mathlib/Topology/Compactness/CompactlyGeneratedSpace.lean
theorem compactlyGeneratedSpace_of_isOpen_of_t2
    (h : ∀ s, (∀ (K : Set X), IsCompact K → IsOpen (K ↓∩ s)) → IsOpen s) :
    CompactlyGeneratedSpace X

Proof state:
X : Type u
inst✝¹ : TopologicalSpace X
inst✝ : T2Space X
h : ∀ (s : Set X), (∀ (K : Set X), IsCompact K → IsOpen (K ↓∩ s)) → IsOpen s
⊢ CompactlyGeneratedSpace X

Tactic:
refine compactlyGeneratedSpace_of_isOpen fun s hs ↦ h s fun K hK ↦ ?_

Result:
X : Type u
inst✝¹ : TopologicalSpace X
inst✝ : T2Space X
h : ∀ (s : Set X), (∀ (K : Set X), IsCompact K → IsOpen (K ↓∩ s)) → IsOpen s
s : Set X
hs :
  ∀ (K : Type u) [inst : TopologicalSpace K] [inst_1 : CompactSpace K] [inst_2 : T2Space K] (f : K → X),
    Continuous f → IsOpen (f ⁻¹' s)
K : Set X
hK : IsCompact K
⊢ IsOpen (K ↓∩ s)

Proof state:
X : Type u
inst✝¹ : TopologicalSpace X
inst✝ : T2Space X
h : ∀ (s : Set X), (∀ (K : Set X), IsCompact K → IsOpen (K ↓∩ s)) → IsOpen s
s : Set X
hs :
  ∀ (K : Type u) [inst : TopologicalSpace K] [inst_1 : CompactSpace K] [inst_2 : T2Space K] (f : K → X),
    Continuous f → IsOpen (f ⁻¹' s)
K : Set X
hK : IsCompact K
this : CompactSpace ↑K
⊢ IsOpen (K ↓∩ s)

Tactic:
exact hs _ Subtype.val continuous_subtype_val

Result:
no goals

Proof state:
X : Type u
inst✝¹ : TopologicalSpace X
inst✝ : T2Space X
h : ∀ (s : Set X), (∀ (K : Set X), IsCompact K → IsOpen (K ↓∩ s)) → IsOpen s
s : Set X
hs :
  ∀ (K : Type u) [inst : TopologicalSpace K] [inst_1 : CompactSpace K] [inst_2 : T2Space K] (f : K → X),
    Continuous f → IsOpen (f ⁻¹' s)
K : Set X
hK : IsCompact K
⊢ IsOpen (K ↓∩ s)

Tactic:
have : CompactSpace ↑K := isCompact_iff_compactSpace.1 hK

Result:
X : Type u
inst✝¹ : TopologicalSpace X
inst✝ : T2Space X
h : ∀ (s : Set X), (∀ (K : Set X), IsCompact K → IsOpen (K ↓∩ s)) → IsOpen s
s : Set X
hs :
  ∀ (K : Type u) [inst : TopologicalSpace K] [inst_1 : CompactSpace K] [inst_2 : T2Space K] (f : K → X),
    Continuous f → IsOpen (f ⁻¹' s)
K : Set X
hK : IsCompact K
this : CompactSpace ↑K
⊢ IsOpen (K ↓∩ s)
-- Mathlib/Algebra/Order/Antidiag/Nat.lean
theorem card_finMulAntidiag_of_squarefree {d n : ℕ} (hn : Squarefree n) :
    #(finMulAntidiag d n) = d ^ ω n

Proof state:
d n : ℕ
hn : Squarefree n
⊢ #(d.finMulAntidiag n) = d ^ ω n

Tactic:
rw [← card_finMulAntidiag_pi d n hn, Finset.card_pi, Finset.prod_const,
  ArithmeticFunction.cardDistinctFactors_apply, ← List.card_toFinset, toFinset_factors,
  Finset.card_fin]

Result:
no goals
-- Mathlib/Topology/NhdsSet.lean
theorem mem_nhdsSet_iff_exists : s ∈ 𝓝ˢ t ↔ ∃ U : Set X, IsOpen U ∧ t ⊆ U ∧ U ⊆ s

Proof state:
X : Type u_1
inst✝ : TopologicalSpace X
s t : Set X
⊢ s ∈ 𝓝ˢ t ↔ ∃ U, IsOpen U ∧ t ⊆ U ∧ U ⊆ s

Tactic:
rw [← subset_interior_iff_mem_nhdsSet, subset_interior_iff]

Result:
no goals
-- Mathlib/RingTheory/HahnSeries/PowerSeries.lean
theorem ofPowerSeries_apply (x : PowerSeries R) :
    ofPowerSeries Γ R x =
      HahnSeries.embDomain
        ⟨⟨((↑) : ℕ → Γ), Nat.strictMono_cast.injective⟩, by
          simp only [Function.Embedding.coeFn_mk]
          exact Nat.cast_le⟩
        (toPowerSeries.symm x) :=
  rfl

Proof state:
Γ : Type u_1
R : Type u_2
inst✝¹ : Semiring R
inst✝ : StrictOrderedSemiring Γ
x : PowerSeries R
⊢ ∀ {a b : ℕ}, ↑a ≤ ↑b ↔ a ≤ b

Tactic:
exact Nat.cast_le

Result:
no goals

Proof state:
Γ : Type u_1
R : Type u_2
inst✝¹ : Semiring R
inst✝ : StrictOrderedSemiring Γ
x : PowerSeries R
⊢ ∀ {a b : ℕ}, { toFun := Nat.cast, inj' := ⋯ } a ≤ { toFun := Nat.cast, inj' := ⋯ } b ↔ a ≤ b

Tactic:
simp only [Function.Embedding.coeFn_mk]

Result:
Γ : Type u_1
R : Type u_2
inst✝¹ : Semiring R
inst✝ : StrictOrderedSemiring Γ
x : PowerSeries R
⊢ ∀ {a b : ℕ}, ↑a ≤ ↑b ↔ a ≤ b
-- Mathlib/Data/DFinsupp/Defs.lean
theorem support_neg [∀ i, AddGroup (β i)] [∀ (i) (x : β i), Decidable (x ≠ 0)] {f : Π₀ i, β i} :
    support (-f) = support f

Proof state:
case h
ι : Type u
β : ι → Type v
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → AddGroup (β i)
inst✝ : (i : ι) → (x : β i) → Decidable (x ≠ 0)
f : Π₀ (i : ι), β i
i : ι
⊢ i ∈ (-f).support ↔ i ∈ f.support

Tactic:
simp

Result:
no goals

Proof state:
ι : Type u
β : ι → Type v
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → AddGroup (β i)
inst✝ : (i : ι) → (x : β i) → Decidable (x ≠ 0)
f : Π₀ (i : ι), β i
⊢ (-f).support = f.support

Tactic:
ext i

Result:
case h
ι : Type u
β : ι → Type v
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → AddGroup (β i)
inst✝ : (i : ι) → (x : β i) → Decidable (x ≠ 0)
f : Π₀ (i : ι), β i
i : ι
⊢ i ∈ (-f).support ↔ i ∈ f.support
-- Mathlib/Analysis/NormedSpace/Pointwise.lean
theorem smul_sphere [Nontrivial E] (c : 𝕜) (x : E) {r : ℝ} (hr : 0 ≤ r) :
    c • sphere x r = sphere (c • x) (‖c‖ * r)

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : NormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedSpace ℝ E
inst✝ : Nontrivial E
c : 𝕜
x : E
r : ℝ
hr : 0 ≤ r
⊢ c • sphere x r = sphere (c • x) (‖c‖ * r)

Tactic:
rcases eq_or_ne c 0 with (rfl | hc)

Result:
case inl
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : NormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedSpace ℝ E
inst✝ : Nontrivial E
x : E
r : ℝ
hr : 0 ≤ r
⊢ 0 • sphere x r = sphere (0 • x) (‖0‖ * r)

case inr
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : NormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedSpace ℝ E
inst✝ : Nontrivial E
c : 𝕜
x : E
r : ℝ
hr : 0 ≤ r
hc : c ≠ 0
⊢ c • sphere x r = sphere (c • x) (‖c‖ * r)

Proof state:
case inl
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : NormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedSpace ℝ E
inst✝ : Nontrivial E
x : E
r : ℝ
hr : 0 ≤ r
⊢ 0 • sphere x r = sphere (0 • x) (‖0‖ * r)

Tactic:
simp [zero_smul_set, Set.singleton_zero, hr]

Result:
no goals

Proof state:
case inr
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : NormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedSpace ℝ E
inst✝ : Nontrivial E
c : 𝕜
x : E
r : ℝ
hr : 0 ≤ r
hc : c ≠ 0
⊢ c • sphere x r = sphere (c • x) (‖c‖ * r)

Tactic:
exact smul_sphere' hc x r

Result:
no goals
-- Mathlib/NumberTheory/ModularForms/JacobiTheta/Bounds.lean
private lemma exp_lt_aux {t : ℝ} (ht : 0 < t) : rexp (-π * t) < 1

Proof state:
t : ℝ
ht : 0 < t
⊢ rexp (-π * t) < 1

Tactic:
simpa only [exp_lt_one_iff, neg_mul, neg_lt_zero] using mul_pos pi_pos ht

Result:
no goals
-- Mathlib/Algebra/Algebra/NonUnitalHom.lean
theorem snd_prod (f : A →ₙₐ[R] B) (g : A →ₙₐ[R] C) : (snd R B C).comp (prod f g) = g

Proof state:
R : Type u
inst✝⁶ : Monoid R
A : Type v
B : Type w
C : Type w₁
inst✝⁵ : NonUnitalNonAssocSemiring A
inst✝⁴ : DistribMulAction R A
inst✝³ : NonUnitalNonAssocSemiring B
inst✝² : NonUnitalNonAssocSemiring C
inst✝¹ : DistribMulAction R B
inst✝ : DistribMulAction R C
f : A →ₙₐ[R] B
g : A →ₙₐ[R] C
⊢ (snd R B C).comp (f.prod g) = g

Tactic:
rfl

Result:
no goals
-- Mathlib/CategoryTheory/Adjunction/Reflective.lean
theorem unitCompPartialBijective_symm_natural [Reflective i] (A : C) {B B' : C} (h : B ⟶ B')
    (hB : i.essImage B) (hB' : i.essImage B') (f : i.obj ((reflector i).obj A) ⟶ B) :
    (unitCompPartialBijective A hB').symm (f ≫ h) = (unitCompPartialBijective A hB).symm f ≫ h

Proof state:
C : Type u₁
D : Type u₂
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Category.{v₂, u₂} D
i : D ⥤ C
inst✝ : Reflective i
A B B' : C
h : B ⟶ B'
hB : i.essImage B
hB' : i.essImage B'
f : i.obj ((reflector i).obj A) ⟶ B
⊢ (unitCompPartialBijective A hB').symm (f ≫ h) = (unitCompPartialBijective A hB).symm f ≫ h

Tactic:
simp

Result:
no goals
-- Mathlib/RepresentationTheory/GroupCohomology/LowDegree.lean
lemma twoCoboundaries_le_twoCocycles : twoCoboundaries A ≤ twoCocycles A

Proof state:
k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A : Rep k G
⊢ twoCoboundaries A ≤ twoCocycles A

Tactic:
rintro _ ⟨x, rfl⟩

Result:
case intro
k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A : Rep k G
x : G → ↑A.V
⊢ (dOne A) x ∈ twoCocycles A

Proof state:
case intro
k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A : Rep k G
x : G → ↑A.V
⊢ (dOne A) x ∈ twoCocycles A

Tactic:
exact dOne_apply_mem_twoCocycles x

Result:
no goals
-- Mathlib/CategoryTheory/Limits/HasLimits.lean
theorem HasLimit.isoOfEquivalence_inv_π {F : J ⥤ C} [HasLimit F] {G : K ⥤ C} [HasLimit G]
    (e : J ≌ K) (w : e.functor ⋙ G ≅ F) (j : J) :
    (HasLimit.isoOfEquivalence e w).inv ≫ limit.π F j =
    limit.π G (e.functor.obj j) ≫ w.hom.app j

Proof state:
J : Type u₁
inst✝⁴ : Category.{v₁, u₁} J
K : Type u₂
inst✝³ : Category.{v₂, u₂} K
C : Type u
inst✝² : Category.{v, u} C
F : J ⥤ C
inst✝¹ : HasLimit F
G : K ⥤ C
inst✝ : HasLimit G
e : J ≌ K
w : e.functor ⋙ G ≅ F
j : J
⊢ ((limit.isLimit F).conePointsIsoOfEquivalence (limit.isLimit G) e w).inv ≫ limit.π F j =
    limit.π G (e.functor.obj j) ≫ w.hom.app j

Tactic:
dsimp

Result:
J : Type u₁
inst✝⁴ : Category.{v₁, u₁} J
K : Type u₂
inst✝³ : Category.{v₂, u₂} K
C : Type u
inst✝² : Category.{v, u} C
F : J ⥤ C
inst✝¹ : HasLimit F
G : K ⥤ C
inst✝ : HasLimit G
e : J ≌ K
w : e.functor ⋙ G ≅ F
j : J
⊢ limit.lift F ((Cones.postcompose w.hom).obj (Cone.whisker e.functor (limit.cone G))) ≫ limit.π F j =
    limit.π G (e.functor.obj j) ≫ w.hom.app j

Proof state:
J : Type u₁
inst✝⁴ : Category.{v₁, u₁} J
K : Type u₂
inst✝³ : Category.{v₂, u₂} K
C : Type u
inst✝² : Category.{v, u} C
F : J ⥤ C
inst✝¹ : HasLimit F
G : K ⥤ C
inst✝ : HasLimit G
e : J ≌ K
w : e.functor ⋙ G ≅ F
j : J
⊢ limit.lift F ((Cones.postcompose w.hom).obj (Cone.whisker e.functor (limit.cone G))) ≫ limit.π F j =
    limit.π G (e.functor.obj j) ≫ w.hom.app j

Tactic:
simp

Result:
no goals

Proof state:
J : Type u₁
inst✝⁴ : Category.{v₁, u₁} J
K : Type u₂
inst✝³ : Category.{v₂, u₂} K
C : Type u
inst✝² : Category.{v, u} C
F : J ⥤ C
inst✝¹ : HasLimit F
G : K ⥤ C
inst✝ : HasLimit G
e : J ≌ K
w : e.functor ⋙ G ≅ F
j : J
⊢ (isoOfEquivalence e w).inv ≫ limit.π F j = limit.π G (e.functor.obj j) ≫ w.hom.app j

Tactic:
simp only [HasLimit.isoOfEquivalence, IsLimit.conePointsIsoOfEquivalence_hom]

Result:
J : Type u₁
inst✝⁴ : Category.{v₁, u₁} J
K : Type u₂
inst✝³ : Category.{v₂, u₂} K
C : Type u
inst✝² : Category.{v, u} C
F : J ⥤ C
inst✝¹ : HasLimit F
G : K ⥤ C
inst✝ : HasLimit G
e : J ≌ K
w : e.functor ⋙ G ≅ F
j : J
⊢ ((limit.isLimit F).conePointsIsoOfEquivalence (limit.isLimit G) e w).inv ≫ limit.π F j =
    limit.π G (e.functor.obj j) ≫ w.hom.app j
-- Mathlib/.lake/packages/lean4/src/lean/Init/Control/Lawful/Basic.lean
theorem pure_id_seq [Applicative f] [LawfulApplicative f] (x : f α) : pure id <*> x = x

Proof state:
f : Type u_1 → Type u_2
α : Type u_1
inst✝¹ : Applicative f
inst✝ : LawfulApplicative f
x : f α
⊢ pure id <*> x = x

Tactic:
simp [pure_seq]

Result:
no goals