harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Algebra/Homology/ShortComplex/LeftHomology.lean
lemma congr_φK {γ₁ γ₂ : LeftHomologyMapData φ h₁ h₂} (eq : γ₁ = γ₂) : γ₁.φK = γ₂.φK

Proof state:
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : HasZeroMorphisms C
S₁ S₂ : ShortComplex C
φ : S₁ ⟶ S₂
h₁ : S₁.LeftHomologyData
h₂ : S₂.LeftHomologyData
γ₁ γ₂ : LeftHomologyMapData φ h₁ h₂
eq : γ₁ = γ₂
⊢ γ₁.φK = γ₂.φK

Tactic:
rw [eq]

Result:
no goals
-- Mathlib/NumberTheory/Zsqrtd/Basic.lean
theorem not_divides_sq (x y) : (x + 1) * (x + 1) ≠ d * (y + 1) * (y + 1) := fun e => by
  have t := (divides_sq_eq_zero e).left
  contradiction

Proof state:
d : ℕ
dnsq : Nonsquare d
x y : ℕ
e : (x + 1) * (x + 1) = d * (y + 1) * (y + 1)
t : x + 1 = 0
⊢ False

Tactic:
contradiction

Result:
no goals

Proof state:
d : ℕ
dnsq : Nonsquare d
x y : ℕ
e : (x + 1) * (x + 1) = d * (y + 1) * (y + 1)
⊢ False

Tactic:
have t := (divides_sq_eq_zero e).left

Result:
d : ℕ
dnsq : Nonsquare d
x y : ℕ
e : (x + 1) * (x + 1) = d * (y + 1) * (y + 1)
t : x + 1 = 0
⊢ False
-- Mathlib/Probability/Process/Stopping.lean
theorem measurableSet_inter_le_const_iff (hτ : IsStoppingTime f τ) (s : Set Ω) (i : ι) :
    MeasurableSet[hτ.measurableSpace] (s ∩ {ω | τ ω ≤ i}) ↔
      MeasurableSet[(hτ.min_const i).measurableSpace] (s ∩ {ω | τ ω ≤ i})

Proof state:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝ : LinearOrder ι
f : Filtration ι m
τ : Ω → ι
hτ : IsStoppingTime f τ
s : Set Ω
i : ι
⊢ (∀ (i_1 : ι), MeasurableSet (s ∩ {ω | τ ω ≤ i} ∩ {ω | τ ω ≤ i_1})) ↔
    (∀ (i_1 : ι), MeasurableSet (s ∩ {ω | τ ω ≤ i} ∩ {ω | τ ω ≤ i_1})) ∧ MeasurableSet (s ∩ {ω | τ ω ≤ i})

Tactic:
refine ⟨fun h => ⟨h, ?_⟩, fun h j => h.1 j⟩

Result:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝ : LinearOrder ι
f : Filtration ι m
τ : Ω → ι
hτ : IsStoppingTime f τ
s : Set Ω
i : ι
h : ∀ (i_1 : ι), MeasurableSet (s ∩ {ω | τ ω ≤ i} ∩ {ω | τ ω ≤ i_1})
⊢ MeasurableSet (s ∩ {ω | τ ω ≤ i})

Proof state:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝ : LinearOrder ι
f : Filtration ι m
τ : Ω → ι
hτ : IsStoppingTime f τ
s : Set Ω
i : ι
h : MeasurableSet (s ∩ {ω | τ ω ≤ i} ∩ {ω | τ ω ≤ i})
⊢ MeasurableSet (s ∩ {ω | τ ω ≤ i})

Tactic:
rwa [Set.inter_assoc, Set.inter_self] at h

Result:
no goals

Proof state:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝ : LinearOrder ι
f : Filtration ι m
τ : Ω → ι
hτ : IsStoppingTime f τ
s : Set Ω
i : ι
⊢ MeasurableSet (s ∩ {ω | τ ω ≤ i}) ↔ MeasurableSet (s ∩ {ω | τ ω ≤ i})

Tactic:
rw [IsStoppingTime.measurableSet_min_iff hτ (isStoppingTime_const _ i),
  IsStoppingTime.measurableSpace_const, IsStoppingTime.measurableSet]

Result:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝ : LinearOrder ι
f : Filtration ι m
τ : Ω → ι
hτ : IsStoppingTime f τ
s : Set Ω
i : ι
⊢ (∀ (i_1 : ι), MeasurableSet (s ∩ {ω | τ ω ≤ i} ∩ {ω | τ ω ≤ i_1})) ↔
    (∀ (i_1 : ι), MeasurableSet (s ∩ {ω | τ ω ≤ i} ∩ {ω | τ ω ≤ i_1})) ∧ MeasurableSet (s ∩ {ω | τ ω ≤ i})

Proof state:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝ : LinearOrder ι
f : Filtration ι m
τ : Ω → ι
hτ : IsStoppingTime f τ
s : Set Ω
i : ι
h : ∀ (i_1 : ι), MeasurableSet (s ∩ {ω | τ ω ≤ i} ∩ {ω | τ ω ≤ i_1})
⊢ MeasurableSet (s ∩ {ω | τ ω ≤ i})

Tactic:
specialize h i

Result:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝ : LinearOrder ι
f : Filtration ι m
τ : Ω → ι
hτ : IsStoppingTime f τ
s : Set Ω
i : ι
h : MeasurableSet (s ∩ {ω | τ ω ≤ i} ∩ {ω | τ ω ≤ i})
⊢ MeasurableSet (s ∩ {ω | τ ω ≤ i})
-- Mathlib/CategoryTheory/CommSq.lean
theorem unop {W X Y Z : Cᵒᵖ} {f : W ⟶ X} {g : W ⟶ Y} {h : X ⟶ Z} {i : Y ⟶ Z} (p : CommSq f g h i) :
    CommSq i.unop h.unop g.unop f.unop :=
  ⟨by simp only [← unop_comp, p.w]⟩

Proof state:
C : Type u_1
inst✝ : Category.{u_2, u_1} C
W X Y Z : Cᵒᵖ
f : W ⟶ X
g : W ⟶ Y
h : X ⟶ Z
i : Y ⟶ Z
p : CommSq f g h i
⊢ i.unop ≫ g.unop = h.unop ≫ f.unop

Tactic:
simp only [← unop_comp, p.w]

Result:
no goals
-- Mathlib/LinearAlgebra/ExteriorPower/Pairing.lean
@[simp]
lemma toTensorPower_apply_ιMulti {n : ℕ} (v : Fin n → M) :
    toTensorPower R M n (ιMulti R n v) =
      ∑ σ : Perm (Fin n), Perm.sign σ • PiTensorProduct.tprod R (fun i ↦ v (σ i))

Proof state:
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
n : ℕ
v : Fin n → M
⊢ (toTensorPower R M n) ((ιMulti R n) v) = ∑ σ : Perm (Fin n), Perm.sign σ • (tprod R) fun i => v (σ i)

Tactic:
dsimp [toTensorPower]

Result:
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
n : ℕ
v : Fin n → M
⊢ (alternatingMapLinearEquiv (MultilinearMap.alternatization (tprod R))) ((ιMulti R n) v) =
    ∑ σ : Perm (Fin n), Perm.sign σ • (tprod R) fun i => v (σ i)

Proof state:
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
n : ℕ
v : Fin n → M
⊢ (alternatingMapLinearEquiv (MultilinearMap.alternatization (tprod R))) ((ιMulti R n) v) =
    ∑ σ : Perm (Fin n), Perm.sign σ • (tprod R) fun i => v (σ i)

Tactic:
simp only [alternatingMapLinearEquiv_apply_ιMulti,
  MultilinearMap.alternatization_apply, MultilinearMap.domDomCongr_apply]

Result:
no goals
-- Mathlib/LinearAlgebra/Determinant.lean
theorem det_toMatrix (b : Basis ι A M) (f : M →ₗ[A] M) :
    Matrix.det (toMatrix b b f) = LinearMap.det f

Proof state:
M : Type u_2
inst✝⁴ : AddCommGroup M
ι : Type u_4
inst✝³ : DecidableEq ι
inst✝² : Fintype ι
A : Type u_5
inst✝¹ : CommRing A
inst✝ : Module A M
b : Basis ι A M
f : M →ₗ[A] M
this : DecidableEq M
⊢ ((toMatrix b b) f).det = LinearMap.det f

Tactic:
rw [det_eq_det_toMatrix_of_finset b.reindexFinsetRange]

Result:
M : Type u_2
inst✝⁴ : AddCommGroup M
ι : Type u_4
inst✝³ : DecidableEq ι
inst✝² : Fintype ι
A : Type u_5
inst✝¹ : CommRing A
inst✝ : Module A M
b : Basis ι A M
f : M →ₗ[A] M
this : DecidableEq M
⊢ ((toMatrix b b) f).det = ((toMatrix b.reindexFinsetRange b.reindexFinsetRange) f).det

Proof state:
M : Type u_2
inst✝⁴ : AddCommGroup M
ι : Type u_4
inst✝³ : DecidableEq ι
inst✝² : Fintype ι
A : Type u_5
inst✝¹ : CommRing A
inst✝ : Module A M
b : Basis ι A M
f : M →ₗ[A] M
⊢ ((toMatrix b b) f).det = LinearMap.det f

Tactic:
haveI := Classical.decEq M

Result:
M : Type u_2
inst✝⁴ : AddCommGroup M
ι : Type u_4
inst✝³ : DecidableEq ι
inst✝² : Fintype ι
A : Type u_5
inst✝¹ : CommRing A
inst✝ : Module A M
b : Basis ι A M
f : M →ₗ[A] M
this : DecidableEq M
⊢ ((toMatrix b b) f).det = LinearMap.det f

Proof state:
M : Type u_2
inst✝⁴ : AddCommGroup M
ι : Type u_4
inst✝³ : DecidableEq ι
inst✝² : Fintype ι
A : Type u_5
inst✝¹ : CommRing A
inst✝ : Module A M
b : Basis ι A M
f : M →ₗ[A] M
this : DecidableEq M
⊢ ((toMatrix b b) f).det = ((toMatrix b.reindexFinsetRange b.reindexFinsetRange) f).det

Tactic:
apply det_toMatrix_eq_det_toMatrix b

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Subgraph.lean
theorem degree_spanningCoe {G' : G.Subgraph} (v : V) [Fintype (G'.neighborSet v)]
    [Fintype (G'.spanningCoe.neighborSet v)] : G'.spanningCoe.degree v = G'.degree v

Proof state:
V : Type u
G : SimpleGraph V
G' : G.Subgraph
v : V
inst✝¹ : Fintype ↑(G'.neighborSet v)
inst✝ : Fintype ↑(G'.spanningCoe.neighborSet v)
⊢ Fintype.card ↑(G'.spanningCoe.neighborSet v) = Fintype.card ↑(G'.neighborSet v)

Tactic:
congr!

Result:
no goals

Proof state:
V : Type u
G : SimpleGraph V
G' : G.Subgraph
v : V
inst✝¹ : Fintype ↑(G'.neighborSet v)
inst✝ : Fintype ↑(G'.spanningCoe.neighborSet v)
⊢ G'.spanningCoe.degree v = G'.degree v

Tactic:
rw [← card_neighborSet_eq_degree, Subgraph.degree]

Result:
V : Type u
G : SimpleGraph V
G' : G.Subgraph
v : V
inst✝¹ : Fintype ↑(G'.neighborSet v)
inst✝ : Fintype ↑(G'.spanningCoe.neighborSet v)
⊢ Fintype.card ↑(G'.spanningCoe.neighborSet v) = Fintype.card ↑(G'.neighborSet v)
-- Mathlib/Data/ZMod/Basic.lean
lemma zmod_smul_mem (hx : x ∈ K) : ∀ a : ZMod n, a • x ∈ K

Proof state:
n : ℕ
S : Type u_1
G : Type u_2
inst✝³ : AddCommGroup G
inst✝² : SetLike S G
inst✝¹ : AddSubgroupClass S G
K : S
inst✝ : Module (ZMod n) G
x : G
hx : x ∈ K
⊢ ∀ (a : ZMod n), a • x ∈ K

Tactic:
simpa [ZMod.forall, Int.cast_smul_eq_zsmul] using zsmul_mem hx

Result:
no goals
-- Mathlib/MeasureTheory/Function/LpSpace/Basic.lean
theorem cauchySeq_Lp_iff_cauchySeq_eLpNorm {ι} [Nonempty ι] [SemilatticeSup ι] [hp : Fact (1 ≤ p)]
    (f : ι → Lp E p μ) :
    CauchySeq f ↔ Tendsto (fun n : ι × ι => eLpNorm (⇑(f n.fst) - ⇑(f n.snd)) p μ) atTop (𝓝 0)

Proof state:
α : Type u_1
E : Type u_4
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝² : NormedAddCommGroup E
ι : Type u_7
inst✝¹ : Nonempty ι
inst✝ : SemilatticeSup ι
hp : Fact (1 ≤ p)
f : ι → ↥(Lp E p μ)
n : ι × ι
⊢ eLpNorm (↑↑(f n.1 - f n.2)) p μ ≠ ⊤

Tactic:
exact eLpNorm_ne_top _

Result:
no goals

Proof state:
α : Type u_1
E : Type u_4
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝² : NormedAddCommGroup E
ι : Type u_7
inst✝¹ : Nonempty ι
inst✝ : SemilatticeSup ι
hp : Fact (1 ≤ p)
f : ι → ↥(Lp E p μ)
n : ι × ι
⊢ eLpNorm (↑↑(f n.1) - ↑↑(f n.2)) p μ ≠ ⊤

Tactic:
rw [eLpNorm_congr_ae (Lp.coeFn_sub _ _).symm]

Result:
α : Type u_1
E : Type u_4
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝² : NormedAddCommGroup E
ι : Type u_7
inst✝¹ : Nonempty ι
inst✝ : SemilatticeSup ι
hp : Fact (1 ≤ p)
f : ι → ↥(Lp E p μ)
n : ι × ι
⊢ eLpNorm (↑↑(f n.1 - f n.2)) p μ ≠ ⊤

Proof state:
α : Type u_1
E : Type u_4
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝² : NormedAddCommGroup E
ι : Type u_7
inst✝¹ : Nonempty ι
inst✝ : SemilatticeSup ι
hp : Fact (1 ≤ p)
f : ι → ↥(Lp E p μ)
⊢ CauchySeq f ↔ Tendsto (fun n => eLpNorm (↑↑(f n.1) - ↑↑(f n.2)) p μ) atTop (𝓝 0)

Tactic:
simp_rw [cauchySeq_iff_tendsto_dist_atTop_0, dist_def]

Result:
α : Type u_1
E : Type u_4
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝² : NormedAddCommGroup E
ι : Type u_7
inst✝¹ : Nonempty ι
inst✝ : SemilatticeSup ι
hp : Fact (1 ≤ p)
f : ι → ↥(Lp E p μ)
⊢ Tendsto (fun n => (eLpNorm (↑↑(f n.1) - ↑↑(f n.2)) p μ).toReal) atTop (𝓝 0) ↔
    Tendsto (fun n => eLpNorm (↑↑(f n.1) - ↑↑(f n.2)) p μ) atTop (𝓝 0)

Proof state:
α : Type u_1
E : Type u_4
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝² : NormedAddCommGroup E
ι : Type u_7
inst✝¹ : Nonempty ι
inst✝ : SemilatticeSup ι
hp : Fact (1 ≤ p)
f : ι → ↥(Lp E p μ)
⊢ Tendsto (fun n => (eLpNorm (↑↑(f n.1) - ↑↑(f n.2)) p μ).toReal) atTop (𝓝 0) ↔
    Tendsto (fun n => eLpNorm (↑↑(f n.1) - ↑↑(f n.2)) p μ) atTop (𝓝 0)

Tactic:
rw [← ENNReal.zero_toReal, ENNReal.tendsto_toReal_iff (fun n => ?_) ENNReal.zero_ne_top]

Result:
α : Type u_1
E : Type u_4
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝² : NormedAddCommGroup E
ι : Type u_7
inst✝¹ : Nonempty ι
inst✝ : SemilatticeSup ι
hp : Fact (1 ≤ p)
f : ι → ↥(Lp E p μ)
n : ι × ι
⊢ eLpNorm (↑↑(f n.1) - ↑↑(f n.2)) p μ ≠ ⊤
-- Mathlib/SetTheory/Cardinal/Arithmetic.lean
theorem mul_le_max_of_aleph0_le_left {a b : Cardinal} (h : ℵ₀ ≤ a) : a * b ≤ max a b

Proof state:
case h.e'_4
a b : Cardinal.{u_1}
h : ℵ₀ ≤ a
⊢ ℵ₀ ≤ a ⊔ b

Tactic:
exact h.trans (le_max_left a b)

Result:
no goals

Proof state:
a b : Cardinal.{u_1}
h : ℵ₀ ≤ a
⊢ a * b ≤ a ⊔ b

Tactic:
convert mul_le_mul' (le_max_left a b) (le_max_right a b) using 1

Result:
case h.e'_4
a b : Cardinal.{u_1}
h : ℵ₀ ≤ a
⊢ a ⊔ b = (a ⊔ b) * (a ⊔ b)

Proof state:
case h.e'_4
a b : Cardinal.{u_1}
h : ℵ₀ ≤ a
⊢ a ⊔ b = (a ⊔ b) * (a ⊔ b)

Tactic:
rw [mul_eq_self]

Result:
case h.e'_4
a b : Cardinal.{u_1}
h : ℵ₀ ≤ a
⊢ ℵ₀ ≤ a ⊔ b
-- Mathlib/Algebra/Polynomial/Derivative.lean
theorem derivative_C_mul_X_pow (a : R) (n : ℕ) :
    derivative (C a * X ^ n) = C (a * n) * X ^ (n - 1)

Proof state:
R : Type u
inst✝ : Semiring R
a : R
n : ℕ
⊢ derivative (C a * X ^ n) = C (a * ↑n) * X ^ (n - 1)

Tactic:
rw [C_mul_X_pow_eq_monomial, C_mul_X_pow_eq_monomial, derivative_monomial]

Result:
no goals
-- Mathlib/Data/Sym/Sym2.lean
theorem mk_prod_swap_eq {p : α × α} : Sym2.mk p.swap = Sym2.mk p

Proof state:
α : Type u_1
p : α × α
⊢ Sym2.mk p.swap = Sym2.mk p

Tactic:
cases p

Result:
case mk
α : Type u_1
fst✝ snd✝ : α
⊢ Sym2.mk (fst✝, snd✝).swap = s(fst✝, snd✝)

Proof state:
case mk
α : Type u_1
fst✝ snd✝ : α
⊢ Sym2.mk (fst✝, snd✝).swap = s(fst✝, snd✝)

Tactic:
exact eq_swap

Result:
no goals
-- Mathlib/Data/Complex/Trigonometric.lean
theorem cos_neg : cos (-x) = cos x

Proof state:
x : ℝ
⊢ cos (-x) = cos x

Tactic:
simp [cos, exp_neg]

Result:
no goals
-- Mathlib/Control/Basic.lean
theorem seq_bind_eq (x : m α) {g : β → m γ} {f : α → β} :
    f <$> x >>= g = x >>= g ∘ f :=
  show bind (f <$> x) g = bind x (g ∘ f) by
    rw [← bind_pure_comp, bind_assoc]
    simp [pure_bind, Function.comp_def]

Proof state:
α β γ : Type u
m : Type u → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
x : m α
g : β → m γ
f : α → β
⊢ f <$> x >>= g = x >>= g ∘ f

Tactic:
rw [← bind_pure_comp, bind_assoc]

Result:
α β γ : Type u
m : Type u → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
x : m α
g : β → m γ
f : α → β
⊢ (x >>= fun x => pure (f x) >>= g) = x >>= g ∘ f

Proof state:
α β γ : Type u
m : Type u → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
x : m α
g : β → m γ
f : α → β
⊢ (x >>= fun x => pure (f x) >>= g) = x >>= g ∘ f

Tactic:
simp [pure_bind, Function.comp_def]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Fin/Lemmas.lean
theorem addCases_left {m n : Nat} {motive : Fin (m + n) → Sort _} {left right} (i : Fin m) :
    addCases (motive := motive) left right (Fin.castAdd n i) = left i

Proof state:
m n : Nat
motive : Fin (m + n) → Sort u_1
left : (i : Fin m) → motive (castAdd n i)
right : (i : Fin n) → motive (natAdd m i)
i : Fin m
⊢ ⋯ ▸ left ((castAdd n i).castLT ⋯) = left i

Tactic:
rfl

Result:
no goals

Proof state:
m n : Nat
motive : Fin (m + n) → Sort u_1
left : (i : Fin m) → motive (castAdd n i)
right : (i : Fin n) → motive (natAdd m i)
i : Fin m
⊢ addCases left right (castAdd n i) = left i

Tactic:
rw [addCases, dif_pos (castAdd_lt _ _)]

Result:
m n : Nat
motive : Fin (m + n) → Sort u_1
left : (i : Fin m) → motive (castAdd n i)
right : (i : Fin n) → motive (natAdd m i)
i : Fin m
⊢ ⋯ ▸ left ((castAdd n i).castLT ⋯) = left i
-- Mathlib/Data/Finset/Density.lean
@[norm_cast] lemma nnratCast_dens (s : Finset α) : (s.dens : 𝕜) = s.card / Fintype.card α

Proof state:
𝕜 : Type u_1
α : Type u_2
inst✝² : Fintype α
inst✝¹ : Semifield 𝕜
inst✝ : CharZero 𝕜
s : Finset α
⊢ ↑s.dens = ↑(#s) / ↑(Fintype.card α)

Tactic:
simp [dens]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem map_filterMap_some_eq_filterMap_isSome (f : α → Option β) (l : Array α) :
    (l.filterMap f).map some = (l.map f).filter fun b => b.isSome

Proof state:
α : Type u_1
β : Type u_2
f : α → Option β
l : Array α
⊢ map some (filterMap f l) = filter (fun b => b.isSome) (map f l)

Tactic:
cases l

Result:
case mk
α : Type u_1
β : Type u_2
f : α → Option β
toList✝ : List α
⊢ map some (filterMap f { toList := toList✝ }) = filter (fun b => b.isSome) (map f { toList := toList✝ })

Proof state:
case mk
α : Type u_1
β : Type u_2
f : α → Option β
toList✝ : List α
⊢ map some (filterMap f { toList := toList✝ }) = filter (fun b => b.isSome) (map f { toList := toList✝ })

Tactic:
simp [List.map_filterMap_some_eq_filter_map_isSome]

Result:
no goals
-- Mathlib/Topology/Order/LeftRightNhds.lean
theorem countable_setOf_isolated_right [SecondCountableTopology α] :
    { x : α | 𝓝[>] x = ⊥ }.Countable

Proof state:
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : SecondCountableTopology α
⊢ {x | 𝓝[>] x = ⊥}.Countable

Tactic:
simp only [nhdsGT_eq_bot_iff, setOf_or]

Result:
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : SecondCountableTopology α
⊢ ({a | IsTop a} ∪ {a | ∃ b, a ⋖ b}).Countable

Proof state:
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : SecondCountableTopology α
⊢ ({a | IsTop a} ∪ {a | ∃ b, a ⋖ b}).Countable

Tactic:
exact (subsingleton_isTop α).countable.union countable_setOf_covBy_right

Result:
no goals
-- Mathlib/CategoryTheory/Monoidal/Preadditive.lean
theorem biproduct_ι_comp_leftDistributor_inv {J : Type} [Fintype J] (X : C) (f : J → C) (j : J) :
    biproduct.ι _ j ≫ (leftDistributor X f).inv = X ◁ biproduct.ι _ j

Proof state:
C : Type u_1
inst✝⁵ : Category.{u_2, u_1} C
inst✝⁴ : Preadditive C
inst✝³ : MonoidalCategory C
inst✝² : MonoidalPreadditive C
inst✝¹ : HasFiniteBiproducts C
J : Type
inst✝ : Fintype J
X : C
f : J → C
j : J
⊢ biproduct.ι (fun j => X ⊗ f j) j ≫ (leftDistributor X f).inv = X ◁ biproduct.ι f j

Tactic:
simp [leftDistributor_inv, Preadditive.comp_sum, ← id_tensor_comp, biproduct.ι_π_assoc, dite_comp]

Result:
no goals

Proof state:
C : Type u_1
inst✝⁵ : Category.{u_2, u_1} C
inst✝⁴ : Preadditive C
inst✝³ : MonoidalCategory C
inst✝² : MonoidalPreadditive C
inst✝¹ : HasFiniteBiproducts C
J : Type
inst✝ : Fintype J
X : C
f : J → C
j : J
⊢ biproduct.ι (fun j => X ⊗ f j) j ≫ (leftDistributor X f).inv = X ◁ biproduct.ι f j

Tactic:
classical
simp [leftDistributor_inv, Preadditive.comp_sum, ← id_tensor_comp, biproduct.ι_π_assoc, dite_comp]

Result:
no goals
-- Mathlib/GroupTheory/GroupExtension/Basic.lean
theorem exists_mul_eq_inl_mul_mul : ∃ n : N, σ (g₁ * g₂) = S.inl n * σ g₁ * σ g₂

Proof state:
case h
N : Type u_1
G : Type u_2
inst✝² : Group N
inst✝¹ : Group G
E : Type u_3
inst✝ : Group E
S : GroupExtension N E G
σ : S.Section
g₁ g₂ : G
n : N
hn : S.inl n = σ g₁ * σ g₂ * (σ (g₁ * g₂))⁻¹
⊢ σ (g₁ * g₂) = S.inl n⁻¹ * σ g₁ * σ g₂

Tactic:
rw [mul_assoc, map_inv, eq_inv_mul_iff_mul_eq, ← eq_mul_inv_iff_mul_eq, hn]

Result:
no goals

Proof state:
case intro
N : Type u_1
G : Type u_2
inst✝² : Group N
inst✝¹ : Group G
E : Type u_3
inst✝ : Group E
S : GroupExtension N E G
σ : S.Section
g₁ g₂ : G
n : N
hn : S.inl n = σ g₁ * σ g₂ * (σ (g₁ * g₂))⁻¹
⊢ ∃ n, σ (g₁ * g₂) = S.inl n * σ g₁ * σ g₂

Tactic:
use n⁻¹

Result:
case h
N : Type u_1
G : Type u_2
inst✝² : Group N
inst✝¹ : Group G
E : Type u_3
inst✝ : Group E
S : GroupExtension N E G
σ : S.Section
g₁ g₂ : G
n : N
hn : S.inl n = σ g₁ * σ g₂ * (σ (g₁ * g₂))⁻¹
⊢ σ (g₁ * g₂) = S.inl n⁻¹ * σ g₁ * σ g₂

Proof state:
N : Type u_1
G : Type u_2
inst✝² : Group N
inst✝¹ : Group G
E : Type u_3
inst✝ : Group E
S : GroupExtension N E G
σ : S.Section
g₁ g₂ : G
⊢ ∃ n, σ (g₁ * g₂) = S.inl n * σ g₁ * σ g₂

Tactic:
obtain ⟨n, hn⟩ := mul_mul_mul_inv_mem_range_inl σ g₁ g₂

Result:
case intro
N : Type u_1
G : Type u_2
inst✝² : Group N
inst✝¹ : Group G
E : Type u_3
inst✝ : Group E
S : GroupExtension N E G
σ : S.Section
g₁ g₂ : G
n : N
hn : S.inl n = σ g₁ * σ g₂ * (σ (g₁ * g₂))⁻¹
⊢ ∃ n, σ (g₁ * g₂) = S.inl n * σ g₁ * σ g₂
-- Mathlib/CategoryTheory/FiberedCategory/Fibered.lean
/-- Alternate constructor for `IsFibered`, a functor `p : 𝒳 ⥤ 𝒴` is fibered if any diagram of the
form
```
          a
          -
          |
          v
R --f--> p(a)
```
admits a strongly cartesian lift `b ⟶ a` of `f`. -/
lemma of_exists_isStronglyCartesian {p : 𝒳 ⥤ 𝒮}
    (h : ∀ (a : 𝒳) (R : 𝒮) (f : R ⟶ p.obj a),
      ∃ (b : 𝒳) (φ : b ⟶ a), IsStronglyCartesian p f φ) :
    IsFibered p where
  exists_isCartesian'

Proof state:
𝒮 : Type u₁
𝒳 : Type u₂
inst✝¹ : Category.{v₁, u₁} 𝒮
inst✝ : Category.{v₂, u₂} 𝒳
p : 𝒳 ⥤ 𝒮
h : ∀ (a : 𝒳) (R : 𝒮) (f : R ⟶ p.obj a), ∃ b φ, p.IsStronglyCartesian f φ
a : 𝒳
R : 𝒮
f : R ⟶ p.obj a
⊢ ∃ b φ, p.IsCartesian f φ

Tactic:
obtain ⟨b, φ, hφ⟩ := h a R f

Result:
case intro.intro
𝒮 : Type u₁
𝒳 : Type u₂
inst✝¹ : Category.{v₁, u₁} 𝒮
inst✝ : Category.{v₂, u₂} 𝒳
p : 𝒳 ⥤ 𝒮
h : ∀ (a : 𝒳) (R : 𝒮) (f : R ⟶ p.obj a), ∃ b φ, p.IsStronglyCartesian f φ
a : 𝒳
R : 𝒮
f : R ⟶ p.obj a
b : 𝒳
φ : b ⟶ a
hφ : p.IsStronglyCartesian f φ
⊢ ∃ b φ, p.IsCartesian f φ

Proof state:
𝒮 : Type u₁
𝒳 : Type u₂
inst✝¹ : Category.{v₁, u₁} 𝒮
inst✝ : Category.{v₂, u₂} 𝒳
p : 𝒳 ⥤ 𝒮
h : ∀ (a : 𝒳) (R : 𝒮) (f : R ⟶ p.obj a), ∃ b φ, p.IsStronglyCartesian f φ
⊢ ∀ {a : 𝒳} {R : 𝒮} (f : R ⟶ p.obj a), ∃ b φ, p.IsCartesian f φ

Tactic:
intro a R f

Result:
𝒮 : Type u₁
𝒳 : Type u₂
inst✝¹ : Category.{v₁, u₁} 𝒮
inst✝ : Category.{v₂, u₂} 𝒳
p : 𝒳 ⥤ 𝒮
h : ∀ (a : 𝒳) (R : 𝒮) (f : R ⟶ p.obj a), ∃ b φ, p.IsStronglyCartesian f φ
a : 𝒳
R : 𝒮
f : R ⟶ p.obj a
⊢ ∃ b φ, p.IsCartesian f φ

Proof state:
case intro.intro
𝒮 : Type u₁
𝒳 : Type u₂
inst✝¹ : Category.{v₁, u₁} 𝒮
inst✝ : Category.{v₂, u₂} 𝒳
p : 𝒳 ⥤ 𝒮
h : ∀ (a : 𝒳) (R : 𝒮) (f : R ⟶ p.obj a), ∃ b φ, p.IsStronglyCartesian f φ
a : 𝒳
R : 𝒮
f : R ⟶ p.obj a
b : 𝒳
φ : b ⟶ a
hφ : p.IsStronglyCartesian f φ
⊢ ∃ b φ, p.IsCartesian f φ

Tactic:
refine ⟨b, φ, inferInstance⟩

Result:
no goals
-- Mathlib/Data/Stream/Init.lean
theorem head_drop (a : Stream' α) (n : ℕ) : (a.drop n).head = a.get n

Proof state:
α : Type u
a : Stream' α
n : ℕ
⊢ (drop n a).head = a.get n

Tactic:
simp

Result:
no goals
-- Mathlib/Probability/Kernel/Basic.lean
/-- See `swap_apply'` for a fully applied version of this lemma. -/
lemma swap_apply (ab : α × β) : swap α β ab = Measure.dirac ab.swap

Proof state:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
ab : α × β
⊢ (swap α β) ab = Measure.dirac ab.swap

Tactic:
rw [swap, deterministic_apply]

Result:
no goals
-- Mathlib/LinearAlgebra/TensorProduct/Matrix.lean
theorem TensorProduct.toMatrix_comm :
    toMatrix (bM.tensorProduct bN) (bN.tensorProduct bM) (TensorProduct.comm R M N) =
      (1 : Matrix (ι × κ) (ι × κ) R).submatrix Prod.swap _root_.id

Proof state:
case a.mk.mk
R : Type u_1
M : Type u_2
N : Type u_3
ι : Type u_7
κ : Type u_8
inst✝⁸ : DecidableEq ι
inst✝⁷ : DecidableEq κ
inst✝⁶ : Fintype ι
inst✝⁵ : Fintype κ
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup N
inst✝¹ : Module R M
inst✝ : Module R N
bM : Basis ι R M
bN : Basis κ R N
i : κ
j i' : ι
j' : κ
⊢ (toMatrix (bM.tensorProduct bN) (bN.tensorProduct bM)) ↑(TensorProduct.comm R M N) (i, j) (i', j') =
    submatrix 1 Prod.swap _root_.id (i, j) (i', j')

Tactic:
simp only [toMatrix_apply, Basis.tensorProduct_apply, LinearEquiv.coe_coe, comm_tmul,
  Basis.tensorProduct_repr_tmul_apply, Basis.repr_self, Finsupp.single_apply, @eq_comm _ i',
  @eq_comm _ j', smul_eq_mul, mul_ite, mul_one, mul_zero, ← ite_and, and_comm, submatrix_apply,
  Matrix.one_apply, Prod.swap_prod_mk, id_eq, Prod.mk.injEq]

Result:
no goals

Proof state:
R : Type u_1
M : Type u_2
N : Type u_3
ι : Type u_7
κ : Type u_8
inst✝⁸ : DecidableEq ι
inst✝⁷ : DecidableEq κ
inst✝⁶ : Fintype ι
inst✝⁵ : Fintype κ
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup N
inst✝¹ : Module R M
inst✝ : Module R N
bM : Basis ι R M
bN : Basis κ R N
⊢ (toMatrix (bM.tensorProduct bN) (bN.tensorProduct bM)) ↑(TensorProduct.comm R M N) = submatrix 1 Prod.swap _root_.id

Tactic:
ext ⟨i, j⟩ ⟨i', j'⟩

Result:
case a.mk.mk
R : Type u_1
M : Type u_2
N : Type u_3
ι : Type u_7
κ : Type u_8
inst✝⁸ : DecidableEq ι
inst✝⁷ : DecidableEq κ
inst✝⁶ : Fintype ι
inst✝⁵ : Fintype κ
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup N
inst✝¹ : Module R M
inst✝ : Module R N
bM : Basis ι R M
bN : Basis κ R N
i : κ
j i' : ι
j' : κ
⊢ (toMatrix (bM.tensorProduct bN) (bN.tensorProduct bM)) ↑(TensorProduct.comm R M N) (i, j) (i', j') =
    submatrix 1 Prod.swap _root_.id (i, j) (i', j')
-- Mathlib/Order/RelClasses.lean
theorem IsOrderConnected.neg_trans {r : α → α → Prop} [IsOrderConnected α r] {a b c}
    (h₁ : ¬r a b) (h₂ : ¬r b c) : ¬r a c :=
  mt (IsOrderConnected.conn a b c) <| by simp [h₁, h₂]

Proof state:
α : Type u
r : α → α → Prop
inst✝ : IsOrderConnected α r
a b c : α
h₁ : ¬r a b
h₂ : ¬r b c
⊢ ¬(r a b ∨ r b c)

Tactic:
simp [h₁, h₂]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/Raw.lean
theorem filter_val [BEq α] [Hashable α] {m : Raw₀ α β} {f : (a : α) → β a → Bool} :
    m.val.filter f = m.filter f

Proof state:
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : Hashable α
m : Raw₀ α β
f : (a : α) → β a → Bool
⊢ Raw.filter f m.val = (Raw₀.filter f m).val

Tactic:
simp [Raw.filter, m.2]

Result:
no goals
-- Mathlib/Data/Set/Card.lean
theorem ncard_eq_toFinset_card' (s : Set α) [Fintype s] :
    s.ncard = s.toFinset.card

Proof state:
α : Type u_1
s : Set α
inst✝ : Fintype ↑s
⊢ s.ncard = s.toFinset.card

Tactic:
simp [← Nat.card_coe_set_eq, Nat.card_eq_fintype_card]

Result:
no goals