harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/CategoryTheory/Monoidal/End.lean
theorem obj_zero_map_μ_app {m : M} {X Y : C} (f : X ⟶ (F.obj m).obj Y) [F.Monoidal] :
    (F.obj (𝟙_ M)).map f ≫ (μ F m (𝟙_ M)).app _ =
    (η F).app _ ≫ f ≫ (F.map (ρ_ m).inv).app _

Proof state:
C : Type u
inst✝³ : Category.{v, u} C
M : Type u_1
inst✝² : Category.{u_2, u_1} M
inst✝¹ : MonoidalCategory M
F : M ⥤ C ⥤ C
m : M
X Y : C
f : X ⟶ (F.obj m).obj Y
inst✝ : F.Monoidal
⊢ (F.obj (𝟙_ M)).map f ≫ (μ F m (𝟙_ M)).app Y = (η F).app X ≫ f ≫ (F.map (ρ_ m).inv).app Y

Tactic:
rw [← cancel_epi ((ε F).app _), ← cancel_mono ((δ F _ _).app _)]

Result:
C : Type u
inst✝³ : Category.{v, u} C
M : Type u_1
inst✝² : Category.{u_2, u_1} M
inst✝¹ : MonoidalCategory M
F : M ⥤ C ⥤ C
m : M
X Y : C
f : X ⟶ (F.obj m).obj Y
inst✝ : F.Monoidal
⊢ ((ε F).app X ≫ (F.obj (𝟙_ M)).map f ≫ (μ F m (𝟙_ M)).app Y) ≫ (δ F m (𝟙_ M)).app Y =
    ((ε F).app X ≫ (η F).app X ≫ f ≫ (F.map (ρ_ m).inv).app Y) ≫ (δ F m (𝟙_ M)).app Y

Proof state:
C : Type u
inst✝³ : Category.{v, u} C
M : Type u_1
inst✝² : Category.{u_2, u_1} M
inst✝¹ : MonoidalCategory M
F : M ⥤ C ⥤ C
m : M
X Y : C
f : X ⟶ (F.obj m).obj Y
inst✝ : F.Monoidal
⊢ ((ε F).app X ≫ (F.obj (𝟙_ M)).map f ≫ (μ F m (𝟙_ M)).app Y) ≫ (δ F m (𝟙_ M)).app Y =
    ((ε F).app X ≫ (η F).app X ≫ f ≫ (F.map (ρ_ m).inv).app Y) ≫ (δ F m (𝟙_ M)).app Y

Tactic:
simp

Result:
no goals
-- Mathlib/Data/Nat/Prime/Defs.lean
theorem minFac_has_prop {n : ℕ} (n1 : n ≠ 1) : minFacProp n (minFac n)

Proof state:
n : ℕ
⊢ n ≠ 1 → ¬n = 0 → 2 ≤ n

Tactic:
rcases n with (_ | _ | _) <;> simp [succ_le_succ]

Result:
no goals

Proof state:
n : ℕ
n1 : n ≠ 1
⊢ Nat.minFacProp n n.minFac

Tactic:
by_cases n0 : n = 0

Result:
case pos
n : ℕ
n1 : n ≠ 1
n0 : n = 0
⊢ Nat.minFacProp n n.minFac

case neg
n : ℕ
n1 : n ≠ 1
n0 : ¬n = 0
⊢ Nat.minFacProp n n.minFac

Proof state:
case pos
n : ℕ
n1 : n ≠ 1
n0 : ¬n = 0
n2 : 2 ≤ n
d2 : 2 ∣ n
⊢ Nat.minFacProp n 2

Tactic:
exact ⟨le_rfl, d2, fun k k2 _ => k2⟩

Result:
no goals

Proof state:
case neg
n : ℕ
n1 : n ≠ 1
n0 : ¬n = 0
n2 : 2 ≤ n
d2 : ¬2 ∣ n
m : ℕ
m2 : 2 ≤ m
d : m ∣ n
⊢ 2 = m → 2 ∣ n

Tactic:
exact fun e => e.symm ▸ d

Result:
no goals

Proof state:
case neg
n : ℕ
n1 : n ≠ 1
n0 : ¬n = 0
n2 : 2 ≤ n
⊢ Nat.minFacProp n (if 2 ∣ n then 2 else n.minFacAux 3)

Tactic:
by_cases d2 : 2 ∣ n <;> simp only [d2, ↓reduceIte]

Result:
case pos
n : ℕ
n1 : n ≠ 1
n0 : ¬n = 0
n2 : 2 ≤ n
d2 : 2 ∣ n
⊢ Nat.minFacProp n 2

case neg
n : ℕ
n1 : n ≠ 1
n0 : ¬n = 0
n2 : 2 ≤ n
d2 : ¬2 ∣ n
⊢ Nat.minFacProp n (n.minFacAux 3)

Proof state:
n : ℕ
n1 : n ≠ 1
n0 : ¬n = 0
⊢ 2 ≤ n

Tactic:
revert n0 n1

Result:
n : ℕ
⊢ n ≠ 1 → ¬n = 0 → 2 ≤ n

Proof state:
case pos
n : ℕ
n1 : n ≠ 1
n0 : n = 0
⊢ Nat.minFacProp n n.minFac

Tactic:
simp [n0, minFacProp, GE.ge]

Result:
no goals

Proof state:
case neg
n : ℕ
n1 : n ≠ 1
n0 : ¬n = 0
⊢ Nat.minFacProp n n.minFac

Tactic:
have n2 : 2 ≤ n := by
  revert n0 n1
  rcases n with (_ | _ | _) <;> simp [succ_le_succ]

Result:
case neg
n : ℕ
n1 : n ≠ 1
n0 : ¬n = 0
n2 : 2 ≤ n
⊢ Nat.minFacProp n n.minFac

Proof state:
case neg
n : ℕ
n1 : n ≠ 1
n0 : ¬n = 0
n2 : 2 ≤ n
d2 : ¬2 ∣ n
⊢ Nat.minFacProp n (n.minFacAux 3)

Tactic:
refine
  minFacAux_has_prop n2 3 0 rfl fun m m2 d => (Nat.eq_or_lt_of_le m2).resolve_left (mt ?_ d2)

Result:
case neg
n : ℕ
n1 : n ≠ 1
n0 : ¬n = 0
n2 : 2 ≤ n
d2 : ¬2 ∣ n
m : ℕ
m2 : 2 ≤ m
d : m ∣ n
⊢ 2 = m → 2 ∣ n

Proof state:
case neg
n : ℕ
n1 : n ≠ 1
n0 : ¬n = 0
n2 : 2 ≤ n
⊢ Nat.minFacProp n n.minFac

Tactic:
simp only [minFac_eq, Nat.isUnit_iff]

Result:
case neg
n : ℕ
n1 : n ≠ 1
n0 : ¬n = 0
n2 : 2 ≤ n
⊢ Nat.minFacProp n (if 2 ∣ n then 2 else n.minFacAux 3)
-- Mathlib/Analysis/SpecialFunctions/Trigonometric/Angle.lean
theorem abs_toReal_neg_coe_eq_self_iff {θ : ℝ} : |(-θ : Angle).toReal| = θ ↔ 0 ≤ θ ∧ θ ≤ π

Proof state:
case pos
θ : ℝ
h : 0 ≤ θ ∧ θ ≤ π
hnegpi : θ = π
⊢ |(-↑θ).toReal| = θ

Tactic:
simp [hnegpi, Real.pi_pos.le]

Result:
no goals

Proof state:
case neg
θ : ℝ
h : 0 ≤ θ ∧ θ ≤ π
hnegpi : ¬θ = π
⊢ |(-↑θ).toReal| = θ

Tactic:
rw [← coe_neg,
  toReal_coe_eq_self_iff.2
    ⟨neg_lt_neg (lt_of_le_of_ne h.2 hnegpi), (neg_nonpos.2 h.1).trans Real.pi_pos.le⟩,
  abs_neg, abs_eq_self.2 h.1]

Result:
no goals

Proof state:
θ : ℝ
⊢ |(-↑θ).toReal| = θ ↔ 0 ≤ θ ∧ θ ≤ π

Tactic:
refine ⟨fun h => h ▸ ⟨abs_nonneg _, abs_toReal_le_pi _⟩, fun h => ?_⟩

Result:
θ : ℝ
h : 0 ≤ θ ∧ θ ≤ π
⊢ |(-↑θ).toReal| = θ

Proof state:
θ : ℝ
h : 0 ≤ θ ∧ θ ≤ π
⊢ |(-↑θ).toReal| = θ

Tactic:
by_cases hnegpi : θ = π

Result:
case pos
θ : ℝ
h : 0 ≤ θ ∧ θ ≤ π
hnegpi : θ = π
⊢ |(-↑θ).toReal| = θ

case neg
θ : ℝ
h : 0 ≤ θ ∧ θ ≤ π
hnegpi : ¬θ = π
⊢ |(-↑θ).toReal| = θ
-- Mathlib/RingTheory/Polynomial/Basic.lean
theorem linearIndependent_powers_iff_aeval (f : M →ₗ[R] M) (v : M) :
    (LinearIndependent R fun n : ℕ => (f ^ n) v) ↔ ∀ p : R[X], aeval f p v = 0 → p = 0

Proof state:
R : Type u
M : Type w
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : M →ₗ[R] M
v : M
⊢ (∀ (l : ℕ →₀ R), (l.sum fun i a => a • (f ^ i) v) = 0 → l = 0) ↔
    ∀ (q : AddMonoidAlgebra R ℕ), ({ toFinsupp := q }.sum fun n b => b • (f ^ n) v) = 0 → q = 0

Tactic:
exact Iff.rfl

Result:
no goals

Proof state:
R : Type u
M : Type w
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : M →ₗ[R] M
v : M
⊢ (LinearIndependent R fun n => (f ^ n) v) ↔ ∀ (p : R[X]), ((aeval f) p) v = 0 → p = 0

Tactic:
rw [linearIndependent_iff]

Result:
R : Type u
M : Type w
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : M →ₗ[R] M
v : M
⊢ (∀ (l : ℕ →₀ R), (Finsupp.linearCombination R fun n => (f ^ n) v) l = 0 → l = 0) ↔
    ∀ (p : R[X]), ((aeval f) p) v = 0 → p = 0

Proof state:
R : Type u
M : Type w
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : M →ₗ[R] M
v : M
⊢ (∀ (l : ℕ →₀ R), (Finsupp.linearCombination R fun n => (f ^ n) v) l = 0 → l = 0) ↔
    ∀ (p : R[X]), ((aeval f) p) v = 0 → p = 0

Tactic:
simp only [Finsupp.linearCombination_apply, aeval_endomorphism, forall_iff_forall_finsupp, Sum,
  support, coeff, ofFinsupp_eq_zero]

Result:
R : Type u
M : Type w
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : M →ₗ[R] M
v : M
⊢ (∀ (l : ℕ →₀ R), (l.sum fun i a => a • (f ^ i) v) = 0 → l = 0) ↔
    ∀ (q : AddMonoidAlgebra R ℕ), ({ toFinsupp := q }.sum fun n b => b • (f ^ n) v) = 0 → q = 0
-- Mathlib/CategoryTheory/Shift/Basic.lean
lemma shiftFunctorAdd_add_zero_inv_app (a : A) (X : C) : (shiftFunctorAdd C a 0).inv.app X =
    (shiftFunctorZero C A).hom.app (X⟦a⟧) ≫ eqToHom (by dsimp; rw [add_zero])

Proof state:
C : Type u
A : Type u_1
inst✝² : Category.{v, u} C
inst✝¹ : AddMonoid A
inst✝ : HasShift C A
a : A
X : C
⊢ (shiftFunctorAdd C a 0).inv.app X = (shiftFunctorZero C A).hom.app ((shiftFunctor C a).obj X) ≫ eqToHom ⋯

Tactic:
simp [← shiftFunctorAdd'_add_zero_inv_app, shiftFunctorAdd']

Result:
no goals

Proof state:
C : Type u
A : Type u_1
inst✝² : Category.{v, u} C
inst✝¹ : AddMonoid A
inst✝ : HasShift C A
a : A
X : C
⊢ (shiftFunctor C a).obj X = (shiftFunctor C (a + 0)).obj X

Tactic:
rw [add_zero]

Result:
no goals

Proof state:
C : Type u
A : Type u_1
inst✝² : Category.{v, u} C
inst✝¹ : AddMonoid A
inst✝ : HasShift C A
a : A
X : C
⊢ (𝟭 C).obj ((shiftFunctor C a).obj X) = (shiftFunctor C (a + 0)).obj X

Tactic:
dsimp

Result:
C : Type u
A : Type u_1
inst✝² : Category.{v, u} C
inst✝¹ : AddMonoid A
inst✝ : HasShift C A
a : A
X : C
⊢ (shiftFunctor C a).obj X = (shiftFunctor C (a + 0)).obj X
-- Mathlib/Data/PFun.lean
theorem Part.bind_comp (f : β →. γ) (g : α →. β) (a : Part α) :
    a.bind (f.comp g) = (a.bind g).bind f

Proof state:
case H
α : Type u_1
β : Type u_2
γ : Type u_3
f : β →. γ
g : α →. β
a : Part α
c : γ
⊢ (∃ a_1 x, a_1 ∈ a ∧ x ∈ g a_1 ∧ c ∈ f x) ↔ ∃ a_1 x, (x ∈ a ∧ a_1 ∈ g x) ∧ c ∈ f a_1

Tactic:
rw [exists_comm]

Result:
case H
α : Type u_1
β : Type u_2
γ : Type u_3
f : β →. γ
g : α →. β
a : Part α
c : γ
⊢ (∃ b, ∃ a_1 ∈ a, b ∈ g a_1 ∧ c ∈ f b) ↔ ∃ a_1 x, (x ∈ a ∧ a_1 ∈ g x) ∧ c ∈ f a_1

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
f : β →. γ
g : α →. β
a : Part α
⊢ a.bind (f.comp g) = (a.bind g).bind f

Tactic:
ext c

Result:
case H
α : Type u_1
β : Type u_2
γ : Type u_3
f : β →. γ
g : α →. β
a : Part α
c : γ
⊢ c ∈ a.bind (f.comp g) ↔ c ∈ (a.bind g).bind f

Proof state:
case H
α : Type u_1
β : Type u_2
γ : Type u_3
f : β →. γ
g : α →. β
a : Part α
c : γ
⊢ (∃ b, ∃ a_1 ∈ a, b ∈ g a_1 ∧ c ∈ f b) ↔ ∃ a_1 x, (x ∈ a ∧ a_1 ∈ g x) ∧ c ∈ f a_1

Tactic:
simp_rw [and_assoc]

Result:
no goals

Proof state:
case H
α : Type u_1
β : Type u_2
γ : Type u_3
f : β →. γ
g : α →. β
a : Part α
c : γ
⊢ c ∈ a.bind (f.comp g) ↔ c ∈ (a.bind g).bind f

Tactic:
simp_rw [Part.mem_bind_iff, comp_apply, Part.mem_bind_iff, ← exists_and_right, ← exists_and_left]

Result:
case H
α : Type u_1
β : Type u_2
γ : Type u_3
f : β →. γ
g : α →. β
a : Part α
c : γ
⊢ (∃ a_1 x, a_1 ∈ a ∧ x ∈ g a_1 ∧ c ∈ f x) ↔ ∃ a_1 x, (x ∈ a ∧ a_1 ∈ g x) ∧ c ∈ f a_1
-- Mathlib/.lake/packages/lean4/src/lean/Init/SimpLemmas.lean
theorem decide_not [g : Decidable p] [h : Decidable (Not p)] : decide (Not p) = !(decide p)

Proof state:
case isTrue
p : Prop
h : Decidable ¬p
gp : p
⊢ (decide ¬p) = !decide p

Tactic:
simp [gp]

Result:
no goals

Proof state:
case isTrue
p : Prop
h : Decidable ¬p
h✝ : p
⊢ (decide ¬p) = !decide p

Tactic:
rename_i gp

Result:
case isTrue
p : Prop
h : Decidable ¬p
gp : p
⊢ (decide ¬p) = !decide p

Proof state:
p : Prop
g : Decidable p
h : Decidable ¬p
⊢ (decide ¬p) = !decide p

Tactic:
cases g <;> (rename_i gp; simp [gp])

Result:
no goals
-- Mathlib/Data/ENNReal/Inv.lean
theorem eq_inv_of_mul_eq_one_left (h : a * b = 1) : a = b⁻¹

Proof state:
a b : ℝ≥0∞
h : a * b = 1
⊢ b ≠ ⊤

Tactic:
rintro rfl

Result:
a : ℝ≥0∞
h : a * ⊤ = 1
⊢ False

Proof state:
a : ℝ≥0∞
h : a * ⊤ = 1
⊢ False

Tactic:
simp [left_ne_zero_of_mul_eq_one h] at h

Result:
no goals

Proof state:
a b : ℝ≥0∞
h : a * b = 1
⊢ a = b⁻¹

Tactic:
rw [← mul_one a, ← ENNReal.mul_inv_cancel (right_ne_zero_of_mul_eq_one h), ← mul_assoc, h,
  one_mul]

Result:
a b : ℝ≥0∞
h : a * b = 1
⊢ b ≠ ⊤
-- Mathlib/Topology/Algebra/Order/Floor.lean
theorem tendsto_floor_left_pure_ceil_sub_one (x : α) :
    Tendsto (floor : α → ℤ) (𝓝[<] x) (pure (⌈x⌉ - 1)) :=
  have h₁ : ↑(⌈x⌉ - 1) < x

Proof state:
α : Type u_1
inst✝³ : LinearOrderedRing α
inst✝² : FloorRing α
inst✝¹ : TopologicalSpace α
inst✝ : OrderClosedTopology α
x : α
⊢ ↑(⌈x⌉ - 1) < x

Tactic:
rw [cast_sub, cast_one, sub_lt_iff_lt_add]

Result:
α : Type u_1
inst✝³ : LinearOrderedRing α
inst✝² : FloorRing α
inst✝¹ : TopologicalSpace α
inst✝ : OrderClosedTopology α
x : α
⊢ ↑⌈x⌉ < x + 1

Proof state:
α : Type u_1
inst✝³ : LinearOrderedRing α
inst✝² : FloorRing α
inst✝¹ : TopologicalSpace α
inst✝ : OrderClosedTopology α
x : α
h₁ : ↑(⌈x⌉ - 1) < x
⊢ x ≤ ↑⌈x⌉

Tactic:
exact le_ceil _

Result:
no goals

Proof state:
α : Type u_1
inst✝³ : LinearOrderedRing α
inst✝² : FloorRing α
inst✝¹ : TopologicalSpace α
inst✝ : OrderClosedTopology α
x : α
h₁ : ↑(⌈x⌉ - 1) < x
⊢ x ≤ ↑(⌈x⌉ - 1) + 1

Tactic:
rw [cast_sub, cast_one, sub_add_cancel]

Result:
α : Type u_1
inst✝³ : LinearOrderedRing α
inst✝² : FloorRing α
inst✝¹ : TopologicalSpace α
inst✝ : OrderClosedTopology α
x : α
h₁ : ↑(⌈x⌉ - 1) < x
⊢ x ≤ ↑⌈x⌉

Proof state:
α : Type u_1
inst✝³ : LinearOrderedRing α
inst✝² : FloorRing α
inst✝¹ : TopologicalSpace α
inst✝ : OrderClosedTopology α
x : α
⊢ ↑⌈x⌉ < x + 1

Tactic:
exact ceil_lt_add_one _

Result:
no goals
-- Mathlib/Algebra/Homology/ShortComplex/HomologicalComplex.lean
@[reassoc (attr := simp)]
lemma homologyι_comp_fromOpcycles :
    K.homologyι i ≫ K.fromOpcycles i j = 0 :=
  K.homologyι_descOpcycles_eq_zero_of_boundary (K.d i j) _ rfl (𝟙 _) (by simp)

Proof state:
C : Type u_1
inst✝² : Category.{u_3, u_1} C
inst✝¹ : HasZeroMorphisms C
ι : Type u_2
c : ComplexShape ι
K : HomologicalComplex C c
i j : ι
inst✝ : K.HasHomology i
⊢ K.d i j = K.d i j ≫ 𝟙 (K.X j)

Tactic:
simp

Result:
no goals
-- Mathlib/MeasureTheory/Integral/Lebesgue.lean
theorem setLIntegral_congr {f : α → ℝ≥0∞} {s t : Set α} (h : s =ᵐ[μ] t) :
    ∫⁻ x in s, f x ∂μ = ∫⁻ x in t, f x ∂μ

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
s t : Set α
h : s =ᶠ[ae μ] t
⊢ ∫⁻ (x : α) in s, f x ∂μ = ∫⁻ (x : α) in t, f x ∂μ

Tactic:
rw [Measure.restrict_congr_set h]

Result:
no goals
-- Mathlib/Data/Matrix/Mul.lean
theorem op_smul_eq_mul_diagonal [Fintype n] [DecidableEq n] (M : Matrix m n α) (a : α) :
    MulOpposite.op a • M = M * (diagonal fun _ : n => a)

Proof state:
m : Type u_2
n : Type u_3
α : Type v
inst✝² : NonUnitalNonAssocSemiring α
inst✝¹ : Fintype n
inst✝ : DecidableEq n
M : Matrix m n α
a : α
⊢ MulOpposite.op a • M = M * diagonal fun x => a

Tactic:
ext

Result:
case a
m : Type u_2
n : Type u_3
α : Type v
inst✝² : NonUnitalNonAssocSemiring α
inst✝¹ : Fintype n
inst✝ : DecidableEq n
M : Matrix m n α
a : α
i✝ : m
j✝ : n
⊢ (MulOpposite.op a • M) i✝ j✝ = (M * diagonal fun x => a) i✝ j✝

Proof state:
case a
m : Type u_2
n : Type u_3
α : Type v
inst✝² : NonUnitalNonAssocSemiring α
inst✝¹ : Fintype n
inst✝ : DecidableEq n
M : Matrix m n α
a : α
i✝ : m
j✝ : n
⊢ (MulOpposite.op a • M) i✝ j✝ = (M * diagonal fun x => a) i✝ j✝

Tactic:
simp

Result:
no goals
-- Mathlib/Logic/Equiv/PartialEquiv.lean
theorem image_source_inter_eq' (s : Set α) : e '' (e.source ∩ s) = e.target ∩ e.symm ⁻¹' s

Proof state:
α : Type u_1
β : Type u_2
e : PartialEquiv α β
s : Set α
⊢ ↑e '' (e.source ∩ s) = e.target ∩ ↑e.symm ⁻¹' s

Tactic:
rw [inter_comm, e.leftInvOn.image_inter', image_source_eq_target, inter_comm]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem xor_assoc (x y z : BitVec w) :
    x ^^^ y ^^^ z = x ^^^ (y ^^^ z)

Proof state:
case pred
w : Nat
x y z : BitVec w
i : Nat
a✝ : i < w
⊢ (x ^^^ y ^^^ z).getLsbD i = (x ^^^ (y ^^^ z)).getLsbD i

Tactic:
simp [Bool.xor_assoc]

Result:
no goals

Proof state:
w : Nat
x y z : BitVec w
⊢ x ^^^ y ^^^ z = x ^^^ (y ^^^ z)

Tactic:
ext i

Result:
case pred
w : Nat
x y z : BitVec w
i : Nat
a✝ : i < w
⊢ (x ^^^ y ^^^ z).getLsbD i = (x ^^^ (y ^^^ z)).getLsbD i
-- Mathlib/Data/Set/Lattice.lean
theorem nonempty_iInter₂ {s : ∀ i, κ i → Set α} :
    (⋂ (i) (j), s i j).Nonempty ↔ ∃ a, ∀ i j, a ∈ s i j

Proof state:
α : Type u_1
ι : Sort u_5
κ : ι → Sort u_8
s : (i : ι) → κ i → Set α
⊢ (⋂ i, ⋂ j, s i j).Nonempty ↔ ∃ a, ∀ (i : ι) (j : κ i), a ∈ s i j

Tactic:
simp

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Attach.lean
theorem unattach_mkVector {p : α → Prop} {n : Nat} {x : { x // p x }} :
    (mkVector n x).unattach = mkVector n x.1

Proof state:
α : Type u_1
p : α → Prop
n : Nat
x : { x // p x }
⊢ (mkVector n x).unattach = mkVector n x.val

Tactic:
simp [unattach]

Result:
no goals
-- Mathlib/GroupTheory/Complement.lean
@[to_additive (attr := simp)]
lemma not_isComplement_empty_right : ¬ IsComplement S ∅ :=
  fun h ↦ by simpa [eq_comm (a := ∅)] using h.mul_eq

Proof state:
G : Type u_1
inst✝ : Group G
S : Set G
h : IsComplement S ∅
⊢ False

Tactic:
simpa [eq_comm (a := ∅)] using h.mul_eq

Result:
no goals
-- Mathlib/MeasureTheory/Measure/Comap.lean
theorem ae_eq_image_of_ae_eq_comap (f : α → β) (μ : Measure β) (hfi : Injective f)
    (hf : ∀ s, MeasurableSet s → NullMeasurableSet (f '' s) μ)
    {s t : Set α} (hst : s =ᵐ[comap f μ] t) : f '' s =ᵐ[μ] f '' t

Proof state:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
f : α → β
μ : Measure β
hfi : Injective f
hf : ∀ (s : Set α), MeasurableSet s → NullMeasurableSet (f '' s) μ
s t : Set α
hst : (comap f μ) {a | ¬s a = t a} = 0
h_eq_α : {a | ¬s a = t a} = s \ t ∪ t \ s
h_eq_β : {a | ¬(f '' s) a = (f '' t) a} = f '' (s \ t ∪ t \ s)
⊢ μ {a | ¬(f '' s) a = (f '' t) a} = 0

Tactic:
rw [h_eq_β]

Result:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
f : α → β
μ : Measure β
hfi : Injective f
hf : ∀ (s : Set α), MeasurableSet s → NullMeasurableSet (f '' s) μ
s t : Set α
hst : (comap f μ) {a | ¬s a = t a} = 0
h_eq_α : {a | ¬s a = t a} = s \ t ∪ t \ s
h_eq_β : {a | ¬(f '' s) a = (f '' t) a} = f '' (s \ t ∪ t \ s)
⊢ μ (f '' (s \ t ∪ t \ s)) = 0

Proof state:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
f : α → β
μ : Measure β
hfi : Injective f
hf : ∀ (s : Set α), MeasurableSet s → NullMeasurableSet (f '' s) μ
s t : Set α
hst : (comap f μ) {a | ¬s a = t a} = 0
h_eq_α : {a | ¬s a = t a} = s \ t ∪ t \ s
h_eq_β : {a | ¬(f '' s) a = (f '' t) a} = f '' (s \ t ∪ t \ s)
⊢ μ (f '' (s \ t ∪ t \ s)) = 0

Tactic:
rw [h_eq_α] at hst

Result:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
f : α → β
μ : Measure β
hfi : Injective f
hf : ∀ (s : Set α), MeasurableSet s → NullMeasurableSet (f '' s) μ
s t : Set α
hst : (comap f μ) (s \ t ∪ t \ s) = 0
h_eq_α : {a | ¬s a = t a} = s \ t ∪ t \ s
h_eq_β : {a | ¬(f '' s) a = (f '' t) a} = f '' (s \ t ∪ t \ s)
⊢ μ (f '' (s \ t ∪ t \ s)) = 0
-- Mathlib/LinearAlgebra/Matrix/LDL.lean
theorem LDL.lower_conj_diag : LDL.lower hS * LDL.diag hS * (LDL.lower hS)ᴴ = S

Proof state:
𝕜 : Type u_1
inst✝⁴ : RCLike 𝕜
n : Type u_2
inst✝³ : LinearOrder n
inst✝² : WellFoundedLT n
inst✝¹ : LocallyFiniteOrderBot n
S : Matrix n n 𝕜
inst✝ : Fintype n
hS : S.PosDef
⊢ diag hS = lowerInv hS * S * (lowerInv hS)ᴴ

Tactic:
exact LDL.diag_eq_lowerInv_conj hS

Result:
no goals

Proof state:
𝕜 : Type u_1
inst✝⁴ : RCLike 𝕜
n : Type u_2
inst✝³ : LinearOrder n
inst✝² : WellFoundedLT n
inst✝¹ : LocallyFiniteOrderBot n
S : Matrix n n 𝕜
inst✝ : Fintype n
hS : S.PosDef
⊢ lower hS * diag hS * (lower hS)ᴴ = S

Tactic:
rw [LDL.lower, conjTranspose_nonsing_inv, Matrix.mul_assoc,
  Matrix.inv_mul_eq_iff_eq_mul_of_invertible (LDL.lowerInv hS),
  Matrix.mul_inv_eq_iff_eq_mul_of_invertible]

Result:
𝕜 : Type u_1
inst✝⁴ : RCLike 𝕜
n : Type u_2
inst✝³ : LinearOrder n
inst✝² : WellFoundedLT n
inst✝¹ : LocallyFiniteOrderBot n
S : Matrix n n 𝕜
inst✝ : Fintype n
hS : S.PosDef
⊢ diag hS = lowerInv hS * S * (lowerInv hS)ᴴ
-- Mathlib/CategoryTheory/Limits/Constructions/EventuallyConstant.lean
lemma coconeιApp_eq (j j' : J) (α : j ⟶ j') (β : i₀ ⟶ j') :
    h.coconeιApp j = F.map α ≫ (h.isoMap β ⟨𝟙 _⟩).inv

Proof state:
J : Type u_1
C : Type u_2
inst✝² : Category.{u_3, u_1} J
inst✝¹ : Category.{u_4, u_2} C
F : J ⥤ C
i₀ : J
h : F.IsEventuallyConstantFrom i₀
inst✝ : IsFiltered J
j j' : J
α : j ⟶ j'
β : i₀ ⟶ j'
⊢ h.coconeιApp j = F.map α ≫ (h.isoMap β ⋯).inv

Tactic:
obtain ⟨s, γ, δ, h₁, h₂⟩ := IsFiltered.bowtie
  (IsFiltered.leftToMax i₀ j) β (IsFiltered.rightToMax i₀ j) α

Result:
case intro.intro.intro.intro
J : Type u_1
C : Type u_2
inst✝² : Category.{u_3, u_1} J
inst✝¹ : Category.{u_4, u_2} C
F : J ⥤ C
i₀ : J
h : F.IsEventuallyConstantFrom i₀
inst✝ : IsFiltered J
j j' : J
α : j ⟶ j'
β : i₀ ⟶ j'
s : J
γ : IsFiltered.max i₀ j ⟶ s
δ : j' ⟶ s
h₁ : leftToMax i₀ j ≫ γ = β ≫ δ
h₂ : rightToMax i₀ j ≫ γ = α ≫ δ
⊢ h.coconeιApp j = F.map α ≫ (h.isoMap β ⋯).inv

Proof state:
case intro.intro.intro.intro
J : Type u_1
C : Type u_2
inst✝² : Category.{u_3, u_1} J
inst✝¹ : Category.{u_4, u_2} C
F : J ⥤ C
i₀ : J
h : F.IsEventuallyConstantFrom i₀
inst✝ : IsFiltered J
j j' : J
α : j ⟶ j'
β : i₀ ⟶ j'
s : J
γ : IsFiltered.max i₀ j ⟶ s
δ : j' ⟶ s
h₁ : leftToMax i₀ j ≫ γ = β ≫ δ
h₂ : rightToMax i₀ j ≫ γ = α ≫ δ
⊢ F.map (rightToMax i₀ j) ≫ (h.isoMap (leftToMax i₀ j) ⋯).inv = F.map α ≫ (h.isoMap β ⋯).inv

Tactic:
rw [← cancel_mono ((h.isoMap β ⟨𝟙 _⟩).hom), assoc, assoc, isoMap_hom, isoMap_inv_hom_id,
  comp_id, ← cancel_mono (h.isoMap δ ⟨β⟩).hom, isoMap_hom, assoc, assoc, ← F.map_comp α δ,
  ← h₂, F.map_comp, ← F.map_comp β δ, ← h₁, F.map_comp, isoMap_inv_hom_id_assoc]

Result:
no goals

Proof state:
case intro.intro.intro.intro
J : Type u_1
C : Type u_2
inst✝² : Category.{u_3, u_1} J
inst✝¹ : Category.{u_4, u_2} C
F : J ⥤ C
i₀ : J
h : F.IsEventuallyConstantFrom i₀
inst✝ : IsFiltered J
j j' : J
α : j ⟶ j'
β : i₀ ⟶ j'
s : J
γ : IsFiltered.max i₀ j ⟶ s
δ : j' ⟶ s
h₁ : leftToMax i₀ j ≫ γ = β ≫ δ
h₂ : rightToMax i₀ j ≫ γ = α ≫ δ
⊢ h.coconeιApp j = F.map α ≫ (h.isoMap β ⋯).inv

Tactic:
dsimp [coconeιApp]

Result:
case intro.intro.intro.intro
J : Type u_1
C : Type u_2
inst✝² : Category.{u_3, u_1} J
inst✝¹ : Category.{u_4, u_2} C
F : J ⥤ C
i₀ : J
h : F.IsEventuallyConstantFrom i₀
inst✝ : IsFiltered J
j j' : J
α : j ⟶ j'
β : i₀ ⟶ j'
s : J
γ : IsFiltered.max i₀ j ⟶ s
δ : j' ⟶ s
h₁ : leftToMax i₀ j ≫ γ = β ≫ δ
h₂ : rightToMax i₀ j ≫ γ = α ≫ δ
⊢ F.map (rightToMax i₀ j) ≫ (h.isoMap (leftToMax i₀ j) ⋯).inv = F.map α ≫ (h.isoMap β ⋯).inv
-- Mathlib/MeasureTheory/Measure/AEMeasurable.lean
theorem aemeasurable_indicator_iff₀ {s} (hs : NullMeasurableSet s μ) :
    AEMeasurable (indicator s f) μ ↔ AEMeasurable f (μ.restrict s)

Proof state:
α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
f : α → β
μ : Measure α
inst✝ : Zero β
s : Set α
hs : NullMeasurableSet s μ
⊢ AEMeasurable (s.indicator f) μ ↔ AEMeasurable f (μ.restrict s)

Tactic:
rcases hs with ⟨t, ht, hst⟩

Result:
case intro.intro
α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
f : α → β
μ : Measure α
inst✝ : Zero β
s t : Set α
ht : MeasurableSet t
hst : s =ᶠ[ae μ] t
⊢ AEMeasurable (s.indicator f) μ ↔ AEMeasurable f (μ.restrict s)

Proof state:
case intro.intro
α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
f : α → β
μ : Measure α
inst✝ : Zero β
s t : Set α
ht : MeasurableSet t
hst : s =ᶠ[ae μ] t
⊢ AEMeasurable (s.indicator f) μ ↔ AEMeasurable f (μ.restrict s)

Tactic:
rw [← aemeasurable_congr (indicator_ae_eq_of_ae_eq_set hst.symm), aemeasurable_indicator_iff ht,
    restrict_congr_set hst]

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Walk.lean
@[simp]
lemma concat_dropLast (p : G.Walk x y) (hp : G.Adj p.penultimate y) :
    p.dropLast.concat hp = p

Proof state:
V : Type u
G : SimpleGraph V
x y : V
p : G.Walk x y
hp : G.Adj p.penultimate y
⊢ p.dropLast.concat hp = p

Tactic:
induction p with
| nil => simp at hp
| cons hadj p hind =>
  cases p with
  | nil => rfl
  | _ => simp [hind]

Result:
no goals

Proof state:
case cons.nil
V : Type u
G : SimpleGraph V
x y u✝ v✝ : V
hadj : G.Adj u✝ v✝
hind : ∀ (hp : G.Adj nil.penultimate v✝), nil.dropLast.concat hp = nil
hp : G.Adj (cons hadj nil).penultimate v✝
⊢ (cons hadj nil).dropLast.concat hp = cons hadj nil

Tactic:
rfl

Result:
no goals

Proof state:
case nil
V : Type u
G : SimpleGraph V
x y u✝ : V
hp : G.Adj nil.penultimate u✝
⊢ nil.dropLast.concat hp = nil

Tactic:
simp at hp

Result:
no goals

Proof state:
case cons
V : Type u
G : SimpleGraph V
x y u✝ v✝ w✝ : V
hadj : G.Adj u✝ v✝
p : G.Walk v✝ w✝
hind : ∀ (hp : G.Adj p.penultimate w✝), p.dropLast.concat hp = p
hp : G.Adj (cons hadj p).penultimate w✝
⊢ (cons hadj p).dropLast.concat hp = cons hadj p

Tactic:
cases p with
| nil => rfl
| _ => simp [hind]

Result:
no goals

Proof state:
case cons.cons
V : Type u
G : SimpleGraph V
x y u✝ v✝¹ w✝ : V
hadj : G.Adj u✝ v✝¹
v✝ : V
h✝ : G.Adj v✝¹ v✝
p✝ : G.Walk v✝ w✝
hind : ∀ (hp : G.Adj (cons h✝ p✝).penultimate w✝), (cons h✝ p✝).dropLast.concat hp = cons h✝ p✝
hp : G.Adj (cons hadj (cons h✝ p✝)).penultimate w✝
⊢ (cons hadj (cons h✝ p✝)).dropLast.concat hp = cons hadj (cons h✝ p✝)

Tactic:
simp [hind]

Result:
no goals