harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Data/Matrix/ConjTranspose.lean
@[simp]
lemma conjTranspose_stdBasisMatrix [DecidableEq n] [DecidableEq m] [AddMonoid α]
    [StarAddMonoid α] (i : m) (j : n) (a : α) :
    (stdBasisMatrix i j a)ᴴ = stdBasisMatrix j i (star a)

Proof state:
m : Type u_2
n : Type u_3
α : Type v
inst✝³ : DecidableEq n
inst✝² : DecidableEq m
inst✝¹ : AddMonoid α
inst✝ : StarAddMonoid α
i : m
j : n
a : α
⊢ (stdBasisMatrix i j a)ᴴ = stdBasisMatrix j i (star a)

Tactic:
show (stdBasisMatrix i j a).transpose.map starAddEquiv = stdBasisMatrix j i (star a)

Result:
m : Type u_2
n : Type u_3
α : Type v
inst✝³ : DecidableEq n
inst✝² : DecidableEq m
inst✝¹ : AddMonoid α
inst✝ : StarAddMonoid α
i : m
j : n
a : α
⊢ (stdBasisMatrix i j a)ᵀ.map ⇑starAddEquiv = stdBasisMatrix j i (star a)

Proof state:
m : Type u_2
n : Type u_3
α : Type v
inst✝³ : DecidableEq n
inst✝² : DecidableEq m
inst✝¹ : AddMonoid α
inst✝ : StarAddMonoid α
i : m
j : n
a : α
⊢ (stdBasisMatrix i j a)ᵀ.map ⇑starAddEquiv = stdBasisMatrix j i (star a)

Tactic:
simp

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem sdiv_eq (x y : BitVec w) : x.sdiv y =
  match x.msb, y.msb with
  | false, false => udiv x y
  | false, true  =>  - (x.udiv (- y))
  | true,  false => - ((- x).udiv y)
  | true,  true  => (- x).udiv (- y)

Proof state:
w : Nat
x y : BitVec w
⊢ (match x.msb, y.msb with
    | false, false => x.udiv y
    | false, true => (x.udiv y.neg).neg
    | true, false => (x.neg.udiv y).neg
    | true, true => x.neg.udiv y.neg) =
    match x.msb, y.msb with
    | false, false => x.udiv y
    | false, true => -x.udiv (-y)
    | true, false => -(-x).udiv y
    | true, true => (-x).udiv (-y)

Tactic:
rcases x.msb <;> rcases y.msb <;> simp

Result:
no goals

Proof state:
w : Nat
x y : BitVec w
⊢ x.sdiv y =
    match x.msb, y.msb with
    | false, false => x.udiv y
    | false, true => -x.udiv (-y)
    | true, false => -(-x).udiv y
    | true, true => (-x).udiv (-y)

Tactic:
rw [BitVec.sdiv]

Result:
w : Nat
x y : BitVec w
⊢ (match x.msb, y.msb with
    | false, false => x.udiv y
    | false, true => (x.udiv y.neg).neg
    | true, false => (x.neg.udiv y).neg
    | true, true => x.neg.udiv y.neg) =
    match x.msb, y.msb with
    | false, false => x.udiv y
    | false, true => -x.udiv (-y)
    | true, false => -(-x).udiv y
    | true, true => (-x).udiv (-y)
-- Mathlib/Analysis/Polynomial/Basic.lean
theorem abs_isBoundedUnder_iff :
    (IsBoundedUnder (· ≤ ·) atTop fun x => |eval x P|) ↔ P.degree ≤ 0

Proof state:
𝕜 : Type u_1
inst✝¹ : NormedLinearOrderedField 𝕜
P : 𝕜[X]
inst✝ : OrderTopology 𝕜
h : IsBoundedUnder (fun x1 x2 => x1 ≤ x2) atTop fun x => |eval x P|
⊢ P.degree ≤ 0

Tactic:
contrapose! h

Result:
𝕜 : Type u_1
inst✝¹ : NormedLinearOrderedField 𝕜
P : 𝕜[X]
inst✝ : OrderTopology 𝕜
h : 0 < P.degree
⊢ ¬IsBoundedUnder (fun x1 x2 => x1 ≤ x2) atTop fun x => |eval x P|

Proof state:
𝕜 : Type u_1
inst✝¹ : NormedLinearOrderedField 𝕜
P : 𝕜[X]
inst✝ : OrderTopology 𝕜
h : 0 < P.degree
⊢ ¬IsBoundedUnder (fun x1 x2 => x1 ≤ x2) atTop fun x => |eval x P|

Tactic:
exact not_isBoundedUnder_of_tendsto_atTop (abs_tendsto_atTop P h)

Result:
no goals

Proof state:
𝕜 : Type u_1
inst✝¹ : NormedLinearOrderedField 𝕜
P : 𝕜[X]
inst✝ : OrderTopology 𝕜
⊢ (IsBoundedUnder (fun x1 x2 => x1 ≤ x2) atTop fun x => |eval x P|) ↔ P.degree ≤ 0

Tactic:
refine ⟨fun h => ?_, fun h => ⟨|P.coeff 0|, eventually_map.mpr (Eventually.of_forall
  (forall_imp (fun _ => le_of_eq) fun x => congr_arg abs <| _root_.trans (congr_arg (eval x)
  (eq_C_of_degree_le_zero h)) eval_C))⟩⟩

Result:
𝕜 : Type u_1
inst✝¹ : NormedLinearOrderedField 𝕜
P : 𝕜[X]
inst✝ : OrderTopology 𝕜
h : IsBoundedUnder (fun x1 x2 => x1 ≤ x2) atTop fun x => |eval x P|
⊢ P.degree ≤ 0
-- Mathlib/Data/Bool/Basic.lean
lemma eq_not_iff : ∀ {a b : Bool}, a = !b ↔ a ≠ b

Proof state:
⊢ ∀ {a b : Bool}, a = !b ↔ a ≠ b

Tactic:
decide

Result:
no goals
-- Mathlib/Analysis/Convex/Deriv.lean
lemma lt_slope_of_hasDerivWithinAt (hfc : StrictConcaveOn ℝ S f)
    (hx : x ∈ S) (hy : y ∈ S) (hxy : x < y) (hf' : HasDerivWithinAt f f' S y) :
    f' < slope f x y

Proof state:
S : Set ℝ
f : ℝ → ℝ
x y f' : ℝ
hfc : StrictConcaveOn ℝ S f
hx : x ∈ S
hy : y ∈ S
hxy : x < y
hf' : HasDerivWithinAt f f' S y
⊢ f' < slope f x y

Tactic:
simpa only [neg_neg, Pi.neg_def, slope_neg] using
  neg_lt_neg (hfc.neg.slope_lt_of_hasDerivWithinAt hx hy hxy hf'.neg)

Result:
no goals
-- Mathlib/GroupTheory/DoubleCoset.lean
theorem disjoint_out {H K : Subgroup G} {a b : Quotient H K} :
    a ≠ b → Disjoint (doset a.out H K) (doset b.out (H : Set G) K)

Proof state:
G : Type u_1
inst✝ : Group G
H K : Subgroup G
a b : Quotient ↑H ↑K
⊢ a ≠ b → Disjoint (doset (Quotient.out a) ↑H ↑K) (doset (Quotient.out b) ↑H ↑K)

Tactic:
contrapose!

Result:
G : Type u_1
inst✝ : Group G
H K : Subgroup G
a b : Quotient ↑H ↑K
⊢ ¬Disjoint (doset (Quotient.out a) ↑H ↑K) (doset (Quotient.out b) ↑H ↑K) → a = b

Proof state:
G : Type u_1
inst✝ : Group G
H K : Subgroup G
a b : Quotient ↑H ↑K
h : ¬Disjoint (doset (Quotient.out a) ↑H ↑K) (doset (Quotient.out b) ↑H ↑K)
⊢ a = b

Tactic:
simpa [out_eq'] using mk_eq_of_doset_eq (eq_of_not_disjoint h)

Result:
no goals

Proof state:
G : Type u_1
inst✝ : Group G
H K : Subgroup G
a b : Quotient ↑H ↑K
⊢ ¬Disjoint (doset (Quotient.out a) ↑H ↑K) (doset (Quotient.out b) ↑H ↑K) → a = b

Tactic:
intro h

Result:
G : Type u_1
inst✝ : Group G
H K : Subgroup G
a b : Quotient ↑H ↑K
h : ¬Disjoint (doset (Quotient.out a) ↑H ↑K) (doset (Quotient.out b) ↑H ↑K)
⊢ a = b
-- Mathlib/MeasureTheory/Function/AEEqOfIntegral.lean
theorem ae_le_of_forall_setIntegral_le {f g : α → ℝ} (hf : Integrable f μ) (hg : Integrable g μ)
    (hf_le : ∀ s, MeasurableSet s → μ s < ∞ → (∫ x in s, f x ∂μ) ≤ ∫ x in s, g x ∂μ) :
    f ≤ᵐ[μ] g

Proof state:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f g : α → ℝ
hf : Integrable f μ
hg : Integrable g μ
hf_le : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → ∫ (x : α) in s, f x ∂μ ≤ ∫ (x : α) in s, g x ∂μ
⊢ 0 ≤ᶠ[ae μ] g - f

Tactic:
refine ae_nonneg_of_forall_setIntegral_nonneg (hg.sub hf) fun s hs => ?_

Result:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f g : α → ℝ
hf : Integrable f μ
hg : Integrable g μ
hf_le : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → ∫ (x : α) in s, f x ∂μ ≤ ∫ (x : α) in s, g x ∂μ
s : Set α
hs : MeasurableSet s
⊢ μ s < ⊤ → 0 ≤ ∫ (x : α) in s, (g - f) x ∂μ

Proof state:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f g : α → ℝ
hf : Integrable f μ
hg : Integrable g μ
hf_le : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → ∫ (x : α) in s, f x ∂μ ≤ ∫ (x : α) in s, g x ∂μ
⊢ f ≤ᶠ[ae μ] g

Tactic:
rw [← eventually_sub_nonneg]

Result:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f g : α → ℝ
hf : Integrable f μ
hg : Integrable g μ
hf_le : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → ∫ (x : α) in s, f x ∂μ ≤ ∫ (x : α) in s, g x ∂μ
⊢ 0 ≤ᶠ[ae μ] g - f

Proof state:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f g : α → ℝ
hf : Integrable f μ
hg : Integrable g μ
hf_le : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → ∫ (x : α) in s, f x ∂μ ≤ ∫ (x : α) in s, g x ∂μ
s : Set α
hs : MeasurableSet s
⊢ μ s < ⊤ → 0 ≤ ∫ (x : α) in s, (g - f) x ∂μ

Tactic:
rw [integral_sub' hg.integrableOn hf.integrableOn, sub_nonneg]

Result:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f g : α → ℝ
hf : Integrable f μ
hg : Integrable g μ
hf_le : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → ∫ (x : α) in s, f x ∂μ ≤ ∫ (x : α) in s, g x ∂μ
s : Set α
hs : MeasurableSet s
⊢ μ s < ⊤ → ∫ (a : α) in s, f a ∂μ ≤ ∫ (a : α) in s, g a ∂μ

Proof state:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f g : α → ℝ
hf : Integrable f μ
hg : Integrable g μ
hf_le : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → ∫ (x : α) in s, f x ∂μ ≤ ∫ (x : α) in s, g x ∂μ
s : Set α
hs : MeasurableSet s
⊢ μ s < ⊤ → ∫ (a : α) in s, f a ∂μ ≤ ∫ (a : α) in s, g a ∂μ

Tactic:
exact hf_le s hs

Result:
no goals
-- Mathlib/Algebra/Polynomial/AlgebraMap.lean
theorem mapAlgEquiv_comp (C : Type z) [Semiring C] [Algebra R C] (f : A ≃ₐ[R] B) (g : B ≃ₐ[R] C) :
    (mapAlgEquiv f).trans (mapAlgEquiv g) = mapAlgEquiv (f.trans g)

Proof state:
R : Type u
A : Type z
B : Type u_2
inst✝⁶ : CommSemiring R
inst✝⁵ : Semiring A
inst✝⁴ : Semiring B
inst✝³ : Algebra R A
inst✝² : Algebra R B
C : Type z
inst✝¹ : Semiring C
inst✝ : Algebra R C
f : A ≃ₐ[R] B
g : B ≃ₐ[R] C
⊢ (mapAlgEquiv f).trans (mapAlgEquiv g) = mapAlgEquiv (f.trans g)

Tactic:
apply AlgEquiv.ext

Result:
case h
R : Type u
A : Type z
B : Type u_2
inst✝⁶ : CommSemiring R
inst✝⁵ : Semiring A
inst✝⁴ : Semiring B
inst✝³ : Algebra R A
inst✝² : Algebra R B
C : Type z
inst✝¹ : Semiring C
inst✝ : Algebra R C
f : A ≃ₐ[R] B
g : B ≃ₐ[R] C
⊢ ∀ (a : A[X]), ((mapAlgEquiv f).trans (mapAlgEquiv g)) a = (mapAlgEquiv (f.trans g)) a

Proof state:
case h
R : Type u
A : Type z
B : Type u_2
inst✝⁶ : CommSemiring R
inst✝⁵ : Semiring A
inst✝⁴ : Semiring B
inst✝³ : Algebra R A
inst✝² : Algebra R B
C : Type z
inst✝¹ : Semiring C
inst✝ : Algebra R C
f : A ≃ₐ[R] B
g : B ≃ₐ[R] C
x : A[X]
⊢ ((mapAlgEquiv f).trans (mapAlgEquiv g)) x = (mapAlgEquiv (f.trans g)) x

Tactic:
simp [AlgEquiv.trans_apply, map_map]

Result:
case h
R : Type u
A : Type z
B : Type u_2
inst✝⁶ : CommSemiring R
inst✝⁵ : Semiring A
inst✝⁴ : Semiring B
inst✝³ : Algebra R A
inst✝² : Algebra R B
C : Type z
inst✝¹ : Semiring C
inst✝ : Algebra R C
f : A ≃ₐ[R] B
g : B ≃ₐ[R] C
x : A[X]
⊢ map ((↑g).comp ↑f) x = map (↑(f.trans g)) x

Proof state:
case h
R : Type u
A : Type z
B : Type u_2
inst✝⁶ : CommSemiring R
inst✝⁵ : Semiring A
inst✝⁴ : Semiring B
inst✝³ : Algebra R A
inst✝² : Algebra R B
C : Type z
inst✝¹ : Semiring C
inst✝ : Algebra R C
f : A ≃ₐ[R] B
g : B ≃ₐ[R] C
x : A[X]
⊢ map ((↑g).comp ↑f) x = map (↑(f.trans g)) x

Tactic:
congr

Result:
no goals

Proof state:
case h
R : Type u
A : Type z
B : Type u_2
inst✝⁶ : CommSemiring R
inst✝⁵ : Semiring A
inst✝⁴ : Semiring B
inst✝³ : Algebra R A
inst✝² : Algebra R B
C : Type z
inst✝¹ : Semiring C
inst✝ : Algebra R C
f : A ≃ₐ[R] B
g : B ≃ₐ[R] C
⊢ ∀ (a : A[X]), ((mapAlgEquiv f).trans (mapAlgEquiv g)) a = (mapAlgEquiv (f.trans g)) a

Tactic:
intro x

Result:
case h
R : Type u
A : Type z
B : Type u_2
inst✝⁶ : CommSemiring R
inst✝⁵ : Semiring A
inst✝⁴ : Semiring B
inst✝³ : Algebra R A
inst✝² : Algebra R B
C : Type z
inst✝¹ : Semiring C
inst✝ : Algebra R C
f : A ≃ₐ[R] B
g : B ≃ₐ[R] C
x : A[X]
⊢ ((mapAlgEquiv f).trans (mapAlgEquiv g)) x = (mapAlgEquiv (f.trans g)) x
-- Mathlib/Algebra/GeomSum.lean
theorem Commute.mul_neg_geom_sum₂ [Ring α] {x y : α} (h : Commute x y) (n : ℕ) :
    ((y - x) * ∑ i ∈ range n, x ^ i * y ^ (n - 1 - i)) = y ^ n - x ^ n

Proof state:
case a
α : Type u
inst✝ : Ring α
x y : α
h : Commute x y
n : ℕ
⊢ MulOpposite.op ((y - x) * ∑ i ∈ range n, x ^ i * y ^ (n - 1 - i)) = MulOpposite.op (y ^ n - x ^ n)

Tactic:
simp only [op_mul, op_sub, op_geom_sum₂, op_pow]

Result:
case a
α : Type u
inst✝ : Ring α
x y : α
h : Commute x y
n : ℕ
⊢ MulOpposite.op (∑ i ∈ range n, x ^ i * y ^ (n - 1 - i)) * (MulOpposite.op y - MulOpposite.op x) =
    MulOpposite.op y ^ n - MulOpposite.op x ^ n

Proof state:
α : Type u
inst✝ : Ring α
x y : α
h : Commute x y
n : ℕ
⊢ (y - x) * ∑ i ∈ range n, x ^ i * y ^ (n - 1 - i) = y ^ n - x ^ n

Tactic:
apply op_injective

Result:
case a
α : Type u
inst✝ : Ring α
x y : α
h : Commute x y
n : ℕ
⊢ MulOpposite.op ((y - x) * ∑ i ∈ range n, x ^ i * y ^ (n - 1 - i)) = MulOpposite.op (y ^ n - x ^ n)

Proof state:
case a
α : Type u
inst✝ : Ring α
x y : α
h : Commute x y
n : ℕ
⊢ MulOpposite.op (∑ i ∈ range n, x ^ i * y ^ (n - 1 - i)) * (MulOpposite.op y - MulOpposite.op x) =
    MulOpposite.op y ^ n - MulOpposite.op x ^ n

Tactic:
simp [(Commute.op h.symm).geom_sum₂_mul n]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Int/DivModLemmas.lean
theorem emod_mul_bmod_congr (x : Int) (n : Nat) : Int.bmod (x%n * y) n = Int.bmod (x * y) n

Proof state:
y x : Int
n : Nat
⊢ (x % ↑n * y).bmod n = (x * y).bmod n

Tactic:
simp [Int.emod_def, Int.sub_eq_add_neg]

Result:
y x : Int
n : Nat
⊢ ((x + -(↑n * (x / ↑n))) * y).bmod n = (x * y).bmod n

Proof state:
y x : Int
n : Nat
⊢ ((x + -(↑n * (x / ↑n))) * y).bmod n = (x * y).bmod n

Tactic:
rw [←Int.mul_neg, Int.add_mul, Int.mul_assoc, Int.bmod_add_mul_cancel]

Result:
no goals
-- Mathlib/LinearAlgebra/TensorProduct/DirectLimit.lean
@[simp] lemma directLimitRight_tmul_of {i : ι} (m : M) (g : G i) :
    directLimitRight f M (m ⊗ₜ of _ _ _ _ _ g) = of _ _ _ _ i (m ⊗ₜ g)

Proof state:
R : Type u_1
inst✝⁶ : CommSemiring R
ι : Type u_2
inst✝⁵ : DecidableEq ι
inst✝⁴ : Preorder ι
G : ι → Type u_3
inst✝³ : (i : ι) → AddCommMonoid (G i)
inst✝² : (i : ι) → Module R (G i)
f : (i j : ι) → i ≤ j → G i →ₗ[R] G j
M : Type u_4
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
i : ι
m : M
g : G i
⊢ (directLimitRight f M) (m ⊗ₜ[R] (of R ι G f i) g) =
    (of R ι (fun x => M ⊗[R] G x) (fun i j h => LinearMap.lTensor M (f i j h)) i) (m ⊗ₜ[R] g)

Tactic:
simp [directLimitRight, congr_apply_of]

Result:
no goals
-- Mathlib/Tactic/CancelDenoms/Core.lean
theorem cancel_factors_lt {α} [LinearOrderedField α] {a b ad bd a' b' gcd : α}
    (ha : ad * a = a') (hb : bd * b = b') (had : 0 < ad) (hbd : 0 < bd) (hgcd : 0 < gcd) :
    (a < b) = (1 / gcd * (bd * a') < 1 / gcd * (ad * b'))

Proof state:
α : Type u_1
inst✝ : LinearOrderedField α
a b ad bd a' b' gcd : α
ha : ad * a = a'
hb : bd * b = b'
had : 0 < ad
hbd : 0 < bd
hgcd : 0 < gcd
⊢ 0 < ad * bd

Tactic:
exact mul_pos had hbd

Result:
no goals

Proof state:
α : Type u_1
inst✝ : LinearOrderedField α
a b ad bd a' b' gcd : α
ha : ad * a = a'
hb : bd * b = b'
had : 0 < ad
hbd : 0 < bd
hgcd : 0 < gcd
⊢ (a < b) = (1 / gcd * (bd * a') < 1 / gcd * (ad * b'))

Tactic:
rw [mul_lt_mul_left, ← ha, ← hb, ← mul_assoc, ← mul_assoc, mul_comm bd, mul_lt_mul_left]

Result:
α : Type u_1
inst✝ : LinearOrderedField α
a b ad bd a' b' gcd : α
ha : ad * a = a'
hb : bd * b = b'
had : 0 < ad
hbd : 0 < bd
hgcd : 0 < gcd
⊢ 0 < ad * bd

α : Type u_1
inst✝ : LinearOrderedField α
a b ad bd a' b' gcd : α
ha : ad * a = a'
hb : bd * b = b'
had : 0 < ad
hbd : 0 < bd
hgcd : 0 < gcd
⊢ 0 < 1 / gcd

Proof state:
α : Type u_1
inst✝ : LinearOrderedField α
a b ad bd a' b' gcd : α
ha : ad * a = a'
hb : bd * b = b'
had : 0 < ad
hbd : 0 < bd
hgcd : 0 < gcd
⊢ 0 < 1 / gcd

Tactic:
exact one_div_pos.2 hgcd

Result:
no goals
-- Mathlib/Data/Multiset/Filter.lean
theorem count_filter_of_pos {p} [DecidablePred p] {a} {s : Multiset α} (h : p a) :
    count a (filter p s) = count a s :=
  Quot.inductionOn s fun _l => by
    simp only [quot_mk_to_coe'', filter_coe, mem_coe, coe_count, decide_eq_true_eq]
    apply count_filter
    simpa using h

Proof state:
α : Type u_1
inst✝¹ : DecidableEq α
p : α → Prop
inst✝ : DecidablePred p
a : α
s : Multiset α
h : p a
_l : List α
⊢ List.count a (List.filter (fun b => decide (p b)) _l) = List.count a _l

Tactic:
apply count_filter

Result:
case h
α : Type u_1
inst✝¹ : DecidableEq α
p : α → Prop
inst✝ : DecidablePred p
a : α
s : Multiset α
h : p a
_l : List α
⊢ decide (p a) = true

Proof state:
α : Type u_1
inst✝¹ : DecidableEq α
p : α → Prop
inst✝ : DecidablePred p
a : α
s : Multiset α
h : p a
_l : List α
⊢ count a (filter p (Quot.mk (⇑(isSetoid α)) _l)) = count a (Quot.mk (⇑(isSetoid α)) _l)

Tactic:
simp only [quot_mk_to_coe'', filter_coe, mem_coe, coe_count, decide_eq_true_eq]

Result:
α : Type u_1
inst✝¹ : DecidableEq α
p : α → Prop
inst✝ : DecidablePred p
a : α
s : Multiset α
h : p a
_l : List α
⊢ List.count a (List.filter (fun b => decide (p b)) _l) = List.count a _l

Proof state:
case h
α : Type u_1
inst✝¹ : DecidableEq α
p : α → Prop
inst✝ : DecidablePred p
a : α
s : Multiset α
h : p a
_l : List α
⊢ decide (p a) = true

Tactic:
simpa using h

Result:
no goals
-- Mathlib/SetTheory/ZFC/Rank.lean
theorem rank_union (x y : ZFSet) : rank (x ∪ y) = max (rank x) (rank y)

Proof state:
x y : ZFSet.{u_1}
⊢ (x ∪ y).rank = x.rank ⊔ y.rank

Tactic:
apply le_antisymm

Result:
case a
x y : ZFSet.{u_1}
⊢ (x ∪ y).rank ≤ x.rank ⊔ y.rank

case a
x y : ZFSet.{u_1}
⊢ x.rank ⊔ y.rank ≤ (x ∪ y).rank

Proof state:
case a
x y : ZFSet.{u_1}
⊢ (x ∪ y).rank ≤ x.rank ⊔ y.rank

Tactic:
simp_rw [rank_le_iff, mem_union, lt_max_iff]

Result:
case a
x y : ZFSet.{u_1}
⊢ ∀ ⦃y_1 : ZFSet.{u_1}⦄, y_1 ∈ x ∨ y_1 ∈ y → y_1.rank < x.rank ∨ y_1.rank < y.rank

Proof state:
case a
x y y✝ : ZFSet.{u_1}
⊢ y✝ ∈ x ∨ y✝ ∈ y → y✝.rank < x.rank ∨ y✝.rank < y.rank

Tactic:
apply Or.imp <;> apply rank_lt_of_mem

Result:
no goals

Proof state:
case a
x y : ZFSet.{u_1}
⊢ ∀ ⦃y_1 : ZFSet.{u_1}⦄, y_1 ∈ x ∨ y_1 ∈ y → y_1.rank < x.rank ∨ y_1.rank < y.rank

Tactic:
intro

Result:
case a
x y y✝ : ZFSet.{u_1}
⊢ y✝ ∈ x ∨ y✝ ∈ y → y✝.rank < x.rank ∨ y✝.rank < y.rank

Proof state:
case a
x y : ZFSet.{u_1}
⊢ x.rank ⊔ y.rank ≤ (x ∪ y).rank

Tactic:
apply max_le <;> apply rank_mono <;> intro _ h <;> simp [h]

Result:
no goals
-- Mathlib/Logic/Equiv/Set.lean
theorem prod_assoc_symm_preimage {α β γ} {s : Set α} {t : Set β} {u : Set γ} :
    (Equiv.prodAssoc α β γ).symm ⁻¹' (s ×ˢ t) ×ˢ u = s ×ˢ t ×ˢ u

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
s : Set α
t : Set β
u : Set γ
⊢ ⇑(prodAssoc α β γ).symm ⁻¹' (s ×ˢ t) ×ˢ u = s ×ˢ t ×ˢ u

Tactic:
ext

Result:
case h
α : Type u_1
β : Type u_2
γ : Type u_3
s : Set α
t : Set β
u : Set γ
x✝ : α × β × γ
⊢ x✝ ∈ ⇑(prodAssoc α β γ).symm ⁻¹' (s ×ˢ t) ×ˢ u ↔ x✝ ∈ s ×ˢ t ×ˢ u

Proof state:
case h
α : Type u_1
β : Type u_2
γ : Type u_3
s : Set α
t : Set β
u : Set γ
x✝ : α × β × γ
⊢ x✝ ∈ ⇑(prodAssoc α β γ).symm ⁻¹' (s ×ˢ t) ×ˢ u ↔ x✝ ∈ s ×ˢ t ×ˢ u

Tactic:
simp [and_assoc]

Result:
no goals
-- Mathlib/Order/ConditionallyCompleteLattice/Indexed.lean
theorem cbiSup_eq_of_forall {p : ι → Prop} {f : Subtype p → α} (hp : ∀ i, p i) :
    ⨆ (i) (h : p i), f ⟨i, h⟩ = iSup f

Proof state:
α : Type u_1
ι : Sort u_4
inst✝ : ConditionallyCompleteLattice α
p : ι → Prop
f : Subtype p → α
hp : ∀ (i : ι), p i
⊢ sSup (range fun i => f ⟨i, ⋯⟩) = sSup (range f)

Tactic:
congr

Result:
case e_a
α : Type u_1
ι : Sort u_4
inst✝ : ConditionallyCompleteLattice α
p : ι → Prop
f : Subtype p → α
hp : ∀ (i : ι), p i
⊢ (range fun i => f ⟨i, ⋯⟩) = range f

Proof state:
case e_a.h₂.intro
α : Type u_1
ι : Sort u_4
inst✝ : ConditionallyCompleteLattice α
p : ι → Prop
f : Subtype p → α
hp : ∀ (i : ι), p i
i : Subtype p
⊢ f i ∈ range fun i => f ⟨i, ⋯⟩

Tactic:
simp

Result:
no goals

Proof state:
case e_a
α : Type u_1
ι : Sort u_4
inst✝ : ConditionallyCompleteLattice α
p : ι → Prop
f : Subtype p → α
hp : ∀ (i : ι), p i
⊢ (range fun i => f ⟨i, ⋯⟩) = range f

Tactic:
apply Subset.antisymm

Result:
case e_a.h₁
α : Type u_1
ι : Sort u_4
inst✝ : ConditionallyCompleteLattice α
p : ι → Prop
f : Subtype p → α
hp : ∀ (i : ι), p i
⊢ (range fun i => f ⟨i, ⋯⟩) ⊆ range f

case e_a.h₂
α : Type u_1
ι : Sort u_4
inst✝ : ConditionallyCompleteLattice α
p : ι → Prop
f : Subtype p → α
hp : ∀ (i : ι), p i
⊢ range f ⊆ range fun i => f ⟨i, ⋯⟩

Proof state:
α : Type u_1
ι : Sort u_4
inst✝ : ConditionallyCompleteLattice α
p : ι → Prop
f : Subtype p → α
hp : ∀ (i : ι), p i
⊢ ⨆ i, ⨆ (h : p i), f ⟨i, h⟩ = iSup f

Tactic:
simp only [hp, ciSup_unique]

Result:
α : Type u_1
ι : Sort u_4
inst✝ : ConditionallyCompleteLattice α
p : ι → Prop
f : Subtype p → α
hp : ∀ (i : ι), p i
⊢ ⨆ i, f ⟨i, ⋯⟩ = iSup f

Proof state:
case e_a.h₂
α : Type u_1
ι : Sort u_4
inst✝ : ConditionallyCompleteLattice α
p : ι → Prop
f : Subtype p → α
hp : ∀ (i : ι), p i
⊢ range f ⊆ range fun i => f ⟨i, ⋯⟩

Tactic:
rintro - ⟨i, rfl⟩

Result:
case e_a.h₂.intro
α : Type u_1
ι : Sort u_4
inst✝ : ConditionallyCompleteLattice α
p : ι → Prop
f : Subtype p → α
hp : ∀ (i : ι), p i
i : Subtype p
⊢ f i ∈ range fun i => f ⟨i, ⋯⟩

Proof state:
α : Type u_1
ι : Sort u_4
inst✝ : ConditionallyCompleteLattice α
p : ι → Prop
f : Subtype p → α
hp : ∀ (i : ι), p i
⊢ ⨆ i, f ⟨i, ⋯⟩ = iSup f

Tactic:
simp only [iSup]

Result:
α : Type u_1
ι : Sort u_4
inst✝ : ConditionallyCompleteLattice α
p : ι → Prop
f : Subtype p → α
hp : ∀ (i : ι), p i
⊢ sSup (range fun i => f ⟨i, ⋯⟩) = sSup (range f)

Proof state:
case e_a.h₁
α : Type u_1
ι : Sort u_4
inst✝ : ConditionallyCompleteLattice α
p : ι → Prop
f : Subtype p → α
hp : ∀ (i : ι), p i
⊢ (range fun i => f ⟨i, ⋯⟩) ⊆ range f

Tactic:
rintro - ⟨i, rfl⟩

Result:
case e_a.h₁.intro
α : Type u_1
ι : Sort u_4
inst✝ : ConditionallyCompleteLattice α
p : ι → Prop
f : Subtype p → α
hp : ∀ (i : ι), p i
i : ι
⊢ (fun i => f ⟨i, ⋯⟩) i ∈ range f

Proof state:
case e_a.h₁.intro
α : Type u_1
ι : Sort u_4
inst✝ : ConditionallyCompleteLattice α
p : ι → Prop
f : Subtype p → α
hp : ∀ (i : ι), p i
i : ι
⊢ (fun i => f ⟨i, ⋯⟩) i ∈ range f

Tactic:
simp [hp i]

Result:
no goals
-- Mathlib/Algebra/Homology/ShortComplex/HomologicalComplex.lean
@[reassoc]
lemma opcyclesMap_comp : opcyclesMap (φ ≫ ψ) i = opcyclesMap φ i ≫ opcyclesMap ψ i

Proof state:
C : Type u_1
inst✝⁴ : Category.{u_3, u_1} C
inst✝³ : HasZeroMorphisms C
ι : Type u_2
c : ComplexShape ι
K L M : HomologicalComplex C c
φ : K ⟶ L
ψ : L ⟶ M
i : ι
inst✝² : K.HasHomology i
inst✝¹ : L.HasHomology i
inst✝ : M.HasHomology i
⊢ opcyclesMap (φ ≫ ψ) i = opcyclesMap φ i ≫ opcyclesMap ψ i

Tactic:
dsimp [opcyclesMap]

Result:
C : Type u_1
inst✝⁴ : Category.{u_3, u_1} C
inst✝³ : HasZeroMorphisms C
ι : Type u_2
c : ComplexShape ι
K L M : HomologicalComplex C c
φ : K ⟶ L
ψ : L ⟶ M
i : ι
inst✝² : K.HasHomology i
inst✝¹ : L.HasHomology i
inst✝ : M.HasHomology i
⊢ ShortComplex.opcyclesMap ((shortComplexFunctor C c i).map (φ ≫ ψ)) =
    ShortComplex.opcyclesMap ((shortComplexFunctor C c i).map φ) ≫
      ShortComplex.opcyclesMap ((shortComplexFunctor C c i).map ψ)

Proof state:
C : Type u_1
inst✝⁴ : Category.{u_3, u_1} C
inst✝³ : HasZeroMorphisms C
ι : Type u_2
c : ComplexShape ι
K L M : HomologicalComplex C c
φ : K ⟶ L
ψ : L ⟶ M
i : ι
inst✝² : K.HasHomology i
inst✝¹ : L.HasHomology i
inst✝ : M.HasHomology i
⊢ ShortComplex.opcyclesMap ((shortComplexFunctor C c i).map (φ ≫ ψ)) =
    ShortComplex.opcyclesMap ((shortComplexFunctor C c i).map φ) ≫
      ShortComplex.opcyclesMap ((shortComplexFunctor C c i).map ψ)

Tactic:
rw [Functor.map_comp, ShortComplex.opcyclesMap_comp]

Result:
no goals
-- Mathlib/Algebra/Homology/HomotopyCategory/HomComplexShift.lean
@[simp]
lemma shift_zero (a : ℤ) :
    (0 : Cochain K L n).shift a = 0

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
K L : CochainComplex C ℤ
n a : ℤ
⊢ (shiftAddHom K L n a) 0 = 0

Tactic:
apply _root_.map_zero

Result:
no goals

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
K L : CochainComplex C ℤ
n a : ℤ
⊢ shift 0 a = 0

Tactic:
change shiftAddHom K L n a 0 = 0

Result:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
K L : CochainComplex C ℤ
n a : ℤ
⊢ (shiftAddHom K L n a) 0 = 0