harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/AlgebraicGeometry/EllipticCurve/Projective.lean
lemma addX_of_X_eq [NoZeroDivisors R] {P Q : Fin 3 → R} (hP : W'.Equation P) (hQ : W'.Equation Q)
    (hPz : P z ≠ 0) (hQz : Q z ≠ 0) (hx : P x * Q z = Q x * P z) : W'.addX P Q = 0

Proof state:
R : Type r
inst✝¹ : CommRing R
W' : Projective R
inst✝ : NoZeroDivisors R
P Q : Fin 3 → R
hP : W'.Equation P
hQ : W'.Equation Q
hPz : P z ≠ 0
hQz : Q z ≠ 0
hx : P x * Q z = Q x * P z
⊢ ((P y * Q z - Q y * P z) ^ 2 * P z * Q z + W'.a₁ * (P y * Q z - Q y * P z) * P z * Q z * (Q x * P z - Q x * P z) -
            W'.a₂ * P z * Q z * (Q x * P z - Q x * P z) ^ 2 -
          Q x * P z * (Q x * P z - Q x * P z) ^ 2 -
        Q x * P z * (Q x * P z - Q x * P z) ^ 2) *
      (Q x * P z - Q x * P z) =
    0

Tactic:
ring1

Result:
no goals

Proof state:
R : Type r
inst✝¹ : CommRing R
W' : Projective R
inst✝ : NoZeroDivisors R
P Q : Fin 3 → R
hP : W'.Equation P
hQ : W'.Equation Q
hPz : P z ≠ 0
hQz : Q z ≠ 0
hx : P x * Q z = Q x * P z
⊢ W'.addX P Q * (P z * Q z) ^ 2 = 0

Tactic:
rw [addX_eq' hP hQ, hx]

Result:
R : Type r
inst✝¹ : CommRing R
W' : Projective R
inst✝ : NoZeroDivisors R
P Q : Fin 3 → R
hP : W'.Equation P
hQ : W'.Equation Q
hPz : P z ≠ 0
hQz : Q z ≠ 0
hx : P x * Q z = Q x * P z
⊢ ((P y * Q z - Q y * P z) ^ 2 * P z * Q z + W'.a₁ * (P y * Q z - Q y * P z) * P z * Q z * (Q x * P z - Q x * P z) -
            W'.a₂ * P z * Q z * (Q x * P z - Q x * P z) ^ 2 -
          Q x * P z * (Q x * P z - Q x * P z) ^ 2 -
        Q x * P z * (Q x * P z - Q x * P z) ^ 2) *
      (Q x * P z - Q x * P z) =
    0

Proof state:
R : Type r
inst✝¹ : CommRing R
W' : Projective R
inst✝ : NoZeroDivisors R
P Q : Fin 3 → R
hP : W'.Equation P
hQ : W'.Equation Q
hPz : P z ≠ 0
hQz : Q z ≠ 0
hx : P x * Q z = Q x * P z
⊢ W'.addX P Q = 0

Tactic:
apply eq_zero_of_ne_zero_of_mul_right_eq_zero <| pow_ne_zero 2 <| mul_ne_zero hPz hQz

Result:
R : Type r
inst✝¹ : CommRing R
W' : Projective R
inst✝ : NoZeroDivisors R
P Q : Fin 3 → R
hP : W'.Equation P
hQ : W'.Equation Q
hPz : P z ≠ 0
hQz : Q z ≠ 0
hx : P x * Q z = Q x * P z
⊢ W'.addX P Q * (P z * Q z) ^ 2 = 0
-- Mathlib/Algebra/Field/Periodic.lean
theorem Antiperiodic.nat_mul_sub_eq [Ring α] [Ring β] (h : Antiperiodic f c) (n : ℕ) :
    f (n * c - x) = (-1) ^ n * f (-x)

Proof state:
α : Type u_1
β : Type u_2
f : α → β
c x : α
inst✝¹ : Ring α
inst✝ : Ring β
h : Antiperiodic f c
n : ℕ
⊢ f (↑n * c - x) = (-1) ^ n * f (-x)

Tactic:
simpa only [nsmul_eq_mul, zsmul_eq_mul, Int.cast_pow, Int.cast_neg,
  Int.cast_one] using h.nsmul_sub_eq n

Result:
no goals
-- Mathlib/Data/Set/Sigma.lean
theorem sigma_inter_sigma : s₁.sigma t₁ ∩ s₂.sigma t₂ = (s₁ ∩ s₂).sigma fun i ↦ t₁ i ∩ t₂ i

Proof state:
ι : Type u_1
α : ι → Type u_3
s₁ s₂ : Set ι
t₁ t₂ : (i : ι) → Set (α i)
⊢ s₁.sigma t₁ ∩ s₂.sigma t₂ = (s₁ ∩ s₂).sigma fun i => t₁ i ∩ t₂ i

Tactic:
ext ⟨x, y⟩

Result:
case h.mk
ι : Type u_1
α : ι → Type u_3
s₁ s₂ : Set ι
t₁ t₂ : (i : ι) → Set (α i)
x : ι
y : α x
⊢ ⟨x, y⟩ ∈ s₁.sigma t₁ ∩ s₂.sigma t₂ ↔ ⟨x, y⟩ ∈ (s₁ ∩ s₂).sigma fun i => t₁ i ∩ t₂ i

Proof state:
case h.mk
ι : Type u_1
α : ι → Type u_3
s₁ s₂ : Set ι
t₁ t₂ : (i : ι) → Set (α i)
x : ι
y : α x
⊢ ⟨x, y⟩ ∈ s₁.sigma t₁ ∩ s₂.sigma t₂ ↔ ⟨x, y⟩ ∈ (s₁ ∩ s₂).sigma fun i => t₁ i ∩ t₂ i

Tactic:
simp [and_assoc, and_left_comm]

Result:
no goals
-- Mathlib/Algebra/BigOperators/Finsupp.lean
theorem prod_ite_eq' [DecidableEq α] (f : α →₀ M) (a : α) (b : α → M → N) :
    (f.prod fun x v => ite (x = a) (b x v) 1) = ite (a ∈ f.support) (b a (f a)) 1

Proof state:
α : Type u_1
M : Type u_8
N : Type u_10
inst✝² : Zero M
inst✝¹ : CommMonoid N
inst✝ : DecidableEq α
f : α →₀ M
a : α
b : α → M → N
⊢ (f.prod fun x v => if x = a then b x v else 1) = if a ∈ f.support then b a (f a) else 1

Tactic:
dsimp [Finsupp.prod]

Result:
α : Type u_1
M : Type u_8
N : Type u_10
inst✝² : Zero M
inst✝¹ : CommMonoid N
inst✝ : DecidableEq α
f : α →₀ M
a : α
b : α → M → N
⊢ (∏ a_1 ∈ f.support, if a_1 = a then b a_1 (f a_1) else 1) = if a ∈ f.support then b a (f a) else 1

Proof state:
α : Type u_1
M : Type u_8
N : Type u_10
inst✝² : Zero M
inst✝¹ : CommMonoid N
inst✝ : DecidableEq α
f : α →₀ M
a : α
b : α → M → N
⊢ (∏ a_1 ∈ f.support, if a_1 = a then b a_1 (f a_1) else 1) = if a ∈ f.support then b a (f a) else 1

Tactic:
rw [f.support.prod_ite_eq']

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Int/Order.lean
theorem natAbs_sign_of_nonzero {z : Int} (hz : z ≠ 0) : z.sign.natAbs = 1

Proof state:
z : Int
hz : z ≠ 0
⊢ z.sign.natAbs = 1

Tactic:
rw [Int.natAbs_sign, if_neg hz]

Result:
no goals
-- Mathlib/RingTheory/Kaehler/CotangentComplex.lean
@[simp]
lemma cotangentSpaceBasis_repr_tmul (r x i) :
    P.cotangentSpaceBasis.repr (r ⊗ₜ[P.Ring] KaehlerDifferential.D R P.Ring x : _) i =
      r * aeval P.val (pderiv i x)

Proof state:
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
P : Generators R S
r : S
x : P.Ring
i : P.vars
⊢ (P.cotangentSpaceBasis.repr (r ⊗ₜ[P.Ring] (D R P.Ring) x)) i = r * (aeval P.val) ((pderiv i) x)

Tactic:
simp only [cotangentSpaceBasis, Basis.baseChange_repr_tmul, mvPolynomialBasis_repr_apply,
  Algebra.smul_def, mul_comm r, algebraMap_apply, toExtension]

Result:
no goals

Proof state:
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
P : Generators R S
r : S
x : P.Ring
i : P.vars
⊢ (P.cotangentSpaceBasis.repr (r ⊗ₜ[P.Ring] (D R P.Ring) x)) i = r * (aeval P.val) ((pderiv i) x)

Tactic:
classical
simp only [cotangentSpaceBasis, Basis.baseChange_repr_tmul, mvPolynomialBasis_repr_apply,
  Algebra.smul_def, mul_comm r, algebraMap_apply, toExtension]

Result:
no goals
-- Mathlib/CategoryTheory/Closed/Monoidal.lean
lemma curry'_ihom_map {X Y Z : C} [Closed X] (f : X ⟶ Y) (g : Y ⟶ Z) :
    curry' f ≫ (ihom X).map g = curry' (f ≫ g)

Proof state:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : MonoidalCategory C
X Y Z : C
inst✝ : Closed X
f : X ⟶ Y
g : Y ⟶ Z
⊢ curry' f ≫ (ihom X).map g = curry' (f ≫ g)

Tactic:
simp only [curry', ← curry_natural_right, Category.assoc]

Result:
no goals
-- Mathlib/LinearAlgebra/Matrix/Transvection.lean
theorem length_listTransvecRow : (listTransvecRow M).length = r

Proof state:
𝕜 : Type u_3
inst✝ : Field 𝕜
r : ℕ
M : Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜
⊢ (listTransvecRow M).length = r

Tactic:
simp [listTransvecRow]

Result:
no goals
-- Mathlib/RingTheory/Polynomial/Basic.lean
theorem span_le_of_C_coeff_mem (cf : ∀ i : ℕ, C (f.coeff i) ∈ I) :
    Ideal.span { g | ∃ i, g = C (f.coeff i) } ≤ I

Proof state:
R : Type u
inst✝ : Semiring R
f : R[X]
I : Ideal R[X]
cf : ∀ (i : ℕ), C (f.coeff i) ∈ I
⊢ Ideal.span {g | ∃ i, g = C (f.coeff i)} ≤ I

Tactic:
simp only [@eq_comm _ _ (C _)]

Result:
R : Type u
inst✝ : Semiring R
f : R[X]
I : Ideal R[X]
cf : ∀ (i : ℕ), C (f.coeff i) ∈ I
⊢ Ideal.span {g | ∃ i, C (f.coeff i) = g} ≤ I

Proof state:
R : Type u
inst✝ : Semiring R
f : R[X]
I : Ideal R[X]
cf : ∀ (i : ℕ), C (f.coeff i) ∈ I
⊢ Ideal.span {g | ∃ i, C (f.coeff i) = g} ≤ I

Tactic:
exact (Ideal.span_le.trans range_subset_iff).mpr cf

Result:
no goals
-- Mathlib/RingTheory/Localization/Defs.lean
theorem smul_mk' (x y : R) (m : M) : x • mk' S y m = mk' S (x * y) m

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
x y : R
m : ↥M
⊢ x • mk' S y m = mk' S (x * y) m

Tactic:
nth_rw 2 [← one_mul m]

Result:
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
x y : R
m : ↥M
⊢ x • mk' S y m = mk' S (x * y) (1 * m)

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
x y : R
m : ↥M
⊢ x • mk' S y m = mk' S (x * y) (1 * m)

Tactic:
rw [mk'_mul, mk'_one, Algebra.smul_def]

Result:
no goals
-- Mathlib/Analysis/Calculus/ContDiff/FTaylorSeries.lean
/-- On a set of unique differentiability, the second derivative is obtained by taking the
derivative of the derivative. -/
lemma iteratedFDerivWithin_two_apply (f : E → F) {z : E} (hs : UniqueDiffOn 𝕜 s) (hz : z ∈ s)
    (m : Fin 2 → E) :
    iteratedFDerivWithin 𝕜 2 f s z m = fderivWithin 𝕜 (fderivWithin 𝕜 f s) s z (m 0) (m 1)

Proof state:
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
s : Set E
f : E → F
z : E
hs : UniqueDiffOn 𝕜 s
hz : z ∈ s
m : Fin 2 → E
⊢ (iteratedFDerivWithin 𝕜 2 f s z) m = ((fderivWithin 𝕜 (fderivWithin 𝕜 f s) s z) (m 0)) (m 1)

Tactic:
simp only [iteratedFDerivWithin_succ_apply_right hs hz]

Result:
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
s : Set E
f : E → F
z : E
hs : UniqueDiffOn 𝕜 s
hz : z ∈ s
m : Fin 2 → E
⊢ (((iteratedFDerivWithin 𝕜 0 (fun y => fderivWithin 𝕜 (fun y => fderivWithin 𝕜 f s y) s y) s z) (init (init m)))
        (init m (last 0)))
      (m (last 1)) =
    ((fderivWithin 𝕜 (fderivWithin 𝕜 f s) s z) (m 0)) (m 1)

Proof state:
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
s : Set E
f : E → F
z : E
hs : UniqueDiffOn 𝕜 s
hz : z ∈ s
m : Fin 2 → E
⊢ (((iteratedFDerivWithin 𝕜 0 (fun y => fderivWithin 𝕜 (fun y => fderivWithin 𝕜 f s y) s y) s z) (init (init m)))
        (init m (last 0)))
      (m (last 1)) =
    ((fderivWithin 𝕜 (fderivWithin 𝕜 f s) s z) (m 0)) (m 1)

Tactic:
rfl

Result:
no goals
-- Mathlib/Data/Real/EReal.lean
private lemma exists_mul_right_lt (h₁ : 0 < a ∨ b ≠ ⊤) (h₂ : a ≠ ⊤ ∨ b ≠ 0) (hc : a * b < c) :
    ∃ b' ∈ Ioo b ⊤, a * b' < c

Proof state:
a b c : EReal
h₁ : 0 < a ∨ b ≠ ⊤
h₂ : a ≠ ⊤ ∨ b ≠ 0
hc : b * a < c
⊢ ∃ b' ∈ Ioo b ⊤, b' * a < c

Tactic:
exact exists_mul_left_lt h₂.symm h₁.symm hc

Result:
no goals

Proof state:
a b c : EReal
h₁ : 0 < a ∨ b ≠ ⊤
h₂ : a ≠ ⊤ ∨ b ≠ 0
hc : a * b < c
⊢ ∃ b' ∈ Ioo b ⊤, a * b' < c

Tactic:
simp_rw [mul_comm a] at hc ⊢

Result:
a b c : EReal
h₁ : 0 < a ∨ b ≠ ⊤
h₂ : a ≠ ⊤ ∨ b ≠ 0
hc : b * a < c
⊢ ∃ b' ∈ Ioo b ⊤, b' * a < c
-- Mathlib/Topology/Category/LightProfinite/AsLimit.lean
lemma surjective_transitionMapLE {n m : ℕ} (h : n ≤ m) :
    Function.Surjective (S.transitionMapLE h)

Proof state:
S : LightProfinite
n m : ℕ
h : n ≤ m
⊢ Function.Surjective ⇑(ConcreteCategory.hom (S.transitionMapLE h))

Tactic:
apply Function.Surjective.of_comp (g := S.proj m)

Result:
S : LightProfinite
n m : ℕ
h : n ≤ m
⊢ Function.Surjective (⇑(ConcreteCategory.hom (S.transitionMapLE h)) ∘ ⇑(ConcreteCategory.hom (S.proj m)))

Proof state:
S : LightProfinite
n m : ℕ
h : n ≤ m
⊢ Function.Surjective (⇑(ConcreteCategory.hom (S.transitionMapLE h)) ∘ ⇑(ConcreteCategory.hom (S.proj m)))

Tactic:
simpa only [proj_comp_transitionMapLE'] using S.proj_surjective n

Result:
no goals
-- Mathlib/Order/SuccPred/Basic.lean
theorem pred_le_iff_eq_or_le : pred a ≤ b ↔ b = pred a ∨ a ≤ b

Proof state:
case pos
α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : PredOrder α
a b : α
ha : IsMin a
⊢ pred a ≤ b ↔ b = pred a ∨ a ≤ b

Tactic:
rw [ha.pred_eq, or_iff_right_of_imp ge_of_eq]

Result:
no goals

Proof state:
α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : PredOrder α
a b : α
⊢ pred a ≤ b ↔ b = pred a ∨ a ≤ b

Tactic:
by_cases ha : IsMin a

Result:
case pos
α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : PredOrder α
a b : α
ha : IsMin a
⊢ pred a ≤ b ↔ b = pred a ∨ a ≤ b

case neg
α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : PredOrder α
a b : α
ha : ¬IsMin a
⊢ pred a ≤ b ↔ b = pred a ∨ a ≤ b

Proof state:
case neg
α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : PredOrder α
a b : α
ha : ¬IsMin a
⊢ pred a ≤ b ↔ b = pred a ∨ a ≤ b

Tactic:
rw [← pred_lt_iff_of_not_isMin ha, le_iff_eq_or_lt, eq_comm]

Result:
no goals
-- Mathlib/Analysis/NormedSpace/MStructure.lean
theorem compl_mul {P : { P : M // IsLprojection X P }} {Q : M} : ↑Pᶜ * Q = Q - ↑P * Q

Proof state:
X : Type u_1
inst✝² : NormedAddCommGroup X
M : Type u_2
inst✝¹ : Ring M
inst✝ : Module M X
P : { P // IsLprojection X P }
Q : M
⊢ ↑Pᶜ * Q = Q - ↑P * Q

Tactic:
rw [coe_compl, sub_mul, one_mul]

Result:
no goals
-- Mathlib/Data/Set/Lattice.lean
theorem image2_sInter_left_subset (S : Set (Set α)) (t : Set β)  (f : α → β → γ) :
    image2 f (⋂₀ S) t ⊆ ⋂ s ∈ S, image2 f s t

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
S : Set (Set α)
t : Set β
f : α → β → γ
⊢ image2 f (⋂₀ S) t ⊆ ⋂ s ∈ S, image2 f s t

Tactic:
aesop

Result:
no goals
-- Mathlib/Order/Interval/Set/SuccPred.lean
lemma Iio_succ_eq_Iic_of_not_isMax (hb : ¬ IsMax b) : Iio (succ b) = Iic b

Proof state:
case h
α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : SuccOrder α
b : α
hb : ¬IsMax b
x : α
⊢ x ∈ Iio (succ b) ↔ x ∈ Iic b

Tactic:
rw [mem_Iio, mem_Iic, lt_succ_iff_of_not_isMax hb]

Result:
no goals

Proof state:
α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : SuccOrder α
b : α
hb : ¬IsMax b
⊢ Iio (succ b) = Iic b

Tactic:
ext x

Result:
case h
α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : SuccOrder α
b : α
hb : ¬IsMax b
x : α
⊢ x ∈ Iio (succ b) ↔ x ∈ Iic b
-- Mathlib/Topology/Algebra/Module/Equiv.lean
lemma IsInvertible.inverse_comp_apply_of_right {g : M₂ →L[R] M₃} {f : M →L[R] M₂} {v : M₃}
    (hf : f.IsInvertible) : (g ∘L f).inverse v = f.inverse (g.inverse v)

Proof state:
R : Type u_3
M : Type u_4
M₂ : Type u_5
M₃ : Type u_6
inst✝⁹ : TopologicalSpace M
inst✝⁸ : TopologicalSpace M₂
inst✝⁷ : TopologicalSpace M₃
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : AddCommMonoid M₂
inst✝² : Module R M₂
inst✝¹ : AddCommMonoid M₃
inst✝ : Module R M₃
g : M₂ →L[R] M₃
f : M →L[R] M₂
v : M₃
hf : f.IsInvertible
⊢ (g.comp f).inverse v = f.inverse (g.inverse v)

Tactic:
simp only [hf.inverse_comp_of_right, coe_comp', Function.comp_apply]

Result:
no goals
-- Mathlib/Analysis/Normed/Group/Lemmas.lean
theorem eventually_nnnorm_sub_lt (x₀ : E) {ε : ℝ≥0} (ε_pos : 0 < ε) :
    ∀ᶠ x in 𝓝 x₀, ‖x - x₀‖₊ < ε :=
  (continuousAt_id.sub continuousAt_const).nnnorm (gt_mem_nhds <| by simpa)

Proof state:
E : Type u_1
inst✝ : SeminormedAddCommGroup E
x₀ : E
ε : ℝ≥0
ε_pos : 0 < ε
⊢ (fun x => ‖id x - x₀‖₊) x₀ < ε

Tactic:
simpa

Result:
no goals
-- Mathlib/Algebra/Polynomial/Degree/Lemmas.lean
@[simp]
lemma nextCoeff_C_mul_X_add_C (ha : a ≠ 0) (c : R) : nextCoeff (C a * X + C c) = c

Proof state:
R : Type u
inst✝ : Semiring R
a : R
ha : a ≠ 0
c : R
⊢ (C a * X + C c).nextCoeff = c

Tactic:
rw [nextCoeff_of_natDegree_pos] <;> simp [ha]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Complex/Log.lean
theorem exp_inj_of_neg_pi_lt_of_le_pi {x y : ℂ} (hx₁ : -π < x.im) (hx₂ : x.im ≤ π) (hy₁ : -π < y.im)
    (hy₂ : y.im ≤ π) (hxy : exp x = exp y) : x = y

Proof state:
x y : ℂ
hx₁ : -π < x.im
hx₂ : x.im ≤ π
hy₁ : -π < y.im
hy₂ : y.im ≤ π
hxy : cexp x = cexp y
⊢ x = y

Tactic:
rw [← log_exp hx₁ hx₂, ← log_exp hy₁ hy₂, hxy]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Grind/Lemmas.lean
theorem Bool.and_eq_of_eq_false_right {a b : Bool} (h : b = false) : (a && b) = false

Proof state:
a b : Bool
h : b = false
⊢ (a && b) = false

Tactic:
simp [h]

Result:
no goals
-- Mathlib/CategoryTheory/Yoneda.lean
lemma map_coyonedaEquiv {X Y : C} {F : C ⥤ Type v₁} (f : coyoneda.obj (op X) ⟶ F)
    (g : X ⟶ Y) : F.map g (coyonedaEquiv f) = f.app Y g

Proof state:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y : C
F : C ⥤ Type v₁
f : coyoneda.obj (op X) ⟶ F
g : X ⟶ Y
⊢ F.map g (coyonedaEquiv f) = f.app Y g

Tactic:
rw [coyonedaEquiv_naturality, coyonedaEquiv_comp, coyonedaEquiv_coyoneda_map]

Result:
no goals
-- Mathlib/Algebra/Order/Module/Defs.lean
lemma smul_nonpos_of_nonneg_of_nonpos [PosSMulMono α β] (ha : 0 ≤ a) (hb : b ≤ 0) : a • b ≤ 0

Proof state:
α : Type u_1
β : Type u_2
a : α
b : β
inst✝⁵ : Zero α
inst✝⁴ : Zero β
inst✝³ : SMulZeroClass α β
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : PosSMulMono α β
ha : 0 ≤ a
hb : b ≤ 0
⊢ a • b ≤ 0

Tactic:
simpa only [smul_zero] using smul_le_smul_of_nonneg_left hb ha

Result:
no goals
-- Mathlib/Data/Int/Bitwise.lean
theorem one_shiftLeft (n : ℕ) : 1 <<< (n : ℤ) = (2 ^ n : ℕ) :=
  congr_arg ((↑) : ℕ → ℤ) (by simp [Nat.shiftLeft_eq])

Proof state:
n : ℕ
⊢ Nat.shiftLeft' false 1 n = 2 ^ n

Tactic:
simp [Nat.shiftLeft_eq]

Result:
no goals
-- Mathlib/Order/Category/BddLat.lean
lemma id_apply (X : Lat) (x : X) :
    (𝟙 X : X ⟶ X) x = x

Proof state:
X : Lat
x : ↑X
⊢ (ConcreteCategory.hom (𝟙 X)) x = x

Tactic:
simp

Result:
no goals
-- Mathlib/Data/Nat/PartENat.lean
theorem withTopEquiv_symm_le {x y : ℕ∞} : withTopEquiv.symm x ≤ withTopEquiv.symm y ↔ x ≤ y

Proof state:
x y : ℕ∞
⊢ withTopEquiv.symm x ≤ withTopEquiv.symm y ↔ x ≤ y

Tactic:
simp

Result:
no goals
-- Mathlib/Data/Fin/Basic.lean
theorem nontrivial_iff_two_le : Nontrivial (Fin n) ↔ 2 ≤ n

Proof state:
n : ℕ
⊢ Nontrivial (Fin n) ↔ 2 ≤ n

Tactic:
rcases n with (_ | _ | n) <;>
simp [Fin.nontrivial, not_nontrivial, Nat.succ_le_iff]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Sat/AIG/LawfulVecOperator.lean
theorem denote_cast_entry (entry : Entrypoint α) {input : β entry.aig len} {h} :
    ⟦(f entry.aig input).aig, entry.ref.cast h, assign⟧
      =
    ⟦entry, assign⟧

Proof state:
α : Type
inst✝² : Hashable α
inst✝¹ : DecidableEq α
β : AIG α → Nat → Type
f : {len : Nat} → (aig : AIG α) → β aig len → RefVecEntry α len
inst✝ : LawfulVecOperator α β fun {len} => f
len : Nat
assign : α → Bool
entry : Entrypoint α
input : β entry.aig len
h : entry.aig.decls.size ≤ (f entry.aig input).aig.decls.size
⊢ ⟦assign, { aig := (f entry.aig input).aig, ref := entry.ref.cast h }⟧ = ⟦assign, entry⟧

Tactic:
simp [Ref.cast]

Result:
no goals
-- Mathlib/LinearAlgebra/CrossProduct.lean
theorem cross_anticomm (v w : Fin 3 → R) : -(v ×₃ w) = w ×₃ v

Proof state:
R : Type u_1
inst✝ : CommRing R
v w : Fin 3 → R
⊢ -(crossProduct v) w = (crossProduct w) v

Tactic:
simp [cross_apply, mul_comm]

Result:
no goals
-- Mathlib/MeasureTheory/Measure/FiniteMeasureProd.lean
@[simp] lemma map_snd_prod : (μ.prod ν).map Prod.snd = μ univ • ν

Proof state:
α : Type u_1
inst✝¹ : MeasurableSpace α
β : Type u_2
inst✝ : MeasurableSpace β
μ : FiniteMeasure α
ν : FiniteMeasure β
⊢ (μ.prod ν).map Prod.snd = μ univ • ν

Tactic:
ext

Result:
case h
α : Type u_1
inst✝¹ : MeasurableSpace α
β : Type u_2
inst✝ : MeasurableSpace β
μ : FiniteMeasure α
ν : FiniteMeasure β
s✝ : Set β
a✝ : MeasurableSet s✝
⊢ ↑((μ.prod ν).map Prod.snd) s✝ = ↑(μ univ • ν) s✝

Proof state:
case h
α : Type u_1
inst✝¹ : MeasurableSpace α
β : Type u_2
inst✝ : MeasurableSpace β
μ : FiniteMeasure α
ν : FiniteMeasure β
s✝ : Set β
a✝ : MeasurableSet s✝
⊢ ↑((μ.prod ν).map Prod.snd) s✝ = ↑(μ univ • ν) s✝

Tactic:
simp

Result:
no goals
-- Mathlib/Data/List/Flatten.lean
theorem drop_sum_flatten' (L : List (List α)) (i : ℕ) :
    L.flatten.drop (Nat.sum ((L.map length).take i)) = (L.drop i).flatten

Proof state:
case nil
α : Type u_1
i : ℕ
⊢ drop (Nat.sum (take i (map length []))) [].flatten = (drop i []).flatten

Tactic:
simp

Result:
no goals

Proof state:
case cons
α : Type u_1
head✝ : List α
tail✝ : List (List α)
tail_ih✝ : ∀ (i : ℕ), drop (Nat.sum (take i (map length tail✝))) tail✝.flatten = (drop i tail✝).flatten
i : ℕ
⊢ drop (Nat.sum (take i (map length (head✝ :: tail✝)))) (head✝ :: tail✝).flatten = (drop i (head✝ :: tail✝)).flatten

Tactic:
cases i <;> simp [drop_append, *]

Result:
no goals

Proof state:
α : Type u_1
L : List (List α)
i : ℕ
⊢ drop (Nat.sum (take i (map length L))) L.flatten = (drop i L).flatten

Tactic:
induction L generalizing i

Result:
case nil
α : Type u_1
i : ℕ
⊢ drop (Nat.sum (take i (map length []))) [].flatten = (drop i []).flatten

case cons
α : Type u_1
head✝ : List α
tail✝ : List (List α)
tail_ih✝ : ∀ (i : ℕ), drop (Nat.sum (take i (map length tail✝))) tail✝.flatten = (drop i tail✝).flatten
i : ℕ
⊢ drop (Nat.sum (take i (map length (head✝ :: tail✝)))) (head✝ :: tail✝).flatten = (drop i (head✝ :: tail✝)).flatten
-- Mathlib/.lake/packages/lean4/src/lean/Std/Sat/AIG/Relabel.lean
theorem relabel_unsat_iff [Nonempty α] {entry : Entrypoint α} {r : α → β}
    (hinj : ∀ x y, x ∈ entry.aig → y ∈ entry.aig → r x = r y → x = y) :
    (entry.relabel r).Unsat ↔ entry.Unsat

Proof state:
α : Type
inst✝⁴ : Hashable α
inst✝³ : DecidableEq α
β : Type
inst✝² : Hashable β
inst✝¹ : DecidableEq β
inst✝ : Nonempty α
entry : Entrypoint α
r : α → β
hinj : ∀ (x y : α), x ∈ entry.aig → y ∈ entry.aig → r x = r y → x = y
⊢ (relabel r entry).Unsat ↔ entry.Unsat

Tactic:
simp [relabel, Unsat]

Result:
α : Type
inst✝⁴ : Hashable α
inst✝³ : DecidableEq α
β : Type
inst✝² : Hashable β
inst✝¹ : DecidableEq β
inst✝ : Nonempty α
entry : Entrypoint α
r : α → β
hinj : ∀ (x y : α), x ∈ entry.aig → y ∈ entry.aig → r x = r y → x = y
⊢ (AIG.relabel r entry.aig).UnsatAt entry.ref.gate ⋯ ↔ entry.aig.UnsatAt entry.ref.gate ⋯

Proof state:
α : Type
inst✝⁴ : Hashable α
inst✝³ : DecidableEq α
β : Type
inst✝² : Hashable β
inst✝¹ : DecidableEq β
inst✝ : Nonempty α
entry : Entrypoint α
r : α → β
hinj : ∀ (x y : α), x ∈ entry.aig → y ∈ entry.aig → r x = r y → x = y
⊢ (AIG.relabel r entry.aig).UnsatAt entry.ref.gate ⋯ ↔ entry.aig.UnsatAt entry.ref.gate ⋯

Tactic:
rw [AIG.relabel_unsat_iff]

Result:
α : Type
inst✝⁴ : Hashable α
inst✝³ : DecidableEq α
β : Type
inst✝² : Hashable β
inst✝¹ : DecidableEq β
inst✝ : Nonempty α
entry : Entrypoint α
r : α → β
hinj : ∀ (x y : α), x ∈ entry.aig → y ∈ entry.aig → r x = r y → x = y
⊢ ∀ (x y : α), x ∈ entry.aig → y ∈ entry.aig → r x = r y → x = y

Proof state:
α : Type
inst✝⁴ : Hashable α
inst✝³ : DecidableEq α
β : Type
inst✝² : Hashable β
inst✝¹ : DecidableEq β
inst✝ : Nonempty α
entry : Entrypoint α
r : α → β
hinj : ∀ (x y : α), x ∈ entry.aig → y ∈ entry.aig → r x = r y → x = y
⊢ ∀ (x y : α), x ∈ entry.aig → y ∈ entry.aig → r x = r y → x = y

Tactic:
assumption

Result:
no goals
-- Mathlib/Data/Real/EReal.lean
lemma coe_ennreal_mul_top {x : ℝ≥0∞} (hx : x ≠ 0) : (x : EReal) * ⊤ = ⊤

Proof state:
x : ℝ≥0∞
hx : x ≠ 0
⊢ ↑x * ⊤ = ⊤

Tactic:
rw [EReal.mul_comm, top_mul_coe_ennreal hx]

Result:
no goals
-- Mathlib/MeasureTheory/Group/FundamentalDomain.lean
theorem setLIntegral_eq (hs : IsFundamentalDomain G s μ) (ht : IsFundamentalDomain G t μ)
    (f : α → ℝ≥0∞) (hf : ∀ (g : G) (x), f (g • x) = f x) :
    ∫⁻ x in s, f x ∂μ = ∫⁻ x in t, f x ∂μ :=
  calc
    ∫⁻ x in s, f x ∂μ = ∑' g : G, ∫⁻ x in s ∩ g • t, f x ∂μ := ht.setLIntegral_eq_tsum _ _
    _ = ∑' g : G, ∫⁻ x in g • t ∩ s, f (g⁻¹ • x) ∂μ

Proof state:
G : Type u_1
α : Type u_3
inst✝⁶ : Group G
inst✝⁵ : MulAction G α
inst✝⁴ : MeasurableSpace α
s t : Set α
μ : Measure α
inst✝³ : MeasurableSpace G
inst✝² : MeasurableSMul G α
inst✝¹ : SMulInvariantMeasure G α μ
inst✝ : Countable G
hs : IsFundamentalDomain G s μ
ht : IsFundamentalDomain G t μ
f : α → ℝ≥0∞
hf : ∀ (g : G) (x : α), f (g • x) = f x
⊢ ∑' (g : G), ∫⁻ (x : α) in s ∩ g • t, f x ∂μ = ∑' (g : G), ∫⁻ (x : α) in g • t ∩ s, f (g⁻¹ • x) ∂μ

Tactic:
simp only [hf, inter_comm]

Result:
no goals
-- Mathlib/Analysis/Normed/Field/Basic.lean
theorem norm_eq (x : ℝ≥0) : ‖(x : ℝ)‖ = x

Proof state:
x : ℝ≥0
⊢ ‖↑x‖ = ↑x

Tactic:
rw [Real.norm_eq_abs, x.abs_eq]

Result:
no goals
-- Mathlib/Topology/Constructions.lean
theorem nhds_pi {a : ∀ i, π i} : 𝓝 a = pi fun i => 𝓝 (a i)

Proof state:
ι : Type u_5
π : ι → Type u_6
T : (i : ι) → TopologicalSpace (π i)
a : (i : ι) → π i
⊢ 𝓝 a = Filter.pi fun i => 𝓝 (a i)

Tactic:
simp only [nhds_iInf, nhds_induced, Filter.pi]

Result:
no goals
-- Mathlib/Data/Stream/Init.lean
theorem map_append_stream (f : α → β) :
    ∀ (l : List α) (s : Stream' α), map f (l ++ₛ s) = List.map f l ++ₛ map f s
  | [], _ => rfl
  | List.cons a l, s => by
    rw [cons_append_stream, List.map_cons, map_cons, cons_append_stream, map_append_stream f l]

Proof state:
α : Type u
β : Type v
f : α → β
a : α
l : List α
s : Stream' α
⊢ map f (a :: l ++ₛ s) = List.map f (a :: l) ++ₛ map f s

Tactic:
rw [cons_append_stream, List.map_cons, map_cons, cons_append_stream, map_append_stream f l]

Result:
no goals
-- Mathlib/Algebra/Ring/BooleanRing.lean
theorem inf_sup_self (a b : α) : a ⊓ (a ⊔ b) = a

Proof state:
α : Type u_1
inst✝ : BooleanRing α
a b : α
⊢ a * (a + b + a * b) = a

Tactic:
rw [mul_add, mul_add, mul_self, ← mul_assoc, mul_self, add_assoc, add_self, add_zero]

Result:
no goals