harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Algebra/GroupWithZero/Basic.lean
theorem mul_left_eq_self₀ : a * b = b ↔ a = 1 ∨ b = 0 :=
  calc
    a * b = b ↔ a * b = 1 * b

Proof state:
M₀ : Type u_1
inst✝ : CancelMonoidWithZero M₀
a b : M₀
⊢ a * b = b ↔ a * b = 1 * b

Tactic:
rw [one_mul]

Result:
no goals
-- Mathlib/Data/Countable/Defs.lean
lemma not_uncountable_iff : ¬Uncountable α ↔ Countable α

Proof state:
α : Sort u
⊢ ¬Uncountable α ↔ Countable α

Tactic:
rw [uncountable_iff_not_countable, not_not]

Result:
no goals
-- Mathlib/Combinatorics/Additive/Energy.lean
@[to_additive (attr := simp)] lemma mulEnergy_empty_left : Eₘ[∅, t] = 0

Proof state:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Mul α
t : Finset α
⊢ Eₘ[∅, t] = 0

Tactic:
simp [mulEnergy]

Result:
no goals
-- Mathlib/Topology/Order/DenselyOrdered.lean
theorem interior_Ici' {a : α} (ha : (Iio a).Nonempty) : interior (Ici a) = Ioi a

Proof state:
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : DenselyOrdered α
a : α
ha : (Iio a).Nonempty
⊢ interior (Ici a) = Ioi a

Tactic:
rw [← compl_Iio, interior_compl, closure_Iio' ha, compl_Iic]

Result:
no goals
-- Mathlib/Algebra/Algebra/Unitization.lean
@[simp high]
lemma starMap_inr (φ : A →⋆ₙₐ[R] B) (a : A) :
    starMap φ (inr a) = inr (φ a)

Proof state:
R : Type u_1
A : Type u_2
B : Type u_3
inst✝¹² : CommSemiring R
inst✝¹¹ : StarRing R
inst✝¹⁰ : NonUnitalSemiring A
inst✝⁹ : StarRing A
inst✝⁸ : Module R A
inst✝⁷ : SMulCommClass R A A
inst✝⁶ : IsScalarTower R A A
inst✝⁵ : NonUnitalSemiring B
inst✝⁴ : StarRing B
inst✝³ : Module R B
inst✝² : SMulCommClass R B B
inst✝¹ : IsScalarTower R B B
inst✝ : StarModule R B
φ : A →⋆ₙₐ[R] B
a : A
⊢ (starMap φ) ↑a = ↑(φ a)

Tactic:
simp

Result:
no goals
-- Mathlib/Algebra/GroupWithZero/Units/Basic.lean
theorem isUnit_zero_iff : IsUnit (0 : M₀) ↔ (0 : M₀) = 1 :=
  ⟨fun ⟨⟨_, a, (a0 : 0 * a = 1), _⟩, rfl⟩ => by rwa [zero_mul] at a0, fun h =>
    @isUnit_of_subsingleton _ _ (subsingleton_of_zero_eq_one h) 0⟩

Proof state:
M₀ : Type u_2
inst✝ : MonoidWithZero M₀
x✝ : IsUnit 0
a : M₀
a0 : 0 * a = 1
inv_val✝ : a * 0 = 1
⊢ 0 = 1

Tactic:
rwa [zero_mul] at a0

Result:
no goals
-- Mathlib/Algebra/Order/ToIntervalMod.lean
theorem toIocMod_add_toIocDiv_zsmul (a b : α) : toIocMod hp a b + toIocDiv hp a b • p = b

Proof state:
α : Type u_1
inst✝ : LinearOrderedAddCommGroup α
hα : Archimedean α
p : α
hp : 0 < p
a b : α
⊢ toIocMod hp a b + toIocDiv hp a b • p = b

Tactic:
rw [toIocMod, sub_add_cancel]

Result:
no goals
-- Mathlib/Data/Bool/Basic.lean
theorem right_le_or : ∀ x y : Bool, y ≤ (x || y)

Proof state:
⊢ ∀ (x y : Bool), y ≤ (x || y)

Tactic:
decide

Result:
no goals
-- Mathlib/Analysis/Complex/AbsMax.lean
theorem eq_of_isMaxOn_of_ball_subset {f : E → F} {s : Set E} {z w : E} (hd : DiffContOnCl ℂ f s)
    (hz : IsMaxOn (norm ∘ f) s z) (hsub : ball z (dist w z) ⊆ s) : f w = f z :=
  have H₁ : ‖f w‖ = ‖f z‖ := norm_eq_norm_of_isMaxOn_of_ball_subset hd hz hsub
  have H₂ : ‖f w + f z‖ = ‖f z + f z‖ :=
    norm_eq_norm_of_isMaxOn_of_ball_subset (hd.add_const _) hz.norm_add_self hsub
  eq_of_norm_eq_of_norm_add_eq H₁ <| by simp only [H₂, SameRay.rfl.norm_add, H₁]

Proof state:
E : Type u
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℂ E
F : Type v
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : StrictConvexSpace ℝ F
f : E → F
s : Set E
z w : E
hd : DiffContOnCl ℂ f s
hz : IsMaxOn (norm ∘ f) s z
hsub : ball z (dist w z) ⊆ s
H₁ : ‖f w‖ = ‖f z‖
H₂ : ‖f w + f z‖ = ‖f z + f z‖
⊢ ‖f w + f z‖ = ‖f w‖ + ‖f z‖

Tactic:
simp only [H₂, SameRay.rfl.norm_add, H₁]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/List/Associative.lean
theorem getKey_append_of_containsKey_eq_false [BEq α] [PartialEquivBEq α]
    {l l' : List ((a : α) × β a)} {a : α} {h} (hl' : containsKey a l' = false) :
    getKey a (l ++ l') h =
      getKey a l ((containsKey_append_of_not_contains_right hl').symm.trans h)

Proof state:
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : PartialEquivBEq α
l l' : List ((a : α) × β a)
a : α
h : containsKey a (l ++ l') = true
hl' : containsKey a l' = false
⊢ getKey a (l ++ l') h = getKey a l ⋯

Tactic:
rw [← Option.some_inj, ← getKey?_eq_some_getKey, ← getKey?_eq_some_getKey,
  getKey?_append_of_containsKey_eq_false hl']

Result:
no goals
-- Mathlib/Data/Set/Function.lean
lemma graphOn_univ_inj {g : α → β} : univ.graphOn f = univ.graphOn g ↔ f = g

Proof state:
α : Type u_1
β : Type u_2
f g : α → β
⊢ graphOn f univ = graphOn g univ ↔ f = g

Tactic:
simp

Result:
no goals
-- Mathlib/Data/Set/Card.lean
theorem ncard_singleton (a : α) : ({a} : Set α).ncard = 1

Proof state:
α : Type u_1
a : α
⊢ {a}.ncard = 1

Tactic:
simp [ncard]

Result:
no goals
-- Mathlib/.lake/packages/batteries/Batteries/Control/ForInStep/Lemmas.lean
theorem ForInStep.bindList_cons' [Monad m] [LawfulMonad m]
    (f : α → β → m (ForInStep β)) (s : ForInStep β) (a l) :
    s.bindList f (a::l) = s.bind (f a) >>= (·.bindList f l)

Proof state:
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : α → β → m (ForInStep β)
s : ForInStep β
a : α
l : List α
⊢ bindList f (a :: l) s = do
    let x ← s.bind (f a)
    bindList f l x

Tactic:
simp

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Grind/Norm.lean
theorem ite_true_false {_ : Decidable p} : (ite p True False) = p

Proof state:
p : Prop
x✝ : Decidable p
⊢ (if p then True else False) = p

Tactic:
by_cases p <;> simp

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Int/DivModLemmas.lean
theorem ediv_left_inj {a b d : Int}
    (hda : d ∣ a) (hdb : d ∣ b) : a / d = b / d ↔ a = b

Proof state:
a b d : Int
hda : d ∣ a
hdb : d ∣ b
h : a / d = b / d
⊢ a = b

Tactic:
rw [← Int.mul_ediv_cancel' hda, ← Int.mul_ediv_cancel' hdb, h]

Result:
no goals
-- Mathlib/Data/Matrix/Basic.lean
@[simp] lemma proj_comp_diagLinearMap (i : m) :
    LinearMap.proj i ∘ₗ diagLinearMap m R α = entryLinearMap R α i i

Proof state:
m : Type u_2
R : Type u_7
α : Type v
inst✝² : Semiring R
inst✝¹ : AddCommMonoid α
inst✝ : Module R α
i : m
⊢ LinearMap.proj i ∘ₗ diagLinearMap m R α = entryLinearMap R α i i

Tactic:
simp [LinearMap.ext_iff]

Result:
no goals
-- Mathlib/Data/Fintype/Card.lean
theorem card_lt_of_injective_of_not_mem (f : α → β) (h : Function.Injective f) {b : β}
    (w : b ∉ Set.range f) : card α < card β :=
  calc
    card α = (univ.map ⟨f, h⟩).card := (card_map _).symm
    _ < card β :=
      Finset.card_lt_univ_of_not_mem (x := b) <| by
        rwa [← mem_coe, coe_map, coe_univ, Set.image_univ]

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : Fintype α
inst✝ : Fintype β
f : α → β
h : Injective f
b : β
w : b ∉ Set.range f
⊢ b ∉ map { toFun := f, inj' := h } univ

Tactic:
rwa [← mem_coe, coe_map, coe_univ, Set.image_univ]

Result:
no goals
-- Mathlib/Algebra/BigOperators/Group/List/Basic.lean
theorem prod_hom (l : List M) {F : Type*} [FunLike F M N] [MonoidHomClass F M N] (f : F) :
    (l.map f).prod = f l.prod

Proof state:
M : Type u_4
N : Type u_5
inst✝³ : Monoid M
inst✝² : Monoid N
l : List M
F : Type u_8
inst✝¹ : FunLike F M N
inst✝ : MonoidHomClass F M N
f : F
⊢ (map (⇑f) l).prod = f l.prod

Tactic:
simp only [prod, foldr_map, ← map_one f]

Result:
M : Type u_4
N : Type u_5
inst✝³ : Monoid M
inst✝² : Monoid N
l : List M
F : Type u_8
inst✝¹ : FunLike F M N
inst✝ : MonoidHomClass F M N
f : F
⊢ foldr (fun x y => f x * y) (f 1) l = f (foldr (fun x1 x2 => x1 * x2) 1 l)
-- Mathlib/Computability/Tape.lean
theorem ListBlank.map_modifyNth {Γ Γ'} [Inhabited Γ] [Inhabited Γ'] (F : PointedMap Γ Γ')
    (f : Γ → Γ) (f' : Γ' → Γ') (H : ∀ x, F (f x) = f' (F x)) (n) (L : ListBlank Γ) :
    (L.modifyNth f n).map F = (L.map F).modifyNth f' n

Proof state:
Γ : Type u_1
Γ' : Type u_2
inst✝¹ : Inhabited Γ
inst✝ : Inhabited Γ'
F : PointedMap Γ Γ'
f : Γ → Γ
f' : Γ' → Γ'
H : ∀ (x : Γ), F.f (f x) = f' (F.f x)
n : ℕ
L : ListBlank Γ
⊢ map F (modifyNth f n L) = modifyNth f' n (map F L)

Tactic:
induction' n with n IH generalizing L <;>
  simp only [*, ListBlank.head_map, ListBlank.modifyNth, ListBlank.map_cons, ListBlank.tail_map]

Result:
no goals
-- Mathlib/Analysis/Normed/Operator/BoundedLinearMaps.lean
theorem nhds [CompleteSpace E] (e : E ≃L[𝕜] F) :
    range ((↑) : (E ≃L[𝕜] F) → E →L[𝕜] F) ∈ 𝓝 (e : E →L[𝕜] F) :=
  IsOpen.mem_nhds ContinuousLinearEquiv.isOpen (by simp)

Proof state:
𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
F : Type u_3
inst✝² : SeminormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
inst✝ : CompleteSpace E
e : E ≃L[𝕜] F
⊢ ↑e ∈ range toContinuousLinearMap

Tactic:
simp

Result:
no goals
-- Mathlib/Algebra/Homology/DerivedCategory/Ext/Basic.lean
lemma homEquiv_chgUniv [HasDerivedCategory.{w''} C] (e : Ext.{w} X Y n) :
    homEquiv.{w'', w'} (chgUniv.{w'} e) = homEquiv.{w'', w} e

Proof state:
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : Abelian C
inst✝² : HasExt C
inst✝¹ : HasExt C
X Y : C
n : ℕ
inst✝ : HasDerivedCategory C
e : Ext X Y n
⊢ homEquiv (chgUniv e) = homEquiv e

Tactic:
apply SmallShiftedHom.equiv_chgUniv

Result:
no goals
-- Mathlib/MeasureTheory/MeasurableSpace/Defs.lean
theorem MeasurableSpace.measurableSet_injective : Injective (@MeasurableSet α)
  | ⟨_, _, _, _⟩, ⟨_, _, _, _⟩, _ => by congr

Proof state:
α : Type u_1
MeasurableSet'✝¹ : Set α → Prop
measurableSet_empty✝¹ : MeasurableSet'✝¹ ∅
measurableSet_compl✝¹ : ∀ (s : Set α), MeasurableSet'✝¹ s → MeasurableSet'✝¹ sᶜ
measurableSet_iUnion✝¹ : ∀ (f : ℕ → Set α), (∀ (i : ℕ), MeasurableSet'✝¹ (f i)) → MeasurableSet'✝¹ (⋃ i, f i)
MeasurableSet'✝ : Set α → Prop
measurableSet_empty✝ : MeasurableSet'✝ ∅
measurableSet_compl✝ : ∀ (s : Set α), MeasurableSet'✝ s → MeasurableSet'✝ sᶜ
measurableSet_iUnion✝ : ∀ (f : ℕ → Set α), (∀ (i : ℕ), MeasurableSet'✝ (f i)) → MeasurableSet'✝ (⋃ i, f i)
x✝ : MeasurableSet = MeasurableSet
⊢ { MeasurableSet' := MeasurableSet'✝¹, measurableSet_empty := measurableSet_empty✝¹,
      measurableSet_compl := measurableSet_compl✝¹, measurableSet_iUnion := measurableSet_iUnion✝¹ } =
    { MeasurableSet' := MeasurableSet'✝, measurableSet_empty := measurableSet_empty✝,
      measurableSet_compl := measurableSet_compl✝, measurableSet_iUnion := measurableSet_iUnion✝ }

Tactic:
congr

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/RawLemmas.lean
theorem getKey_erase [EquivBEq α] [LawfulHashable α] (h : m.1.WF) {k a : α} {h'} :
    (m.erase k).getKey a h' = m.getKey a (contains_of_contains_erase _ h h')

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

Tactic:
simp_to_model [erase] using List.getKey_eraseKey

Result:
no goals
-- Mathlib/Order/InitialSeg.lean
theorem eq [IsWellOrder β s] (f g : r ≺i s) (a) : f a = g a

Proof state:
α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
inst✝ : IsWellOrder β s
f g : r ≺i s
a : α
⊢ f.toRelEmbedding a = g.toRelEmbedding a

Tactic:
rw [Subsingleton.elim f g]

Result:
no goals
-- Mathlib/Order/Interval/Set/Basic.lean
@[simp] lemma Iio_False : Iio False = ∅

Proof state:
⊢ Iio False = ∅

Tactic:
aesop

Result:
no goals
-- Mathlib/Tactic/Ring/Basic.lean
theorem pow_one_cast (a : R) : a ^ (nat_lit 1).rawCast = a

Proof state:
R : Type u_1
inst✝ : CommSemiring R
a : R
⊢ a ^ Nat.rawCast 1 = a

Tactic:
simp

Result:
no goals
-- Mathlib/Tactic/LinearCombination/Lemmas.lean
theorem lt_of_eq [OrderedCancelAddCommMonoid α] (p : (a:α) = b) (H : a' + b < b' + a) :
    a' < b'

Proof state:
α : Type u_1
a a' b b' : α
inst✝ : OrderedCancelAddCommMonoid α
p : a = b
H : a' + b < b' + a
⊢ a' < b'

Tactic:
rwa [p, add_lt_add_iff_right] at H

Result:
no goals
-- Mathlib/SetTheory/Cardinal/Arithmetic.lean
theorem nat_add_eq {a : Cardinal} (n : ℕ) (ha : ℵ₀ ≤ a) : n + a = a

Proof state:
a : Cardinal.{u_1}
n : ℕ
ha : ℵ₀ ≤ a
⊢ ↑n + a = a

Tactic:
rw [add_comm, add_nat_eq n ha]

Result:
no goals
-- Mathlib/LinearAlgebra/Span/Defs.lean
theorem span_insert (x) (s : Set M) : span R (insert x s) = (R ∙ x) ⊔ span R s

Proof state:
R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
x : M
s : Set M
⊢ span R (insert x s) = span R {x} ⊔ span R s

Tactic:
rw [insert_eq, span_union]

Result:
no goals
-- Mathlib/Data/Matroid/Closure.lean
lemma coindep_iff_compl_spanning (hI : I ⊆ M.E

Proof state:
α : Type u_2
M : Matroid α
I : Set α
hI : autoParam (I ⊆ M.E) _auto✝
⊢ M.Coindep I ↔ M.Spanning (M.E \ I)

Tactic:
rw [coindep_iff_exists, spanning_iff_exists_isBase_subset]

Result:
no goals
-- Mathlib/LinearAlgebra/Span/Basic.lean
theorem map_eq_top_iff {f : F} (hf : range f = ⊤) {p : Submodule R M} :
    p.map f = ⊤ ↔ p ⊔ LinearMap.ker f = ⊤

Proof state:
R : Type u_1
R₂ : Type u_2
M : Type u_4
M₂ : Type u_5
inst✝⁸ : Semiring R
inst✝⁷ : Semiring R₂
inst✝⁶ : AddCommGroup M
inst✝⁵ : AddCommGroup M₂
inst✝⁴ : Module R M
inst✝³ : Module R₂ M₂
τ₁₂ : R →+* R₂
inst✝² : RingHomSurjective τ₁₂
F : Type u_8
inst✝¹ : FunLike F M M₂
inst✝ : SemilinearMapClass F τ₁₂ M M₂
f : F
hf : range f = ⊤
p : Submodule R M
⊢ map f p = ⊤ ↔ p ⊔ ker f = ⊤

Tactic:
simp_rw [← top_le_iff, ← hf, range_eq_map, LinearMap.map_le_map_iff]

Result:
no goals
-- Mathlib/MeasureTheory/Group/Arithmetic.lean
theorem Multiset.measurable_prod (s : Multiset (α → M)) (hs : ∀ f ∈ s, Measurable f) :
    Measurable fun x => (s.map fun f : α → M => f x).prod

Proof state:
M : Type u_2
α : Type u_4
inst✝² : CommMonoid M
inst✝¹ : MeasurableSpace M
inst✝ : MeasurableMul₂ M
m : MeasurableSpace α
s : Multiset (α → M)
hs : ∀ f ∈ s, Measurable f
⊢ Measurable fun x => (map (fun f => f x) s).prod

Tactic:
simpa only [← Pi.multiset_prod_apply] using s.measurable_prod' hs

Result:
no goals
-- Mathlib/Topology/Semicontinuous.lean
theorem lowerSemicontinuousOn_iff_le_liminf {f : α → γ} :
    LowerSemicontinuousOn f s ↔ ∀ x ∈ s, f x ≤ liminf f (𝓝[s] x)

Proof state:
α : Type u_1
inst✝² : TopologicalSpace α
s : Set α
γ : Type u_3
inst✝¹ : CompleteLinearOrder γ
inst✝ : DenselyOrdered γ
f : α → γ
⊢ LowerSemicontinuousOn f s ↔ ∀ x ∈ s, f x ≤ liminf f (𝓝[s] x)

Tactic:
simp only [← lowerSemicontinuousWithinAt_iff_le_liminf, LowerSemicontinuousOn]

Result:
no goals
-- Mathlib/CategoryTheory/Iso.lean
theorem inv_eq_inv (f g : X ≅ Y) : f.inv = g.inv ↔ f.hom = g.hom :=
  have : ∀ {X Y : C} (f g : X ≅ Y), f.hom = g.hom → f.inv = g.inv := fun f g h => by rw [ext h]
  ⟨this f.symm g.symm, this f g⟩

Proof state:
C : Type u
inst✝ : Category.{v, u} C
X Y : C
f✝ g✝ : X ≅ Y
X✝ Y✝ : C
f g : X✝ ≅ Y✝
h : f.hom = g.hom
⊢ f.inv = g.inv

Tactic:
rw [ext h]

Result:
no goals
-- Mathlib/CategoryTheory/MorphismProperty/Representable.lean
@[reassoc (attr := simp)]
lemma lift_snd [Full F] [Faithful F] : hf.lift i h hi ≫ hf.snd g = h :=
  F.map_injective <| by simpa [lift] using PullbackCone.IsLimit.lift_snd _ _ _ _

Proof state:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
F : C ⥤ D
X Y : D
f : X ⟶ Y
hf : F.relativelyRepresentable f
a : C
g : F.obj a ⟶ Y
c : C
i : F.obj c ⟶ X
h : c ⟶ a
hi : i ≫ f = F.map h ≫ g
inst✝¹ : F.Full
inst✝ : F.Faithful
⊢ F.map (hf.lift i h hi ≫ hf.snd g) = F.map h

Tactic:
simpa [lift] using PullbackCone.IsLimit.lift_snd _ _ _ _

Result:
no goals
-- Mathlib/Algebra/Polynomial/Laurent.lean
theorem smeval_zero : (0 : R[T;T⁻¹]).smeval x = (0 : S)

Proof state:
R : Type u_1
S : Type u_2
inst✝³ : Semiring R
inst✝² : AddCommMonoid S
inst✝¹ : SMulWithZero R S
inst✝ : Monoid S
x : Sˣ
⊢ smeval 0 x = 0

Tactic:
simp only [smeval_eq_sum, Finsupp.sum_zero_index]

Result:
no goals
-- Mathlib/Algebra/Homology/TotalComplex.lean
@[reassoc]
lemma D₁_D₂ (i₁₂ i₁₂' i₁₂'' : I₁₂) :
    K.D₁ c₁₂ i₁₂ i₁₂' ≫ K.D₂ c₁₂ i₁₂' i₁₂'' = - K.D₂ c₁₂ i₁₂ i₁₂' ≫ K.D₁ c₁₂ i₁₂' i₁₂''

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 : HomologicalComplex₂ C c₁ c₂
c₁₂ : ComplexShape I₁₂
inst✝² : TotalComplexShape c₁ c₂ c₁₂
inst✝¹ : DecidableEq I₁₂
inst✝ : K.HasTotal c₁₂
i₁₂ i₁₂' i₁₂'' : I₁₂
⊢ K.D₁ c₁₂ i₁₂ i₁₂' ≫ K.D₂ c₁₂ i₁₂' i₁₂'' = -K.D₂ c₁₂ i₁₂ i₁₂' ≫ K.D₁ c₁₂ i₁₂' i₁₂''

Tactic:
simp

Result:
no goals
-- Mathlib/Data/Complex/Trigonometric.lean
theorem exp_ofReal_mul_I_im (x : ℝ) : (exp (x * I)).im = Real.sin x

Proof state:
x : ℝ
⊢ (cexp (↑x * I)).im = Real.sin x

Tactic:
simp [exp_mul_I, sin_ofReal_re]

Result:
no goals
-- Mathlib/LinearAlgebra/CrossProduct.lean
theorem cross_anticomm' (v w : Fin 3 → R) : v ×₃ w + w ×₃ v = 0

Proof state:
R : Type u_1
inst✝ : CommRing R
v w : Fin 3 → R
⊢ (crossProduct v) w + (crossProduct w) v = 0

Tactic:
rw [add_eq_zero_iff_eq_neg, cross_anticomm]

Result:
no goals
-- Mathlib/LinearAlgebra/Dimension/Finite.lean
@[simp]
lemma Submodule.one_le_finrank_iff [StrongRankCondition R] [NoZeroSMulDivisors R M]
    {S : Submodule R M} [Module.Finite R S] :
    1 ≤ finrank R S ↔ S ≠ ⊥

Proof state:
R : Type u
M : Type v
inst✝⁵ : Ring R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : StrongRankCondition R
inst✝¹ : NoZeroSMulDivisors R M
S : Submodule R M
inst✝ : Module.Finite R ↥S
⊢ 1 ≤ finrank R ↥S ↔ S ≠ ⊥

Tactic:
simp [← not_iff_not]

Result:
no goals
-- Mathlib/Data/ENNReal/Inv.lean
lemma biSup_add' {p : ι → Prop} (h : ∃ i, p i) (f : ι → ℝ≥0∞) :
    (⨆ i, ⨆ _ : p i, f i) + a = ⨆ i, ⨆ _ : p i, f i + a

Proof state:
ι : Sort u_1
a : ℝ≥0∞
p : ι → Prop
h : ∃ i, p i
f : ι → ℝ≥0∞
⊢ (⨆ i, ⨆ (_ : p i), f i) + a = ⨆ i, ⨆ (_ : p i), f i + a

Tactic:
simp only [add_comm, add_biSup' h]

Result:
no goals
-- Mathlib/Topology/Order/DenselyOrdered.lean
theorem frontier_Ioo {a b : α} (h : a < b) : frontier (Ioo a b) = {a, b}

Proof state:
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : DenselyOrdered α
a b : α
h : a < b
⊢ frontier (Ioo a b) = {a, b}

Tactic:
rw [frontier, closure_Ioo h.ne, interior_Ioo, Icc_diff_Ioo_same h.le]

Result:
no goals
-- Mathlib/RingTheory/MvPolynomial/Homogeneous.lean
lemma C_mul (hφ : φ.IsHomogeneous m) (r : R) :
    (C r * φ).IsHomogeneous m

Proof state:
σ : Type u_1
R : Type u_3
inst✝ : CommSemiring R
φ : MvPolynomial σ R
m : ℕ
hφ : φ.IsHomogeneous m
r : R
⊢ (C r * φ).IsHomogeneous m

Tactic:
simpa only [zero_add] using (isHomogeneous_C _ _).mul hφ

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Pow/Asymptotics.lean
theorem isTheta_cpow_rpow (hl_im : IsBoundedUnder (· ≤ ·) l fun x => |(g x).im|)
    (hl : ∀ᶠ x in l, f x = 0 → re (g x) = 0 → g x = 0) :
    (fun x => f x ^ g x) =Θ[l] fun x => ‖f x‖ ^ (g x).re :=
  calc
    (fun x => f x ^ g x) =Θ[l]
        (fun x => ‖f x‖ ^ (g x).re / Real.exp (arg (f x) * im (g x))) :=
      .of_norm_eventuallyEq <| hl.mono fun _ => norm_cpow_of_imp
    _ =Θ[l] fun x => ‖f x‖ ^ (g x).re / (1 : ℝ) :=
      (isTheta_refl _ _).div (isTheta_exp_arg_mul_im hl_im)
    _ =ᶠ[l] (fun x => ‖f x‖ ^ (g x).re)

Proof state:
α : Type u_1
l : Filter α
f g : α → ℂ
hl_im : IsBoundedUnder (fun x1 x2 => x1 ≤ x2) l fun x => |(g x).im|
hl : ∀ᶠ (x : α) in l, f x = 0 → (g x).re = 0 → g x = 0
⊢ (fun x => ‖f x‖ ^ (g x).re / 1) =ᶠ[l] fun x => ‖f x‖ ^ (g x).re

Tactic:
simp only [ofReal_one, div_one, EventuallyEq.rfl]

Result:
no goals
-- Mathlib/Data/Ordmap/Ordset.lean
theorem all_node4R {P l x m y r} :
    @All α P (node4R l x m y r) ↔ All P l ∧ P x ∧ All P m ∧ P y ∧ All P r

Proof state:
α : Type u_1
P : α → Prop
l : Ordnode α
x : α
m : Ordnode α
y : α
r : Ordnode α
⊢ All P (l.node4R x m y r) ↔ All P l ∧ P x ∧ All P m ∧ P y ∧ All P r

Tactic:
cases m <;> simp [node4R, all_node', All, all_node3R, and_assoc]

Result:
no goals
-- Mathlib/Analysis/Convex/Gauge.lean
theorem gauge_lt_one_of_mem_of_isOpen (hs₂ : IsOpen s) {x : E} (hx : x ∈ s) :
    gauge s x < 1 :=
  interior_subset_gauge_lt_one s <| by rwa [hs₂.interior_eq]

Proof state:
E : Type u_2
inst✝³ : AddCommGroup E
inst✝² : Module ℝ E
s : Set E
inst✝¹ : TopologicalSpace E
inst✝ : ContinuousSMul ℝ E
hs₂ : IsOpen s
x : E
hx : x ∈ s
⊢ x ∈ interior s

Tactic:
rwa [hs₂.interior_eq]

Result:
no goals
-- Mathlib/Algebra/MvPolynomial/Basic.lean
theorem support_mul_X (s : σ) (p : MvPolynomial σ R) :
    (p * X s).support = p.support.map (addRightEmbedding (Finsupp.single s 1)) :=
  AddMonoidAlgebra.support_mul_single p _ (by simp) _

Proof state:
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
s : σ
p : MvPolynomial σ R
⊢ ∀ (y : R), y * 1 = 0 ↔ y = 0

Tactic:
simp

Result:
no goals
-- Mathlib/Algebra/MvPolynomial/Basic.lean
@[simp]
lemma C_mem_coeffsIn : C x ∈ coeffsIn σ M ↔ x ∈ M

Proof state:
R : Type u_2
S : Type u_3
σ : Type u_4
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : Module R S
M : Submodule R S
x : S
⊢ C x ∈ coeffsIn σ M ↔ x ∈ M

Tactic:
simpa using monomial_mem_coeffsIn (i := 0)

Result:
no goals
-- Mathlib/MeasureTheory/Integral/IntervalIntegral.lean
theorem integral_eq_zero_iff_of_le_of_nonneg_ae (hab : a ≤ b) (hf : 0 ≤ᵐ[μ.restrict (Ioc a b)] f)
    (hfi : IntervalIntegrable f μ a b) :
    ∫ x in a..b, f x ∂μ = 0 ↔ f =ᵐ[μ.restrict (Ioc a b)] 0

Proof state:
f : ℝ → ℝ
a b : ℝ
μ : Measure ℝ
hab : a ≤ b
hf : 0 ≤ᶠ[ae (μ.restrict (Ioc a b))] f
hfi : IntervalIntegrable f μ a b
⊢ ∫ (x : ℝ) in a..b, f x ∂μ = 0 ↔ f =ᶠ[ae (μ.restrict (Ioc a b))] 0

Tactic:
rw [integral_of_le hab, integral_eq_zero_iff_of_nonneg_ae hf hfi.1]

Result:
no goals
-- Mathlib/Data/List/Perm/Basic.lean
theorem rel_perm_imp (hr : RightUnique r) : (Forall₂ r ⇒ Forall₂ r ⇒ (· → ·)) Perm Perm :=
  fun a b h₁ c d h₂ h =>
  have : (flip (Forall₂ r) ∘r Perm ∘r Forall₂ r) b d := ⟨a, h₁, c, h, h₂⟩
  have : ((flip (Forall₂ r) ∘r Forall₂ r) ∘r Perm) b d

Proof state:
α : Type u_1
β : Type u_2
r : α → β → Prop
hr : RightUnique r
a : List α
b : List β
h₁ : Forall₂ r a b
c : List α
d : List β
h₂ : Forall₂ r c d
h : a ~ c
this : (flip (Forall₂ r) ∘r Perm ∘r Forall₂ r) b d
⊢ ((flip (Forall₂ r) ∘r Forall₂ r) ∘r Perm) b d

Tactic:
rwa [← forall₂_comp_perm_eq_perm_comp_forall₂, ← Relation.comp_assoc] at this

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

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

Tactic:
rw [lt_neg_iff, neg_zero]

Result:
no goals
-- Mathlib/GroupTheory/CoprodI.lean
theorem inv_prod {i j} (w : NeWord G i j) : w.inv.prod = w.prod⁻¹

Proof state:
ι : Type u_1
G : ι → Type u_4
inst✝ : (i : ι) → Group (G i)
i j : ι
w : NeWord G i j
⊢ w.inv.prod = w.prod⁻¹

Tactic:
induction w <;> simp [inv, *]

Result:
no goals
-- Mathlib/Data/Real/Pi/Bounds.lean
theorem pi_gt_d2 : 3.14 < π

Proof state:
⊢ 3.14 < π

Tactic:
pi_lower_bound [338 / 239, 704 / 381, 1940 / 989, 1447 / 727]

Result:
no goals
-- Mathlib/LinearAlgebra/Matrix/ToLin.lean
theorem Matrix.toLin_one : Matrix.toLin v₁ v₁ 1 = LinearMap.id

Proof state:
R : Type u_1
inst✝⁴ : CommSemiring R
n : Type u_4
inst✝³ : Fintype n
inst✝² : DecidableEq n
M₁ : Type u_5
inst✝¹ : AddCommMonoid M₁
inst✝ : Module R M₁
v₁ : Basis n R M₁
⊢ (toLin v₁ v₁) 1 = LinearMap.id

Tactic:
rw [← LinearMap.toMatrix_id v₁, Matrix.toLin_toMatrix]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/RawLemmas.lean
theorem get!_eq_default [LawfulBEq α] (h : m.1.WF) {a : α} [Inhabited (β a)] :
    m.contains a = false → m.get! a = default

Proof state:
α : Type u
β : α → Type v
m : Raw₀ α β
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : LawfulBEq α
h : m.val.WF
a : α
inst✝ : Inhabited (β a)
⊢ m.contains a = false → m.get! a = default

Tactic:
simp_to_model using List.getValueCast!_eq_default

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Option/Attach.lean
theorem attachWith_eq_none_iff {p : α → Prop} {o : Option α} (H : ∀ a ∈ o, p a) :
    o.attachWith p H = none ↔ o = none

Proof state:
α : Type u_1
p : α → Prop
o : Option α
H : ∀ (a : α), a ∈ o → p a
⊢ o.attachWith p H = none ↔ o = none

Tactic:
cases o <;> simp

Result:
no goals
-- Mathlib/Data/Matrix/Notation.lean
theorem vec2_add [Add α] (a₀ a₁ b₀ b₁ : α) : ![a₀, a₁] + ![b₀, b₁] = ![a₀ + b₀, a₁ + b₁]

Proof state:
α : Type u
inst✝ : Add α
a₀ a₁ b₀ b₁ : α
⊢ ![a₀, a₁] + ![b₀, b₁] = ![a₀ + b₀, a₁ + b₁]

Tactic:
rw [cons_add_cons, cons_add_cons, empty_add_empty]

Result:
no goals