harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/LinearAlgebra/Dual.lean
theorem dualAnnihilator_dualAnnihilator_eq (W : Subspace K V) :
    W.dualAnnihilator.dualAnnihilator = Module.mapEvalEquiv K V W

Proof state:
K : Type u
V : Type v
inst✝³ : Field K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
W : Subspace K V
this : (dualAnnihilator W).dualCoannihilator = W
⊢ (dualAnnihilator W).dualAnnihilator = (mapEvalEquiv K V) W

Tactic:
rw [dualCoannihilator, ← Module.mapEvalEquiv_symm_apply] at this

Result:
K : Type u
V : Type v
inst✝³ : Field K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
W : Subspace K V
this : (mapEvalEquiv K V).symm (dualAnnihilator W).dualAnnihilator = W
⊢ (dualAnnihilator W).dualAnnihilator = (mapEvalEquiv K V) W

Proof state:
K : Type u
V : Type v
inst✝³ : Field K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
W : Subspace K V
this : (mapEvalEquiv K V).symm (dualAnnihilator W).dualAnnihilator = W
⊢ (dualAnnihilator W).dualAnnihilator = (mapEvalEquiv K V) W

Tactic:
rwa [← OrderIso.symm_apply_eq]

Result:
no goals

Proof state:
K : Type u
V : Type v
inst✝³ : Field K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
W : Subspace K V
⊢ (dualAnnihilator W).dualAnnihilator = (mapEvalEquiv K V) W

Tactic:
have : _ = W := Subspace.dualAnnihilator_dualCoannihilator_eq

Result:
K : Type u
V : Type v
inst✝³ : Field K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
W : Subspace K V
this : (dualAnnihilator W).dualCoannihilator = W
⊢ (dualAnnihilator W).dualAnnihilator = (mapEvalEquiv K V) W
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Lemmas.lean
theorem map_inj_left {f g : α → β} : map f l = map g l ↔ ∀ a ∈ l, f a = g a

Proof state:
α : Type u_1
β : Type u_2
l : List α
f g : α → β
⊢ map f l = map g l ↔ ∀ (a : α), a ∈ l → f a = g a

Tactic:
induction l <;> simp_all

Result:
no goals
-- Mathlib/Data/Finset/Sym.lean
theorem sym2_nonempty : s.sym2.Nonempty ↔ s.Nonempty

Proof state:
α : Type u_1
s : Finset α
⊢ ¬s.sym2.Nonempty ↔ ¬s.Nonempty

Tactic:
simp_rw [not_nonempty_iff_eq_empty, sym2_eq_empty]

Result:
no goals

Proof state:
α : Type u_1
s : Finset α
⊢ s.sym2.Nonempty ↔ s.Nonempty

Tactic:
rw [← not_iff_not]

Result:
α : Type u_1
s : Finset α
⊢ ¬s.sym2.Nonempty ↔ ¬s.Nonempty
-- Mathlib/Algebra/Homology/HomotopyCategory/Pretriangulated.lean
@[reassoc (attr := simp)]
lemma inr_triangleδ : inr φ ≫ (triangle φ).mor₃ = 0

Proof state:
case h
C : Type u_1
inst✝² : Category.{u_3, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasBinaryBiproducts C
K L : CochainComplex C ℤ
φ : K ⟶ L
i✝ : ℤ
⊢ (inr φ).f i✝ ≫ (triangle φ).mor₃.f i✝ = 0

Tactic:
simp

Result:
no goals

Proof state:
C : Type u_1
inst✝² : Category.{u_3, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasBinaryBiproducts C
K L : CochainComplex C ℤ
φ : K ⟶ L
⊢ inr φ ≫ (triangle φ).mor₃ = 0

Tactic:
ext

Result:
case h
C : Type u_1
inst✝² : Category.{u_3, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasBinaryBiproducts C
K L : CochainComplex C ℤ
φ : K ⟶ L
i✝ : ℤ
⊢ (inr φ ≫ (triangle φ).mor₃).f i✝ = HomologicalComplex.Hom.f 0 i✝

Proof state:
case h
C : Type u_1
inst✝² : Category.{u_3, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasBinaryBiproducts C
K L : CochainComplex C ℤ
φ : K ⟶ L
i✝ : ℤ
⊢ (inr φ ≫ (triangle φ).mor₃).f i✝ = HomologicalComplex.Hom.f 0 i✝

Tactic:
dsimp

Result:
case h
C : Type u_1
inst✝² : Category.{u_3, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasBinaryBiproducts C
K L : CochainComplex C ℤ
φ : K ⟶ L
i✝ : ℤ
⊢ (inr φ).f i✝ ≫ (triangle φ).mor₃.f i✝ = 0
-- Mathlib/MeasureTheory/Integral/Bochner.lean
theorem ofReal_integral_eq_lintegral_ofReal {f : α → ℝ} (hfi : Integrable f μ) (f_nn : 0 ≤ᵐ[μ] f) :
    ENNReal.ofReal (∫ x, f x ∂μ) = ∫⁻ x, ENNReal.ofReal (f x) ∂μ

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hfi : Integrable f μ
f_nn : 0 ≤ᶠ[ae μ] f
this : f =ᶠ[ae μ] fun x => ‖f x‖
⊢ ENNReal.ofReal (∫ (x : α), f x ∂μ) = ∫⁻ (x : α), ENNReal.ofReal (f x) ∂μ

Tactic:
simp_rw [integral_congr_ae this, ofReal_integral_norm_eq_lintegral_enorm hfi,
  ← ofReal_norm_eq_enorm]

Result:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hfi : Integrable f μ
f_nn : 0 ≤ᶠ[ae μ] f
this : f =ᶠ[ae μ] fun x => ‖f x‖
⊢ ∫⁻ (x : α), ENNReal.ofReal ‖f x‖ ∂μ = ∫⁻ (x : α), ENNReal.ofReal (f x) ∂μ

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hfi : Integrable f μ
f_nn : 0 ≤ᶠ[ae μ] f
this : f =ᶠ[ae μ] fun x => ‖f x‖
⊢ ∫⁻ (x : α), ENNReal.ofReal ‖f x‖ ∂μ = ∫⁻ (x : α), ENNReal.ofReal (f x) ∂μ

Tactic:
exact lintegral_congr_ae (this.symm.fun_comp ENNReal.ofReal)

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem setIfInBounds_append_left {s t : Array α} {i : Nat} {x : α} (h : i < s.size) :
    (s ++ t).setIfInBounds i x = s.setIfInBounds i x ++ t

Proof state:
α : Type u_1
s t : Array α
i : Nat
x : α
h : i < s.size
⊢ (s ++ t).setIfInBounds i x = s.setIfInBounds i x ++ t

Tactic:
simp [setIfInBounds_append, h]

Result:
no goals
-- Mathlib/Data/List/Chain.lean
theorem Chain'.append_overlap {l₁ l₂ l₃ : List α} (h₁ : Chain' R (l₁ ++ l₂))
    (h₂ : Chain' R (l₂ ++ l₃)) (hn : l₂ ≠ []) : Chain' R (l₁ ++ l₂ ++ l₃) :=
  h₁.append h₂.right_of_append <| by
    simpa only [getLast?_append_of_ne_nil _ hn] using (chain'_append.1 h₂).2.2

Proof state:
α : Type u
R : α → α → Prop
l₁ l₂ l₃ : List α
h₁ : Chain' R (l₁ ++ l₂)
h₂ : Chain' R (l₂ ++ l₃)
hn : l₂ ≠ []
⊢ ∀ (x : α), x ∈ (l₁ ++ l₂).getLast? → ∀ (y : α), y ∈ l₃.head? → R x y

Tactic:
simpa only [getLast?_append_of_ne_nil _ hn] using (chain'_append.1 h₂).2.2

Result:
no goals
-- Mathlib/Order/Interval/Set/Basic.lean
theorem Icc_inter_Icc_eq_singleton (hab : a ≤ b) (hbc : b ≤ c) : Icc a b ∩ Icc b c = {b}

Proof state:
α : Type u_1
inst✝ : Lattice α
a b c : α
hab : a ≤ b
hbc : b ≤ c
⊢ Icc a b ∩ Icc b c = {b}

Tactic:
rw [Icc_inter_Icc, sup_of_le_right hab, inf_of_le_left hbc, Icc_self]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Lemmas.lean
theorem some_eq_getElem?_iff {l : List α} : some a = l[i]? ↔ ∃ h : i < l.length, l[i] = a

Proof state:
α : Type u_1
a : α
i : Nat
l : List α
⊢ some a = l[i]? ↔ ∃ h, l[i] = a

Tactic:
rw [eq_comm, getElem?_eq_some_iff]

Result:
no goals
-- Mathlib/Computability/RegularExpressions.lean
theorem map_pow (f : α → β) (P : RegularExpression α) :
    ∀ n : ℕ, map f (P ^ n) = map f P ^ n
  | 0 => by unfold map; rfl
  | n + 1 => (congr_arg (· * map f P) (RegularExpression.map_pow f P n) :)

Proof state:
α : Type u_1
β : Type u_2
f : α → β
P : RegularExpression α
⊢ map f (P ^ 0) = map f P ^ 0

Tactic:
unfold map

Result:
α : Type u_1
β : Type u_2
f : α → β
P : RegularExpression α
⊢ (match P ^ 0 with
    | zero => 0
    | epsilon => 1
    | char a => char (f a)
    | R.plus S => map f R + map f S
    | R.comp S => map f R * map f S
    | R.star => (map f R).star) =
    (match P with
      | zero => 0
      | epsilon => 1
      | char a => char (f a)
      | R.plus S => map f R + map f S
      | R.comp S => map f R * map f S
      | R.star => (map f R).star) ^
      0

Proof state:
α : Type u_1
β : Type u_2
f : α → β
P : RegularExpression α
⊢ (match P ^ 0 with
    | zero => 0
    | epsilon => 1
    | char a => char (f a)
    | R.plus S => map f R + map f S
    | R.comp S => map f R * map f S
    | R.star => (map f R).star) =
    (match P with
      | zero => 0
      | epsilon => 1
      | char a => char (f a)
      | R.plus S => map f R + map f S
      | R.comp S => map f R * map f S
      | R.star => (map f R).star) ^
      0

Tactic:
rfl

Result:
no goals
-- Mathlib/LinearAlgebra/TensorProduct/Basic.lean
theorem lift.unique {g : M ⊗[R] N →ₗ[R] P} (H : ∀ x y, g (x ⊗ₜ y) = f x y) : g = lift f :=
  ext' fun m n => by rw [H, lift.tmul]

Proof state:
R : Type u_1
inst✝⁶ : CommSemiring R
M : Type u_5
N : Type u_6
P : Type u_7
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid N
inst✝³ : AddCommMonoid P
inst✝² : Module R M
inst✝¹ : Module R N
inst✝ : Module R P
f : M →ₗ[R] N →ₗ[R] P
g : M ⊗[R] N →ₗ[R] P
H : ∀ (x : M) (y : N), g (x ⊗ₜ[R] y) = (f x) y
m : M
n : N
⊢ g (m ⊗ₜ[R] n) = (lift f) (m ⊗ₜ[R] n)

Tactic:
rw [H, lift.tmul]

Result:
no goals
-- Mathlib/Algebra/CubicDiscriminant.lean
theorem leadingCoeff_of_c_ne_zero (ha : P.a = 0) (hb : P.b = 0) (hc : P.c ≠ 0) :
    P.toPoly.leadingCoeff = P.c

Proof state:
R : Type u_1
P : Cubic R
inst✝ : Semiring R
ha : P.a = 0
hb : P.b = 0
hc : P.c ≠ 0
⊢ P.toPoly.leadingCoeff = P.c

Tactic:
rw [of_b_eq_zero ha hb, leadingCoeff_linear hc]

Result:
no goals
-- Mathlib/Order/Atoms.lean
theorem isAtom_iff {p : Prop} : IsAtom p ↔ p

Proof state:
p : Prop
⊢ IsAtom p ↔ p

Tactic:
simp [IsAtom, show ⊥ = False from rfl, fun q r : Prop => show q < r ↔ _ ∧ _ from .rfl]

Result:
no goals
-- Mathlib/Topology/Order/OrderClosed.lean
@[simp] lemma bddAbove_closure : BddAbove (closure s) ↔ BddAbove s

Proof state:
α : Type u
inst✝² : TopologicalSpace α
inst✝¹ : Preorder α
inst✝ : ClosedIicTopology α
s : Set α
⊢ BddAbove (closure s) ↔ BddAbove s

Tactic:
simp_rw [BddAbove, upperBounds_closure]

Result:
no goals
-- Mathlib/CategoryTheory/Adjunction/Restrict.lean
@[simp, reassoc]
lemma map_restrictFullyFaithful_counit_app (X : D) :
    iD.map ((adj.restrictFullyFaithful hiC hiD comm1 comm2).counit.app X) =
    comm1.inv.app (R.obj X) ≫ L'.map (comm2.inv.app X) ≫ adj.counit.app (iD.obj X)

Proof state:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
C' : Type u₃
inst✝¹ : Category.{v₃, u₃} C'
D' : Type u₄
inst✝ : Category.{v₄, u₄} D'
iC : C ⥤ C'
iD : D ⥤ D'
L' : C' ⥤ D'
R' : D' ⥤ C'
adj : L' ⊣ R'
hiC : iC.FullyFaithful
hiD : iD.FullyFaithful
L : C ⥤ D
R : D ⥤ C
comm1 : iC ⋙ L' ≅ L ⋙ iD
comm2 : iD ⋙ R' ≅ R ⋙ iC
X : D
⊢ iD.map
      (hiD.preimage
        (comm1.inv.app (R.obj X) ≫
          (adj.homEquiv (iC.obj (R.obj X)) (iD.obj X)).symm
              (𝟙 (iC.obj (R.obj X)) ≫ iC.map (𝟙 (R.obj X)) ≫ comm2.inv.app X) ≫
            𝟙 (iD.obj X))) =
    comm1.inv.app (R.obj X) ≫ L'.map (comm2.inv.app X) ≫ adj.counit.app (iD.obj X)

Tactic:
simp

Result:
no goals

Proof state:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
C' : Type u₃
inst✝¹ : Category.{v₃, u₃} C'
D' : Type u₄
inst✝ : Category.{v₄, u₄} D'
iC : C ⥤ C'
iD : D ⥤ D'
L' : C' ⥤ D'
R' : D' ⥤ C'
adj : L' ⊣ R'
hiC : iC.FullyFaithful
hiD : iD.FullyFaithful
L : C ⥤ D
R : D ⥤ C
comm1 : iC ⋙ L' ≅ L ⋙ iD
comm2 : iD ⋙ R' ≅ R ⋙ iC
X : D
⊢ iD.map ((adj.restrictFullyFaithful hiC hiD comm1 comm2).counit.app X) =
    comm1.inv.app (R.obj X) ≫ L'.map (comm2.inv.app X) ≫ adj.counit.app (iD.obj X)

Tactic:
dsimp [restrictFullyFaithful]

Result:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
C' : Type u₃
inst✝¹ : Category.{v₃, u₃} C'
D' : Type u₄
inst✝ : Category.{v₄, u₄} D'
iC : C ⥤ C'
iD : D ⥤ D'
L' : C' ⥤ D'
R' : D' ⥤ C'
adj : L' ⊣ R'
hiC : iC.FullyFaithful
hiD : iD.FullyFaithful
L : C ⥤ D
R : D ⥤ C
comm1 : iC ⋙ L' ≅ L ⋙ iD
comm2 : iD ⋙ R' ≅ R ⋙ iC
X : D
⊢ iD.map
      (hiD.preimage
        (comm1.inv.app (R.obj X) ≫
          (adj.homEquiv (iC.obj (R.obj X)) (iD.obj X)).symm
              (𝟙 (iC.obj (R.obj X)) ≫ iC.map (𝟙 (R.obj X)) ≫ comm2.inv.app X) ≫
            𝟙 (iD.obj X))) =
    comm1.inv.app (R.obj X) ≫ L'.map (comm2.inv.app X) ≫ adj.counit.app (iD.obj X)
-- Mathlib/MeasureTheory/Integral/Bochner.lean
theorem integral_unique [Unique α] (f : α → E) : ∫ x, f x ∂μ = (μ univ).toReal • f default :=
  calc
    ∫ x, f x ∂μ = ∫ _, f default ∂μ

Proof state:
case e_f.h.e_a
α : Type u_1
E : Type u_2
inst✝² : NormedAddCommGroup E
hE : CompleteSpace E
inst✝¹ : NormedSpace ℝ E
m : MeasurableSpace α
μ : Measure α
inst✝ : Unique α
f : α → E
x : α
⊢ x = default

Tactic:
exact Unique.uniq _ x

Result:
no goals

Proof state:
case e_f.h
α : Type u_1
E : Type u_2
inst✝² : NormedAddCommGroup E
hE : CompleteSpace E
inst✝¹ : NormedSpace ℝ E
m : MeasurableSpace α
μ : Measure α
inst✝ : Unique α
f : α → E
x : α
⊢ f x = f default

Tactic:
congr

Result:
case e_f.h.e_a
α : Type u_1
E : Type u_2
inst✝² : NormedAddCommGroup E
hE : CompleteSpace E
inst✝¹ : NormedSpace ℝ E
m : MeasurableSpace α
μ : Measure α
inst✝ : Unique α
f : α → E
x : α
⊢ x = default

Proof state:
α : Type u_1
E : Type u_2
inst✝² : NormedAddCommGroup E
hE : CompleteSpace E
inst✝¹ : NormedSpace ℝ E
m : MeasurableSpace α
μ : Measure α
inst✝ : Unique α
f : α → E
⊢ ∫ (x : α), f x ∂μ = ∫ (x : α), f default ∂μ

Tactic:
congr with x

Result:
case e_f.h
α : Type u_1
E : Type u_2
inst✝² : NormedAddCommGroup E
hE : CompleteSpace E
inst✝¹ : NormedSpace ℝ E
m : MeasurableSpace α
μ : Measure α
inst✝ : Unique α
f : α → E
x : α
⊢ f x = f default

Proof state:
α : Type u_1
E : Type u_2
inst✝² : NormedAddCommGroup E
hE : CompleteSpace E
inst✝¹ : NormedSpace ℝ E
m : MeasurableSpace α
μ : Measure α
inst✝ : Unique α
f : α → E
⊢ ∫ (x : α), f default ∂μ = (μ univ).toReal • f default

Tactic:
rw [integral_const]

Result:
no goals
-- Mathlib/GroupTheory/Perm/Option.lean
theorem Equiv.Perm.decomposeOption_symm_sign {α : Type*} [DecidableEq α] [Fintype α] (e : Perm α) :
    Perm.sign (Equiv.Perm.decomposeOption.symm (none, e)) = Perm.sign e

Proof state:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
e : Perm α
⊢ sign (decomposeOption.symm (none, e)) = sign e

Tactic:
simp

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/GetElem.lean
theorem getElem_cons_succ (a : α) (as : List α) (i : Nat) (h : i + 1 < (a :: as).length) : getElem (a :: as) (i+1) h = getElem as i (Nat.lt_of_succ_lt_succ h)

Proof state:
α : Type u_1
a : α
as : List α
i : Nat
h : i + 1 < (a :: as).length
⊢ getElem (a :: as) (i + 1) h = getElem as i ⋯

Tactic:
rfl

Result:
no goals
-- Mathlib/Topology/Filter.lean
theorem specializes_iff_le {l₁ l₂ : Filter α} : l₁ ⤳ l₂ ↔ l₁ ≤ l₂

Proof state:
α : Type u_2
l₁ l₂ : Filter α
⊢ l₁ ⤳ l₂ ↔ l₁ ≤ l₂

Tactic:
simp only [specializes_iff_closure_subset, Filter.closure_singleton, Ici_subset_Ici]

Result:
no goals
-- Mathlib/Analysis/Calculus/ContDiff/FiniteDimension.lean
theorem contDiff_clm_apply_iff {f : D → E →L[𝕜] F} [FiniteDimensional 𝕜 E] :
    ContDiff 𝕜 n f ↔ ∀ y, ContDiff 𝕜 n fun x => f x y

Proof state:
𝕜 : Type u_1
inst✝⁸ : NontriviallyNormedField 𝕜
D : Type uD
inst✝⁷ : NormedAddCommGroup D
inst✝⁶ : NormedSpace 𝕜 D
E : Type uE
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type uF
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
n : WithTop ℕ∞
inst✝¹ : CompleteSpace 𝕜
f : D → E →L[𝕜] F
inst✝ : FiniteDimensional 𝕜 E
⊢ ContDiff 𝕜 n f ↔ ∀ (y : E), ContDiff 𝕜 n fun x => (f x) y

Tactic:
simp_rw [← contDiffOn_univ, contDiffOn_clm_apply]

Result:
no goals
-- Mathlib/Topology/UniformSpace/UniformEmbedding.lean
theorem IsUniformInducing.id : IsUniformInducing (@id α) :=
  ⟨by rw [← Prod.map_def, Prod.map_id, comap_id]⟩

Proof state:
α : Type u
inst✝ : UniformSpace α
⊢ comap (fun x => (_root_.id x.1, _root_.id x.2)) (𝓤 α) = 𝓤 α

Tactic:
rw [← Prod.map_def, Prod.map_id, comap_id]

Result:
no goals
-- Mathlib/LinearAlgebra/TensorAlgebra/Basis.lean
lemma rank_eq [Nontrivial R] [Module.Free R M] :
    Module.rank R (TensorAlgebra R M) = Cardinal.lift.{uR} (sum fun n ↦ Module.rank R M ^ n)

Proof state:
R : Type uR
M : Type uM
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : Nontrivial R
inst✝ : Module.Free R M
⊢ Module.rank R (TensorAlgebra R M) = Cardinal.lift.{uR, uM} (sum fun n => Module.rank R M ^ n)

Tactic:
let ⟨⟨κ, b⟩⟩ := Module.Free.exists_basis (R := R) (M := M)

Result:
R : Type uR
M : Type uM
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : Nontrivial R
inst✝ : Module.Free R M
κ : Type uM
b : Basis κ R M
⊢ Module.rank R (TensorAlgebra R M) = Cardinal.lift.{uR, uM} (sum fun n => Module.rank R M ^ n)

Proof state:
R : Type uR
M : Type uM
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : Nontrivial R
inst✝ : Module.Free R M
κ : Type uM
b : Basis κ R M
⊢ Module.rank R (TensorAlgebra R M) = Cardinal.lift.{uR, uM} (sum fun n => Module.rank R M ^ n)

Tactic:
rw [(equivFreeAlgebra b).toLinearEquiv.rank_eq, FreeAlgebra.rank_eq, mk_list_eq_sum_pow,
  Basis.mk_eq_rank'' b]

Result:
no goals
-- Mathlib/Data/List/Destutter.lean
theorem destutter'_cons_pos (h : R b a) : (a :: l).destutter' R b = b :: l.destutter' R a

Proof state:
α : Type u_1
l : List α
R : α → α → Prop
inst✝ : DecidableRel R
a b : α
h : R b a
⊢ destutter' R b (a :: l) = b :: destutter' R a l

Tactic:
rw [destutter', if_pos h]

Result:
no goals
-- Mathlib/LinearAlgebra/CliffordAlgebra/Conjugation.lean
theorem ι_range_comap_reverse :
    (ι Q).range.comap (reverse : CliffordAlgebra Q →ₗ[R] CliffordAlgebra Q)
      = LinearMap.range (ι Q)

Proof state:
R : Type u_1
inst✝² : CommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
⊢ Submodule.comap reverse (LinearMap.range (ι Q)) = LinearMap.range (ι Q)

Tactic:
rw [← submodule_map_reverse_eq_comap, ι_range_map_reverse]

Result:
no goals
-- Mathlib/Topology/Instances/Rat.lean
theorem uniformContinuous_abs : UniformContinuous (abs : ℚ → ℚ) :=
  Metric.uniformContinuous_iff.2 fun ε ε0 =>
    ⟨ε, ε0, fun _ _ h =>
      lt_of_le_of_lt (by simpa [Rat.dist_eq] using abs_abs_sub_abs_le_abs_sub _ _) h⟩

Proof state:
ε : ℝ
ε0 : ε > 0
x✝¹ x✝ : ℚ
h : dist x✝¹ x✝ < ε
⊢ dist |x✝¹| |x✝| ≤ dist x✝¹ x✝

Tactic:
simpa [Rat.dist_eq] using abs_abs_sub_abs_le_abs_sub _ _

Result:
no goals
-- Mathlib/Data/Finset/Erase.lean
theorem erase_right_comm {a b : α} {s : Finset α} : erase (erase s a) b = erase (erase s b) a

Proof state:
case h
α : Type u_1
inst✝ : DecidableEq α
a b : α
s : Finset α
x : α
⊢ (x ≠ b ∧ x ≠ a) ∧ x ∈ s ↔ (x ≠ a ∧ x ≠ b) ∧ x ∈ s

Tactic:
rw [@and_comm (x ≠ a)]

Result:
no goals

Proof state:
case h
α : Type u_1
inst✝ : DecidableEq α
a b : α
s : Finset α
x : α
⊢ x ∈ (s.erase a).erase b ↔ x ∈ (s.erase b).erase a

Tactic:
simp only [mem_erase, ← and_assoc]

Result:
case h
α : Type u_1
inst✝ : DecidableEq α
a b : α
s : Finset α
x : α
⊢ (x ≠ b ∧ x ≠ a) ∧ x ∈ s ↔ (x ≠ a ∧ x ≠ b) ∧ x ∈ s

Proof state:
α : Type u_1
inst✝ : DecidableEq α
a b : α
s : Finset α
⊢ (s.erase a).erase b = (s.erase b).erase a

Tactic:
ext x

Result:
case h
α : Type u_1
inst✝ : DecidableEq α
a b : α
s : Finset α
x : α
⊢ x ∈ (s.erase a).erase b ↔ x ∈ (s.erase b).erase a
-- Mathlib/LinearAlgebra/Ray.lean
theorem sameRay_or_ne_zero_and_sameRay_neg_iff_not_linearIndependent {x y : M} :
    SameRay R x y ∨ x ≠ 0 ∧ y ≠ 0 ∧ SameRay R x (-y) ↔ ¬LinearIndependent R ![x, y]

Proof state:
R : Type u_1
inst✝³ : LinearOrderedCommRing R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : NoZeroSMulDivisors R M
x y : M
⊢ SameRay R x y ∨ x ≠ 0 ∧ y ≠ 0 ∧ SameRay R x (-y) ↔ ¬LinearIndependent R ![x, y]

Tactic:
rw [← sameRay_or_sameRay_neg_iff_not_linearIndependent]

Result:
R : Type u_1
inst✝³ : LinearOrderedCommRing R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : NoZeroSMulDivisors R M
x y : M
⊢ SameRay R x y ∨ x ≠ 0 ∧ y ≠ 0 ∧ SameRay R x (-y) ↔ SameRay R x y ∨ SameRay R x (-y)

Proof state:
case neg
R : Type u_1
inst✝³ : LinearOrderedCommRing R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : NoZeroSMulDivisors R M
x y : M
hx : ¬x = 0
⊢ SameRay R x y ∨ x ≠ 0 ∧ y ≠ 0 ∧ SameRay R x (-y) ↔ SameRay R x y ∨ SameRay R x (-y)

Tactic:
by_cases hy : y = 0 <;> simp [hx, hy]

Result:
no goals

Proof state:
R : Type u_1
inst✝³ : LinearOrderedCommRing R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : NoZeroSMulDivisors R M
x y : M
⊢ SameRay R x y ∨ x ≠ 0 ∧ y ≠ 0 ∧ SameRay R x (-y) ↔ SameRay R x y ∨ SameRay R x (-y)

Tactic:
by_cases hx : x = 0

Result:
case pos
R : Type u_1
inst✝³ : LinearOrderedCommRing R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : NoZeroSMulDivisors R M
x y : M
hx : x = 0
⊢ SameRay R x y ∨ x ≠ 0 ∧ y ≠ 0 ∧ SameRay R x (-y) ↔ SameRay R x y ∨ SameRay R x (-y)

case neg
R : Type u_1
inst✝³ : LinearOrderedCommRing R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : NoZeroSMulDivisors R M
x y : M
hx : ¬x = 0
⊢ SameRay R x y ∨ x ≠ 0 ∧ y ≠ 0 ∧ SameRay R x (-y) ↔ SameRay R x y ∨ SameRay R x (-y)

Proof state:
case pos
R : Type u_1
inst✝³ : LinearOrderedCommRing R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : NoZeroSMulDivisors R M
x y : M
hx : x = 0
⊢ SameRay R x y ∨ x ≠ 0 ∧ y ≠ 0 ∧ SameRay R x (-y) ↔ SameRay R x y ∨ SameRay R x (-y)

Tactic:
simp [hx]

Result:
no goals
-- Mathlib/SetTheory/Cardinal/Aleph.lean
theorem aleph1_le_lift {c : Cardinal.{u}} : ℵ₁ ≤ lift.{v} c ↔ ℵ₁ ≤ c

Proof state:
c : Cardinal.{u}
⊢ ℵ_ 1 ≤ lift.{v, u} c ↔ ℵ_ 1 ≤ c

Tactic:
simpa using lift_le (a := ℵ₁)

Result:
no goals
-- Mathlib/Algebra/Category/ModuleCat/EpiMono.lean
theorem epi_iff_range_eq_top : Epi f ↔ LinearMap.range f.hom = ⊤ :=
  ⟨fun _ => range_eq_top_of_epi _, fun hf =>
    ConcreteCategory.epi_of_surjective _ <| by convert LinearMap.range_eq_top.1 hf⟩

Proof state:
R : Type u
inst✝ : Ring R
X Y : ModuleCat R
f : X ⟶ Y
hf : LinearMap.range (Hom.hom f) = ⊤
⊢ Function.Surjective ⇑(ConcreteCategory.hom f)

Tactic:
convert LinearMap.range_eq_top.1 hf

Result:
no goals
-- Mathlib/RingTheory/PowerSeries/Trunc.lean
theorem trunc_mul_trunc {n} (f g : R ⟦X⟧) :
    trunc n (f * (trunc n g) : R⟦X⟧) = trunc n (f * g)

Proof state:
R : Type u_2
inst✝ : CommSemiring R
n : ℕ
f g : R⟦X⟧
⊢ trunc n (f * ↑(trunc n g)) = trunc n (f * g)

Tactic:
rw [mul_comm, trunc_trunc_mul, mul_comm]

Result:
no goals
-- Mathlib/Data/Real/EReal.lean
theorem range_coe : range Real.toEReal = {⊥, ⊤}ᶜ

Proof state:
⊢ range Real.toEReal = {⊥, ⊤}ᶜ

Tactic:
ext x

Result:
case h
x : EReal
⊢ x ∈ range Real.toEReal ↔ x ∈ {⊥, ⊤}ᶜ

Proof state:
case h
x : EReal
⊢ x ∈ range Real.toEReal ↔ x ∈ {⊥, ⊤}ᶜ

Tactic:
induction x <;> simp

Result:
no goals
-- Mathlib/Data/Real/Sign.lean
theorem sign_zero : sign 0 = 0

Proof state:
⊢ sign 0 = 0

Tactic:
rw [sign, if_neg (lt_irrefl _), if_neg (lt_irrefl _)]

Result:
no goals
-- Mathlib/Order/WithBot.lean
@[simp] lemma map₂_coe_right (f : α → β → γ) (a) (b : β) : map₂ f a b = a.map (f · b)

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
a : WithBot α
b : β
⊢ map₂ f a ↑b = map (fun x => f x b) a

Tactic:
cases a <;> rfl

Result:
no goals
-- Mathlib/MeasureTheory/Measure/Restrict.lean
theorem map_comap_subtype_coe {m0 : MeasurableSpace α} {s : Set α} (hs : MeasurableSet s)
    (μ : Measure α) : (comap (↑) μ).map ((↑) : s → α) = μ.restrict s

Proof state:
α : Type u_2
m0 : MeasurableSpace α
s : Set α
hs : MeasurableSet s
μ : Measure α
⊢ Measure.map Subtype.val (Measure.comap Subtype.val μ) = μ.restrict s

Tactic:
rw [(MeasurableEmbedding.subtype_coe hs).map_comap, Subtype.range_coe]

Result:
no goals
-- Mathlib/Algebra/Group/Pointwise/Finset/Basic.lean
theorem isUnit_iff_singleton : IsUnit s ↔ ∃ a, s = {a}

Proof state:
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Group α
s : Finset α
⊢ IsUnit s ↔ ∃ a, s = {a}

Tactic:
simp only [isUnit_iff, Group.isUnit, and_true]

Result:
no goals
-- Mathlib/Order/Interval/Finset/Basic.lean
lemma uIcc_map_sectR [Lattice α] [Lattice β] [LocallyFiniteOrder α] [LocallyFiniteOrder β]
    [DecidableRel (α := α × β) (· ≤ ·)] (c : α) (a b : β) :
    (uIcc a b).map (.sectR c _) = uIcc (c, a) (c, b)

Proof state:
α : Type u_2
β : Type u_3
inst✝⁴ : Lattice α
inst✝³ : Lattice β
inst✝² : LocallyFiniteOrder α
inst✝¹ : LocallyFiniteOrder β
inst✝ : DecidableRel fun x1 x2 => x1 ≤ x2
c : α
a b : β
⊢ map (Embedding.sectR c β) [[a, b]] = [[(c, a), (c, b)]]

Tactic:
aesop (add safe forward [le_antisymm])

Result:
no goals
-- Mathlib/Order/WithBot.lean
theorem monotone_map_iff {f : α → β} : Monotone (WithTop.map f) ↔ Monotone f :=
  monotone_iff.trans <| by simp [Monotone]

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
f : α → β
⊢ ((Monotone fun a => map f ↑a) ∧ ∀ (x : α), map f ↑x ≤ map f ⊤) ↔ Monotone f

Tactic:
simp [Monotone]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Range.lean
theorem map_fst_add_enumFrom_eq_enumFrom (l : List α) (n k : Nat) :
    map (Prod.map (· + n) id) (enumFrom k l) = enumFrom (n + k) l :=
  ext_getElem? fun i ↦ by simp [(· ∘ ·), Nat.add_comm, Nat.add_left_comm]; rfl

Proof state:
α : Type u_1
l : List α
n k i : Nat
⊢ Option.map (Prod.map (fun x => n + x) id ∘ fun a => (k + i, a)) l[i]? = Option.map (fun a => (n + (k + i), a)) l[i]?

Tactic:
rfl

Result:
no goals