harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Data/Nat/Choose/Basic.lean
theorem choose_self (n : ℕ) : choose n n = 1

Proof state:
n : ℕ
⊢ n.choose n = 1

Tactic:
induction n <;> simp [*, choose, choose_eq_zero_of_lt (lt_succ_self _)]

Result:
no goals
-- Mathlib/Probability/Moments/MGFAnalytic.lean
/-- The derivatives of the moment generating function at zero are the moments. -/
lemma iteratedDeriv_mgf_zero (h : 0 ∈ interior (integrableExpSet X μ)) (n : ℕ) :
    iteratedDeriv n (mgf X μ) 0 = μ[X ^ n]

Proof state:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
h : 0 ∈ interior (integrableExpSet X μ)
n : ℕ
⊢ iteratedDeriv n (mgf X μ) 0 = ∫ (x : Ω), (X ^ n) x ∂μ

Tactic:
simp [iteratedDeriv_mgf h n]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Grind/Norm.lean
theorem not_eq_prop (p q : Prop) : (¬(p = q)) = (p = ¬q)

Proof state:
p q : Prop
⊢ (¬p = q) = (p = ¬q)

Tactic:
by_cases p <;> by_cases q <;> simp [*]

Result:
no goals
-- Mathlib/Algebra/Group/Pointwise/Set/ListOfFn.lean
theorem mem_pow {a : α} {n : ℕ} :
    a ∈ s ^ n ↔ ∃ f : Fin n → s, (List.ofFn fun i ↦ (f i : α)).prod = a

Proof state:
α : Type u_1
inst✝ : Monoid α
s : Set α
a : α
n : ℕ
⊢ a ∈ s ^ n ↔ ∃ f, (List.ofFn fun i => ↑(f i)).prod = a

Tactic:
rw [← mem_prod_list_ofFn, List.ofFn_const, List.prod_replicate]

Result:
no goals
-- Mathlib/Topology/MetricSpace/Lipschitz.lean
theorem of_le_add_mul {f : α → ℝ} (K : ℝ≥0) (h : ∀ x y, f x ≤ f y + K * dist x y) :
    LipschitzWith K f

Proof state:
α : Type u
inst✝ : PseudoMetricSpace α
f : α → ℝ
K : ℝ≥0
h : ∀ (x y : α), f x ≤ f y + ↑K * dist x y
⊢ LipschitzWith K f

Tactic:
simpa only [Real.toNNReal_coe] using LipschitzWith.of_le_add_mul' K h

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Log/Base.lean
theorem logb_rpow_eq_mul_logb_of_pos (hx : 0 < x) : logb b (x ^ y) = y * logb b x

Proof state:
b x y : ℝ
hx : 0 < x
⊢ logb b (x ^ y) = y * logb b x

Tactic:
rw [logb, log_rpow hx, logb, mul_div_assoc]

Result:
no goals
-- Mathlib/Algebra/Polynomial/Bivariate.lean
@[simp]
lemma evalEval_CC (x y : R) (p : R) : (CC p).evalEval x y = p

Proof state:
R : Type u_1
inst✝ : Semiring R
x y p : R
⊢ evalEval x y (CC p) = p

Tactic:
rw [evalEval_C, eval_C]

Result:
no goals
-- Mathlib/AlgebraicGeometry/Morphisms/ClosedImmersion.lean
lemma iff_isPreimmersion {X Y : Scheme} {f : X ⟶ Y} :
    IsClosedImmersion f ↔ IsPreimmersion f ∧ IsClosed (Set.range f.base)

Proof state:
X Y : Scheme
f : X ⟶ Y
⊢ IsClosedImmersion f ↔ IsPreimmersion f ∧ IsClosed (Set.range ⇑(ConcreteCategory.hom f.base))

Tactic:
rw [isClosedImmersion_iff, isPreimmersion_iff, and_assoc, isClosedEmbedding_iff]

Result:
no goals
-- Mathlib/RingTheory/IsAdjoinRoot.lean
theorem modByMonicHom_root (h : IsAdjoinRootMonic S f) (hdeg : 1 < natDegree f) :
    h.modByMonicHom h.root = X

Proof state:
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : Ring S
f : R[X]
inst✝ : Algebra R S
h : IsAdjoinRootMonic S f
hdeg : 1 < f.natDegree
⊢ h.modByMonicHom h.root = X

Tactic:
simpa using modByMonicHom_root_pow h hdeg

Result:
no goals
-- Mathlib/CategoryTheory/Equivalence.lean
theorem cancel_unit_right_assoc' {W X X' Y Y' Z : C} (f : W ⟶ X) (g : X ⟶ Y) (h : Y ⟶ Z)
    (f' : W ⟶ X') (g' : X' ⟶ Y') (h' : Y' ⟶ Z) :
    f ≫ g ≫ h ≫ e.unit.app Z = f' ≫ g' ≫ h' ≫ e.unit.app Z ↔ f ≫ g ≫ h = f' ≫ g' ≫ h'

Proof state:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
e : C ≌ D
W X X' Y Y' Z : C
f : W ⟶ X
g : X ⟶ Y
h : Y ⟶ Z
f' : W ⟶ X'
g' : X' ⟶ Y'
h' : Y' ⟶ Z
⊢ f ≫ g ≫ h ≫ e.unit.app Z = f' ≫ g' ≫ h' ≫ e.unit.app Z ↔ f ≫ g ≫ h = f' ≫ g' ≫ h'

Tactic:
simp only [← Category.assoc, cancel_mono]

Result:
no goals
-- Mathlib/FieldTheory/Separable.lean
theorem isSeparable_algebraMap (x : F) : IsSeparable F (algebraMap F K x) :=
  Polynomial.Separable.of_dvd (Polynomial.separable_X_sub_C (x := x))
    (minpoly.dvd F (algebraMap F K x) (by simp only [map_sub, aeval_X, aeval_C, sub_self]))

Proof state:
F : Type u_1
inst✝² : Field F
K : Type u_2
inst✝¹ : Ring K
inst✝ : Algebra F K
x : F
⊢ (aeval ((algebraMap F K) x)) (X - C x) = 0

Tactic:
simp only [map_sub, aeval_X, aeval_C, sub_self]

Result:
no goals
-- Mathlib/Order/Filter/Basic.lean
lemma compl_mem_comk {p : Set α → Prop} {he hmono hunion s} :
    sᶜ ∈ comk p he hmono hunion ↔ p s

Proof state:
α : Type u_1
p : Set α → Prop
he : p ∅
hmono : ∀ (t : Set α), p t → ∀ s ⊆ t, p s
hunion : ∀ (s : Set α), p s → ∀ (t : Set α), p t → p (s ∪ t)
s : Set α
⊢ sᶜ ∈ comk p he hmono hunion ↔ p s

Tactic:
simp

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Trigonometric/Angle.lean
theorem cos_add_pi_div_two (θ : Angle) : cos (θ + ↑(π / 2)) = -sin θ

Proof state:
case h
x✝ : ℝ
⊢ (↑x✝ + ↑(π / 2)).cos = -(↑x✝).sin

Tactic:
exact Real.cos_add_pi_div_two _

Result:
no goals

Proof state:
θ : Angle
⊢ (θ + ↑(π / 2)).cos = -θ.sin

Tactic:
induction θ using Real.Angle.induction_on

Result:
case h
x✝ : ℝ
⊢ (↑x✝ + ↑(π / 2)).cos = -(↑x✝).sin
-- Mathlib/Topology/UniformSpace/Equiv.lean
theorem range_coe (h : α ≃ᵤ β) : range h = univ

Proof state:
α : Type u
β : Type u_1
inst✝¹ : UniformSpace α
inst✝ : UniformSpace β
h : α ≃ᵤ β
⊢ range ⇑h = univ

Tactic:
simp

Result:
no goals
-- Mathlib/AlgebraicGeometry/EllipticCurve/DivisionPolynomial/Basic.lean
@[simp]
lemma Φ_neg (n : ℤ) : W.Φ (-n) = W.Φ n

Proof state:
R : Type r
inst✝ : CommRing R
W : WeierstrassCurve R
n : ℤ
⊢ W.Φ (-n) = W.Φ n

Tactic:
simp only [Φ, ΨSq_neg, neg_add_eq_sub, ← neg_sub n, preΨ_neg, ← neg_add', preΨ_neg, neg_mul_neg,
  mul_comm <| W.preΨ <| n - 1, even_neg]

Result:
no goals
-- Mathlib/NumberTheory/Padics/PadicNumbers.lean
theorem addValuation.apply {x : ℚ_[p]} (hx : x ≠ 0) :
    Padic.addValuation x = (x.valuation : WithTop ℤ)

Proof state:
p : ℕ
hp : Fact (Nat.Prime p)
x : ℚ_[p]
hx : x ≠ 0
⊢ addValuation x = ↑x.valuation

Tactic:
simp only [Padic.addValuation, AddValuation.of_apply, addValuationDef, if_neg hx]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Trigonometric/Angle.lean
theorem toReal_neg_pi_div_two : ((-π / 2 : ℝ) : Angle).toReal = -π / 2 :=
  toReal_coe_eq_self_iff.2 <| by constructor <;> linarith [pi_pos]

Proof state:
⊢ -π < -π / 2 ∧ -π / 2 ≤ π

Tactic:
constructor <;> linarith [pi_pos]

Result:
no goals
-- Mathlib/Data/Int/Log.lean
theorem log_zero_left (r : R) : log 0 r = 0

Proof state:
R : Type u_1
inst✝¹ : LinearOrderedSemifield R
inst✝ : FloorSemiring R
r : R
⊢ log 0 r = 0

Tactic:
simp only [log, Nat.log_zero_left, Nat.cast_zero, Nat.clog_zero_left, neg_zero, ite_self]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Log/Base.lean
theorem logb_mul (hx : x ≠ 0) (hy : y ≠ 0) : logb b (x * y) = logb b x + logb b y

Proof state:
b x y : ℝ
hx : x ≠ 0
hy : y ≠ 0
⊢ logb b (x * y) = logb b x + logb b y

Tactic:
simp_rw [logb, log_mul hx hy, add_div]

Result:
no goals
-- Mathlib/Data/Matrix/PEquiv.lean
theorem mul_toMatrix_toPEquiv [Fintype m] [DecidableEq n]
    [Semiring α] (M : Matrix l m α) (f : m ≃ n) :
    (M * f.toPEquiv.toMatrix) = M.submatrix id f.symm :=
  Matrix.ext fun i j => by
    rw [PEquiv.mul_toMatrix_apply, ← Equiv.toPEquiv_symm, Equiv.toPEquiv_apply,
      Matrix.submatrix_apply, id]

Proof state:
l : Type u_2
m : Type u_3
n : Type u_4
α : Type u_5
inst✝² : Fintype m
inst✝¹ : DecidableEq n
inst✝ : Semiring α
M : Matrix l m α
f : m ≃ n
i : l
j : n
⊢ (M * f.toPEquiv.toMatrix) i j = M.submatrix id (⇑f.symm) i j

Tactic:
rw [PEquiv.mul_toMatrix_apply, ← Equiv.toPEquiv_symm, Equiv.toPEquiv_apply,
  Matrix.submatrix_apply, id]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/RawLemmas.lean
theorem getKey?_erase_self [EquivBEq α] [LawfulHashable α] (h : m.WF) {k : α} :
    (m.erase k).getKey? k = none

Proof state:
α : Type u
β : α → Type v
m : Raw α β
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
h : m.WF
k : α
⊢ (m.erase k).getKey? k = none

Tactic:
simp_to_raw using Raw₀.getKey?_erase_self

Result:
no goals
-- Mathlib/Algebra/BigOperators/Intervals.lean
@[to_additive]
lemma mul_prod_Ioc_eq_prod_Icc (h : a ≤ b) : f a * ∏ x ∈ Ioc a b, f x = ∏ x ∈ Icc a b, f x

Proof state:
α : Type u_1
M : Type u_2
inst✝² : PartialOrder α
inst✝¹ : CommMonoid M
f : α → M
a b : α
inst✝ : LocallyFiniteOrder α
h : a ≤ b
⊢ f a * ∏ x ∈ Ioc a b, f x = ∏ x ∈ Icc a b, f x

Tactic:
rw [Icc_eq_cons_Ioc h, prod_cons]

Result:
no goals
-- Mathlib/Data/Vector3.lean
theorem append_add :
    ∀ {m} (v : Vector3 α m) {n} (w : Vector3 α n) (i : Fin2 n), (v +-+ w) (add i m) = w i
  | 0, _, _, _, _ => rfl
  | m + 1, v, n, w, i => v.consElim fun _a t => by simp [append_add, add]

Proof state:
α : Type u_1
m : ℕ
v : Vector3 α (m + 1)
n : ℕ
w : Vector3 α n
i : Fin2 n
_a : α
t : Vector3 α m
⊢ ((_a :: t) +-+ w) (i.add (m + 1)) = w i

Tactic:
simp [append_add, add]

Result:
no goals
-- Mathlib/Logic/Relation.lean
@[simp] lemma reflTransGen_reflGen : ReflTransGen (ReflGen r) = ReflTransGen r

Proof state:
α : Type u_1
r : α → α → Prop
⊢ ReflTransGen (ReflGen r) = ReflTransGen r

Tactic:
simp only [← transGen_reflGen, reflGen_eq_self reflexive_reflGen]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Sum/Lemmas.lean
theorem isLeft_iff : x.isLeft ↔ ∃ y, x = Sum.inl y

Proof state:
α✝ : Type u_1
β✝ : Type u_2
x : α✝ ⊕ β✝
⊢ x.isLeft = true ↔ ∃ y, x = inl y

Tactic:
cases x <;> simp

Result:
no goals
-- Mathlib/Analysis/Calculus/VectorField.lean
theorem _root_.Filter.EventuallyEq.lieBracketWithin_vectorField_eq_of_insert
    (hV : V₁ =ᶠ[𝓝[insert x s] x] V) (hW : W₁ =ᶠ[𝓝[insert x s] x] W) :
    lieBracketWithin 𝕜 V₁ W₁ s x = lieBracketWithin 𝕜 V W s x

Proof state:
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
V W V₁ W₁ : E → E
s : Set E
x : E
hV : V₁ =ᶠ[𝓝[insert x s] x] V
hW : W₁ =ᶠ[𝓝[insert x s] x] W
⊢ lieBracketWithin 𝕜 V₁ W₁ s x = lieBracketWithin 𝕜 V W s x

Tactic:
apply mem_of_mem_nhdsWithin (mem_insert x s) (hV.lieBracketWithin_vectorField' hW
  (subset_insert x s))

Result:
no goals
-- Mathlib/Data/Fin/Basic.lean
theorem castpred_succ_le_iff {a b : Fin (n + 1)} (ha : succ a ≠ last (n + 1)) :
    (succ a).castPred ha ≤ b ↔ a < b

Proof state:
n : ℕ
a b : Fin (n + 1)
ha : a.succ ≠ last (n + 1)
⊢ a.succ.castPred ha ≤ b ↔ a < b

Tactic:
rw [castPred_le_iff, succ_le_castSucc_iff]

Result:
no goals
-- Mathlib/AlgebraicGeometry/EllipticCurve/NormalForms.lean
theorem toCharThreeNF_spec_of_b₂_eq_zero (hb₂ : W.b₂ = 0) :
    (W.variableChange W.toCharThreeNF).IsShortNF

Proof state:
F : Type u_2
inst✝¹ : Field F
inst✝ : CharP F 3
W : WeierstrassCurve F
hb₂ : W.b₂ = 0
⊢ (W.variableChange W.toCharThreeNF).IsShortNF

Tactic:
rw [toCharThreeNF, toShortNFOfCharThree_a₂, hb₂, div_zero, ← VariableChange.id,
  VariableChange.id_comp]

Result:
F : Type u_2
inst✝¹ : Field F
inst✝ : CharP F 3
W : WeierstrassCurve F
hb₂ : W.b₂ = 0
⊢ (W.variableChange W.toShortNFOfCharThree).IsShortNF

Proof state:
F : Type u_2
inst✝¹ : Field F
inst✝ : CharP F 3
W : WeierstrassCurve F
hb₂ : W.b₂ = 0
⊢ (W.variableChange W.toShortNFOfCharThree).IsShortNF

Tactic:
exact W.toShortNFOfCharThree_spec hb₂

Result:
no goals
-- Mathlib/NumberTheory/MulChar/Lemmas.lean
/-- The values of a multiplicative character on `R` are `n`th roots of unity, where `n = #Rˣ`. -/
lemma apply_mem_rootsOfUnity [Fintype Rˣ] (a : Rˣ) {χ : MulChar R R'} :
    equivToUnitHom χ a ∈ rootsOfUnity (Fintype.card Rˣ) R'

Proof state:
R : Type u_1
R' : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing R'
inst✝ : Fintype Rˣ
a : Rˣ
χ : MulChar R R'
⊢ (equivToUnitHom χ) a ∈ rootsOfUnity (Fintype.card Rˣ) R'

Tactic:
rw [mem_rootsOfUnity, ← map_pow, ← (equivToUnitHom χ).map_one, pow_card_eq_one]

Result:
no goals
-- Mathlib/Analysis/RCLike/Basic.lean
theorem norm_conj (z : K) : ‖conj z‖ = ‖z‖

Proof state:
K : Type u_1
inst✝ : RCLike K
z : K
⊢ ‖(starRingEnd K) z‖ = ‖z‖

Tactic:
simp only [← sqrt_normSq_eq_norm, normSq_conj]

Result:
no goals
-- Mathlib/Order/Interval/Finset/Basic.lean
theorem Ioi_insert [DecidableEq α] (a : α) : insert a (Ioi a) = Ici a

Proof state:
α : Type u_2
inst✝² : PartialOrder α
inst✝¹ : LocallyFiniteOrderTop α
inst✝ : DecidableEq α
a : α
⊢ insert a (Ioi a) = Ici a

Tactic:
ext

Result:
case h
α : Type u_2
inst✝² : PartialOrder α
inst✝¹ : LocallyFiniteOrderTop α
inst✝ : DecidableEq α
a a✝ : α
⊢ a✝ ∈ insert a (Ioi a) ↔ a✝ ∈ Ici a

Proof state:
case h
α : Type u_2
inst✝² : PartialOrder α
inst✝¹ : LocallyFiniteOrderTop α
inst✝ : DecidableEq α
a a✝ : α
⊢ a✝ ∈ insert a (Ioi a) ↔ a✝ ∈ Ici a

Tactic:
simp_rw [Finset.mem_insert, mem_Ici, mem_Ioi, le_iff_lt_or_eq, or_comm, eq_comm]

Result:
no goals
-- Mathlib/Data/Matrix/Notation.lean
theorem cons_val' (v : n' → α) (B : Fin m → n' → α) (i j) :
    vecCons v B i j = vecCons (v j) (fun i => B i j) i

Proof state:
α : Type u
m : ℕ
n' : Type uₙ
v : n' → α
B : Fin m → n' → α
i : Fin m.succ
j : n'
⊢ vecCons v B i j = vecCons (v j) (fun i => B i j) i

Tactic:
refine Fin.cases ?_ ?_ i <;> simp

Result:
no goals
-- Mathlib/CategoryTheory/Limits/Preserves/Shapes/Equalizers.lean
theorem map_π_preserves_coequalizer_inv_colimMap_desc {X' Y' : D} (f' g' : X' ⟶ Y')
    [HasCoequalizer f' g'] (p : G.obj X ⟶ X') (q : G.obj Y ⟶ Y') (wf : G.map f ≫ q = p ≫ f')
    (wg : G.map g ≫ q = p ≫ g') {Z' : D} (h : Y' ⟶ Z') (wh : f' ≫ h = g' ≫ h) :
    G.map (coequalizer.π f g) ≫
        (PreservesCoequalizer.iso G f g).inv ≫
          colimMap (parallelPairHom (G.map f) (G.map g) f' g' p q wf wg) ≫ coequalizer.desc h wh =
      q ≫ h

Proof state:
C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
G : C ⥤ D
X Y : C
f g : X ⟶ Y
inst✝³ : HasCoequalizer f g
inst✝² : HasCoequalizer (G.map f) (G.map g)
inst✝¹ : PreservesColimit (parallelPair f g) G
X' Y' : D
f' g' : X' ⟶ Y'
inst✝ : HasCoequalizer f' g'
p : G.obj X ⟶ X'
q : G.obj Y ⟶ Y'
wf : G.map f ≫ q = p ≫ f'
wg : G.map g ≫ q = p ≫ g'
Z' : D
h : Y' ⟶ Z'
wh : f' ≫ h = g' ≫ h
⊢ (q ≫ coequalizer.π f' g') ≫ coequalizer.desc h wh = q ≫ h

Tactic:
slice_lhs 2 3 => rw [coequalizer.π_desc]

Result:
no goals

Proof state:
C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
G : C ⥤ D
X Y : C
f g : X ⟶ Y
inst✝³ : HasCoequalizer f g
inst✝² : HasCoequalizer (G.map f) (G.map g)
inst✝¹ : PreservesColimit (parallelPair f g) G
X' Y' : D
f' g' : X' ⟶ Y'
inst✝ : HasCoequalizer f' g'
p : G.obj X ⟶ X'
q : G.obj Y ⟶ Y'
wf : G.map f ≫ q = p ≫ f'
wg : G.map g ≫ q = p ≫ g'
Z' : D
h : Y' ⟶ Z'
wh : f' ≫ h = g' ≫ h
⊢ G.map (coequalizer.π f g) ≫
      (PreservesCoequalizer.iso G f g).inv ≫
        colimMap (parallelPairHom (G.map f) (G.map g) f' g' p q wf wg) ≫ coequalizer.desc h wh =
    q ≫ h

Tactic:
slice_lhs 1 3 => rw [map_π_preserves_coequalizer_inv_colimMap]

Result:
C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
G : C ⥤ D
X Y : C
f g : X ⟶ Y
inst✝³ : HasCoequalizer f g
inst✝² : HasCoequalizer (G.map f) (G.map g)
inst✝¹ : PreservesColimit (parallelPair f g) G
X' Y' : D
f' g' : X' ⟶ Y'
inst✝ : HasCoequalizer f' g'
p : G.obj X ⟶ X'
q : G.obj Y ⟶ Y'
wf : G.map f ≫ q = p ≫ f'
wg : G.map g ≫ q = p ≫ g'
Z' : D
h : Y' ⟶ Z'
wh : f' ≫ h = g' ≫ h
⊢ (q ≫ coequalizer.π f' g') ≫ coequalizer.desc h wh = q ≫ h
-- Mathlib/Combinatorics/Colex.lean
@[simp] lemma toColex_sdiff_le_toColex_sdiff' :
    toColex (s \ t) ≤ toColex (t \ s) ↔ toColex s ≤ toColex t

Proof state:
α : Type u_1
inst✝¹ : PartialOrder α
s t : Finset α
inst✝ : DecidableEq α
⊢ { ofColex := s \ t } ≤ { ofColex := t \ s } ↔ { ofColex := s } ≤ { ofColex := t }

Tactic:
simpa using toColex_sdiff_le_toColex_sdiff (inter_subset_left (s₁ := s)) inter_subset_right

Result:
no goals
-- Mathlib/Algebra/GCDMonoid/Basic.lean
theorem coe_normUnit {a : G₀} (h0 : a ≠ 0) : (↑(normUnit a) : G₀) = a⁻¹

Proof state:
G₀ : Type u_2
inst✝¹ : CommGroupWithZero G₀
inst✝ : DecidableEq G₀
a : G₀
h0 : a ≠ 0
⊢ ↑(normUnit a) = a⁻¹

Tactic:
simp [normUnit, h0]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Tactic/BVDecide/LRAT/Internal/Assignment.lean
theorem not_hasNeg_removeNeg (assignment : Assignment) :
    ¬hasNegAssignment (removeNegAssignment assignment)

Proof state:
assignment : Assignment
⊢ ¬assignment.removeNegAssignment.hasNegAssignment = true

Tactic:
cases assignment <;> simp [removeNegAssignment, hasNegAssignment]

Result:
no goals
-- Mathlib/Data/Finsupp/MonomialOrder/DegLex.lean
theorem degLex_single_le_iff {a b : σ} :
    single a 1 ≼[degLex] single b 1 ↔ b ≤ a

Proof state:
σ : Type u_2
inst✝¹ : LinearOrder σ
inst✝ : WellFoundedGT σ
a b : σ
⊢ degLex.toSyn (single a 1) ≤ degLex.toSyn (single b 1) ↔ b ≤ a

Tactic:
rw [MonomialOrder.degLex_le_iff, DegLex.single_le_iff]

Result:
no goals
-- Mathlib/Tactic/Module.lean
theorem neg_eq_eval [AddCommGroup M] [Semiring S] [Module S M] [Ring R] [Module R M] {l : NF R M}
    {l₀ : NF S M} (hl : l.eval = l₀.eval) {x : M} (h : x = l₀.eval) :
    - x = (-l).eval

Proof state:
S : Type u_1
R : Type u_2
M : Type u_3
inst✝⁴ : AddCommGroup M
inst✝³ : Semiring S
inst✝² : Module S M
inst✝¹ : Ring R
inst✝ : Module R M
l : NF R M
l₀ : NF S M
hl : l.eval = l₀.eval
x : M
h : x = l₀.eval
⊢ -x = (-l).eval

Tactic:
rw [h, ← hl, eval_neg]

Result:
no goals
-- Mathlib/Order/Filter/AtTopBot/Basic.lean
theorem eventually_atBot_prod_self'  [Nonempty α] [Preorder α] [IsDirected α (· ≥ ·)]
    {p : α × α → Prop} : (∀ᶠ x in atBot, p x) ↔ ∃ a, ∀ k ≤ a, ∀ l ≤ a, p (k, l)

Proof state:
α : Type u_3
inst✝² : Nonempty α
inst✝¹ : Preorder α
inst✝ : IsDirected α fun x1 x2 => x1 ≥ x2
p : α × α → Prop
⊢ (∀ᶠ (x : α × α) in atBot, p x) ↔ ∃ a, ∀ k ≤ a, ∀ l ≤ a, p (k, l)

Tactic:
simp only [eventually_atBot_prod_self, forall_cond_comm]

Result:
no goals
-- Mathlib/Data/Sym/Sym2.lean
theorem eq_iff {x y z w : α} : s(x, y) = s(z, w) ↔ x = z ∧ y = w ∨ x = w ∧ y = z

Proof state:
α : Type u_1
x y z w : α
⊢ s(x, y) = s(z, w) ↔ x = z ∧ y = w ∨ x = w ∧ y = z

Tactic:
simp

Result:
no goals
-- Mathlib/Algebra/RingQuot.lean
theorem eq_lift_comp_mkRingHom {r : R → R → Prop} (f : RingQuot r →+* T) :
    f = lift ⟨f.comp (mkRingHom r), fun _ _ h ↦ congr_arg f (mkRingHom_rel h)⟩

Proof state:
R : Type uR
inst✝¹ : Semiring R
T : Type uT
inst✝ : Semiring T
r : R → R → Prop
f : RingQuot r →+* T
⊢ { toFun := fun f => preLift ⋯, invFun := fun F => ⟨F.comp (mkRingHom r), ⋯⟩, left_inv := ⋯, right_inv := ⋯ }
      ({ toFun := fun f => preLift ⋯, invFun := fun F => ⟨F.comp (mkRingHom r), ⋯⟩, left_inv := ⋯, right_inv := ⋯ }.symm
        f) =
    { toFun := fun f => preLift ⋯, invFun := fun F => ⟨F.comp (mkRingHom r), ⋯⟩, left_inv := ⋯, right_inv := ⋯ }
      ⟨f.comp (mkRingHom r), ⋯⟩

Tactic:
rfl

Result:
no goals

Proof state:
R : Type uR
inst✝¹ : Semiring R
T : Type uT
inst✝ : Semiring T
r : R → R → Prop
f : RingQuot r →+* T
⊢ f = lift ⟨f.comp (mkRingHom r), ⋯⟩

Tactic:
conv_lhs => rw [← lift.apply_symm_apply f]

Result:
R : Type uR
inst✝¹ : Semiring R
T : Type uT
inst✝ : Semiring T
r : R → R → Prop
f : RingQuot r →+* T
⊢ lift (lift.symm f) = lift ⟨f.comp (mkRingHom r), ⋯⟩

Proof state:
R : Type uR
inst✝¹ : Semiring R
T : Type uT
inst✝ : Semiring T
r : R → R → Prop
f : RingQuot r →+* T
⊢ lift (lift.symm f) = lift ⟨f.comp (mkRingHom r), ⋯⟩

Tactic:
rw [lift_def]

Result:
R : Type uR
inst✝¹ : Semiring R
T : Type uT
inst✝ : Semiring T
r : R → R → Prop
f : RingQuot r →+* T
⊢ { toFun := fun f => preLift ⋯, invFun := fun F => ⟨F.comp (mkRingHom r), ⋯⟩, left_inv := ⋯, right_inv := ⋯ }
      ({ toFun := fun f => preLift ⋯, invFun := fun F => ⟨F.comp (mkRingHom r), ⋯⟩, left_inv := ⋯, right_inv := ⋯ }.symm
        f) =
    { toFun := fun f => preLift ⋯, invFun := fun F => ⟨F.comp (mkRingHom r), ⋯⟩, left_inv := ⋯, right_inv := ⋯ }
      ⟨f.comp (mkRingHom r), ⋯⟩
-- Mathlib/RingTheory/Invariant.lean
theorem smul_coeff_charpoly (b : B) (n : ℕ) (g : G) :
    g • (charpoly G b).coeff n = (charpoly G b).coeff n

Proof state:
B : Type u_2
G : Type u_3
inst✝³ : CommRing B
inst✝² : Group G
inst✝¹ : MulSemiringAction G B
inst✝ : Fintype G
b : B
n : ℕ
g : G
⊢ g • (charpoly G b).coeff n = (charpoly G b).coeff n

Tactic:
rw [← coeff_smul, smul_charpoly]

Result:
no goals
-- Mathlib/CategoryTheory/Localization/HomEquiv.lean
@[simp]
lemma id_homMap (f : L₁.obj X ⟶ L₁.obj Y) :
    (id W₁).homMap L₁ L₁ f = f

Proof state:
C₁ : Type u_2
D₁ : Type u_5
inst✝² : Category.{u_9, u_2} C₁
inst✝¹ : Category.{u_8, u_5} D₁
W₁ : MorphismProperty C₁
L₁ : C₁ ⥤ D₁
inst✝ : L₁.IsLocalization W₁
X Y : C₁
f : L₁.obj X ⟶ L₁.obj Y
⊢ (id W₁).homMap L₁ L₁ f = f

Tactic:
simpa using (id W₁).homMap_apply L₁ L₁ (𝟭 D₁) (Iso.refl _) f

Result:
no goals
-- Mathlib/Data/List/DropRight.lean
theorem rtakeWhile_concat_neg (x : α) (h : ¬p x) : rtakeWhile p (l ++ [x]) = []

Proof state:
α : Type u_1
p : α → Bool
l : List α
x : α
h : ¬p x = true
⊢ rtakeWhile p (l ++ [x]) = []

Tactic:
rw [rtakeWhile_concat, if_neg h]

Result:
no goals
-- Mathlib/Topology/Basic.lean
theorem frontier_union_subset (s t : Set X) :
    frontier (s ∪ t) ⊆ frontier s ∩ closure tᶜ ∪ closure sᶜ ∩ frontier t

Proof state:
X : Type u
inst✝ : TopologicalSpace X
s t : Set X
⊢ frontier (s ∪ t) ⊆ frontier s ∩ closure tᶜ ∪ closure sᶜ ∩ frontier t

Tactic:
simpa only [frontier_compl, ← compl_union] using frontier_inter_subset sᶜ tᶜ

Result:
no goals
-- Mathlib/Data/Set/Card.lean
lemma even_card_insert_iff {a : α} (ha : a ∉ s) (hs : s.Finite

Proof state:
α : Type u_1
s : Set α
a : α
ha : a ∉ s
hs : autoParam s.Finite _auto✝
⊢ Even (insert a s).ncard ↔ Odd s.ncard

Tactic:
rw [ncard_insert_of_not_mem ha hs, Nat.even_add_one, Nat.not_even_iff_odd]

Result:
no goals
-- Mathlib/GroupTheory/Perm/Option.lean
theorem Equiv.Perm.decomposeOption_symm_of_none_apply {α : Type*} [DecidableEq α] (e : Perm α)
    (i : Option α) : Equiv.Perm.decomposeOption.symm (none, e) i = i.map e

Proof state:
α : Type u_1
inst✝ : DecidableEq α
e : Perm α
i : Option α
⊢ (decomposeOption.symm (none, e)) i = Option.map (⇑e) i

Tactic:
simp

Result:
no goals
-- Mathlib/LinearAlgebra/TensorProduct/Pi.lean
@[simp]
lemma piScalarRight_symm_single (x : N) (i : ι) :
    (piScalarRight R S N ι).symm (Pi.single i x) = x ⊗ₜ Pi.single i 1

Proof state:
R : Type u_1
inst✝⁸ : CommSemiring R
S : Type u_2
inst✝⁷ : CommSemiring S
inst✝⁶ : Algebra R S
N : Type u_3
inst✝⁵ : AddCommMonoid N
inst✝⁴ : Module R N
inst✝³ : Module S N
inst✝² : IsScalarTower R S N
ι : Type u_4
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
x : N
i : ι
⊢ (piScalarRight R S N ι).symm (Pi.single i x) = x ⊗ₜ[R] Pi.single i 1

Tactic:
simp [piScalarRight]

Result:
no goals
-- Mathlib/Data/Part.lean
theorem mod_mem_mod [Mod α] (a b : Part α) (ma mb : α) (ha : ma ∈ a) (hb : mb ∈ b) :
    ma % mb ∈ a % b

Proof state:
α : Type u_1
inst✝ : Mod α
a b : Part α
ma mb : α
ha : ma ∈ a
hb : mb ∈ b
⊢ ∃ a_1 ∈ a, ∃ a ∈ b, a_1 % a = ma % mb

Tactic:
aesop

Result:
no goals

Proof state:
α : Type u_1
inst✝ : Mod α
a b : Part α
ma mb : α
ha : ma ∈ a
hb : mb ∈ b
⊢ ma % mb ∈ a % b

Tactic:
simp [mod_def]

Result:
α : Type u_1
inst✝ : Mod α
a b : Part α
ma mb : α
ha : ma ∈ a
hb : mb ∈ b
⊢ ∃ a_1 ∈ a, ∃ a ∈ b, a_1 % a = ma % mb
-- Mathlib/Algebra/Order/ToIntervalMod.lean
theorem toIcoMod_sub' (a b : α) : toIcoMod hp (a - p) b = toIcoMod hp a b - p

Proof state:
α : Type u_1
inst✝ : LinearOrderedAddCommGroup α
hα : Archimedean α
p : α
hp : 0 < p
a b : α
⊢ toIcoMod hp (a - p) b = toIcoMod hp a b - p

Tactic:
simpa only [one_zsmul] using toIcoMod_sub_zsmul' hp a b 1

Result:
no goals
-- Mathlib/CategoryTheory/Limits/Preserves/FunctorCategory.lean
theorem whiskerRight_ι_colimitCompWhiskeringRightIsoColimitComp_inv {C : Type*} [Category C]
    {D : Type*} [Category D] {E : Type*} [Category E] {J : Type*} [Category J]
    [HasColimitsOfShape J D] (F : D ⥤ E) [PreservesColimitsOfShape J F] (G : J ⥤ C ⥤ D) (j : J) :
    whiskerRight (colimit.ι G j) F ≫ (colimitCompWhiskeringRightIsoColimitComp F G).inv =
      colimit.ι (G ⋙ (whiskeringRight _ _ _).obj F) j

Proof state:
C : Type u_1
inst✝⁵ : Category.{u_5, u_1} C
D : Type u_2
inst✝⁴ : Category.{u_6, u_2} D
E : Type u_3
inst✝³ : Category.{u_7, u_3} E
J : Type u_4
inst✝² : Category.{u_8, u_4} J
inst✝¹ : HasColimitsOfShape J D
F : D ⥤ E
inst✝ : PreservesColimitsOfShape J F
G : J ⥤ C ⥤ D
j : J
⊢ whiskerRight (colimit.ι G j) F ≫ (colimitCompWhiskeringRightIsoColimitComp F G).inv =
    colimit.ι (G ⋙ (whiskeringRight C D E).obj F) j

Tactic:
simp [Iso.comp_inv_eq]

Result:
no goals