harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Erase.lean
theorem eraseP_filter (f : α → Bool) (l : List α) :
    (filter f l).eraseP p = filter f (l.eraseP (fun x => p x && f x))

Proof state:
case e_a.e_p
α : Type u_1
p f : α → Bool
l : List α
⊢ (fun x =>
      match Option.guard (fun x => f x = true) x with
      | some y => p y
      | none => false) =
    fun x => p x && f x

Tactic:
ext x

Result:
case e_a.e_p.h
α : Type u_1
p f : α → Bool
l : List α
x : α
⊢ (match Option.guard (fun x => f x = true) x with
    | some y => p y
    | none => false) =
    (p x && f x)

Proof state:
α : Type u_1
p f : α → Bool
l : List α
⊢ filterMap (Option.guard fun x => f x = true)
      (eraseP
        (fun x =>
          match Option.guard (fun x => f x = true) x with
          | some y => p y
          | none => false)
        l) =
    filterMap (Option.guard fun x => f x = true) (eraseP (fun x => p x && f x) l)

Tactic:
congr

Result:
case e_a.e_p
α : Type u_1
p f : α → Bool
l : List α
⊢ (fun x =>
      match Option.guard (fun x => f x = true) x with
      | some y => p y
      | none => false) =
    fun x => p x && f x

Proof state:
case e_a.e_p.h
α : Type u_1
p f : α → Bool
l : List α
x : α
⊢ (match Option.guard (fun x => f x = true) x with
    | some y => p y
    | none => false) =
    (p x && f x)

Tactic:
simp only [Option.guard]

Result:
case e_a.e_p.h
α : Type u_1
p f : α → Bool
l : List α
x : α
⊢ (match if f x = true then some x else none with
    | some y => p y
    | none => false) =
    (p x && f x)

Proof state:
case e_a.e_p.h
α : Type u_1
p f : α → Bool
l : List α
x : α
⊢ (match if f x = true then some x else none with
    | some y => p y
    | none => false) =
    (p x && f x)

Tactic:
split <;> split at * <;> simp_all

Result:
no goals

Proof state:
α : Type u_1
p f : α → Bool
l : List α
⊢ eraseP p (filter f l) = filter f (eraseP (fun x => p x && f x) l)

Tactic:
rw [← filterMap_eq_filter, eraseP_filterMap]

Result:
α : Type u_1
p f : α → Bool
l : List α
⊢ filterMap (Option.guard fun x => f x = true)
      (eraseP
        (fun x =>
          match Option.guard (fun x => f x = true) x with
          | some y => p y
          | none => false)
        l) =
    filterMap (Option.guard fun x => f x = true) (eraseP (fun x => p x && f x) l)
-- Mathlib/Data/Real/EReal.lean
lemma add_ne_top_iff_of_ne_bot_of_ne_top {x y : EReal} (hy : y ≠ ⊥) (hy' : y ≠ ⊤) :
    x + y ≠ ⊤ ↔ x ≠ ⊤

Proof state:
x y : EReal
hy : y ≠ ⊥
hy' : y ≠ ⊤
⊢ x + y ≠ ⊤ ↔ x ≠ ⊤

Tactic:
induction x <;> simp [add_ne_top_iff_of_ne_bot, hy, hy']

Result:
no goals
-- Mathlib/Data/Int/Log.lean
theorem clog_natCast (b : ℕ) (n : ℕ) : clog b (n : R) = Nat.clog b n

Proof state:
case zero
R : Type u_1
inst✝¹ : LinearOrderedSemifield R
inst✝ : FloorSemiring R
b : ℕ
⊢ clog b ↑0 = ↑(Nat.clog b 0)

Tactic:
simp [clog_of_right_le_one]

Result:
no goals

Proof state:
case succ
R : Type u_1
inst✝¹ : LinearOrderedSemifield R
inst✝ : FloorSemiring R
b n : ℕ
⊢ clog b ↑(n + 1) = ↑(Nat.clog b (n + 1))

Tactic:
rw [clog_of_one_le_right, (Nat.ceil_eq_iff (Nat.succ_ne_zero n)).mpr] <;> simp

Result:
no goals

Proof state:
R : Type u_1
inst✝¹ : LinearOrderedSemifield R
inst✝ : FloorSemiring R
b n : ℕ
⊢ clog b ↑n = ↑(Nat.clog b n)

Tactic:
rcases n with - | n

Result:
case zero
R : Type u_1
inst✝¹ : LinearOrderedSemifield R
inst✝ : FloorSemiring R
b : ℕ
⊢ clog b ↑0 = ↑(Nat.clog b 0)

case succ
R : Type u_1
inst✝¹ : LinearOrderedSemifield R
inst✝ : FloorSemiring R
b n : ℕ
⊢ clog b ↑(n + 1) = ↑(Nat.clog b (n + 1))
-- Mathlib/Algebra/Lie/CartanSubalgebra.lean
theorem isCartanSubalgebra_iff_isUcsLimit : H.IsCartanSubalgebra ↔ H.toLieSubmodule.IsUcsLimit

Proof state:
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
H : LieSubalgebra R L
k : ℕ
hk : ∀ (l : ℕ), k ≤ l → LieSubmodule.ucs l ⊥ = H.toLieSubmodule
hk' : LieSubmodule.ucs (k + 1) ⊥ = H.toLieSubmodule
⊢ H.normalizer = H

Tactic:
rw [LieSubmodule.ucs_succ, hk k (le_refl k)] at hk'

Result:
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
H : LieSubalgebra R L
k : ℕ
hk : ∀ (l : ℕ), k ≤ l → LieSubmodule.ucs l ⊥ = H.toLieSubmodule
hk' : H.toLieSubmodule.normalizer = H.toLieSubmodule
⊢ H.normalizer = H
-- Mathlib/Analysis/Convex/Star.lean
theorem StarConvex.add_left (hs : StarConvex 𝕜 x s) (z : E) :
    StarConvex 𝕜 (z + x) ((fun x => z + x) '' s)

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝² : OrderedSemiring 𝕜
inst✝¹ : AddCommMonoid E
inst✝ : Module 𝕜 E
x : E
s : Set E
hs : StarConvex 𝕜 x s
z y : E
hy : y ∈ (fun x => z + x) '' s
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
⊢ a • (z + x) + b • y ∈ (fun x => z + x) '' s

Tactic:
obtain ⟨y', hy', rfl⟩ := hy

Result:
case intro.intro
𝕜 : Type u_1
E : Type u_2
inst✝² : OrderedSemiring 𝕜
inst✝¹ : AddCommMonoid E
inst✝ : Module 𝕜 E
x : E
s : Set E
hs : StarConvex 𝕜 x s
z : E
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
y' : E
hy' : y' ∈ s
⊢ a • (z + x) + b • (fun x => z + x) y' ∈ (fun x => z + x) '' s

Proof state:
case intro.intro
𝕜 : Type u_1
E : Type u_2
inst✝² : OrderedSemiring 𝕜
inst✝¹ : AddCommMonoid E
inst✝ : Module 𝕜 E
x : E
s : Set E
hs : StarConvex 𝕜 x s
z : E
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
y' : E
hy' : y' ∈ s
⊢ (fun x => z + x) (a • x + b • y') = a • (z + x) + b • (fun x => z + x) y'

Tactic:
match_scalars <;> simp [hab]

Result:
no goals

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝² : OrderedSemiring 𝕜
inst✝¹ : AddCommMonoid E
inst✝ : Module 𝕜 E
x : E
s : Set E
hs : StarConvex 𝕜 x s
z : E
⊢ StarConvex 𝕜 (z + x) ((fun x => z + x) '' s)

Tactic:
intro y hy a b ha hb hab

Result:
𝕜 : Type u_1
E : Type u_2
inst✝² : OrderedSemiring 𝕜
inst✝¹ : AddCommMonoid E
inst✝ : Module 𝕜 E
x : E
s : Set E
hs : StarConvex 𝕜 x s
z y : E
hy : y ∈ (fun x => z + x) '' s
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
⊢ a • (z + x) + b • y ∈ (fun x => z + x) '' s

Proof state:
case intro.intro
𝕜 : Type u_1
E : Type u_2
inst✝² : OrderedSemiring 𝕜
inst✝¹ : AddCommMonoid E
inst✝ : Module 𝕜 E
x : E
s : Set E
hs : StarConvex 𝕜 x s
z : E
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
y' : E
hy' : y' ∈ s
⊢ a • (z + x) + b • (fun x => z + x) y' ∈ (fun x => z + x) '' s

Tactic:
refine ⟨a • x + b • y', hs hy' ha hb hab, ?_⟩

Result:
case intro.intro
𝕜 : Type u_1
E : Type u_2
inst✝² : OrderedSemiring 𝕜
inst✝¹ : AddCommMonoid E
inst✝ : Module 𝕜 E
x : E
s : Set E
hs : StarConvex 𝕜 x s
z : E
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
y' : E
hy' : y' ∈ s
⊢ (fun x => z + x) (a • x + b • y') = a • (z + x) + b • (fun x => z + x) y'
-- Mathlib/.lake/packages/batteries/Batteries/Data/List/Lemmas.lean
theorem nil_union (l : List α) : nil ∪ l = l

Proof state:
α : Type u_1
inst✝ : BEq α
l : List α
⊢ [] ∪ l = l

Tactic:
simp [List.union_def, foldr]

Result:
no goals
-- Mathlib/Algebra/Algebra/Quasispectrum.lean
lemma isQuasiregular_iff_isUnit' (R : Type*) {A : Type*} [CommSemiring R] [NonUnitalSemiring A]
    [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] {x : A} :
    IsQuasiregular x ↔ IsUnit (1 + x : Unitization R A)

Proof state:
case refine_1.intro
R : Type u_1
A : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : NonUnitalSemiring A
inst✝² : Module R A
inst✝¹ : IsScalarTower R A A
inst✝ : SMulCommClass R A A
u : (PreQuasiregular A)ˣ
⊢ IsUnit (1 + ↑(PreQuasiregular.equiv.symm ↑u))

Tactic:
exact (Unitization.unitsFstOne_mulEquiv_quasiregular R).symm u |>.val.isUnit

Result:
no goals

Proof state:
R : Type u_1
A : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : NonUnitalSemiring A
inst✝² : Module R A
inst✝¹ : IsScalarTower R A A
inst✝ : SMulCommClass R A A
x : A
⊢ IsQuasiregular x ↔ IsUnit (1 + ↑x)

Tactic:
refine ⟨?_, fun hx ↦ ?_⟩

Result:
case refine_1
R : Type u_1
A : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : NonUnitalSemiring A
inst✝² : Module R A
inst✝¹ : IsScalarTower R A A
inst✝ : SMulCommClass R A A
x : A
⊢ IsQuasiregular x → IsUnit (1 + ↑x)

case refine_2
R : Type u_1
A : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : NonUnitalSemiring A
inst✝² : Module R A
inst✝¹ : IsScalarTower R A A
inst✝ : SMulCommClass R A A
x : A
hx : IsUnit (1 + ↑x)
⊢ IsQuasiregular x

Proof state:
case refine_2
R : Type u_1
A : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : NonUnitalSemiring A
inst✝² : Module R A
inst✝¹ : IsScalarTower R A A
inst✝ : SMulCommClass R A A
x : A
hx : IsUnit (1 + ↑x)
⊢ IsQuasiregular x

Tactic:
exact ⟨(Unitization.unitsFstOne_mulEquiv_quasiregular R) ⟨hx.unit, by simp⟩, by simp⟩

Result:
no goals

Proof state:
R : Type u_1
A : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : NonUnitalSemiring A
inst✝² : Module R A
inst✝¹ : IsScalarTower R A A
inst✝ : SMulCommClass R A A
x : A
hx : IsUnit (1 + ↑x)
⊢ hx.unit ∈ Unitization.unitsFstOne R A

Tactic:
simp

Result:
no goals

Proof state:
case refine_1
R : Type u_1
A : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : NonUnitalSemiring A
inst✝² : Module R A
inst✝¹ : IsScalarTower R A A
inst✝ : SMulCommClass R A A
x : A
⊢ IsQuasiregular x → IsUnit (1 + ↑x)

Tactic:
rintro ⟨u, rfl⟩

Result:
case refine_1.intro
R : Type u_1
A : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : NonUnitalSemiring A
inst✝² : Module R A
inst✝¹ : IsScalarTower R A A
inst✝ : SMulCommClass R A A
u : (PreQuasiregular A)ˣ
⊢ IsUnit (1 + ↑(PreQuasiregular.equiv.symm ↑u))

Proof state:
R : Type u_1
A : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : NonUnitalSemiring A
inst✝² : Module R A
inst✝¹ : IsScalarTower R A A
inst✝ : SMulCommClass R A A
x : A
hx : IsUnit (1 + ↑x)
⊢ PreQuasiregular.equiv.symm ↑((Unitization.unitsFstOne_mulEquiv_quasiregular R) ⟨hx.unit, ⋯⟩) = x

Tactic:
simp

Result:
no goals
-- Mathlib/MeasureTheory/Integral/Prod.lean
theorem integral_prod_symm (f : α × β → E) (hf : Integrable f (μ.prod ν)) :
    ∫ z, f z ∂μ.prod ν = ∫ y, ∫ x, f (x, y) ∂μ ∂ν

Proof state:
α : Type u_1
β : Type u_2
E : Type u_3
inst✝⁵ : MeasurableSpace α
inst✝⁴ : MeasurableSpace β
μ : Measure α
ν : Measure β
inst✝³ : NormedAddCommGroup E
inst✝² : SFinite ν
inst✝¹ : NormedSpace ℝ E
inst✝ : SFinite μ
f : α × β → E
hf : Integrable f (μ.prod ν)
⊢ ∫ (z : α × β), f z ∂μ.prod ν = ∫ (y : β), ∫ (x : α), f (x, y) ∂μ ∂ν

Tactic:
rw [← integral_prod_swap f]

Result:
α : Type u_1
β : Type u_2
E : Type u_3
inst✝⁵ : MeasurableSpace α
inst✝⁴ : MeasurableSpace β
μ : Measure α
ν : Measure β
inst✝³ : NormedAddCommGroup E
inst✝² : SFinite ν
inst✝¹ : NormedSpace ℝ E
inst✝ : SFinite μ
f : α × β → E
hf : Integrable f (μ.prod ν)
⊢ ∫ (z : β × α), f z.swap ∂ν.prod μ = ∫ (y : β), ∫ (x : α), f (x, y) ∂μ ∂ν

Proof state:
α : Type u_1
β : Type u_2
E : Type u_3
inst✝⁵ : MeasurableSpace α
inst✝⁴ : MeasurableSpace β
μ : Measure α
ν : Measure β
inst✝³ : NormedAddCommGroup E
inst✝² : SFinite ν
inst✝¹ : NormedSpace ℝ E
inst✝ : SFinite μ
f : α × β → E
hf : Integrable f (μ.prod ν)
⊢ ∫ (z : β × α), f z.swap ∂ν.prod μ = ∫ (y : β), ∫ (x : α), f (x, y) ∂μ ∂ν

Tactic:
exact integral_prod _ hf.swap

Result:
no goals
-- Mathlib/RepresentationTheory/GroupCohomology/Functoriality.lean
theorem H0Map_id : H0Map (MonoidHom.id _) (𝟙 A) = 𝟙 _

Proof state:
k H : Type u
inst✝¹ : CommRing k
inst✝ : Group H
A : Rep k H
⊢ H0Map (MonoidHom.id H) (𝟙 A) = 𝟙 (H0 A)

Tactic:
rfl

Result:
no goals
-- Mathlib/Data/Matrix/Mul.lean
theorem comp_equiv_symm_dotProduct (e : m ≃ n) : u ∘ e.symm ⬝ᵥ x = u ⬝ᵥ x ∘ e :=
  (e.sum_comp _).symm.trans <|
    Finset.sum_congr rfl fun _ _ => by simp only [Function.comp, Equiv.symm_apply_apply]

Proof state:
m : Type u_2
n : Type u_3
α : Type v
inst✝² : Fintype m
inst✝¹ : Fintype n
inst✝ : NonUnitalNonAssocSemiring α
u : m → α
x : n → α
e : m ≃ n
x✝¹ : m
x✝ : x✝¹ ∈ Finset.univ
⊢ (u ∘ ⇑e.symm) (e x✝¹) * x (e x✝¹) = u x✝¹ * (x ∘ ⇑e) x✝¹

Tactic:
simp only [Function.comp, Equiv.symm_apply_apply]

Result:
no goals
-- Mathlib/RingTheory/Polynomial/HilbertPoly.lean
lemma preHilbertPoly_eq_choose_sub_add [CharZero F] (d : ℕ) {k n : ℕ} (hkn : k ≤ n):
    (preHilbertPoly F d k).eval (n : F) = (n - k + d).choose d

Proof state:
F : Type u_1
inst✝¹ : Field F
inst✝ : CharZero F
d k n : ℕ
hkn : k ≤ n
⊢ ¬d ! = 0

Tactic:
positivity

Result:
no goals

Proof state:
F : Type u_1
inst✝¹ : Field F
inst✝ : CharZero F
d k n : ℕ
hkn : k ≤ n
this : ↑d ! ≠ 0
⊢ eval (↑n) (preHilbertPoly F d k) = (↑d !)⁻¹ * eval (↑(n - k + 1)) (ascPochhammer F d)

Tactic:
simp [cast_sub hkn, preHilbertPoly]

Result:
no goals

Proof state:
F : Type u_1
inst✝¹ : Field F
inst✝ : CharZero F
d k n : ℕ
hkn : k ≤ n
this : ↑d ! ≠ 0
⊢ (↑d !)⁻¹ * eval (↑(n - k + 1)) (ascPochhammer F d) = ↑((n - k + d).choose d)

Tactic:
rw [ascPochhammer_nat_eq_natCast_ascFactorial]

Result:
F : Type u_1
inst✝¹ : Field F
inst✝ : CharZero F
d k n : ℕ
hkn : k ≤ n
this : ↑d ! ≠ 0
⊢ (↑d !)⁻¹ * ↑((n - k + 1).ascFactorial d) = ↑((n - k + d).choose d)

Proof state:
F : Type u_1
inst✝¹ : Field F
inst✝ : CharZero F
d k n : ℕ
hkn : k ≤ n
⊢ ↑d ! ≠ 0

Tactic:
norm_cast

Result:
F : Type u_1
inst✝¹ : Field F
inst✝ : CharZero F
d k n : ℕ
hkn : k ≤ n
⊢ ¬d ! = 0

Proof state:
F : Type u_1
inst✝¹ : Field F
inst✝ : CharZero F
d k n : ℕ
hkn : k ≤ n
this : ↑d ! ≠ 0
⊢ eval (↑n) (preHilbertPoly F d k) = ↑((n - k + d).choose d)

Tactic:
calc
_ = (↑d !)⁻¹ * eval (↑(n - k + 1)) (ascPochhammer F d) := by simp [cast_sub hkn, preHilbertPoly]
_ = (n - k + d).choose d := by
  rw [ascPochhammer_nat_eq_natCast_ascFactorial];
  field_simp [ascFactorial_eq_factorial_mul_choose]

Result:
no goals

Proof state:
F : Type u_1
inst✝¹ : Field F
inst✝ : CharZero F
d k n : ℕ
hkn : k ≤ n
this : ↑d ! ≠ 0
⊢ (↑d !)⁻¹ * ↑((n - k + 1).ascFactorial d) = ↑((n - k + d).choose d)

Tactic:
field_simp [ascFactorial_eq_factorial_mul_choose]

Result:
no goals

Proof state:
F : Type u_1
inst✝¹ : Field F
inst✝ : CharZero F
d k n : ℕ
hkn : k ≤ n
⊢ eval (↑n) (preHilbertPoly F d k) = ↑((n - k + d).choose d)

Tactic:
have : (d ! : F) ≠ 0 := by norm_cast; positivity

Result:
F : Type u_1
inst✝¹ : Field F
inst✝ : CharZero F
d k n : ℕ
hkn : k ≤ n
this : ↑d ! ≠ 0
⊢ eval (↑n) (preHilbertPoly F d k) = ↑((n - k + d).choose d)
-- Mathlib/LinearAlgebra/Matrix/PosDef.lean
theorem intCast [StarOrderedRing R] [DecidableEq n] [NoZeroDivisors R]
    (d : ℤ) (hd : 0 < d) :
    PosDef (d : Matrix n n R) :=
  ⟨isHermitian_intCast _, fun x hx => by
    simp only [intCast_mulVec, dotProduct_smul]
    rw [Int.cast_smul_eq_zsmul]
    exact zsmul_pos (dotProduct_star_self_pos_iff.mpr hx) hd⟩

Proof state:
n : Type u_2
R : Type u_3
inst✝⁶ : Fintype n
inst✝⁵ : CommRing R
inst✝⁴ : PartialOrder R
inst✝³ : StarRing R
inst✝² : StarOrderedRing R
inst✝¹ : DecidableEq n
inst✝ : NoZeroDivisors R
d : ℤ
hd : 0 < d
x : n → R
hx : x ≠ 0
⊢ 0 < ↑d • (star x ⬝ᵥ x)

Tactic:
rw [Int.cast_smul_eq_zsmul]

Result:
n : Type u_2
R : Type u_3
inst✝⁶ : Fintype n
inst✝⁵ : CommRing R
inst✝⁴ : PartialOrder R
inst✝³ : StarRing R
inst✝² : StarOrderedRing R
inst✝¹ : DecidableEq n
inst✝ : NoZeroDivisors R
d : ℤ
hd : 0 < d
x : n → R
hx : x ≠ 0
⊢ 0 < d • (star x ⬝ᵥ x)

Proof state:
n : Type u_2
R : Type u_3
inst✝⁶ : Fintype n
inst✝⁵ : CommRing R
inst✝⁴ : PartialOrder R
inst✝³ : StarRing R
inst✝² : StarOrderedRing R
inst✝¹ : DecidableEq n
inst✝ : NoZeroDivisors R
d : ℤ
hd : 0 < d
x : n → R
hx : x ≠ 0
⊢ 0 < d • (star x ⬝ᵥ x)

Tactic:
exact zsmul_pos (dotProduct_star_self_pos_iff.mpr hx) hd

Result:
no goals

Proof state:
n : Type u_2
R : Type u_3
inst✝⁶ : Fintype n
inst✝⁵ : CommRing R
inst✝⁴ : PartialOrder R
inst✝³ : StarRing R
inst✝² : StarOrderedRing R
inst✝¹ : DecidableEq n
inst✝ : NoZeroDivisors R
d : ℤ
hd : 0 < d
x : n → R
hx : x ≠ 0
⊢ 0 < star x ⬝ᵥ ↑d *ᵥ x

Tactic:
simp only [intCast_mulVec, dotProduct_smul]

Result:
n : Type u_2
R : Type u_3
inst✝⁶ : Fintype n
inst✝⁵ : CommRing R
inst✝⁴ : PartialOrder R
inst✝³ : StarRing R
inst✝² : StarOrderedRing R
inst✝¹ : DecidableEq n
inst✝ : NoZeroDivisors R
d : ℤ
hd : 0 < d
x : n → R
hx : x ≠ 0
⊢ 0 < ↑d • (star x ⬝ᵥ x)
-- Mathlib/GroupTheory/PushoutI.lean
theorem rcons_injective {i : ι} : Function.Injective (rcons (d := d) i)

Proof state:
case mk.mk.mk.mk
ι : Type u_1
G : ι → Type u_2
H : Type u_3
inst✝³ : (i : ι) → Group (G i)
inst✝² : Group H
φ : (i : ι) → H →* G i
d : Transversal φ
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → DecidableEq (G i)
i : ι
head₁ : G i
tail₁ : Word G
fstIdx_ne✝¹ : tail₁.fstIdx ≠ some i
normalized✝¹ :
  ∀ (i_1 : ι) (g : G i_1),
    ⟨i_1, g⟩ ∈ { head := head₁, tail := tail₁, fstIdx_ne := fstIdx_ne✝¹ }.tail.toList → g ∈ d.set i_1
head₂ : G i
tail₂ : Word G
fstIdx_ne✝ : tail₂.fstIdx ≠ some i
normalized✝ :
  ∀ (i_1 : ι) (g : G i_1),
    ⟨i_1, g⟩ ∈ { head := head₂, tail := tail₂, fstIdx_ne := fstIdx_ne✝ }.tail.toList → g ∈ d.set i_1
⊢ rcons i { head := head₁, tail := tail₁, fstIdx_ne := fstIdx_ne✝¹, normalized := normalized✝¹ } =
      rcons i { head := head₂, tail := tail₂, fstIdx_ne := fstIdx_ne✝, normalized := normalized✝ } →
    { head := head₁, tail := tail₁, fstIdx_ne := fstIdx_ne✝¹, normalized := normalized✝¹ } =
      { head := head₂, tail := tail₂, fstIdx_ne := fstIdx_ne✝, normalized := normalized✝ }

Tactic:
simp only [rcons, NormalWord.mk.injEq, EmbeddingLike.apply_eq_iff_eq,
  Word.Pair.mk.injEq, Pair.mk.injEq, and_imp]

Result:
case mk.mk.mk.mk
ι : Type u_1
G : ι → Type u_2
H : Type u_3
inst✝³ : (i : ι) → Group (G i)
inst✝² : Group H
φ : (i : ι) → H →* G i
d : Transversal φ
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → DecidableEq (G i)
i : ι
head₁ : G i
tail₁ : Word G
fstIdx_ne✝¹ : tail₁.fstIdx ≠ some i
normalized✝¹ :
  ∀ (i_1 : ι) (g : G i_1),
    ⟨i_1, g⟩ ∈ { head := head₁, tail := tail₁, fstIdx_ne := fstIdx_ne✝¹ }.tail.toList → g ∈ d.set i_1
head₂ : G i
tail₂ : Word G
fstIdx_ne✝ : tail₂.fstIdx ≠ some i
normalized✝ :
  ∀ (i_1 : ι) (g : G i_1),
    ⟨i_1, g⟩ ∈ { head := head₂, tail := tail₂, fstIdx_ne := fstIdx_ne✝ }.tail.toList → g ∈ d.set i_1
⊢ ↑(⋯.equiv head₁).2 = ↑(⋯.equiv head₂).2 →
    tail₁ = tail₂ → (⋯.equiv head₁).1 = (⋯.equiv head₂).1 → head₁ = head₂ ∧ tail₁ = tail₂
-- Mathlib/Tactic/NormNum/Eq.lean
theorem isInt_eq_false [Ring α] [CharZero α] : {a b : α} → {a' b' : ℤ} →
    IsInt a a' → IsInt b b' → decide (a' = b') = false → ¬a = b
  | _, _, _, _, ⟨rfl⟩, ⟨rfl⟩, h => by simpa using of_decide_eq_false h

Proof state:
α : Type u_1
inst✝¹ : Ring α
inst✝ : CharZero α
n✝¹ n✝ : ℤ
h : decide (n✝¹ = n✝) = false
⊢ ¬↑n✝¹ = ↑n✝

Tactic:
simpa using of_decide_eq_false h

Result:
no goals
-- Mathlib/Order/Directed.lean
theorem directedOn_image {s : Set β} {f : β → α} :
    DirectedOn r (f '' s) ↔ DirectedOn (f ⁻¹'o r) s

Proof state:
α : Type u
β : Type v
r : α → α → Prop
s : Set β
f : β → α
⊢ DirectedOn r (f '' s) ↔ DirectedOn (f ⁻¹'o r) s

Tactic:
simp only [DirectedOn, Set.mem_image, exists_exists_and_eq_and, forall_exists_index, and_imp,
  forall_apply_eq_imp_iff₂, Order.Preimage]

Result:
no goals
-- Mathlib/RingTheory/Support.lean
lemma Module.support_subset_of_surjective (hf : Function.Surjective f) :
    Module.support R N ⊆ Module.support R M

Proof state:
R : Type u_1
M : Type u_2
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
N : Type u_3
inst✝¹ : AddCommGroup N
inst✝ : Module R N
f : M →ₗ[R] N
hf : Function.Surjective ⇑f
x : PrimeSpectrum R
m : M
hm : ∀ r ∉ x.asIdeal, r • f m ≠ 0
r : R
hr : r ∉ x.asIdeal
e : r • m = 0
⊢ r • f m = 0

Tactic:
simpa using congr(f $e)

Result:
no goals

Proof state:
case intro
R : Type u_1
M : Type u_2
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
N : Type u_3
inst✝¹ : AddCommGroup N
inst✝ : Module R N
f : M →ₗ[R] N
hf : Function.Surjective ⇑f
x : PrimeSpectrum R
m : N
hm : ∀ r ∉ x.asIdeal, r • m ≠ 0
⊢ ∃ m, ∀ r ∉ x.asIdeal, r • m ≠ 0

Tactic:
obtain ⟨m, rfl⟩ := hf m

Result:
case intro.intro
R : Type u_1
M : Type u_2
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
N : Type u_3
inst✝¹ : AddCommGroup N
inst✝ : Module R N
f : M →ₗ[R] N
hf : Function.Surjective ⇑f
x : PrimeSpectrum R
m : M
hm : ∀ r ∉ x.asIdeal, r • f m ≠ 0
⊢ ∃ m, ∀ r ∉ x.asIdeal, r • m ≠ 0

Proof state:
R : Type u_1
M : Type u_2
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
N : Type u_3
inst✝¹ : AddCommGroup N
inst✝ : Module R N
f : M →ₗ[R] N
hf : Function.Surjective ⇑f
⊢ support R N ⊆ support R M

Tactic:
simp_rw [Set.subset_def, mem_support_iff']

Result:
R : Type u_1
M : Type u_2
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
N : Type u_3
inst✝¹ : AddCommGroup N
inst✝ : Module R N
f : M →ₗ[R] N
hf : Function.Surjective ⇑f
⊢ ∀ (x : PrimeSpectrum R), (∃ m, ∀ r ∉ x.asIdeal, r • m ≠ 0) → ∃ m, ∀ r ∉ x.asIdeal, r • m ≠ 0

Proof state:
R : Type u_1
M : Type u_2
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
N : Type u_3
inst✝¹ : AddCommGroup N
inst✝ : Module R N
f : M →ₗ[R] N
hf : Function.Surjective ⇑f
⊢ ∀ (x : PrimeSpectrum R), (∃ m, ∀ r ∉ x.asIdeal, r • m ≠ 0) → ∃ m, ∀ r ∉ x.asIdeal, r • m ≠ 0

Tactic:
rintro x ⟨m, hm⟩

Result:
case intro
R : Type u_1
M : Type u_2
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
N : Type u_3
inst✝¹ : AddCommGroup N
inst✝ : Module R N
f : M →ₗ[R] N
hf : Function.Surjective ⇑f
x : PrimeSpectrum R
m : N
hm : ∀ r ∉ x.asIdeal, r • m ≠ 0
⊢ ∃ m, ∀ r ∉ x.asIdeal, r • m ≠ 0

Proof state:
case intro.intro
R : Type u_1
M : Type u_2
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
N : Type u_3
inst✝¹ : AddCommGroup N
inst✝ : Module R N
f : M →ₗ[R] N
hf : Function.Surjective ⇑f
x : PrimeSpectrum R
m : M
hm : ∀ r ∉ x.asIdeal, r • f m ≠ 0
⊢ ∃ m, ∀ r ∉ x.asIdeal, r • m ≠ 0

Tactic:
exact ⟨m, fun r hr e ↦ hm r hr (by simpa using congr(f $e))⟩

Result:
no goals
-- Mathlib/Analysis/InnerProductSpace/Defs.lean
theorem inner_add_right (x y z : F) : ⟪x, y + z⟫ = ⟪x, y⟫ + ⟪x, z⟫

Proof state:
𝕜 : Type u_1
F : Type u_3
inst✝² : RCLike 𝕜
inst✝¹ : AddCommGroup F
inst✝ : Module 𝕜 F
c : PreInnerProductSpace.Core 𝕜 F
x y z : F
⊢ (starRingEnd 𝕜) ⟪y, x⟫_𝕜 + (starRingEnd 𝕜) ⟪z, x⟫_𝕜 = ⟪x, y⟫_𝕜 + ⟪x, z⟫_𝕜

Tactic:
simp only [inner_conj_symm]

Result:
no goals

Proof state:
𝕜 : Type u_1
F : Type u_3
inst✝² : RCLike 𝕜
inst✝¹ : AddCommGroup F
inst✝ : Module 𝕜 F
c : PreInnerProductSpace.Core 𝕜 F
x y z : F
⊢ ⟪x, y + z⟫_𝕜 = ⟪x, y⟫_𝕜 + ⟪x, z⟫_𝕜

Tactic:
rw [← inner_conj_symm, inner_add_left, RingHom.map_add]

Result:
𝕜 : Type u_1
F : Type u_3
inst✝² : RCLike 𝕜
inst✝¹ : AddCommGroup F
inst✝ : Module 𝕜 F
c : PreInnerProductSpace.Core 𝕜 F
x y z : F
⊢ (starRingEnd 𝕜) ⟪y, x⟫_𝕜 + (starRingEnd 𝕜) ⟪z, x⟫_𝕜 = ⟪x, y⟫_𝕜 + ⟪x, z⟫_𝕜
-- Mathlib/Analysis/SpecialFunctions/Trigonometric/Deriv.lean
theorem sinh_nonpos_iff : sinh x ≤ 0 ↔ x ≤ 0

Proof state:
x : ℝ
⊢ sinh x ≤ 0 ↔ x ≤ 0

Tactic:
simpa only [sinh_zero] using @sinh_le_sinh x 0

Result:
no goals