harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Data/Matroid/Basic.lean
theorem Indep.subset_isBasis'_of_subset (hI : M.Indep I) (hIX : I ⊆ X) :
    ∃ J, M.IsBasis' J X ∧ I ⊆ J

Proof state:
α : Type u_1
M : Matroid α
I X : Set α
hI : M.Indep I
hIX : I ⊆ X
⊢ ∃ J, M.IsBasis J (X ∩ M.E) ∧ I ⊆ J

Tactic:
exact hI.subset_isBasis_of_subset (subset_inter hIX hI.subset_ground)

Result:
no goals

Proof state:
α : Type u_1
M : Matroid α
I X : Set α
hI : M.Indep I
hIX : I ⊆ X
⊢ ∃ J, M.IsBasis' J X ∧ I ⊆ J

Tactic:
simp_rw [isBasis'_iff_isBasis_inter_ground]

Result:
α : Type u_1
M : Matroid α
I X : Set α
hI : M.Indep I
hIX : I ⊆ X
⊢ ∃ J, M.IsBasis J (X ∩ M.E) ∧ I ⊆ J
-- Mathlib/Data/Semiquot.lean
theorem mem_bind (q : Semiquot α) (f : α → Semiquot β) (b : β) :
    b ∈ bind q f ↔ ∃ a ∈ q, b ∈ f a

Proof state:
α : Type u_1
β : Type u_2
q : Semiquot α
f : α → Semiquot β
b : β
⊢ b ∈ q.bind f ↔ ∃ a, ∃ (_ : a ∈ q), b ∈ f a

Tactic:
exact Set.mem_iUnion₂

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
q : Semiquot α
f : α → Semiquot β
b : β
⊢ b ∈ q.bind f ↔ ∃ a ∈ q, b ∈ f a

Tactic:
simp_rw [← exists_prop]

Result:
α : Type u_1
β : Type u_2
q : Semiquot α
f : α → Semiquot β
b : β
⊢ b ∈ q.bind f ↔ ∃ a, ∃ (_ : a ∈ q), b ∈ f a
-- Mathlib/Topology/Sheaves/Presheaf.lean
theorem restrict_restrict
    {F : X.Presheaf C} {U V W : Opens X} (e₁ : U ≤ V) (e₂ : V ≤ W) (x : ToType (F.obj (op W))) :
    x |_ V |_ U = x |_ U

Proof state:
X : TopCat
C : Type u_1
inst✝² : Category.{u_5, u_1} C
FC : C → C → Type u_2
CC : C → Type u_3
inst✝¹ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝ : ConcreteCategory C FC
F : Presheaf C X
U V W : Opens ↑X
e₁ : U ≤ V
e₂ : V ≤ W
x : ToType (F.obj (op W))
⊢ ((x |_ V) e₂ |_ U) e₁ = (x |_ U) ⋯

Tactic:
delta restrictOpen restrict

Result:
X : TopCat
C : Type u_1
inst✝² : Category.{u_5, u_1} C
FC : C → C → Type u_2
CC : C → Type u_3
inst✝¹ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝ : ConcreteCategory C FC
F : Presheaf C X
U V W : Opens ↑X
e₁ : U ≤ V
e₂ : V ≤ W
x : ToType (F.obj (op W))
⊢ (ConcreteCategory.hom (F.map (homOfLE e₁).op)) ((ConcreteCategory.hom (F.map (homOfLE e₂).op)) x) =
    (ConcreteCategory.hom (F.map (homOfLE ⋯).op)) x

Proof state:
X : TopCat
C : Type u_1
inst✝² : Category.{u_5, u_1} C
FC : C → C → Type u_2
CC : C → Type u_3
inst✝¹ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝ : ConcreteCategory C FC
F : Presheaf C X
U V W : Opens ↑X
e₁ : U ≤ V
e₂ : V ≤ W
x : ToType (F.obj (op W))
⊢ (ConcreteCategory.hom (F.map ((homOfLE e₂).op ≫ (homOfLE e₁).op))) x = (ConcreteCategory.hom (F.map (homOfLE ⋯).op)) x

Tactic:
rfl

Result:
no goals

Proof state:
X : TopCat
C : Type u_1
inst✝² : Category.{u_5, u_1} C
FC : C → C → Type u_2
CC : C → Type u_3
inst✝¹ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝ : ConcreteCategory C FC
F : Presheaf C X
U V W : Opens ↑X
e₁ : U ≤ V
e₂ : V ≤ W
x : ToType (F.obj (op W))
⊢ (ConcreteCategory.hom (F.map (homOfLE e₁).op)) ((ConcreteCategory.hom (F.map (homOfLE e₂).op)) x) =
    (ConcreteCategory.hom (F.map (homOfLE ⋯).op)) x

Tactic:
rw [← ConcreteCategory.comp_apply, ← Functor.map_comp]

Result:
X : TopCat
C : Type u_1
inst✝² : Category.{u_5, u_1} C
FC : C → C → Type u_2
CC : C → Type u_3
inst✝¹ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝ : ConcreteCategory C FC
F : Presheaf C X
U V W : Opens ↑X
e₁ : U ≤ V
e₂ : V ≤ W
x : ToType (F.obj (op W))
⊢ (ConcreteCategory.hom (F.map ((homOfLE e₂).op ≫ (homOfLE e₁).op))) x = (ConcreteCategory.hom (F.map (homOfLE ⋯).op)) x
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/RawLemmas.lean
theorem get?_insert_self [LawfulBEq α] (h : m.WF) {k : α} {v : β k} :
    (m.insert k v).get? k = some v

Proof state:
α : Type u
β : α → Type v
m : Raw α β
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : LawfulBEq α
h : m.WF
k : α
v : β k
⊢ (m.insert k v).get? k = some v

Tactic:
simp_to_raw using Raw₀.get?_insert_self

Result:
no goals
-- Mathlib/.lake/packages/batteries/Batteries/Data/String/Lemmas.lean
theorem Valid.le_endPos : ∀ {s p}, Valid s p → p ≤ endPos s
  | ⟨_⟩, ⟨_⟩, ⟨cs, cs', rfl, rfl⟩ => by simp [Nat.le_add_right]

Proof state:
cs cs' : List Char
⊢ { byteIdx := utf8ByteSize.go cs } ≤ { data := cs ++ cs' }.endPos

Tactic:
simp [Nat.le_add_right]

Result:
no goals
-- Mathlib/Combinatorics/HalesJewett.lean
theorem map_apply {α α' ι} (f : α → α') (l : Line α ι) (x : α) : l.map f (f x) = f ∘ l x

Proof state:
α : Type u_5
α' : Type u_6
ι : Type u_7
f : α → α'
l : Line α ι
x : α
⊢ ↑(map f l) (f x) = f ∘ ↑l x

Tactic:
simp only [Line.apply_def, Line.map, Option.getD_map, comp_def]

Result:
no goals
-- Mathlib/Data/PFunctor/Multivariate/Basic.lean
theorem const.get_map (f : α ⟹ β) (x : const n A α) : const.get (f <$$> x) = const.get x

Proof state:
n : ℕ
A : Type u
α β : TypeVec.{u} n
f : α ⟹ β
x : ↑(const n A) α
⊢ get (f <$$> x) = get x

Tactic:
cases x

Result:
case mk
n : ℕ
A : Type u
α β : TypeVec.{u} n
f : α ⟹ β
fst✝ : (const n A).A
snd✝ : (const n A).B fst✝ ⟹ α
⊢ get (f <$$> ⟨fst✝, snd✝⟩) = get ⟨fst✝, snd✝⟩

Proof state:
case mk
n : ℕ
A : Type u
α β : TypeVec.{u} n
f : α ⟹ β
fst✝ : (const n A).A
snd✝ : (const n A).B fst✝ ⟹ α
⊢ get (f <$$> ⟨fst✝, snd✝⟩) = get ⟨fst✝, snd✝⟩

Tactic:
rfl

Result:
no goals
-- Mathlib/Algebra/Ring/Periodic.lean
theorem Periodic.add_period [AddSemigroup α] (h1 : Periodic f c₁) (h2 : Periodic f c₂) :
    Periodic f (c₁ + c₂)

Proof state:
α : Type u_1
β : Type u_2
f : α → β
c₁ c₂ : α
inst✝ : AddSemigroup α
h1 : Periodic f c₁
h2 : Periodic f c₂
⊢ Periodic f (c₁ + c₂)

Tactic:
simp_all [← add_assoc]

Result:
no goals
-- Mathlib/Data/List/FinRange.lean
theorem finRange_eq_pmap_range (n : ℕ) : finRange n = (range n).pmap Fin.mk (by simp)

Proof state:
α : Type u
n : ℕ
⊢ ∀ a ∈ range n, a < n

Tactic:
simp

Result:
no goals

Proof state:
n : ℕ
⊢ finRange n = pmap Fin.mk (range n) ⋯

Tactic:
apply List.ext_getElem <;> simp [finRange]

Result:
no goals
-- Mathlib/MeasureTheory/Group/Action.lean
theorem measure_preimage_smul_of_nullMeasurableSet (hs : NullMeasurableSet s μ) (c : G) :
    μ ((c • ·) ⁻¹' s) = μ s

Proof state:
G : Type u
α : Type w
m : MeasurableSpace α
inst✝¹ : SMul G α
μ : Measure α
inst✝ : SMulInvariantMeasure G α μ
s : Set α
hs : NullMeasurableSet s μ
c : G
⊢ μ ((fun x => c • x) ⁻¹' s) = μ s

Tactic:
rw [← measure_toMeasurable s,
  ← SMulInvariantMeasure.measure_preimage_smul c (measurableSet_toMeasurable μ s)]

Result:
G : Type u
α : Type w
m : MeasurableSpace α
inst✝¹ : SMul G α
μ : Measure α
inst✝ : SMulInvariantMeasure G α μ
s : Set α
hs : NullMeasurableSet s μ
c : G
⊢ μ ((fun x => c • x) ⁻¹' s) = μ ((fun x => c • x) ⁻¹' toMeasurable μ s)

Proof state:
G : Type u
α : Type w
m : MeasurableSpace α
inst✝¹ : SMul G α
μ : Measure α
inst✝ : SMulInvariantMeasure G α μ
s : Set α
hs : NullMeasurableSet s μ
c : G
⊢ μ ((fun x => c • x) ⁻¹' s) = μ ((fun x => c • x) ⁻¹' toMeasurable μ s)

Tactic:
exact measure_congr (tendsto_smul_ae μ c hs.toMeasurable_ae_eq) |>.symm

Result:
no goals
-- Mathlib/Algebra/Group/Int/Even.lean
@[parity_simps] lemma even_pow {n : ℕ} : Even (m ^ n) ↔ Even m ∧ n ≠ 0

Proof state:
m : ℤ
n : ℕ
⊢ Even (m ^ n) ↔ Even m ∧ n ≠ 0

Tactic:
induction n <;> simp [*, even_mul, pow_succ]

Result:
case succ
m : ℤ
n✝ : ℕ
a✝ : Even (m ^ n✝) ↔ Even m ∧ n✝ ≠ 0
⊢ Even m → ¬n✝ = 0 → Even m

Proof state:
case succ
m : ℤ
n✝ : ℕ
a✝ : Even (m ^ n✝) ↔ Even m ∧ n✝ ≠ 0
⊢ Even m → ¬n✝ = 0 → Even m

Tactic:
tauto

Result:
no goals
-- Mathlib/Algebra/Homology/TotalComplex.lean
@[reassoc (attr := simp)]
lemma ιTotal_map (i₁ : I₁) (i₂ : I₂) (i₁₂ : I₁₂) (h : ComplexShape.π c₁ c₂ c₁₂ (i₁, i₂) = i₁₂) :
    K.ιTotal c₁₂ i₁ i₂ i₁₂ h ≫ (total.map φ c₁₂).f i₁₂ =
      (φ.f i₁).f i₂ ≫ L.ιTotal c₁₂ i₁ i₂ i₁₂ h

Proof state:
C : Type u_1
inst✝⁵ : Category.{u_5, u_1} C
inst✝⁴ : Preadditive C
I₁ : Type u_2
I₂ : Type u_3
I₁₂ : Type u_4
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
K L : HomologicalComplex₂ C c₁ c₂
φ : K ⟶ L
c₁₂ : ComplexShape I₁₂
inst✝³ : TotalComplexShape c₁ c₂ c₁₂
inst✝² : DecidableEq I₁₂
inst✝¹ : K.HasTotal c₁₂
inst✝ : L.HasTotal c₁₂
i₁ : I₁
i₂ : I₂
i₁₂ : I₁₂
h : c₁.π c₂ c₁₂ (i₁, i₂) = i₁₂
⊢ K.ιTotal c₁₂ i₁ i₂ i₁₂ h ≫ (total.map φ c₁₂).f i₁₂ = (φ.f i₁).f i₂ ≫ L.ιTotal c₁₂ i₁ i₂ i₁₂ h

Tactic:
simp [total.map, ιTotal]

Result:
no goals
-- Mathlib/Data/Nat/Choose/Basic.lean
theorem choose_succ_right_eq (n k : ℕ) : choose n (k + 1) * (k + 1) = choose n k * (n - k)

Proof state:
n k : ℕ
⊢ (n + 1) * n.choose k = n.choose (k + 1) * (k + 1) + n.choose k * (k + 1)

Tactic:
rw [← Nat.add_mul, Nat.add_comm (choose _ _), ← choose_succ_succ, succ_mul_choose_eq]

Result:
no goals

Proof state:
n k : ℕ
e : (n + 1) * n.choose k = n.choose (k + 1) * (k + 1) + n.choose k * (k + 1)
⊢ n.choose (k + 1) * (k + 1) = n.choose k * (n - k)

Tactic:
rw [← Nat.sub_eq_of_eq_add e, Nat.mul_comm, ← Nat.mul_sub_left_distrib, Nat.add_sub_add_right]

Result:
no goals

Proof state:
n k : ℕ
⊢ n.choose (k + 1) * (k + 1) = n.choose k * (n - k)

Tactic:
have e : (n + 1) * choose n k = choose n (k + 1) * (k + 1) + choose n k * (k + 1) := by
  rw [← Nat.add_mul, Nat.add_comm (choose _ _), ← choose_succ_succ, succ_mul_choose_eq]

Result:
n k : ℕ
e : (n + 1) * n.choose k = n.choose (k + 1) * (k + 1) + n.choose k * (k + 1)
⊢ n.choose (k + 1) * (k + 1) = n.choose k * (n - k)
-- Mathlib/RingTheory/Algebraic/Basic.lean
theorem isAlgebraic_int [Nontrivial R] (n : ℤ) : IsAlgebraic R (n : A)

Proof state:
R : Type u
A : Type v
inst✝³ : CommRing R
inst✝² : Ring A
inst✝¹ : Algebra R A
inst✝ : Nontrivial R
n : ℤ
⊢ IsAlgebraic R ↑n

Tactic:
rw [← map_intCast (algebraMap R A)]

Result:
R : Type u
A : Type v
inst✝³ : CommRing R
inst✝² : Ring A
inst✝¹ : Algebra R A
inst✝ : Nontrivial R
n : ℤ
⊢ IsAlgebraic R ((algebraMap R A) ↑n)

Proof state:
R : Type u
A : Type v
inst✝³ : CommRing R
inst✝² : Ring A
inst✝¹ : Algebra R A
inst✝ : Nontrivial R
n : ℤ
⊢ IsAlgebraic R ((algebraMap R A) ↑n)

Tactic:
exact isAlgebraic_algebraMap (Int.cast n)

Result:
no goals
-- Mathlib/RingTheory/Filtration.lean
theorem inf_submodule : (F ⊓ F').submodule = F.submodule ⊓ F'.submodule

Proof state:
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
F F' : I.Filtration M
⊢ (F ⊓ F').submodule = F.submodule ⊓ F'.submodule

Tactic:
ext

Result:
case h
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
F F' : I.Filtration M
x✝ : PolynomialModule R M
⊢ x✝ ∈ (F ⊓ F').submodule ↔ x✝ ∈ F.submodule ⊓ F'.submodule

Proof state:
case h
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
F F' : I.Filtration M
x✝ : PolynomialModule R M
⊢ x✝ ∈ (F ⊓ F').submodule ↔ x✝ ∈ F.submodule ⊓ F'.submodule

Tactic:
exact forall_and

Result:
no goals
-- Mathlib/Data/Seq/Computation.lean
theorem not_mem_empty (a : α) : a ∉ empty α := fun ⟨n, h⟩ => by contradiction

Proof state:
α : Type u
a : α
x✝ : a ∈ empty α
n : ℕ
h : (fun b => some a = b) ((↑(empty α)).get n)
⊢ False

Tactic:
contradiction

Result:
no goals
-- Mathlib/Data/Matroid/Restrict.lean
theorem IsBasis.eq_exchange_of_diff_eq_singleton (hI : M.IsBasis I X) (hJ : M.IsBasis J X)
    (hIJ : I \ J = {e}) : ∃ f ∈ J \ I, J = insert f I \ {e}

Proof state:
α : Type u_1
M : Matroid α
I X J : Set α
e : α
hI : M.IsBasis I X
hJ : M.IsBasis J X
hIJ : I \ J = {e}
⊢ ∃ f ∈ J \ I, J = insert f I \ {e}

Tactic:
rw [← isBase_restrict_iff] at hI hJ

Result:
α : Type u_1
M : Matroid α
I X J : Set α
e : α
hI : (M ↾ X).IsBase I
hJ : (M ↾ X).IsBase J
hIJ : I \ J = {e}
⊢ ∃ f ∈ J \ I, J = insert f I \ {e}

Proof state:
α : Type u_1
M : Matroid α
I X J : Set α
e : α
hI : (M ↾ X).IsBase I
hJ : (M ↾ X).IsBase J
hIJ : I \ J = {e}
⊢ ∃ f ∈ J \ I, J = insert f I \ {e}

Tactic:
exact hI.eq_exchange_of_diff_eq_singleton hJ hIJ

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Maps.lean
theorem toHom_comp_symm_toHom : f.toHom.comp f.symm.toHom = Hom.id

Proof state:
case h
V : Type u_1
W : Type u_2
G : SimpleGraph V
G' : SimpleGraph W
f : G ≃g G'
v : W
⊢ (f.toHom.comp f.symm.toHom) v = Hom.id v

Tactic:
simp only [RelHom.comp_apply, RelEmbedding.coe_toRelHom, RelIso.coe_toRelEmbedding,
  RelIso.apply_symm_apply, RelHom.id_apply]

Result:
no goals

Proof state:
V : Type u_1
W : Type u_2
G : SimpleGraph V
G' : SimpleGraph W
f : G ≃g G'
⊢ f.toHom.comp f.symm.toHom = Hom.id

Tactic:
ext v

Result:
case h
V : Type u_1
W : Type u_2
G : SimpleGraph V
G' : SimpleGraph W
f : G ≃g G'
v : W
⊢ (f.toHom.comp f.symm.toHom) v = Hom.id v
-- Mathlib/CategoryTheory/MorphismProperty/Comma.lean
@[reassoc]
lemma Under.w {A B : P.Under Q X} (f : A ⟶ B) :
    A.hom ≫ f.right = B.hom

Proof state:
T : Type u_1
inst✝¹ : Category.{u_2, u_1} T
P Q : MorphismProperty T
X : T
inst✝ : Q.IsMultiplicative
A B : P.Under Q X
f : A ⟶ B
⊢ A.hom ≫ f.right = B.hom

Tactic:
simp

Result:
no goals
-- Mathlib/FieldTheory/IntermediateField/Basic.lean
theorem toSubalgebra_toIntermediateField' (S : Subalgebra K L) (hS : IsField S) :
    (S.toIntermediateField' hS).toSubalgebra = S

Proof state:
case h
K : Type u_1
L : Type u_2
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
S : Subalgebra K L
hS : IsField ↥S
x✝ : L
⊢ x✝ ∈ (S.toIntermediateField' hS).toSubalgebra ↔ x✝ ∈ S

Tactic:
rfl

Result:
no goals

Proof state:
K : Type u_1
L : Type u_2
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
S : Subalgebra K L
hS : IsField ↥S
⊢ (S.toIntermediateField' hS).toSubalgebra = S

Tactic:
ext

Result:
case h
K : Type u_1
L : Type u_2
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
S : Subalgebra K L
hS : IsField ↥S
x✝ : L
⊢ x✝ ∈ (S.toIntermediateField' hS).toSubalgebra ↔ x✝ ∈ S
-- Mathlib/Order/CompleteLattice.lean
theorem iSup_eq_top (f : ι → α) : iSup f = ⊤ ↔ ∀ b < ⊤, ∃ i, b < f i

Proof state:
α : Type u_1
ι : Sort u_4
inst✝ : CompleteLinearOrder α
f : ι → α
⊢ iSup f = ⊤ ↔ ∀ b < ⊤, ∃ i, b < f i

Tactic:
simp only [← sSup_range, sSup_eq_top, Set.exists_range_iff]

Result:
no goals
-- Mathlib/Analysis/Normed/Group/SemiNormedGrp/Kernels.lean
theorem explicitCokernelDesc_comp_eq_desc {X Y Z W : SemiNormedGrp.{u}} {f : X ⟶ Y} {g : Y ⟶ Z}
    -- Porting note: renamed `cond` to `cond'` to avoid
    -- failed to rewrite using equation theorems for 'cond'
    {h : Z ⟶ W} {cond' : f ≫ g = 0} :
    explicitCokernelDesc cond' ≫ h =
      explicitCokernelDesc
        (show f ≫ g ≫ h = 0 by rw [← CategoryTheory.Category.assoc, cond', Limits.zero_comp])

Proof state:
X Y Z W : SemiNormedGrp
f : X ⟶ Y
g : Y ⟶ Z
h : Z ⟶ W
cond' : f ≫ g = 0
⊢ f ≫ g ≫ h = 0

Tactic:
rw [← CategoryTheory.Category.assoc, cond', Limits.zero_comp]

Result:
no goals

Proof state:
X Y Z W : SemiNormedGrp
f : X ⟶ Y
g : Y ⟶ Z
h : Z ⟶ W
cond' : f ≫ g = 0
⊢ explicitCokernelDesc cond' ≫ h = explicitCokernelDesc ⋯

Tactic:
refine explicitCokernelDesc_unique _ _ ?_

Result:
X Y Z W : SemiNormedGrp
f : X ⟶ Y
g : Y ⟶ Z
h : Z ⟶ W
cond' : f ≫ g = 0
⊢ explicitCokernelπ f ≫ explicitCokernelDesc cond' ≫ h = g ≫ h

Proof state:
X Y Z W : SemiNormedGrp
f : X ⟶ Y
g : Y ⟶ Z
h : Z ⟶ W
cond' : f ≫ g = 0
⊢ explicitCokernelπ f ≫ explicitCokernelDesc cond' ≫ h = g ≫ h

Tactic:
rw [← CategoryTheory.Category.assoc, explicitCokernelπ_desc]

Result:
no goals
-- Mathlib/Algebra/Lie/TensorProduct.lean
theorem toModuleHom_apply (x : L) (m : M) : toModuleHom R L M (x ⊗ₜ m) = ⁅x, m⁆

Proof state:
R : Type u
inst✝⁶ : CommRing R
L : Type v
M : Type w
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
x : L
m : M
⊢ (toModuleHom R L M) (x ⊗ₜ[R] m) = ⁅x, m⁆

Tactic:
simp only [toModuleHom, TensorProduct.LieModule.liftLie_apply, LieModuleHom.coe_mk,
  LinearMap.coe_mk, LinearMap.coe_toAddHom, LieHom.coe_toLinearMap, toEnd_apply_apply]

Result:
no goals
-- Mathlib/Algebra/CubicDiscriminant.lean
theorem a_of_eq (h : P.toPoly = Q.toPoly) : P.a = Q.a

Proof state:
R : Type u_1
P Q : Cubic R
inst✝ : Semiring R
h : P.toPoly = Q.toPoly
⊢ P.a = Q.a

Tactic:
rw [← coeff_eq_a, h, coeff_eq_a]

Result:
no goals
-- Mathlib/LinearAlgebra/Matrix/NonsingularInverse.lean
theorem invOf_submatrix_equiv_eq (A : Matrix m m α) (e₁ e₂ : n ≃ m) [Invertible A]
    [Invertible (A.submatrix e₁ e₂)] : ⅟ (A.submatrix e₁ e₂) = (⅟ A).submatrix e₂ e₁

Proof state:
m : Type u
n : Type u'
α : Type v
inst✝⁶ : Fintype n
inst✝⁵ : DecidableEq n
inst✝⁴ : CommRing α
inst✝³ : Fintype m
inst✝² : DecidableEq m
A : Matrix m m α
e₁ e₂ : n ≃ m
inst✝¹ : Invertible A
inst✝ : Invertible (A.submatrix ⇑e₁ ⇑e₂)
this : Invertible (A.submatrix ⇑e₁ ⇑e₂) := A.submatrixEquivInvertible e₁ e₂
⊢ ⅟(A.submatrix ⇑e₁ ⇑e₂) = (⅟A).submatrix ⇑e₂ ⇑e₁

Tactic:
convert (rfl : ⅟ (A.submatrix e₁ e₂) = _)

Result:
no goals

Proof state:
m : Type u
n : Type u'
α : Type v
inst✝⁶ : Fintype n
inst✝⁵ : DecidableEq n
inst✝⁴ : CommRing α
inst✝³ : Fintype m
inst✝² : DecidableEq m
A : Matrix m m α
e₁ e₂ : n ≃ m
inst✝¹ : Invertible A
inst✝ : Invertible (A.submatrix ⇑e₁ ⇑e₂)
⊢ ⅟(A.submatrix ⇑e₁ ⇑e₂) = (⅟A).submatrix ⇑e₂ ⇑e₁

Tactic:
letI := submatrixEquivInvertible A e₁ e₂

Result:
m : Type u
n : Type u'
α : Type v
inst✝⁶ : Fintype n
inst✝⁵ : DecidableEq n
inst✝⁴ : CommRing α
inst✝³ : Fintype m
inst✝² : DecidableEq m
A : Matrix m m α
e₁ e₂ : n ≃ m
inst✝¹ : Invertible A
inst✝ : Invertible (A.submatrix ⇑e₁ ⇑e₂)
this : Invertible (A.submatrix ⇑e₁ ⇑e₂) := A.submatrixEquivInvertible e₁ e₂
⊢ ⅟(A.submatrix ⇑e₁ ⇑e₂) = (⅟A).submatrix ⇑e₂ ⇑e₁
-- Mathlib/Dynamics/PeriodicPts/Defs.lean
theorem zpow_smul_eq_iff_minimalPeriod_dvd {n : ℤ} :
    a ^ n • b = b ↔ (minimalPeriod (a • ·) b : ℤ) ∣ n

Proof state:
α : Type v
G : Type u
inst✝¹ : Group G
inst✝ : MulAction G α
a : G
b : α
n : ℤ
⊢ a ^ n • b = b ↔ ↑(minimalPeriod (fun x => a • x) b) ∣ n

Tactic:
rw [← period_eq_minimalPeriod, zpow_smul_eq_iff_period_dvd]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Bool.lean
theorem and_not_iff_right_iff_imp : ∀ {a b : Bool}, ((a && !b) = b) ↔ !a ∧ !b

Proof state:
⊢ ∀ {a b : Bool}, (a && !b) = b ↔ (!a) = true ∧ (!b) = true

Tactic:
decide

Result:
no goals
-- Mathlib/Topology/Category/TopCat/Opens.lean
theorem functor_obj_map_obj {X Y : TopCat} {f : X ⟶ Y} (hf : IsOpenMap f) (U : Opens Y) :
    hf.functor.obj ((Opens.map f).obj U) = hf.functor.obj ⊤ ⊓ U

Proof state:
case h.h.mp.intro.intro
X Y : TopCat
f : X ⟶ Y
hf : IsOpenMap ⇑(ConcreteCategory.hom f)
U : Opens ↑Y
x : ↑X
hx : x ∈ ↑((map f).obj U)
⊢ (ConcreteCategory.hom f) x ∈ ↑(hf.functor.obj ⊤ ⊓ U)

Tactic:
exact ⟨⟨x, trivial, rfl⟩, hx⟩

Result:
no goals

Proof state:
case h.h.mpr.intro.intro.intro
X Y : TopCat
f : X ⟶ Y
hf : IsOpenMap ⇑(ConcreteCategory.hom f)
U : Opens ↑Y
x : ↑X
hx : (ConcreteCategory.hom f) x ∈ ↑U
⊢ (ConcreteCategory.hom f) x ∈ ↑(hf.functor.obj ((map f).obj U))

Tactic:
exact ⟨x, hx, rfl⟩

Result:
no goals

Proof state:
case h.h
X Y : TopCat
f : X ⟶ Y
hf : IsOpenMap ⇑(ConcreteCategory.hom f)
U : Opens ↑Y
x✝ : ↑Y
⊢ x✝ ∈ ↑(hf.functor.obj ((map f).obj U)) ↔ x✝ ∈ ↑(hf.functor.obj ⊤ ⊓ U)

Tactic:
constructor

Result:
case h.h.mp
X Y : TopCat
f : X ⟶ Y
hf : IsOpenMap ⇑(ConcreteCategory.hom f)
U : Opens ↑Y
x✝ : ↑Y
⊢ x✝ ∈ ↑(hf.functor.obj ((map f).obj U)) → x✝ ∈ ↑(hf.functor.obj ⊤ ⊓ U)

case h.h.mpr
X Y : TopCat
f : X ⟶ Y
hf : IsOpenMap ⇑(ConcreteCategory.hom f)
U : Opens ↑Y
x✝ : ↑Y
⊢ x✝ ∈ ↑(hf.functor.obj ⊤ ⊓ U) → x✝ ∈ ↑(hf.functor.obj ((map f).obj U))

Proof state:
case h.h.mpr
X Y : TopCat
f : X ⟶ Y
hf : IsOpenMap ⇑(ConcreteCategory.hom f)
U : Opens ↑Y
x✝ : ↑Y
⊢ x✝ ∈ ↑(hf.functor.obj ⊤ ⊓ U) → x✝ ∈ ↑(hf.functor.obj ((map f).obj U))

Tactic:
rintro ⟨⟨x, -, rfl⟩, hx⟩

Result:
case h.h.mpr.intro.intro.intro
X Y : TopCat
f : X ⟶ Y
hf : IsOpenMap ⇑(ConcreteCategory.hom f)
U : Opens ↑Y
x : ↑X
hx : (ConcreteCategory.hom f) x ∈ ↑U
⊢ (ConcreteCategory.hom f) x ∈ ↑(hf.functor.obj ((map f).obj U))

Proof state:
case h.h.mp
X Y : TopCat
f : X ⟶ Y
hf : IsOpenMap ⇑(ConcreteCategory.hom f)
U : Opens ↑Y
x✝ : ↑Y
⊢ x✝ ∈ ↑(hf.functor.obj ((map f).obj U)) → x✝ ∈ ↑(hf.functor.obj ⊤ ⊓ U)

Tactic:
rintro ⟨x, hx, rfl⟩

Result:
case h.h.mp.intro.intro
X Y : TopCat
f : X ⟶ Y
hf : IsOpenMap ⇑(ConcreteCategory.hom f)
U : Opens ↑Y
x : ↑X
hx : x ∈ ↑((map f).obj U)
⊢ (ConcreteCategory.hom f) x ∈ ↑(hf.functor.obj ⊤ ⊓ U)

Proof state:
X Y : TopCat
f : X ⟶ Y
hf : IsOpenMap ⇑(ConcreteCategory.hom f)
U : Opens ↑Y
⊢ hf.functor.obj ((map f).obj U) = hf.functor.obj ⊤ ⊓ U

Tactic:
ext

Result:
case h.h
X Y : TopCat
f : X ⟶ Y
hf : IsOpenMap ⇑(ConcreteCategory.hom f)
U : Opens ↑Y
x✝ : ↑Y
⊢ x✝ ∈ ↑(hf.functor.obj ((map f).obj U)) ↔ x✝ ∈ ↑(hf.functor.obj ⊤ ⊓ U)
-- Mathlib/Order/SymmDiff.lean
theorem IsCompl.symmDiff_eq_top {a b : α} (h : IsCompl a b) : a ∆ b = ⊤

Proof state:
α : Type u_2
inst✝ : CoheytingAlgebra α
a b : α
h : IsCompl a b
⊢ a ∆ b = ⊤

Tactic:
rw [h.eq_hnot, hnot_symmDiff_self]

Result:
no goals
-- Mathlib/Analysis/Calculus/FDeriv/Basic.lean
theorem Filter.EventuallyEq.fderivWithin_eq (hs : f₁ =ᶠ[𝓝[s] x] f) (hx : f₁ x = f x) :
    fderivWithin 𝕜 f₁ s x = fderivWithin 𝕜 f s x

Proof state:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f f₁ : E → F
x : E
s : Set E
hs : f₁ =ᶠ[𝓝[s] x] f
hx : f₁ x = f x
⊢ fderivWithin 𝕜 f₁ s x = fderivWithin 𝕜 f s x

Tactic:
simp only [fderivWithin, DifferentiableWithinAt, hs.hasFDerivWithinAt_iff hx]

Result:
no goals

Proof state:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f f₁ : E → F
x : E
s : Set E
hs : f₁ =ᶠ[𝓝[s] x] f
hx : f₁ x = f x
⊢ fderivWithin 𝕜 f₁ s x = fderivWithin 𝕜 f s x

Tactic:
classical
simp only [fderivWithin, DifferentiableWithinAt, hs.hasFDerivWithinAt_iff hx]

Result:
no goals
-- Mathlib/Probability/Variance.lean
theorem evariance_eq_zero_iff (hX : AEMeasurable X μ) :
    evariance X μ = 0 ↔ X =ᵐ[μ] fun _ => μ[X]

Proof state:
Ω : Type u_1
mΩ : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
hX : AEMeasurable X μ
⊢ eVar[X; μ] = 0 ↔ X =ᶠ[ae μ] fun x => ∫ (x : Ω), X x ∂μ

Tactic:
simp [evariance, lintegral_eq_zero_iff' ((hX.sub_const _).enorm.pow_const _), EventuallyEq,
  sub_eq_zero]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Complex/LogDeriv.lean
theorem HasDerivWithinAt.clog_real {f : ℝ → ℂ} {s : Set ℝ} {x : ℝ} {f' : ℂ}
    (h₁ : HasDerivWithinAt f f' s x) (h₂ : f x ∈ slitPlane) :
    HasDerivWithinAt (fun t => log (f t)) (f' / f x) s x

Proof state:
f : ℝ → ℂ
s : Set ℝ
x : ℝ
f' : ℂ
h₁ : HasDerivWithinAt f f' s x
h₂ : f x ∈ slitPlane
⊢ HasDerivWithinAt (fun t => log (f t)) (f' / f x) s x

Tactic:
simpa only [div_eq_inv_mul] using
  (hasStrictFDerivAt_log_real h₂).hasFDerivAt.comp_hasDerivWithinAt x h₁

Result:
no goals
-- Mathlib/CategoryTheory/Functor/Category.lean
theorem id_hcomp_app {H : E ⥤ C} (α : F ⟶ G) (X : E) : (𝟙 H ◫ α).app X = α.app _

Proof state:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
E : Type u₃
inst✝ : Category.{v₃, u₃} E
F G : C ⥤ D
H : E ⥤ C
α : F ⟶ G
X : E
⊢ (𝟙 H ◫ α).app X = α.app (H.obj X)

Tactic:
simp

Result:
no goals
-- Mathlib/Algebra/Order/Field/Basic.lean
theorem one_div_le (ha : 0 < a) (hb : 0 < b) : 1 / a ≤ b ↔ 1 / b ≤ a

Proof state:
α : Type u_2
inst✝ : LinearOrderedSemifield α
a b : α
ha : 0 < a
hb : 0 < b
⊢ 1 / a ≤ b ↔ 1 / b ≤ a

Tactic:
simpa using inv_le_comm₀ ha hb

Result:
no goals
-- Mathlib/Algebra/Star/Conjneg.lean
@[simp] lemma conjneg_zero : conjneg (0 : G → R) = 0

Proof state:
case h
G : Type u_2
R : Type u_3
inst✝² : AddGroup G
inst✝¹ : CommSemiring R
inst✝ : StarRing R
x✝ : G
⊢ conjneg 0 x✝ = 0 x✝

Tactic:
simp

Result:
no goals

Proof state:
G : Type u_2
R : Type u_3
inst✝² : AddGroup G
inst✝¹ : CommSemiring R
inst✝ : StarRing R
⊢ conjneg 0 = 0

Tactic:
ext

Result:
case h
G : Type u_2
R : Type u_3
inst✝² : AddGroup G
inst✝¹ : CommSemiring R
inst✝ : StarRing R
x✝ : G
⊢ conjneg 0 x✝ = 0 x✝
-- Mathlib/MeasureTheory/MeasurableSpace/Basic.lean
theorem measurable_pi_iff {g : α → ∀ a, π a} : Measurable g ↔ ∀ a, Measurable fun x => g x a

Proof state:
α : Type u_1
δ : Type u_4
π : δ → Type u_6
inst✝¹ : MeasurableSpace α
inst✝ : (a : δ) → MeasurableSpace (π a)
g : α → (a : δ) → π a
⊢ Measurable g ↔ ∀ (a : δ), Measurable fun x => g x a

Tactic:
simp_rw [measurable_iff_comap_le, MeasurableSpace.pi, MeasurableSpace.comap_iSup,
  MeasurableSpace.comap_comp, Function.comp_def, iSup_le_iff]

Result:
no goals