harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Topology/Algebra/Module/LinearMap.lean
theorem comp_neg [RingHomCompTriple σ₁₂ σ₂₃ σ₁₃] [IsTopologicalAddGroup M₂]
    [IsTopologicalAddGroup M₃] (g : M₂ →SL[σ₂₃] M₃) (f : M →SL[σ₁₂] M₂) :
    g.comp (-f) = -g.comp f

Proof state:
R : Type u_1
inst✝¹⁴ : Ring R
R₂ : Type u_2
inst✝¹³ : Ring R₂
R₃ : Type u_3
inst✝¹² : Ring R₃
M : Type u_4
inst✝¹¹ : TopologicalSpace M
inst✝¹⁰ : AddCommGroup M
M₂ : Type u_5
inst✝⁹ : TopologicalSpace M₂
inst✝⁸ : AddCommGroup M₂
M₃ : Type u_6
inst✝⁷ : TopologicalSpace M₃
inst✝⁶ : AddCommGroup M₃
inst✝⁵ : Module R M
inst✝⁴ : Module R₂ M₂
inst✝³ : Module R₃ M₃
σ₁₂ : R →+* R₂
σ₂₃ : R₂ →+* R₃
σ₁₃ : R →+* R₃
inst✝² : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
inst✝¹ : IsTopologicalAddGroup M₂
inst✝ : IsTopologicalAddGroup M₃
g : M₂ →SL[σ₂₃] M₃
f : M →SL[σ₁₂] M₂
⊢ g.comp (-f) = -g.comp f

Tactic:
ext x

Result:
case h
R : Type u_1
inst✝¹⁴ : Ring R
R₂ : Type u_2
inst✝¹³ : Ring R₂
R₃ : Type u_3
inst✝¹² : Ring R₃
M : Type u_4
inst✝¹¹ : TopologicalSpace M
inst✝¹⁰ : AddCommGroup M
M₂ : Type u_5
inst✝⁹ : TopologicalSpace M₂
inst✝⁸ : AddCommGroup M₂
M₃ : Type u_6
inst✝⁷ : TopologicalSpace M₃
inst✝⁶ : AddCommGroup M₃
inst✝⁵ : Module R M
inst✝⁴ : Module R₂ M₂
inst✝³ : Module R₃ M₃
σ₁₂ : R →+* R₂
σ₂₃ : R₂ →+* R₃
σ₁₃ : R →+* R₃
inst✝² : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
inst✝¹ : IsTopologicalAddGroup M₂
inst✝ : IsTopologicalAddGroup M₃
g : M₂ →SL[σ₂₃] M₃
f : M →SL[σ₁₂] M₂
x : M
⊢ (g.comp (-f)) x = (-g.comp f) x

Proof state:
case h
R : Type u_1
inst✝¹⁴ : Ring R
R₂ : Type u_2
inst✝¹³ : Ring R₂
R₃ : Type u_3
inst✝¹² : Ring R₃
M : Type u_4
inst✝¹¹ : TopologicalSpace M
inst✝¹⁰ : AddCommGroup M
M₂ : Type u_5
inst✝⁹ : TopologicalSpace M₂
inst✝⁸ : AddCommGroup M₂
M₃ : Type u_6
inst✝⁷ : TopologicalSpace M₃
inst✝⁶ : AddCommGroup M₃
inst✝⁵ : Module R M
inst✝⁴ : Module R₂ M₂
inst✝³ : Module R₃ M₃
σ₁₂ : R →+* R₂
σ₂₃ : R₂ →+* R₃
σ₁₃ : R →+* R₃
inst✝² : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
inst✝¹ : IsTopologicalAddGroup M₂
inst✝ : IsTopologicalAddGroup M₃
g : M₂ →SL[σ₂₃] M₃
f : M →SL[σ₁₂] M₂
x : M
⊢ (g.comp (-f)) x = (-g.comp f) x

Tactic:
simp

Result:
no goals
-- Mathlib/RepresentationTheory/GroupCohomology/Resolution.lean
theorem diagonalHomEquiv_apply (f : Rep.diagonal k G (n + 1) ⟶ A) (x : Fin n → G) :
    diagonalHomEquiv n A f x = f.hom (Finsupp.single (Fin.partialProd x) 1)

Proof state:
k G : Type u
inst✝¹ : CommRing k
n : ℕ
inst✝ : Group G
A : Rep k G
f : diagonal k G (n + 1) ⟶ A
x : Fin n → G
⊢ (ConcreteCategory.hom f.hom) ((ConcreteCategory.hom (diagonalSucc k G n).inv.hom) (single 1 1 ⊗ₜ[k] single x 1)) =
    (ConcreteCategory.hom f.hom) (single (Fin.partialProd x) 1)

Tactic:
rw [diagonalSucc_inv_single_single, one_smul, one_mul]

Result:
no goals

Proof state:
k G : Type u
inst✝¹ : CommRing k
n : ℕ
inst✝ : Group G
A : Rep k G
f : diagonal k G (n + 1) ⟶ A
x : Fin n → G
⊢ (diagonalHomEquiv n A) f x = (ConcreteCategory.hom f.hom) (single (Fin.partialProd x) 1)

Tactic:
change f.hom ((diagonalSucc k G n).inv.hom (Finsupp.single 1 1 ⊗ₜ[k] Finsupp.single x 1)) = _

Result:
k G : Type u
inst✝¹ : CommRing k
n : ℕ
inst✝ : Group G
A : Rep k G
f : diagonal k G (n + 1) ⟶ A
x : Fin n → G
⊢ (ConcreteCategory.hom f.hom) ((ConcreteCategory.hom (diagonalSucc k G n).inv.hom) (single 1 1 ⊗ₜ[k] single x 1)) =
    (ConcreteCategory.hom f.hom) (single (Fin.partialProd x) 1)
-- Mathlib/MeasureTheory/Function/ConditionalExpectation/CondexpL1.lean
theorem condExpInd_ae_eq_condExpIndSMul (hm : m ≤ m0) [SigmaFinite (μ.trim hm)]
    (hs : MeasurableSet s) (hμs : μ s ≠ ∞) (x : G) :
    condExpInd G hm μ s x =ᵐ[μ] condExpIndSMul hm hs hμs x

Proof state:
α : Type u_1
G : Type u_4
inst✝² : NormedAddCommGroup G
m m0 : MeasurableSpace α
μ : Measure α
s : Set α
inst✝¹ : NormedSpace ℝ G
hm : m ≤ m0
inst✝ : SigmaFinite (μ.trim hm)
hs : MeasurableSet s
hμs : μ s ≠ ⊤
x : G
⊢ ↑↑((condExpInd G hm μ s) x) =ᶠ[ae μ] ↑↑(condExpIndL1Fin hm hs hμs x)

Tactic:
simp [condExpInd, condExpIndL1, hs, hμs]

Result:
no goals

Proof state:
α : Type u_1
G : Type u_4
inst✝² : NormedAddCommGroup G
m m0 : MeasurableSpace α
μ : Measure α
s : Set α
inst✝¹ : NormedSpace ℝ G
hm : m ≤ m0
inst✝ : SigmaFinite (μ.trim hm)
hs : MeasurableSet s
hμs : μ s ≠ ⊤
x : G
⊢ ↑↑((condExpInd G hm μ s) x) =ᶠ[ae μ] ↑↑(condExpIndSMul hm hs hμs x)

Tactic:
refine EventuallyEq.trans ?_ (condExpIndL1Fin_ae_eq_condExpIndSMul hm hs hμs x)

Result:
α : Type u_1
G : Type u_4
inst✝² : NormedAddCommGroup G
m m0 : MeasurableSpace α
μ : Measure α
s : Set α
inst✝¹ : NormedSpace ℝ G
hm : m ≤ m0
inst✝ : SigmaFinite (μ.trim hm)
hs : MeasurableSet s
hμs : μ s ≠ ⊤
x : G
⊢ ↑↑((condExpInd G hm μ s) x) =ᶠ[ae μ] ↑↑(condExpIndL1Fin hm hs hμs x)
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/RawLemmas.lean
theorem contains_erase [EquivBEq α] [LawfulHashable α] (h : m.1.WF) {k a : α} :
    (m.erase k).contains a = (!(k == a) && m.contains a)

Proof state:
α : Type u
β : α → Type v
m : Raw₀ α β
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
h : m.val.WF
k a : α
⊢ (m.erase k).contains a = (!k == a && m.contains a)

Tactic:
simp_to_model [erase] using List.containsKey_eraseKey

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Lemmas.lean
theorem getKey!_alter_self [EquivBEq α] [LawfulHashable α] [Inhabited α] {k : α}
    {f : Option β → Option β} :
    (Const.alter m k f).getKey! k = if (f (Const.get? m k)).isSome then k else default

Proof state:
α : Type u
x✝¹ : BEq α
x✝ : Hashable α
β : Type v
m : DHashMap α fun x => β
inst✝² : EquivBEq α
inst✝¹ : LawfulHashable α
inst✝ : Inhabited α
k : α
f : Option β → Option β
⊢ (alter m k f).getKey! k = if (f (get? m k)).isSome = true then k else default

Tactic:
simp [getKey!_alter]

Result:
no goals
-- Mathlib/Order/Interval/Set/Basic.lean
theorem Ioo_inter_Ioo : Ioo a₁ b₁ ∩ Ioo a₂ b₂ = Ioo (a₁ ⊔ a₂) (b₁ ⊓ b₂)

Proof state:
α : Type u_1
inst✝ : LinearOrder α
a₁ a₂ b₁ b₂ : α
⊢ Ioo a₁ b₁ ∩ Ioo a₂ b₂ = Ioo (a₁ ⊔ a₂) (b₁ ⊓ b₂)

Tactic:
simp only [Ioi_inter_Iio.symm, Ioi_inter_Ioi.symm, Iio_inter_Iio.symm]

Result:
α : Type u_1
inst✝ : LinearOrder α
a₁ a₂ b₁ b₂ : α
⊢ Ioi a₁ ∩ Iio b₁ ∩ (Ioi a₂ ∩ Iio b₂) = Ioi a₁ ∩ Ioi a₂ ∩ (Iio b₁ ∩ Iio b₂)

Proof state:
α : Type u_1
inst✝ : LinearOrder α
a₁ a₂ b₁ b₂ : α
⊢ Ioi a₁ ∩ Iio b₁ ∩ (Ioi a₂ ∩ Iio b₂) = Ioi a₁ ∩ Ioi a₂ ∩ (Iio b₁ ∩ Iio b₂)

Tactic:
ac_rfl

Result:
no goals
-- Mathlib/Combinatorics/Pigeonhole.lean
theorem exists_lt_card_fiber_of_nsmul_lt_card_of_maps_to (hf : ∀ a ∈ s, f a ∈ t)
    (ht : #t • b < #s) : ∃ y ∈ t, b < #{x ∈ s | f x = y}

Proof state:
α : Type u
β : Type v
M : Type w
inst✝¹ : DecidableEq β
s : Finset α
t : Finset β
f : α → β
b : M
inst✝ : LinearOrderedCommSemiring M
hf : ∀ a ∈ s, f a ∈ t
ht : #t • b < ↑(#s)
⊢ ∃ y ∈ t, b < ↑(#(filter (fun x => f x = y) s))

Tactic:
simp_rw [cast_card] at ht ⊢

Result:
α : Type u
β : Type v
M : Type w
inst✝¹ : DecidableEq β
s : Finset α
t : Finset β
f : α → β
b : M
inst✝ : LinearOrderedCommSemiring M
hf : ∀ a ∈ s, f a ∈ t
ht : #t • b < ∑ x ∈ s, 1
⊢ ∃ y ∈ t, b < ∑ x ∈ filter (fun x => f x = y) s, 1

Proof state:
α : Type u
β : Type v
M : Type w
inst✝¹ : DecidableEq β
s : Finset α
t : Finset β
f : α → β
b : M
inst✝ : LinearOrderedCommSemiring M
hf : ∀ a ∈ s, f a ∈ t
ht : #t • b < ∑ x ∈ s, 1
⊢ ∃ y ∈ t, b < ∑ x ∈ filter (fun x => f x = y) s, 1

Tactic:
exact exists_lt_sum_fiber_of_maps_to_of_nsmul_lt_sum hf ht

Result:
no goals
-- Mathlib/SetTheory/Game/PGame.lean
theorem neg_lt_iff {x y : PGame} : -y < x ↔ -x < y

Proof state:
x y : PGame
⊢ -y < x ↔ -x < y

Tactic:
rw [← neg_neg x, neg_lt_neg_iff, neg_neg]

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

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

Tactic:
simp

Result:
no goals
-- Mathlib/NumberTheory/FLT/Four.lean
theorem exists_pos_odd_minimal {a b c : ℤ} (h : Fermat42 a b c) :
    ∃ a0 b0 c0, Minimal a0 b0 c0 ∧ a0 % 2 = 1 ∧ 0 < c0

Proof state:
a b c : ℤ
h : Fermat42 a b c
⊢ ∃ a0 b0 c0, Minimal a0 b0 c0 ∧ a0 % 2 = 1 ∧ 0 < c0

Tactic:
obtain ⟨a0, b0, c0, hf, hc⟩ := exists_odd_minimal h

Result:
case intro.intro.intro.intro
a b c : ℤ
h : Fermat42 a b c
a0 b0 c0 : ℤ
hf : Minimal a0 b0 c0
hc : a0 % 2 = 1
⊢ ∃ a0 b0 c0, Minimal a0 b0 c0 ∧ a0 % 2 = 1 ∧ 0 < c0

Proof state:
case intro.intro.intro.intro.inr.inr
a b c : ℤ
h : Fermat42 a b c
a0 b0 c0 : ℤ
hf : Minimal a0 b0 c0
hc : a0 % 2 = 1
h1 : c0 < 0
⊢ ∃ a0 b0 c0, Minimal a0 b0 c0 ∧ a0 % 2 = 1 ∧ 0 < c0

Tactic:
use a0, b0, -c0, neg_of_minimal hf, hc

Result:
case right
a b c : ℤ
h : Fermat42 a b c
a0 b0 c0 : ℤ
hf : Minimal a0 b0 c0
hc : a0 % 2 = 1
h1 : c0 < 0
⊢ 0 < -c0

Proof state:
case intro.intro.intro.intro.inr.inl
a b c : ℤ
h : Fermat42 a b c
a0 b0 c0 : ℤ
hf : Minimal a0 b0 c0
hc : a0 % 2 = 1
h1 : 0 = c0
⊢ ∃ a0 b0 c0, Minimal a0 b0 c0 ∧ a0 % 2 = 1 ∧ 0 < c0

Tactic:
exfalso

Result:
case intro.intro.intro.intro.inr.inl
a b c : ℤ
h : Fermat42 a b c
a0 b0 c0 : ℤ
hf : Minimal a0 b0 c0
hc : a0 % 2 = 1
h1 : 0 = c0
⊢ False

Proof state:
case right
a b c : ℤ
h : Fermat42 a b c
a0 b0 c0 : ℤ
hf : Minimal a0 b0 c0
hc : a0 % 2 = 1
h1 : c0 < 0
⊢ 0 < -c0

Tactic:
exact neg_pos.mpr h1

Result:
no goals

Proof state:
case intro.intro.intro.intro.inl
a b c : ℤ
h : Fermat42 a b c
a0 b0 c0 : ℤ
hf : Minimal a0 b0 c0
hc : a0 % 2 = 1
h1 : 0 < c0
⊢ ∃ a0 b0 c0, Minimal a0 b0 c0 ∧ a0 % 2 = 1 ∧ 0 < c0

Tactic:
use a0, b0, c0

Result:
no goals

Proof state:
case intro.intro.intro.intro
a b c : ℤ
h : Fermat42 a b c
a0 b0 c0 : ℤ
hf : Minimal a0 b0 c0
hc : a0 % 2 = 1
⊢ ∃ a0 b0 c0, Minimal a0 b0 c0 ∧ a0 % 2 = 1 ∧ 0 < c0

Tactic:
rcases lt_trichotomy 0 c0 with (h1 | h1 | h1)

Result:
case intro.intro.intro.intro.inl
a b c : ℤ
h : Fermat42 a b c
a0 b0 c0 : ℤ
hf : Minimal a0 b0 c0
hc : a0 % 2 = 1
h1 : 0 < c0
⊢ ∃ a0 b0 c0, Minimal a0 b0 c0 ∧ a0 % 2 = 1 ∧ 0 < c0

case intro.intro.intro.intro.inr.inl
a b c : ℤ
h : Fermat42 a b c
a0 b0 c0 : ℤ
hf : Minimal a0 b0 c0
hc : a0 % 2 = 1
h1 : 0 = c0
⊢ ∃ a0 b0 c0, Minimal a0 b0 c0 ∧ a0 % 2 = 1 ∧ 0 < c0

case intro.intro.intro.intro.inr.inr
a b c : ℤ
h : Fermat42 a b c
a0 b0 c0 : ℤ
hf : Minimal a0 b0 c0
hc : a0 % 2 = 1
h1 : c0 < 0
⊢ ∃ a0 b0 c0, Minimal a0 b0 c0 ∧ a0 % 2 = 1 ∧ 0 < c0

Proof state:
case intro.intro.intro.intro.inr.inl
a b c : ℤ
h : Fermat42 a b c
a0 b0 c0 : ℤ
hf : Minimal a0 b0 c0
hc : a0 % 2 = 1
h1 : 0 = c0
⊢ False

Tactic:
exact ne_zero hf.1 h1.symm

Result:
no goals
-- Mathlib/Topology/MetricSpace/Infsep.lean
theorem Nontrivial.infsep_eq_iInf (hs : s.Nontrivial) :
    s.infsep = ⨅ d : s.offDiag, (uncurry dist) (d : α × α)

Proof state:
α : Type u_1
inst✝ : PseudoMetricSpace α
s : Set α
hs : s.Nontrivial
⊢ s.infsep = ⨅ d, uncurry dist ↑d

Tactic:
classical rw [Set.infsep_eq_iInf, if_pos hs]

Result:
no goals

Proof state:
α : Type u_1
inst✝ : PseudoMetricSpace α
s : Set α
hs : s.Nontrivial
⊢ s.infsep = ⨅ d, uncurry dist ↑d

Tactic:
rw [Set.infsep_eq_iInf, if_pos hs]

Result:
no goals
-- Mathlib/Order/RelSeries.lean
theorem subsingleton_of_length_eq_zero (hs : s.length = 0) : {x | x ∈ s}.Subsingleton

Proof state:
α : Type u_1
r : Rel α α
s : RelSeries r
hs : s.length = 0
⊢ {x | x ∈ s}.Subsingleton

Tactic:
rintro - ⟨i, rfl⟩ - ⟨j, rfl⟩

Result:
case intro.intro
α : Type u_1
r : Rel α α
s : RelSeries r
hs : s.length = 0
i j : Fin (s.length + 1)
⊢ s.toFun i = s.toFun j

Proof state:
case intro.intro.h.e'_4
α : Type u_1
r : Rel α α
s : RelSeries r
hs : s.length = 0
i j : Fin (s.length + 1)
⊢ i = j

Tactic:
exact finCongr (by rw [hs, zero_add]) |>.injective <| Subsingleton.elim (α := Fin 1) _ _

Result:
no goals

Proof state:
α : Type u_1
r : Rel α α
s : RelSeries r
hs : s.length = 0
i j : Fin (s.length + 1)
⊢ s.length + 1 = 1

Tactic:
rw [hs, zero_add]

Result:
no goals

Proof state:
case intro.intro
α : Type u_1
r : Rel α α
s : RelSeries r
hs : s.length = 0
i j : Fin (s.length + 1)
⊢ s.toFun i = s.toFun j

Tactic:
congr!

Result:
case intro.intro.h.e'_4
α : Type u_1
r : Rel α α
s : RelSeries r
hs : s.length = 0
i j : Fin (s.length + 1)
⊢ i = j
-- Mathlib/CategoryTheory/Subobject/FactorThru.lean
theorem factorThru_add_sub_factorThru_right {X Y : C} {P : Subobject Y} (f g : X ⟶ Y)
    (w : P.Factors (f + g)) (wg : P.Factors g) :
    P.factorThru (f + g) w - P.factorThru g wg =
      P.factorThru f (factors_left_of_factors_add f g w wg)

Proof state:
case h
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Preadditive C
X Y : C
P : Subobject Y
f g : X ⟶ Y
w : P.Factors (f + g)
wg : P.Factors g
⊢ (P.factorThru (f + g) w - P.factorThru g wg) ≫ P.arrow = P.factorThru f ⋯ ≫ P.arrow

Tactic:
simp

Result:
no goals

Proof state:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Preadditive C
X Y : C
P : Subobject Y
f g : X ⟶ Y
w : P.Factors (f + g)
wg : P.Factors g
⊢ P.factorThru (f + g) w - P.factorThru g wg = P.factorThru f ⋯

Tactic:
ext

Result:
case h
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Preadditive C
X Y : C
P : Subobject Y
f g : X ⟶ Y
w : P.Factors (f + g)
wg : P.Factors g
⊢ (P.factorThru (f + g) w - P.factorThru g wg) ≫ P.arrow = P.factorThru f ⋯ ≫ P.arrow
-- Mathlib/Order/Fin/Basic.lean
@[simp]
lemma castOrderIso_refl (h : n = n := rfl) : castOrderIso h = OrderIso.refl (Fin n)

Proof state:
case h.h.h
n : ℕ
h : optParam (n = n) ⋯
x✝ : Fin n
⊢ ↑((castOrderIso h) x✝) = ↑((OrderIso.refl (Fin n)) x✝)

Tactic:
simp

Result:
no goals

Proof state:
n : ℕ
h : optParam (n = n) ⋯
⊢ castOrderIso h = OrderIso.refl (Fin n)

Tactic:
ext

Result:
case h.h.h
n : ℕ
h : optParam (n = n) ⋯
x✝ : Fin n
⊢ ↑((castOrderIso h) x✝) = ↑((OrderIso.refl (Fin n)) x✝)
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem getElem?_eq_none_iff {a : Array α} : a[i]? = none ↔ a.size ≤ i

Proof state:
case neg
α : Type u_1
i : Nat
a : Array α
h : ¬i < a.size
⊢ a[i]? = none ↔ a.size ≤ i

Tactic:
rw [getElem?_neg a i h]

Result:
case neg
α : Type u_1
i : Nat
a : Array α
h : ¬i < a.size
⊢ none = none ↔ a.size ≤ i

Proof state:
case pos
α : Type u_1
i : Nat
a : Array α
h : i < a.size
⊢ a[i]? = none ↔ a.size ≤ i

Tactic:
simp [getElem?_pos, h]

Result:
no goals

Proof state:
case neg
α : Type u_1
i : Nat
a : Array α
h : ¬i < a.size
⊢ none = none ↔ a.size ≤ i

Tactic:
simp_all

Result:
no goals

Proof state:
α : Type u_1
i : Nat
a : Array α
⊢ a[i]? = none ↔ a.size ≤ i

Tactic:
by_cases h : i < a.size

Result:
case pos
α : Type u_1
i : Nat
a : Array α
h : i < a.size
⊢ a[i]? = none ↔ a.size ≤ i

case neg
α : Type u_1
i : Nat
a : Array α
h : ¬i < a.size
⊢ a[i]? = none ↔ a.size ≤ i
-- Mathlib/Data/Fintype/Card.lean
theorem existsUnique_iff_card_one {α} [Fintype α] (p : α → Prop) [DecidablePred p] :
    (∃! a : α, p a) ↔ #{x | p x} = 1

Proof state:
α : Type u_4
inst✝¹ : Fintype α
p : α → Prop
inst✝ : DecidablePred p
x : α
⊢ ((fun a => p a) x ∧ ∀ (y : α), (fun a => p a) y → y = x) ↔ filter (fun x => p x) univ = {x}

Tactic:
simp only [forall_true_left, Subset.antisymm_iff, subset_singleton_iff', singleton_subset_iff,
    true_and, and_comm, mem_univ, mem_filter]

Result:
no goals

Proof state:
α : Type u_4
inst✝¹ : Fintype α
p : α → Prop
inst✝ : DecidablePred p
⊢ (∃! a, p a) ↔ ∃ a, filter (fun x => p x) univ = {a}

Tactic:
refine exists_congr fun x => ?_

Result:
α : Type u_4
inst✝¹ : Fintype α
p : α → Prop
inst✝ : DecidablePred p
x : α
⊢ ((fun a => p a) x ∧ ∀ (y : α), (fun a => p a) y → y = x) ↔ filter (fun x => p x) univ = {x}

Proof state:
α : Type u_4
inst✝¹ : Fintype α
p : α → Prop
inst✝ : DecidablePred p
⊢ (∃! a, p a) ↔ #(filter (fun x => p x) univ) = 1

Tactic:
rw [Finset.card_eq_one]

Result:
α : Type u_4
inst✝¹ : Fintype α
p : α → Prop
inst✝ : DecidablePred p
⊢ (∃! a, p a) ↔ ∃ a, filter (fun x => p x) univ = {a}
-- Mathlib/Data/Fintype/Pi.lean
lemma filter_piFinset_of_not_mem (t : ∀ a, Finset (δ a)) (a : α) (x : δ a) (hx : x ∉ t a) :
    {f ∈ piFinset t | f a = x} = ∅

Proof state:
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Fintype α
δ : α → Type u_4
inst✝ : (a : α) → DecidableEq (δ a)
t : (a : α) → Finset (δ a)
a : α
x : δ a
hx : x ∉ t a
⊢ ∀ ⦃x_1 : (a : α) → δ a⦄, (∀ (a : α), x_1 a ∈ t a) → ¬x_1 a = x

Tactic:
rintro f hf rfl

Result:
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Fintype α
δ : α → Type u_4
inst✝ : (a : α) → DecidableEq (δ a)
t : (a : α) → Finset (δ a)
a : α
f : (a : α) → δ a
hf : ∀ (a : α), f a ∈ t a
hx : f a ∉ t a
⊢ False

Proof state:
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Fintype α
δ : α → Type u_4
inst✝ : (a : α) → DecidableEq (δ a)
t : (a : α) → Finset (δ a)
a : α
x : δ a
hx : x ∉ t a
⊢ filter (fun f => f a = x) (piFinset t) = ∅

Tactic:
simp only [filter_eq_empty_iff, mem_piFinset]

Result:
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Fintype α
δ : α → Type u_4
inst✝ : (a : α) → DecidableEq (δ a)
t : (a : α) → Finset (δ a)
a : α
x : δ a
hx : x ∉ t a
⊢ ∀ ⦃x_1 : (a : α) → δ a⦄, (∀ (a : α), x_1 a ∈ t a) → ¬x_1 a = x

Proof state:
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Fintype α
δ : α → Type u_4
inst✝ : (a : α) → DecidableEq (δ a)
t : (a : α) → Finset (δ a)
a : α
f : (a : α) → δ a
hf : ∀ (a : α), f a ∈ t a
hx : f a ∉ t a
⊢ False

Tactic:
exact hx (hf _)

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Lemmas.lean
theorem getElem?_push {a : Vector α n} {x} : (a.push x)[i]? = if i = n then some x else a[i]?

Proof state:
case isFalse.isFalse.isTrue
α : Type u_1
n i : Nat
a : Vector α n
x : α
h✝² : ¬i < n + 1
h✝¹ : ¬i = n
h✝ : i < n
⊢ none = some a[i]

Tactic:
omega

Result:
no goals

Proof state:
α : Type u_1
n i : Nat
a : Vector α n
x : α
⊢ (a.push x)[i]? = if i = n then some x else a[i]?

Tactic:
simp [getElem?_def, getElem_push]

Result:
α : Type u_1
n i : Nat
a : Vector α n
x : α
⊢ (if i < n + 1 then some (if h : i < n then a[i] else x) else none) =
    if i = n then some x else if h : i < n then some a[i] else none

Proof state:
case isFalse.isFalse.isFalse
α : Type u_1
n i : Nat
a : Vector α n
x : α
h✝² : ¬i < n + 1
h✝¹ : ¬i = n
h✝ : ¬i < n
⊢ none = none

Tactic:
rfl

Result:
no goals

Proof state:
α : Type u_1
n i : Nat
a : Vector α n
x : α
⊢ (if i < n + 1 then some (if h : i < n then a[i] else x) else none) =
    if i = n then some x else if h : i < n then some a[i] else none

Tactic:
repeat' split

Result:
case isTrue.isTrue.isTrue
α : Type u_1
n i : Nat
a : Vector α n
x : α
h✝² : i < n + 1
h✝¹ : i < n
h✝ : i = n
⊢ some a[i] = some x

case isTrue.isTrue.isFalse
α : Type u_1
n i : Nat
a : Vector α n
x : α
h✝² : i < n + 1
h✝¹ : i < n
h✝ : ¬i = n
⊢ some a[i] = some a[i]

case isTrue.isFalse.isTrue
α : Type u_1
n i : Nat
a : Vector α n
x : α
h✝² : i < n + 1
h✝¹ : ¬i < n
h✝ : i = n
⊢ some x = some x

case isTrue.isFalse.isFalse
α : Type u_1
n i : Nat
a : Vector α n
x : α
h✝² : i < n + 1
h✝¹ : ¬i < n
h✝ : ¬i = n
⊢ some x = none

case isFalse.isTrue
α : Type u_1
n i : Nat
a : Vector α n
x : α
h✝¹ : ¬i < n + 1
h✝ : i = n
⊢ none = some x

case isFalse.isFalse.isTrue
α : Type u_1
n i : Nat
a : Vector α n
x : α
h✝² : ¬i < n + 1
h✝¹ : ¬i = n
h✝ : i < n
⊢ none = some a[i]

case isFalse.isFalse.isFalse
α : Type u_1
n i : Nat
a : Vector α n
x : α
h✝² : ¬i < n + 1
h✝¹ : ¬i = n
h✝ : ¬i < n
⊢ none = none

Proof state:
case isFalse.isFalse
α : Type u_1
n i : Nat
a : Vector α n
x : α
h✝¹ : ¬i < n + 1
h✝ : ¬i = n
⊢ none = if h : i < n then some a[i] else none

Tactic:
split

Result:
case isFalse.isFalse.isTrue
α : Type u_1
n i : Nat
a : Vector α n
x : α
h✝² : ¬i < n + 1
h✝¹ : ¬i = n
h✝ : i < n
⊢ none = some a[i]

case isFalse.isFalse.isFalse
α : Type u_1
n i : Nat
a : Vector α n
x : α
h✝² : ¬i < n + 1
h✝¹ : ¬i = n
h✝ : ¬i < n
⊢ none = none

Proof state:
α : Type u_1
n i : Nat
a : Vector α n
x : α
⊢ (if i < n + 1 then some (if h : i < n then a[i] else x) else none) =
    if i = n then some x else if h : i < n then some a[i] else none

Tactic:
(repeat' split) <;> first | rfl | omega

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/SimpLemmas.lean
theorem beq_eq_false_iff_ne [BEq α] [LawfulBEq α] {a b : α} : (a == b) = false ↔ a ≠ b

Proof state:
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
a b : α
⊢ (a == b) = false ↔ ¬(a == b) = true

Tactic:
cases a == b <;> decide

Result:
no goals

Proof state:
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
a b : α
⊢ (a == b) = false ↔ a ≠ b

Tactic:
rw [ne_eq, ← beq_iff_eq (a := a) (b := b)]

Result:
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
a b : α
⊢ (a == b) = false ↔ ¬(a == b) = true
-- Mathlib/Data/ENNReal/Real.lean
theorem trichotomy (p : ℝ≥0∞) : p = 0 ∨ p = ∞ ∨ 0 < p.toReal

Proof state:
p : ℝ≥0∞
⊢ p = 0 ∨ p = ⊤ ∨ 0 < p.toReal

Tactic:
simpa only [or_iff_not_imp_left] using toReal_pos

Result:
no goals
-- Mathlib/LinearAlgebra/Matrix/NonsingularInverse.lean
theorem nonsing_inv_cancel_or_zero : A⁻¹ * A = 1 ∧ A * A⁻¹ = 1 ∨ A⁻¹ = 0

Proof state:
case pos
n : Type u'
α : Type v
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommRing α
A : Matrix n n α
h : IsUnit A.det
⊢ A⁻¹ * A = 1 ∧ A * A⁻¹ = 1 ∨ A⁻¹ = 0

Tactic:
exact Or.inl ⟨nonsing_inv_mul _ h, mul_nonsing_inv _ h⟩

Result:
no goals

Proof state:
case neg
n : Type u'
α : Type v
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommRing α
A : Matrix n n α
h : ¬IsUnit A.det
⊢ A⁻¹ * A = 1 ∧ A * A⁻¹ = 1 ∨ A⁻¹ = 0

Tactic:
exact Or.inr (nonsing_inv_apply_not_isUnit _ h)

Result:
no goals

Proof state:
n : Type u'
α : Type v
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommRing α
A : Matrix n n α
⊢ A⁻¹ * A = 1 ∧ A * A⁻¹ = 1 ∨ A⁻¹ = 0

Tactic:
by_cases h : IsUnit A.det

Result:
case pos
n : Type u'
α : Type v
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommRing α
A : Matrix n n α
h : IsUnit A.det
⊢ A⁻¹ * A = 1 ∧ A * A⁻¹ = 1 ∨ A⁻¹ = 0

case neg
n : Type u'
α : Type v
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommRing α
A : Matrix n n α
h : ¬IsUnit A.det
⊢ A⁻¹ * A = 1 ∧ A * A⁻¹ = 1 ∨ A⁻¹ = 0
-- Mathlib/Data/Finset/BooleanAlgebra.lean
@[simp]
lemma filter_univ_mem (s : Finset α) : univ.filter (· ∈ s) = s

Proof state:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Finset α
⊢ filter (fun x => x ∈ s) univ = s

Tactic:
simp [filter_mem_eq_inter]

Result:
no goals
-- Mathlib/Topology/Algebra/InfiniteSum/Basic.lean
theorem Finset.tprod_subtype' (s : Finset β) (f : β → α) :
    ∏' x : (s : Set β), f x = ∏ x ∈ s, f x

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : CommMonoid α
inst✝ : TopologicalSpace α
s : Finset β
f : β → α
⊢ ∏' (x : ↑↑s), f ↑x = ∏ x ∈ s, f x

Tactic:
simp

Result:
no goals