harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Topology/Separation/Hausdorff.lean
theorem SeparationQuotient.t2Space_iff : T2Space (SeparationQuotient X) ↔ R1Space X

Proof state:
X : Type u_1
inst✝ : TopologicalSpace X
⊢ T2Space (SeparationQuotient X) ↔ R1Space X

Tactic:
simp only [t2Space_iff_disjoint_nhds, Pairwise, surjective_mk.forall₂, ne_eq, mk_eq_mk,
  r1Space_iff_inseparable_or_disjoint_nhds, ← disjoint_comap_iff surjective_mk, comap_mk_nhds_mk,
  ← or_iff_not_imp_left]

Result:
no goals
-- Mathlib/LinearAlgebra/Matrix/Charpoly/LinearMap.lean
theorem Matrix.isRepresentation.toEnd_exists_mem_ideal (f : Module.End R M) (I : Ideal R)
    (hI : LinearMap.range f ≤ I • ⊤) :
    ∃ M, Matrix.isRepresentation.toEnd R b hb M = f ∧ ∀ i j, M.1 i j ∈ I

Proof state:
ι : Type u_1
inst✝⁴ : Fintype ι
M : Type u_2
inst✝³ : AddCommGroup M
R : Type u_3
inst✝² : CommRing R
inst✝¹ : Module R M
b : ι → M
inst✝ : DecidableEq ι
hb : Submodule.span R (Set.range b) = ⊤
f : Module.End R M
I : Ideal R
hI : LinearMap.range f ≤ I • ⊤
bM' : M → ι →₀ ↥I
hbM' : ∀ (x : M), (Ideal.finsuppTotal ι M I b) (bM' x) = f x
A : Matrix ι ι R := fun i j => ↑((bM' (b j)) i)
this : Represents b A f
⊢ ∃ M_1, (toEnd R b hb) M_1 = f ∧ ∀ (i j : ι), ↑M_1 i j ∈ I

Tactic:
exact
  ⟨⟨A, f, this⟩, Matrix.isRepresentation.eq_toEnd_of_represents R b hb ⟨A, f, this⟩ this,
    fun i j => (bM' (b j) i).prop⟩

Result:
no goals

Proof state:
ι : Type u_1
inst✝⁴ : Fintype ι
M : Type u_2
inst✝³ : AddCommGroup M
R : Type u_3
inst✝² : CommRing R
inst✝¹ : Module R M
b : ι → M
inst✝ : DecidableEq ι
hb : Submodule.span R (Set.range b) = ⊤
f : Module.End R M
I : Ideal R
hI : LinearMap.range f ≤ I • ⊤
⊢ ∀ (x : M), f x ∈ LinearMap.range (Ideal.finsuppTotal ι M I b)

Tactic:
rw [Ideal.range_finsuppTotal, hb]

Result:
ι : Type u_1
inst✝⁴ : Fintype ι
M : Type u_2
inst✝³ : AddCommGroup M
R : Type u_3
inst✝² : CommRing R
inst✝¹ : Module R M
b : ι → M
inst✝ : DecidableEq ι
hb : Submodule.span R (Set.range b) = ⊤
f : Module.End R M
I : Ideal R
hI : LinearMap.range f ≤ I • ⊤
⊢ ∀ (x : M), f x ∈ I • ⊤

Proof state:
ι : Type u_1
inst✝⁴ : Fintype ι
M : Type u_2
inst✝³ : AddCommGroup M
R : Type u_3
inst✝² : CommRing R
inst✝¹ : Module R M
b : ι → M
inst✝ : DecidableEq ι
hb : Submodule.span R (Set.range b) = ⊤
f : Module.End R M
I : Ideal R
hI : LinearMap.range f ≤ I • ⊤
bM' : M → ι →₀ ↥I
hbM' : ∀ (x : M), (Ideal.finsuppTotal ι M I b) (bM' x) = f x
A : Matrix ι ι R := fun i j => ↑((bM' (b j)) i)
⊢ Represents b A f

Tactic:
rw [Matrix.represents_iff']

Result:
ι : Type u_1
inst✝⁴ : Fintype ι
M : Type u_2
inst✝³ : AddCommGroup M
R : Type u_3
inst✝² : CommRing R
inst✝¹ : Module R M
b : ι → M
inst✝ : DecidableEq ι
hb : Submodule.span R (Set.range b) = ⊤
f : Module.End R M
I : Ideal R
hI : LinearMap.range f ≤ I • ⊤
bM' : M → ι →₀ ↥I
hbM' : ∀ (x : M), (Ideal.finsuppTotal ι M I b) (bM' x) = f x
A : Matrix ι ι R := fun i j => ↑((bM' (b j)) i)
⊢ ∀ (j : ι), ∑ i : ι, A i j • b i = f (b j)
-- Mathlib/Algebra/Order/Floor.lean
theorem fract_add (a b : α) : ∃ z : ℤ, fract (a + b) - fract a - fract b = z :=
  ⟨⌊a⌋ + ⌊b⌋ - ⌊a + b⌋, by
    unfold fract
    simp only [sub_eq_add_neg, neg_add_rev, neg_neg, cast_add, cast_neg]
    abel⟩

Proof state:
α : Type u_2
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
a b : α
⊢ a + b + -↑⌊a + b⌋ + (↑⌊a⌋ + -a) + (↑⌊b⌋ + -b) = ↑⌊a⌋ + ↑⌊b⌋ + -↑⌊a + b⌋

Tactic:
abel

Result:
no goals

Proof state:
α : Type u_2
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
a b : α
⊢ a + b - ↑⌊a + b⌋ - (a - ↑⌊a⌋) - (b - ↑⌊b⌋) = ↑(⌊a⌋ + ⌊b⌋ - ⌊a + b⌋)

Tactic:
simp only [sub_eq_add_neg, neg_add_rev, neg_neg, cast_add, cast_neg]

Result:
α : Type u_2
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
a b : α
⊢ a + b + -↑⌊a + b⌋ + (↑⌊a⌋ + -a) + (↑⌊b⌋ + -b) = ↑⌊a⌋ + ↑⌊b⌋ + -↑⌊a + b⌋

Proof state:
α : Type u_2
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
a b : α
⊢ fract (a + b) - fract a - fract b = ↑(⌊a⌋ + ⌊b⌋ - ⌊a + b⌋)

Tactic:
unfold fract

Result:
α : Type u_2
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
a b : α
⊢ a + b - ↑⌊a + b⌋ - (a - ↑⌊a⌋) - (b - ↑⌊b⌋) = ↑(⌊a⌋ + ⌊b⌋ - ⌊a + b⌋)
-- Mathlib/Algebra/GroupWithZero/Indicator.lean
lemma inter_indicator_one : (s ∩ t).indicator (1 : ι → M₀) = s.indicator 1 * t.indicator 1 :=
  funext fun _ ↦ by simp only [← inter_indicator_mul, Pi.mul_apply, Pi.one_apply, one_mul]; congr

Proof state:
ι : Type u_1
M₀ : Type u_4
inst✝ : MulZeroOneClass M₀
s t : Set ι
x✝ : ι
⊢ (s ∩ t).indicator 1 x✝ = (s ∩ t).indicator (fun j => 1) x✝

Tactic:
congr

Result:
no goals

Proof state:
ι : Type u_1
M₀ : Type u_4
inst✝ : MulZeroOneClass M₀
s t : Set ι
x✝ : ι
⊢ (s ∩ t).indicator 1 x✝ = (s.indicator 1 * t.indicator 1) x✝

Tactic:
simp only [← inter_indicator_mul, Pi.mul_apply, Pi.one_apply, one_mul]

Result:
ι : Type u_1
M₀ : Type u_4
inst✝ : MulZeroOneClass M₀
s t : Set ι
x✝ : ι
⊢ (s ∩ t).indicator 1 x✝ = (s ∩ t).indicator (fun j => 1) x✝
-- Mathlib/Analysis/Convex/Side.lean
theorem wSameSide_iff_exists_left {s : AffineSubspace R P} {x y p₁ : P} (h : p₁ ∈ s) :
    s.WSameSide x y ↔ x ∈ s ∨ ∃ p₂ ∈ s, SameRay R (x -ᵥ p₁) (y -ᵥ p₂)

Proof state:
case mpr
R : Type u_1
V : Type u_2
P : Type u_4
inst✝³ : LinearOrderedField R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
s : AffineSubspace R P
x y p₁ : P
h : p₁ ∈ s
⊢ (x ∈ s ∨ ∃ p₂ ∈ s, SameRay R (x -ᵥ p₁) (y -ᵥ p₂)) → s.WSameSide x y

Tactic:
rintro (h' | ⟨h₁, h₂, h₃⟩)

Result:
case mpr.inl
R : Type u_1
V : Type u_2
P : Type u_4
inst✝³ : LinearOrderedField R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
s : AffineSubspace R P
x y p₁ : P
h : p₁ ∈ s
h' : x ∈ s
⊢ s.WSameSide x y

case mpr.inr.intro.intro
R : Type u_1
V : Type u_2
P : Type u_4
inst✝³ : LinearOrderedField R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
s : AffineSubspace R P
x y p₁ : P
h : p₁ ∈ s
h₁ : P
h₂ : h₁ ∈ s
h₃ : SameRay R (x -ᵥ p₁) (y -ᵥ h₁)
⊢ s.WSameSide x y

Proof state:
case mp.intro.intro.intro.intro.inl
R : Type u_1
V : Type u_2
P : Type u_4
inst✝³ : LinearOrderedField R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
s : AffineSubspace R P
x y p₁ : P
h : p₁ ∈ s
p₁' : P
hp₁' : p₁' ∈ s
p₂' : P
hp₂' : p₂' ∈ s
h0 : x -ᵥ p₁' = 0
⊢ x ∈ s ∨ ∃ p₂ ∈ s, SameRay R (x -ᵥ p₁) (y -ᵥ p₂)

Tactic:
rw [vsub_eq_zero_iff_eq] at h0

Result:
case mp.intro.intro.intro.intro.inl
R : Type u_1
V : Type u_2
P : Type u_4
inst✝³ : LinearOrderedField R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
s : AffineSubspace R P
x y p₁ : P
h : p₁ ∈ s
p₁' : P
hp₁' : p₁' ∈ s
p₂' : P
hp₂' : p₂' ∈ s
h0 : x = p₁'
⊢ x ∈ s ∨ ∃ p₂ ∈ s, SameRay R (x -ᵥ p₁) (y -ᵥ p₂)

Proof state:
case mpr.inl
R : Type u_1
V : Type u_2
P : Type u_4
inst✝³ : LinearOrderedField R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
s : AffineSubspace R P
x y p₁ : P
h : p₁ ∈ s
h' : x ∈ s
⊢ s.WSameSide x y

Tactic:
exact wSameSide_of_left_mem y h'

Result:
no goals
-- Mathlib/LinearAlgebra/Dimension/Free.lean
/-- See `rank_lt_aleph0` for the inverse direction without `Module.Free R M`. -/
lemma rank_lt_aleph0_iff : Module.rank R M < ℵ₀ ↔ Module.Finite R M

Proof state:
R : Type u
M : Type v
inst✝⁴ : Semiring R
inst✝³ : StrongRankCondition R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Free R M
⊢ Module.rank R M < ℵ₀ ↔ Module.Finite R M

Tactic:
rw [Free.rank_eq_card_chooseBasisIndex, mk_lt_aleph0_iff]

Result:
R : Type u
M : Type v
inst✝⁴ : Semiring R
inst✝³ : StrongRankCondition R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Free R M
⊢ Finite (ChooseBasisIndex R M) ↔ Module.Finite R M

Proof state:
R : Type u
M : Type v
inst✝⁴ : Semiring R
inst✝³ : StrongRankCondition R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Free R M
⊢ Finite (ChooseBasisIndex R M) ↔ Module.Finite R M

Tactic:
exact ⟨fun h ↦ Finite.of_basis (Free.chooseBasis R M),
  fun I ↦ Finite.of_fintype (Free.ChooseBasisIndex R M)⟩

Result:
no goals
-- Mathlib/Algebra/Polynomial/Eval/Defs.lean
theorem comp_assoc {R : Type*} [CommSemiring R] (φ ψ χ : R[X]) :
    (φ.comp ψ).comp χ = φ.comp (ψ.comp χ)

Proof state:
case refine_3
R : Type u_1
inst✝ : CommSemiring R
φ ψ χ : R[X]
n✝ : ℕ
a✝¹ : R
a✝ : ((C a✝¹ * X ^ n✝).comp ψ).comp χ = (C a✝¹ * X ^ n✝).comp (ψ.comp χ)
⊢ ((C a✝¹ * X ^ (n✝ + 1)).comp ψ).comp χ = (C a✝¹ * X ^ (n✝ + 1)).comp (ψ.comp χ)

Tactic:
simp_all only [add_comp, mul_comp, C_comp, X_comp, pow_succ, ← mul_assoc]

Result:
no goals

Proof state:
case refine_3
R : Type u_1
inst✝ : CommSemiring R
φ ψ χ : R[X]
⊢ ∀ (n : ℕ) (a : R),
    ((C a * X ^ n).comp ψ).comp χ = (C a * X ^ n).comp (ψ.comp χ) →
      ((C a * X ^ (n + 1)).comp ψ).comp χ = (C a * X ^ (n + 1)).comp (ψ.comp χ)

Tactic:
intros

Result:
case refine_3
R : Type u_1
inst✝ : CommSemiring R
φ ψ χ : R[X]
n✝ : ℕ
a✝¹ : R
a✝ : ((C a✝¹ * X ^ n✝).comp ψ).comp χ = (C a✝¹ * X ^ n✝).comp (ψ.comp χ)
⊢ ((C a✝¹ * X ^ (n✝ + 1)).comp ψ).comp χ = (C a✝¹ * X ^ (n✝ + 1)).comp (ψ.comp χ)
-- Mathlib/RingTheory/LocalRing/ResidueField/Basic.lean
theorem isLocalHom_residue : IsLocalHom (IsLocalRing.residue R)

Proof state:
case map_nonunit
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsLocalRing R
⊢ ∀ (a : R), IsUnit ((residue R) a) → IsUnit a

Tactic:
intro a ha

Result:
case map_nonunit
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsLocalRing R
a : R
ha : IsUnit ((residue R) a)
⊢ IsUnit a

Proof state:
case map_nonunit
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsLocalRing R
a : R
ha : IsUnit 0
h : ¬IsUnit a
⊢ False

Tactic:
exact ha.ne_zero rfl

Result:
no goals

Proof state:
case map_nonunit
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsLocalRing R
a : R
ha : IsUnit ((residue R) a)
⊢ IsUnit a

Tactic:
by_contra h

Result:
case map_nonunit
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsLocalRing R
a : R
ha : IsUnit ((residue R) a)
h : ¬IsUnit a
⊢ False

Proof state:
case map_nonunit
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsLocalRing R
a : R
ha : IsUnit ((residue R) a)
h : ¬IsUnit a
⊢ False

Tactic:
erw [Ideal.Quotient.eq_zero_iff_mem.mpr ((IsLocalRing.mem_maximalIdeal _).mpr h)] at ha

Result:
case map_nonunit
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsLocalRing R
a : R
ha : IsUnit 0
h : ¬IsUnit a
⊢ False

Proof state:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsLocalRing R
⊢ IsLocalHom (residue R)

Tactic:
constructor

Result:
case map_nonunit
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsLocalRing R
⊢ ∀ (a : R), IsUnit ((residue R) a) → IsUnit a
-- Mathlib/Algebra/EuclideanDomain/Basic.lean
theorem gcd_mul_lcm (x y : R) : gcd x y * lcm x y = x * y

Proof state:
R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
x y : R
⊢ gcd x y * lcm x y = x * y

Tactic:
rw [lcm]

Result:
R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
x y : R
⊢ gcd x y * (x * y / gcd x y) = x * y

Proof state:
case neg.intro.intro.intro
R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
x y r s : R
hs : y = gcd x y * s
g : R
h : ¬g = 0
hr : x = g * r
⊢ g * (x * y / g) = x * y

Tactic:
subst hr

Result:
case neg.intro.intro.intro
R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
y r s g : R
h : ¬g = 0
hs : y = gcd (g * r) y * s
⊢ g * (g * r * y / g) = g * r * y

Proof state:
case neg.intro.intro.intro
R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
x y : R
h : ¬gcd x y = 0
r : R
hr : x = gcd x y * r
s : R
hs : y = gcd x y * s
⊢ gcd x y * (x * y / gcd x y) = x * y

Tactic:
generalize gcd x y = g at h hr ⊢

Result:
case neg.intro.intro.intro
R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
x y r s : R
hs : y = gcd x y * s
g : R
h : ¬g = 0
hr : x = g * r
⊢ g * (x * y / g) = x * y

Proof state:
case pos
R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
x y : R
h : gcd x y = 0
⊢ gcd x y * (x * y / gcd x y) = x * y

Tactic:
rw [h, zero_mul]

Result:
case pos
R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
x y : R
h : gcd x y = 0
⊢ 0 = x * y

Proof state:
case neg.intro.intro.intro
R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
y r s g : R
h : ¬g = 0
hs : y = gcd (g * r) y * s
⊢ g * (g * r * y / g) = g * r * y

Tactic:
rw [mul_assoc, mul_div_cancel_left₀ _ h]

Result:
no goals

Proof state:
case pos
R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
x y : R
h : x = 0 ∧ y = 0
⊢ 0 = x * y

Tactic:
rw [h.1, zero_mul]

Result:
no goals

Proof state:
case pos
R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
x y : R
h : gcd x y = 0
⊢ 0 = x * y

Tactic:
rw [EuclideanDomain.gcd_eq_zero_iff] at h

Result:
case pos
R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
x y : R
h : x = 0 ∧ y = 0
⊢ 0 = x * y

Proof state:
case neg
R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
x y : R
h : ¬gcd x y = 0
⊢ gcd x y * (x * y / gcd x y) = x * y

Tactic:
rcases gcd_dvd x y with ⟨⟨r, hr⟩, ⟨s, hs⟩⟩

Result:
case neg.intro.intro.intro
R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
x y : R
h : ¬gcd x y = 0
r : R
hr : x = gcd x y * r
s : R
hs : y = gcd x y * s
⊢ gcd x y * (x * y / gcd x y) = x * y

Proof state:
R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
x y : R
⊢ gcd x y * (x * y / gcd x y) = x * y

Tactic:
by_cases h : gcd x y = 0

Result:
case pos
R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
x y : R
h : gcd x y = 0
⊢ gcd x y * (x * y / gcd x y) = x * y

case neg
R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
x y : R
h : ¬gcd x y = 0
⊢ gcd x y * (x * y / gcd x y) = x * y
-- Mathlib/AlgebraicTopology/SimplicialSet/NerveAdjunction.lean
lemma toNerve₂.mk_naturality_σ1i (i : Fin 2) : toNerve₂.mk.naturalityProperty F (σ₂ i)

Proof state:
case e_g
C : Type u
inst✝ : SmallCategory C
X : SSet.Truncated 2
F : oneTruncation₂.obj X ⟶ ReflQuiv.of C
hyp : ∀ (φ : X.obj (op { obj := [2], property := ⋯ })), F.map (ev02₂ φ) = F.map (ev01₂ φ) ≫ F.map (ev12₂ φ)
i : Fin 2
⊢ X.map (σ₂ i ⋯ ⋯).op ≫
      mk.app F { obj := [1 + 1], property := ⋯ } ≫
        (nerveFunctor₂.obj (Cat.of C)).map (δ₂ 0 δ0₂.proof_2 δ0₂.proof_3).op =
    mk.app F { obj := [1], property := ⋯ } ≫
      (nerveFunctor₂.obj (Cat.of C)).map (δ₂ 0 δ0₂.proof_2 δ0₂.proof_3 ≫ σ₂ i ⋯ ⋯).op

Tactic:
rw [← toNerve₂.mk_naturality_δ1i F hyp, ← assoc, ← map_comp, ← op_comp]

Result:
case e_g
C : Type u
inst✝ : SmallCategory C
X : SSet.Truncated 2
F : oneTruncation₂.obj X ⟶ ReflQuiv.of C
hyp : ∀ (φ : X.obj (op { obj := [2], property := ⋯ })), F.map (ev02₂ φ) = F.map (ev01₂ φ) ≫ F.map (ev12₂ φ)
i : Fin 2
⊢ X.map (δ₂ 0 ⋯ ⋯ ≫ σ₂ i ⋯ ⋯).op ≫ (fun n => mk.app F (unop n)) (op { obj := [1], property := ⋯ }) =
    mk.app F { obj := [1], property := ⋯ } ≫
      (nerveFunctor₂.obj (Cat.of C)).map (δ₂ 0 δ0₂.proof_2 δ0₂.proof_3 ≫ σ₂ i ⋯ ⋯).op
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Sublist.lean
theorem isPrefix_filterMap_iff {β} {f : α → Option β} {l₁ : List α} {l₂ : List β} :
    l₂ <+: filterMap f l₁ ↔ ∃ l, l <+: l₁ ∧ l₂ = filterMap f l

Proof state:
case mp
α : Type u_1
β : Type u_2
f : α → Option β
l₁ : List α
l₂ : List β
⊢ (∃ t l₁_1 l₂_1, l₁ = l₁_1 ++ l₂_1 ∧ filterMap f l₁_1 = l₂ ∧ filterMap f l₂_1 = t) →
    ∃ l, (∃ t, l ++ t = l₁) ∧ l₂ = filterMap f l

Tactic:
rintro ⟨_, l₁, l₂, rfl, rfl, rfl⟩

Result:
case mp.intro.intro.intro.intro.intro
α : Type u_1
β : Type u_2
f : α → Option β
l₁ l₂ : List α
⊢ ∃ l, (∃ t, l ++ t = l₁ ++ l₂) ∧ filterMap f l₁ = filterMap f l

Proof state:
case mpr
α : Type u_1
β : Type u_2
f : α → Option β
l₁ : List α
l₂ : List β
⊢ (∃ l, (∃ t, l ++ t = l₁) ∧ l₂ = filterMap f l) →
    ∃ t l₁_1 l₂_1, l₁ = l₁_1 ++ l₂_1 ∧ filterMap f l₁_1 = l₂ ∧ filterMap f l₂_1 = t

Tactic:
rintro ⟨l₁, ⟨l₂, rfl⟩, rfl⟩

Result:
case mpr.intro.intro.intro
α : Type u_1
β : Type u_2
f : α → Option β
l₁ l₂ : List α
⊢ ∃ t l₁_1 l₂_1, l₁ ++ l₂ = l₁_1 ++ l₂_1 ∧ filterMap f l₁_1 = filterMap f l₁ ∧ filterMap f l₂_1 = t

Proof state:
α : Type u_1
β : Type u_2
f : α → Option β
l₁ : List α
l₂ : List β
⊢ l₂ <+: filterMap f l₁ ↔ ∃ l, l <+: l₁ ∧ l₂ = filterMap f l

Tactic:
simp only [IsPrefix, append_eq_filterMap_iff]

Result:
α : Type u_1
β : Type u_2
f : α → Option β
l₁ : List α
l₂ : List β
⊢ (∃ t l₁_1 l₂_1, l₁ = l₁_1 ++ l₂_1 ∧ filterMap f l₁_1 = l₂ ∧ filterMap f l₂_1 = t) ↔
    ∃ l, (∃ t, l ++ t = l₁) ∧ l₂ = filterMap f l

Proof state:
case mp.intro.intro.intro.intro.intro
α : Type u_1
β : Type u_2
f : α → Option β
l₁ l₂ : List α
⊢ ∃ l, (∃ t, l ++ t = l₁ ++ l₂) ∧ filterMap f l₁ = filterMap f l

Tactic:
exact ⟨l₁, ⟨l₂, rfl⟩, rfl⟩

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
f : α → Option β
l₁ : List α
l₂ : List β
⊢ (∃ t l₁_1 l₂_1, l₁ = l₁_1 ++ l₂_1 ∧ filterMap f l₁_1 = l₂ ∧ filterMap f l₂_1 = t) ↔
    ∃ l, (∃ t, l ++ t = l₁) ∧ l₂ = filterMap f l

Tactic:
constructor

Result:
case mp
α : Type u_1
β : Type u_2
f : α → Option β
l₁ : List α
l₂ : List β
⊢ (∃ t l₁_1 l₂_1, l₁ = l₁_1 ++ l₂_1 ∧ filterMap f l₁_1 = l₂ ∧ filterMap f l₂_1 = t) →
    ∃ l, (∃ t, l ++ t = l₁) ∧ l₂ = filterMap f l

case mpr
α : Type u_1
β : Type u_2
f : α → Option β
l₁ : List α
l₂ : List β
⊢ (∃ l, (∃ t, l ++ t = l₁) ∧ l₂ = filterMap f l) →
    ∃ t l₁_1 l₂_1, l₁ = l₁_1 ++ l₂_1 ∧ filterMap f l₁_1 = l₂ ∧ filterMap f l₂_1 = t

Proof state:
case mpr.intro.intro.intro
α : Type u_1
β : Type u_2
f : α → Option β
l₁ l₂ : List α
⊢ ∃ t l₁_1 l₂_1, l₁ ++ l₂ = l₁_1 ++ l₂_1 ∧ filterMap f l₁_1 = filterMap f l₁ ∧ filterMap f l₂_1 = t

Tactic:
exact ⟨_, l₁, l₂, rfl, rfl, rfl⟩

Result:
no goals
-- Mathlib/CategoryTheory/Closed/Cartesian.lean
theorem curry_id_eq_coev (A X : C) [Exponentiable A] : curry (𝟙 _) = (exp.coev A).app X

Proof state:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : ChosenFiniteProducts C
A X : C
inst✝ : Exponentiable A
⊢ (exp.coev A).app ((𝟭 C).obj X) ≫ 𝟙 (A ⟹ A ⊗ (𝟭 C).obj X) = (exp.coev A).app X

Tactic:
apply comp_id

Result:
no goals

Proof state:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : ChosenFiniteProducts C
A X : C
inst✝ : Exponentiable A
⊢ curry (𝟙 (A ⊗ (𝟭 C).obj X)) = (exp.coev A).app X

Tactic:
rw [curry_eq, (exp A).map_id (A ⊗ _)]

Result:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : ChosenFiniteProducts C
A X : C
inst✝ : Exponentiable A
⊢ (exp.coev A).app ((𝟭 C).obj X) ≫ 𝟙 (A ⟹ A ⊗ (𝟭 C).obj X) = (exp.coev A).app X
-- Mathlib/Probability/Distributions/Pareto.lean
/-- The Pareto pdf is positive for all reals `>= t`. -/
lemma paretoPDFReal_pos (ht : 0 < t) (hr : 0 < r) (hx : t ≤ x) :
    0 < paretoPDFReal t r x

Proof state:
t r x : ℝ
ht : 0 < t
hr : 0 < r
hx : t ≤ x
⊢ 0 < paretoPDFReal t r x

Tactic:
rw [paretoPDFReal, if_pos hx]

Result:
t r x : ℝ
ht : 0 < t
hr : 0 < r
hx : t ≤ x
⊢ 0 < r * t ^ r * x ^ (-(r + 1))

Proof state:
t r x : ℝ
ht : 0 < t
hr : 0 < r
hx : t ≤ x
⊢ 0 < r * t ^ r * x ^ (-(r + 1))

Tactic:
have _ : 0 < x := by linarith

Result:
t r x : ℝ
ht : 0 < t
hr : 0 < r
hx : t ≤ x
x✝ : 0 < x
⊢ 0 < r * t ^ r * x ^ (-(r + 1))

Proof state:
t r x : ℝ
ht : 0 < t
hr : 0 < r
hx : t ≤ x
⊢ 0 < x

Tactic:
linarith

Result:
no goals

Proof state:
t r x : ℝ
ht : 0 < t
hr : 0 < r
hx : t ≤ x
x✝ : 0 < x
⊢ 0 < r * t ^ r * x ^ (-(r + 1))

Tactic:
positivity

Result:
no goals
-- Mathlib/MeasureTheory/Measure/MeasureSpace.lean
@[simp]
lemma sum_zero : Measure.sum (fun (_ : ι) ↦ (0 : Measure α)) = 0

Proof state:
case h
α : Type u_1
ι : Type u_5
m0 : MeasurableSpace α
s : Set α
hs : MeasurableSet s
⊢ (sum fun x => 0) s = 0 s

Tactic:
simp [Measure.sum_apply _ hs]

Result:
no goals

Proof state:
α : Type u_1
ι : Type u_5
m0 : MeasurableSpace α
⊢ (sum fun x => 0) = 0

Tactic:
ext s hs

Result:
case h
α : Type u_1
ι : Type u_5
m0 : MeasurableSpace α
s : Set α
hs : MeasurableSet s
⊢ (sum fun x => 0) s = 0 s
-- Mathlib/CategoryTheory/Localization/CalculusOfFractions.lean
lemma LeftFractionRel.unop {W : MorphismProperty Cᵒᵖ} {X Y : Cᵒᵖ}
    {z₁ z₂ : W.LeftFraction X Y}
    (h : LeftFractionRel z₁ z₂) : RightFractionRel z₁.unop z₂.unop

Proof state:
case intro.intro.intro.intro.intro
C : Type u_1
inst✝ : Category.{u_3, u_1} C
W : MorphismProperty Cᵒᵖ
X Y : Cᵒᵖ
z₁ z₂ : W.LeftFraction X Y
Z : Cᵒᵖ
t₁ : z₁.Y' ⟶ Z
t₂ : z₂.Y' ⟶ Z
hs : z₁.s ≫ t₁ = z₂.s ≫ t₂
hf : z₁.f ≫ t₁ = z₂.f ≫ t₂
ht : W (z₁.s ≫ t₁)
⊢ RightFractionRel z₁.unop z₂.unop

Tactic:
exact ⟨Opposite.unop Z, t₁.unop, t₂.unop, Quiver.Hom.op_inj hs,
  Quiver.Hom.op_inj hf, ht⟩

Result:
no goals

Proof state:
C : Type u_1
inst✝ : Category.{u_3, u_1} C
W : MorphismProperty Cᵒᵖ
X Y : Cᵒᵖ
z₁ z₂ : W.LeftFraction X Y
h : LeftFractionRel z₁ z₂
⊢ RightFractionRel z₁.unop z₂.unop

Tactic:
obtain ⟨Z, t₁, t₂, hs, hf, ht⟩ := h

Result:
case intro.intro.intro.intro.intro
C : Type u_1
inst✝ : Category.{u_3, u_1} C
W : MorphismProperty Cᵒᵖ
X Y : Cᵒᵖ
z₁ z₂ : W.LeftFraction X Y
Z : Cᵒᵖ
t₁ : z₁.Y' ⟶ Z
t₂ : z₂.Y' ⟶ Z
hs : z₁.s ≫ t₁ = z₂.s ≫ t₂
hf : z₁.f ≫ t₁ = z₂.f ≫ t₂
ht : W (z₁.s ≫ t₁)
⊢ RightFractionRel z₁.unop z₂.unop
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Count.lean
theorem countP_eq_length_filter (l) : countP p l = length (filter p l)

Proof state:
α : Type u_1
p : α → Bool
x : α
l : List α
ih : countP p l = (filter p l).length
h : ¬p x = true
⊢ countP p (x :: l) = (filter p (x :: l)).length

Tactic:
rw [countP_cons_of_neg p l h, ih, filter_cons_of_neg h]

Result:
no goals

Proof state:
case cons
α : Type u_1
p : α → Bool
x : α
l : List α
ih : countP p l = (filter p l).length
⊢ countP p (x :: l) = (filter p (x :: l)).length

Tactic:
if h : p x
then rw [countP_cons_of_pos p l h, ih, filter_cons_of_pos h, length]
else rw [countP_cons_of_neg p l h, ih, filter_cons_of_neg h]

Result:
no goals

Proof state:
α : Type u_1
p : α → Bool
l : List α
⊢ countP p l = (filter p l).length

Tactic:
induction l with
| nil => rfl
| cons x l ih =>
  if h : p x
  then rw [countP_cons_of_pos p l h, ih, filter_cons_of_pos h, length]
  else rw [countP_cons_of_neg p l h, ih, filter_cons_of_neg h]

Result:
no goals

Proof state:
case nil
α : Type u_1
p : α → Bool
⊢ countP p [] = (filter p []).length

Tactic:
rfl

Result:
no goals

Proof state:
α : Type u_1
p : α → Bool
x : α
l : List α
ih : countP p l = (filter p l).length
h : p x = true
⊢ countP p (x :: l) = (filter p (x :: l)).length

Tactic:
rw [countP_cons_of_pos p l h, ih, filter_cons_of_pos h, length]

Result:
no goals
-- Mathlib/Algebra/GeomSum.lean
theorem geom_sum_mul [Ring α] (x : α) (n : ℕ) : (∑ i ∈ range n, x ^ i) * (x - 1) = x ^ n - 1

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

Tactic:
have := (Commute.one_right x).geom_sum₂_mul n

Result:
α : Type u
inst✝ : Ring α
x : α
n : ℕ
this : (∑ i ∈ range n, x ^ i * 1 ^ (n - 1 - i)) * (x - 1) = x ^ n - 1 ^ n
⊢ (∑ i ∈ range n, x ^ i) * (x - 1) = x ^ n - 1

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

Tactic:
rw [one_pow, geom_sum₂_with_one] at this

Result:
α : Type u
inst✝ : Ring α
x : α
n : ℕ
this : (∑ i ∈ range n, x ^ i) * (x - 1) = x ^ n - 1
⊢ (∑ i ∈ range n, x ^ i) * (x - 1) = x ^ n - 1

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

Tactic:
exact this

Result:
no goals
-- Mathlib/Topology/Algebra/InfiniteSum/Basic.lean
theorem tprod_dite_right (P : Prop) [Decidable P] (x : β → ¬P → α) :
    ∏' b : β, (if h : P then (1 : α) else x b h) = if h : P then (1 : α) else ∏' b : β, x b h

Proof state:
α : Type u_1
β : Type u_2
inst✝² : CommMonoid α
inst✝¹ : TopologicalSpace α
P : Prop
inst✝ : Decidable P
x : β → ¬P → α
⊢ (∏' (b : β), if h : P then 1 else x b h) = if h : P then 1 else ∏' (b : β), x b h

Tactic:
by_cases hP : P <;> simp [hP]

Result:
no goals