harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Order/PiLex.lean
theorem lex_lt_of_lt [∀ i, PartialOrder (β i)] {r} (hwf : WellFounded r) {x y : ∀ i, β i}
    (hlt : x < y) : Pi.Lex r (@fun _ => (· < ·)) x y

Proof state:
ι : Type u_1
β : ι → Type u_2
inst✝ : (i : ι) → PartialOrder (β i)
r : ι → ι → Prop
hwf : WellFounded r
x y : (i : ι) → β i
hlt : x < y
⊢ Pi.Lex r (fun x x1 x2 => x1 < x2) x y

Tactic:
simp_rw [Pi.Lex, le_antisymm_iff]

Result:
ι : Type u_1
β : ι → Type u_2
inst✝ : (i : ι) → PartialOrder (β i)
r : ι → ι → Prop
hwf : WellFounded r
x y : (i : ι) → β i
hlt : x < y
⊢ ∃ i, (∀ (j : ι), r j i → x j ≤ y j ∧ y j ≤ x j) ∧ x i < y i

Proof state:
ι : Type u_1
β : ι → Type u_2
inst✝ : (i : ι) → PartialOrder (β i)
r : ι → ι → Prop
hwf : WellFounded r
x y : (i : ι) → β i
hlt : x < y
⊢ ∃ i, (∀ (j : ι), r j i → x j ≤ y j ∧ y j ≤ x j) ∧ x i < y i

Tactic:
exact lex_lt_of_lt_of_preorder hwf hlt

Result:
no goals
-- Mathlib/Order/UpperLower/Basic.lean
theorem isLowerSet_iff_Iic_subset : IsLowerSet s ↔ ∀ ⦃a⦄, a ∈ s → Iic a ⊆ s

Proof state:
α : Type u_1
inst✝ : Preorder α
s : Set α
⊢ IsLowerSet s ↔ ∀ ⦃a : α⦄, a ∈ s → Iic a ⊆ s

Tactic:
simp [IsLowerSet, subset_def, @forall_swap (_ ∈ s)]

Result:
no goals
-- Mathlib/Topology/Algebra/Module/LinearMap.lean
theorem zero_comp (f : M₁ →SL[σ₁₂] M₂) : (0 : M₂ →SL[σ₂₃] M₃).comp f = 0

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

Tactic:
simp

Result:
no goals

Proof state:
R₁ : Type u_1
R₂ : Type u_2
R₃ : Type u_3
inst✝¹² : Semiring R₁
inst✝¹¹ : Semiring R₂
inst✝¹⁰ : Semiring R₃
σ₁₂ : R₁ →+* R₂
σ₂₃ : R₂ →+* R₃
σ₁₃ : R₁ →+* R₃
M₁ : Type u_4
inst✝⁹ : TopologicalSpace M₁
inst✝⁸ : AddCommMonoid M₁
M₂ : Type u_6
inst✝⁷ : TopologicalSpace M₂
inst✝⁶ : AddCommMonoid M₂
M₃ : Type u_7
inst✝⁵ : TopologicalSpace M₃
inst✝⁴ : AddCommMonoid M₃
inst✝³ : Module R₁ M₁
inst✝² : Module R₂ M₂
inst✝¹ : Module R₃ M₃
inst✝ : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
f : M₁ →SL[σ₁₂] M₂
⊢ comp 0 f = 0

Tactic:
ext

Result:
case h
R₁ : Type u_1
R₂ : Type u_2
R₃ : Type u_3
inst✝¹² : Semiring R₁
inst✝¹¹ : Semiring R₂
inst✝¹⁰ : Semiring R₃
σ₁₂ : R₁ →+* R₂
σ₂₃ : R₂ →+* R₃
σ₁₃ : R₁ →+* R₃
M₁ : Type u_4
inst✝⁹ : TopologicalSpace M₁
inst✝⁸ : AddCommMonoid M₁
M₂ : Type u_6
inst✝⁷ : TopologicalSpace M₂
inst✝⁶ : AddCommMonoid M₂
M₃ : Type u_7
inst✝⁵ : TopologicalSpace M₃
inst✝⁴ : AddCommMonoid M₃
inst✝³ : Module R₁ M₁
inst✝² : Module R₂ M₂
inst✝¹ : Module R₃ M₃
inst✝ : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
f : M₁ →SL[σ₁₂] M₂
x✝ : M₁
⊢ (comp 0 f) x✝ = 0 x✝
-- Mathlib/Order/CompleteSublattice.lean
theorem coe_sInf' (S : Set L) : (↑(sInf S) : α) = ⨅ N ∈ S, (N : α)

Proof state:
α : Type u_1
inst✝ : CompleteLattice α
L : CompleteSublattice α
S : Set ↥L
⊢ ↑(sInf S) = ⨅ N ∈ S, ↑N

Tactic:
rw [coe_sInf, ← Set.image, sInf_image]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/RawLemmas.lean
theorem get?_eq_some_get!_of_contains [EquivBEq α] [LawfulHashable α] [Inhabited β] (h : m.WF)
    {a : α} : m.contains a = true → get? m a = some (get! m a)

Proof state:
α : Type u
inst✝⁴ : BEq α
inst✝³ : Hashable α
β : Type v
m : Raw α fun x => β
inst✝² : EquivBEq α
inst✝¹ : LawfulHashable α
inst✝ : Inhabited β
h : m.WF
a : α
⊢ m.contains a = true → get? m a = some (get! m a)

Tactic:
simp_to_raw using Raw₀.Const.get?_eq_some_get!

Result:
no goals
-- Mathlib/Algebra/BigOperators/Finprod.lean
theorem finprod_of_infinite_mulSupport {f : α → M} (hf : (mulSupport f).Infinite) :
    ∏ᶠ i, f i = 1

Proof state:
α : Type u_1
M : Type u_5
inst✝ : CommMonoid M
f : α → M
hf : (mulSupport f).Infinite
⊢ ∏ᶠ (i : α), f i = 1

Tactic:
classical rw [finprod_def, dif_neg hf]

Result:
no goals

Proof state:
α : Type u_1
M : Type u_5
inst✝ : CommMonoid M
f : α → M
hf : (mulSupport f).Infinite
⊢ ∏ᶠ (i : α), f i = 1

Tactic:
rw [finprod_def, dif_neg hf]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Nat/Lemmas.lean
theorem le_iff_lt_add_one : x ≤ y ↔ x < y + 1

Proof state:
x y : Nat
⊢ x ≤ y ↔ x < y + 1

Tactic:
omega

Result:
no goals
-- Mathlib/Logic/Equiv/Defs.lean
theorem permCongr_refl : e.permCongr (Equiv.refl _) = Equiv.refl _

Proof state:
α' : Type u_1
β' : Type u_2
e : α' ≃ β'
⊢ e.permCongr (Equiv.refl α') = Equiv.refl β'

Tactic:
simp [permCongr_def]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem toNat_cons (b : Bool) (x : BitVec w) :
    (cons b x).toNat = (b.toNat <<< w) ||| x.toNat

Proof state:
w : Nat
b : Bool
x : BitVec w
⊢ (cons b x).toNat = b.toNat <<< w ||| x.toNat

Tactic:
let ⟨x, _⟩ := x

Result:
w : Nat
b : Bool
x✝ : BitVec w
x : Nat
isLt✝ : x < 2 ^ w
⊢ (cons b { toFin := ⟨x, isLt✝⟩ }).toNat = b.toNat <<< w ||| { toFin := ⟨x, isLt✝⟩ }.toNat

Proof state:
w : Nat
b : Bool
x✝ : BitVec w
x : Nat
isLt✝ : x < 2 ^ w
⊢ (cons b { toFin := ⟨x, isLt✝⟩ }).toNat = b.toNat <<< w ||| { toFin := ⟨x, isLt✝⟩ }.toNat

Tactic:
simp [cons, toNat_append, toNat_ofBool]

Result:
no goals
-- Mathlib/MeasureTheory/Measure/Lebesgue/EqHaar.lean
theorem addHaar_ball_of_pos (x : E) {r : ℝ} (hr : 0 < r) :
    μ (ball x r) = ENNReal.ofReal (r ^ finrank ℝ E) * μ (ball 0 1)

Proof state:
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : FiniteDimensional ℝ E
μ : Measure E
inst✝ : μ.IsAddHaarMeasure
x : E
r : ℝ
hr : 0 < r
⊢ μ (ball x r) = ENNReal.ofReal (r ^ finrank ℝ E) * μ (ball 0 1)

Tactic:
rw [← addHaar_ball_mul_of_pos μ x hr, mul_one]

Result:
no goals
-- Mathlib/AlgebraicGeometry/Scheme.lean
lemma appLE_congr (e : V ≤ f ⁻¹ᵁ U) (e₁ : U = U') (e₂ : V = V')
    (P : ∀ {R S : CommRingCat.{u}} (_ : R ⟶ S), Prop) :
    P (f.appLE U V e) ↔ P (f.appLE U' V' (e₁ ▸ e₂ ▸ e))

Proof state:
X Y : Scheme
f : X.Hom Y
U U' : Y.Opens
V V' : X.Opens
e : V ≤ f ⁻¹ᵁ U
e₁ : U = U'
e₂ : V = V'
P : {R S : CommRingCat} → (R ⟶ S) → Prop
⊢ P (f.appLE U V e) ↔ P (f.appLE U' V' ⋯)

Tactic:
subst e₁

Result:
X Y : Scheme
f : X.Hom Y
U : Y.Opens
V V' : X.Opens
e : V ≤ f ⁻¹ᵁ U
e₂ : V = V'
P : {R S : CommRingCat} → (R ⟶ S) → Prop
⊢ P (f.appLE U V e) ↔ P (f.appLE U V' ⋯)

Proof state:
X Y : Scheme
f : X.Hom Y
U : Y.Opens
V V' : X.Opens
e : V ≤ f ⁻¹ᵁ U
e₂ : V = V'
P : {R S : CommRingCat} → (R ⟶ S) → Prop
⊢ P (f.appLE U V e) ↔ P (f.appLE U V' ⋯)

Tactic:
subst e₂

Result:
X Y : Scheme
f : X.Hom Y
U : Y.Opens
V : X.Opens
e : V ≤ f ⁻¹ᵁ U
P : {R S : CommRingCat} → (R ⟶ S) → Prop
⊢ P (f.appLE U V e) ↔ P (f.appLE U V ⋯)

Proof state:
X Y : Scheme
f : X.Hom Y
U : Y.Opens
V : X.Opens
e : V ≤ f ⁻¹ᵁ U
P : {R S : CommRingCat} → (R ⟶ S) → Prop
⊢ P (f.appLE U V e) ↔ P (f.appLE U V ⋯)

Tactic:
rfl

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Zip.lean
theorem zip_eq_append_iff {l₁ : List α} {l₂ : List β} :
    zip l₁ l₂ = l₁' ++ l₂' ↔
      ∃ w x y z, w.length = y.length ∧ l₁ = w ++ x ∧ l₂ = y ++ z ∧ l₁' = zip w y ∧ l₂' = zip x z

Proof state:
α : Type u_1
β : Type u_2
l₁' l₂' : List (α × β)
l₁ : List α
l₂ : List β
⊢ l₁.zip l₂ = l₁' ++ l₂' ↔ ∃ w x y z, w.length = y.length ∧ l₁ = w ++ x ∧ l₂ = y ++ z ∧ l₁' = w.zip y ∧ l₂' = x.zip z

Tactic:
simp [zip_eq_zipWith, zipWith_eq_append_iff]

Result:
no goals
-- Mathlib/Algebra/Order/ToIntervalMod.lean
theorem toIcoDiv_add_zsmul (a b : α) (m : ℤ) : toIcoDiv hp a (b + m • p) = toIcoDiv hp a b + m :=
  toIcoDiv_eq_of_sub_zsmul_mem_Ico hp <| by
    simpa only [add_smul, add_sub_add_right_eq_sub] using sub_toIcoDiv_zsmul_mem_Ico hp a b

Proof state:
α : Type u_1
inst✝ : LinearOrderedAddCommGroup α
hα : Archimedean α
p : α
hp : 0 < p
a b : α
m : ℤ
⊢ b + m • p - (toIcoDiv hp a b + m) • p ∈ Set.Ico a (a + p)

Tactic:
simpa only [add_smul, add_sub_add_right_eq_sub] using sub_toIcoDiv_zsmul_mem_Ico hp a b

Result:
no goals
-- Mathlib/MeasureTheory/Function/SimpleFunc.lean
theorem restrict_univ (f : α →ₛ β) : restrict f univ = f

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : Zero β
f : α →ₛ β
⊢ f.restrict univ = f

Tactic:
simp [restrict]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Log/Base.lean
theorem logb_le_iff_le_rpow (hx : 0 < x) : logb b x ≤ y ↔ x ≤ b ^ y

Proof state:
b x y : ℝ
hb : 1 < b
hx : 0 < x
⊢ logb b x ≤ y ↔ x ≤ b ^ y

Tactic:
rw [← rpow_le_rpow_left_iff hb, rpow_logb (b_pos hb) (b_ne_one' hb) hx]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Int/DivModLemmas.lean
theorem add_bmod_eq_add_bmod_right (i : Int)
    (H : bmod x n = bmod y n) : bmod (x + i) n = bmod (y + i) n

Proof state:
x : Int
n : Nat
y i : Int
H : x.bmod n = y.bmod n
⊢ (x + i).bmod n = (y + i).bmod n

Tactic:
rw [← bmod_add_bmod_congr, ← @bmod_add_bmod_congr y, H]

Result:
no goals
-- Mathlib/AlgebraicGeometry/Morphisms/IsIso.lean
lemma isomorphisms_eq_isOpenImmersion_inf_surjective :
    isomorphisms Scheme = (@IsOpenImmersion ⊓ @Surjective : MorphismProperty Scheme)

Proof state:
⊢ isomorphisms Scheme = @IsOpenImmersion ⊓ @Surjective

Tactic:
ext

Result:
case h
X✝ Y✝ : Scheme
f✝ : X✝ ⟶ Y✝
⊢ isomorphisms Scheme f✝ ↔ (@IsOpenImmersion ⊓ @Surjective) f✝

Proof state:
case h
X✝ Y✝ : Scheme
f✝ : X✝ ⟶ Y✝
⊢ isomorphisms Scheme f✝ ↔ (@IsOpenImmersion ⊓ @Surjective) f✝

Tactic:
exact (isIso_iff_isOpenImmersion _).trans
  (and_congr Iff.rfl ((TopCat.epi_iff_surjective _).trans (surjective_iff _).symm))

Result:
no goals
-- Mathlib/Algebra/Group/Subgroup/Lattice.lean
@[to_additive (attr := simp)]
lemma mem_closure_singleton_self (x : G) : x ∈ closure ({x} : Set G)

Proof state:
G : Type u_1
inst✝ : Group G
x : G
⊢ x ∈ closure {x}

Tactic:
simpa [-subset_closure] using subset_closure (k := {x})

Result:
no goals
-- Mathlib/Tactic/CategoryTheory/Monoidal/Datatypes.lean
theorem structuralIsoOfExpr_comp {f g h : C}
    (η : f ⟶ g) (η' : f ≅ g) (ih_η : η'.hom = η)
    (θ : g ⟶ h) (θ' : g ≅ h) (ih_θ : θ'.hom = θ) :
    (η' ≪≫ θ').hom  = η ≫ θ

Proof state:
C : Type u
inst✝ : Category.{v, u} C
f g h : C
η : f ⟶ g
η' : f ≅ g
ih_η : η'.hom = η
θ : g ⟶ h
θ' : g ≅ h
ih_θ : θ'.hom = θ
⊢ (η' ≪≫ θ').hom = η ≫ θ

Tactic:
simp [ih_η, ih_θ]

Result:
no goals
-- Mathlib/Topology/Algebra/Support.lean
theorem hasCompactMulSupport_def : HasCompactMulSupport f ↔ IsCompact (closure (mulSupport f))

Proof state:
α : Type u_2
β : Type u_4
inst✝¹ : TopologicalSpace α
inst✝ : One β
f : α → β
⊢ HasCompactMulSupport f ↔ IsCompact (closure (mulSupport f))

Tactic:
rfl

Result:
no goals
-- Mathlib/LinearAlgebra/TensorProduct/Basic.lean
theorem uncurry_apply (f : M →ₗ[R] N →ₗ[R] P) (m : M) (n : N) :
    uncurry R M N P f (m ⊗ₜ n) = f m n

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
m : M
n : N
⊢ ((uncurry R M N P) f) (m ⊗ₜ[R] n) = (f m) n

Tactic:
rw [uncurry, LinearMap.flip_apply, lift.tmul]

Result:
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
m : M
n : N
⊢ (((LinearMap.lflip ∘ₗ LinearMap.id.flip) m) n) f = (f m) n

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
m : M
n : N
⊢ (((LinearMap.lflip ∘ₗ LinearMap.id.flip) m) n) f = (f m) n

Tactic:
rfl

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Lemmas.lean
theorem getLast?_eq_get? (l : List α) : getLast? l = l.get? (l.length - 1)

Proof state:
α : Type u_1
l : List α
⊢ l.getLast? = l.get? (l.length - 1)

Tactic:
simp [getLast?_eq_getElem?]

Result:
no goals
-- Mathlib/Algebra/Order/Group/MinMax.lean
@[to_additive]
lemma max_inv_one (a : α) : max a⁻¹ 1 = a⁻¹ * max a 1

Proof state:
α : Type u_1
inst✝² : Group α
inst✝¹ : LinearOrder α
inst✝ : MulLeftMono α
a : α
⊢ a⁻¹ ⊔ 1 = a⁻¹ * (a ⊔ 1)

Tactic:
rw [eq_inv_mul_iff_mul_eq, ← eq_div_iff_mul_eq', max_one_div_max_inv_one_eq_self]

Result:
no goals
-- Mathlib/GroupTheory/Coprod/Basic.lean
theorem range_eq (f : G ∗ H →* K) :
    MonoidHom.range f = MonoidHom.range (f.comp inl) ⊔ MonoidHom.range (f.comp inr)

Proof state:
G : Type u_1
H : Type u_2
inst✝² : Group G
inst✝¹ : Group H
K : Type u_3
inst✝ : Group K
f : G ∗ H →* K
⊢ f.range = (f.comp inl).range ⊔ (f.comp inr).range

Tactic:
rw [MonoidHom.range_eq_map, ← range_inl_sup_range_inr, Subgroup.map_sup, MonoidHom.map_range,
  MonoidHom.map_range]

Result:
no goals
-- Mathlib/CategoryTheory/Subobject/Limits.lean
theorem imageSubobject_zero {A B : C} : imageSubobject (0 : A ⟶ B) = ⊥ :=
  Subobject.eq_of_comm (imageSubobjectIso _ ≪≫ imageZero ≪≫ Subobject.botCoeIsoZero.symm) (by simp)

Proof state:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
inst✝ : HasZeroObject C
A B : C
⊢ (imageSubobjectIso 0 ≪≫ imageZero ≪≫ botCoeIsoZero.symm).hom ≫ ⊥.arrow = (imageSubobject 0).arrow

Tactic:
simp

Result:
no goals
-- Mathlib/CategoryTheory/Limits/Preserves/Shapes/Terminal.lean
/-- If there is any isomorphism `G.obj ⊤ ⟶ ⊤`, then `G` preserves terminal objects. -/
lemma preservesTerminal_of_isIso (f : G.obj (⊤_ C) ⟶ ⊤_ D) [i : IsIso f] :
    PreservesLimit (Functor.empty.{0} C) G

Proof state:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
G : C ⥤ D
inst✝¹ : HasTerminal C
inst✝ : HasTerminal D
f : G.obj (⊤_ C) ⟶ ⊤_ D
i : IsIso (terminalComparison G)
⊢ PreservesLimit (Functor.empty C) G

Tactic:
exact PreservesTerminal.of_iso_comparison G

Result:
no goals

Proof state:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
G : C ⥤ D
inst✝¹ : HasTerminal C
inst✝ : HasTerminal D
f : G.obj (⊤_ C) ⟶ ⊤_ D
i : IsIso f
⊢ PreservesLimit (Functor.empty C) G

Tactic:
rw [Subsingleton.elim f (terminalComparison G)] at i

Result:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
G : C ⥤ D
inst✝¹ : HasTerminal C
inst✝ : HasTerminal D
f : G.obj (⊤_ C) ⟶ ⊤_ D
i : IsIso (terminalComparison G)
⊢ PreservesLimit (Functor.empty C) G
-- Mathlib/Data/Finset/Powerset.lean
theorem not_mem_of_mem_powerset_of_not_mem {s t : Finset α} {a : α} (ht : t ∈ s.powerset)
    (h : a ∉ s) : a ∉ t

Proof state:
α : Type u_1
s t : Finset α
a : α
ht : t ∈ s.powerset
h : a ∉ s
⊢ a ∉ t

Tactic:
apply mt _ h

Result:
α : Type u_1
s t : Finset α
a : α
ht : t ∈ s.powerset
h : a ∉ s
⊢ a ∈ t → a ∈ s

Proof state:
α : Type u_1
s t : Finset α
a : α
ht : t ∈ s.powerset
h : a ∉ s
⊢ a ∈ t → a ∈ s

Tactic:
apply mem_powerset.1 ht

Result:
no goals
-- Mathlib/Algebra/BigOperators/Group/Multiset/Defs.lean
theorem prod_map_one : prod (m.map fun _ => (1 : α)) = 1

Proof state:
ι : Type u_2
α : Type u_3
inst✝ : CommMonoid α
m : Multiset ι
⊢ (map (fun x => 1) m).prod = 1

Tactic:
rw [map_const', prod_replicate, one_pow]

Result:
no goals
-- Mathlib/Data/Nat/Init.lean
lemma div_add_mod' (a b : ℕ) : a / b * b + a % b = a

Proof state:
a b : ℕ
⊢ b * (a / b) + a % b = a

Tactic:
exact div_add_mod _ _

Result:
no goals

Proof state:
a b : ℕ
⊢ a / b * b + a % b = a

Tactic:
rw [Nat.mul_comm]

Result:
a b : ℕ
⊢ b * (a / b) + a % b = a
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Find.lean
theorem lookup_eq_none_iff {l : List (α × β)} {k : α} :
    l.lookup k = none ↔ ∀ p ∈ l, k != p.1

Proof state:
α : Type u_2
inst✝¹ : BEq α
inst✝ : LawfulBEq α
β : Type u_1
l : List (α × β)
k : α
⊢ lookup k l = none ↔ ∀ (p : α × β), p ∈ l → (k != p.fst) = true

Tactic:
simp [lookup_eq_findSome?]

Result:
no goals
-- Mathlib/Probability/Independence/Basic.lean
lemma iIndepSets_iff (π : ι → Set (Set Ω)) (μ : Measure Ω) :
    iIndepSets π μ ↔ ∀ (s : Finset ι) {f : ι → Set Ω} (_H : ∀ i, i ∈ s → f i ∈ π i),
      μ (⋂ i ∈ s, f i) = ∏ i ∈ s, μ (f i)

Proof state:
Ω : Type u_1
ι : Type u_2
x✝ : MeasurableSpace Ω
π : ι → Set (Set Ω)
μ : Measure Ω
⊢ iIndepSets π μ ↔ ∀ (s : Finset ι) {f : ι → Set Ω}, (∀ i ∈ s, f i ∈ π i) → μ (⋂ i ∈ s, f i) = ∏ i ∈ s, μ (f i)

Tactic:
simp only [iIndepSets, Kernel.iIndepSets, ae_dirac_eq, Filter.eventually_pure, Kernel.const_apply]

Result:
no goals
-- Mathlib/Combinatorics/SetFamily/Shadow.lean
/-- `t ∈ ∂𝒜` iff `t` is exactly one element less than something from `𝒜`.

See also `Finset.mem_shadow_iff_exists_mem_card_add_one`. -/
lemma mem_shadow_iff_exists_sdiff : t ∈ ∂ 𝒜 ↔ ∃ s ∈ 𝒜, t ⊆ s ∧ #(s \ t) = 1

Proof state:
α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
t : Finset α
⊢ t ∈ ∂ 𝒜 ↔ ∃ s ∈ 𝒜, t ⊆ s ∧ #(s \ t) = 1

Tactic:
simp_rw [mem_shadow_iff, ← covBy_iff_card_sdiff_eq_one, covBy_iff_exists_erase]

Result:
no goals
-- Mathlib/Algebra/Order/GroupWithZero/Canonical.lean
theorem mul_inv_lt_of_lt_mul₀ (h : a < b * c) : a * c⁻¹ < b

Proof state:
α : Type u_1
inst✝ : LinearOrderedCommGroupWithZero α
a b c : α
h : a < b * c
⊢ a * c⁻¹ < b

Tactic:
contrapose! h

Result:
α : Type u_1
inst✝ : LinearOrderedCommGroupWithZero α
a b c : α
h : b ≤ a * c⁻¹
⊢ b * c ≤ a

Proof state:
α : Type u_1
inst✝ : LinearOrderedCommGroupWithZero α
a b c : α
h : b ≤ a * c⁻¹
⊢ b * c ≤ a

Tactic:
simpa only [inv_inv] using mul_inv_le_of_le_mul₀ zero_le' zero_le' h

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/List/Associative.lean
theorem getEntry?_insertEntry [BEq α] [PartialEquivBEq α] {l : List ((a : α) × β a)} {k a : α}
    {v : β k} :
    getEntry? a (insertEntry k v l) = if k == a then some ⟨k, v⟩ else getEntry? a l

Proof state:
case false
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : PartialEquivBEq α
l : List ((a : α) × β a)
k a : α
v : β k
hl : containsKey k l = false
⊢ getEntry? a (insertEntry k v l) = if (k == a) = true then some ⟨k, v⟩ else getEntry? a l

Tactic:
rw [insertEntry_of_containsKey_eq_false hl, getEntry?_cons, cond_eq_if]

Result:
no goals

Proof state:
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : PartialEquivBEq α
l : List ((a : α) × β a)
k a : α
v : β k
⊢ getEntry? a (insertEntry k v l) = if (k == a) = true then some ⟨k, v⟩ else getEntry? a l

Tactic:
cases hl : containsKey k l

Result:
case false
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : PartialEquivBEq α
l : List ((a : α) × β a)
k a : α
v : β k
hl : containsKey k l = false
⊢ getEntry? a (insertEntry k v l) = if (k == a) = true then some ⟨k, v⟩ else getEntry? a l

case true
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : PartialEquivBEq α
l : List ((a : α) × β a)
k a : α
v : β k
hl : containsKey k l = true
⊢ getEntry? a (insertEntry k v l) = if (k == a) = true then some ⟨k, v⟩ else getEntry? a l

Proof state:
case true
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : PartialEquivBEq α
l : List ((a : α) × β a)
k a : α
v : β k
hl : containsKey k l = true
⊢ getEntry? a (insertEntry k v l) = if (k == a) = true then some ⟨k, v⟩ else getEntry? a l

Tactic:
simp [insertEntry_of_containsKey hl, getEntry?_replaceEntry, hl]

Result:
no goals
-- Mathlib/Algebra/Order/ToIntervalMod.lean
theorem toIocDiv_add_zsmul (a b : α) (m : ℤ) : toIocDiv hp a (b + m • p) = toIocDiv hp a b + m :=
  toIocDiv_eq_of_sub_zsmul_mem_Ioc hp <| by
    simpa only [add_smul, add_sub_add_right_eq_sub] using sub_toIocDiv_zsmul_mem_Ioc hp a b

Proof state:
α : Type u_1
inst✝ : LinearOrderedAddCommGroup α
hα : Archimedean α
p : α
hp : 0 < p
a b : α
m : ℤ
⊢ b + m • p - (toIocDiv hp a b + m) • p ∈ Set.Ioc a (a + p)

Tactic:
simpa only [add_smul, add_sub_add_right_eq_sub] using sub_toIocDiv_zsmul_mem_Ioc hp a b

Result:
no goals
-- Mathlib/Analysis/Calculus/ContDiff/Basic.lean
theorem contDiff_succ_iff_deriv :
    ContDiff 𝕜 (n + 1) f₂ ↔ Differentiable 𝕜 f₂ ∧ (n = ω → AnalyticOn 𝕜 f₂ univ) ∧
      ContDiff 𝕜 n (deriv f₂)

Proof state:
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
n : WithTop ℕ∞
f₂ : 𝕜 → F
⊢ ContDiff 𝕜 (n + 1) f₂ ↔ Differentiable 𝕜 f₂ ∧ (n = ω → AnalyticOn 𝕜 f₂ univ) ∧ ContDiff 𝕜 n (deriv f₂)

Tactic:
simp only [← contDiffOn_univ, contDiffOn_succ_iff_deriv_of_isOpen, isOpen_univ,
  differentiableOn_univ]

Result:
no goals
-- Mathlib/Data/List/Infix.lean
theorem IsSuffix.flatten {l₁ l₂ : List (List α)} (h : l₁ <:+ l₂) :
    l₁.flatten <:+ l₂.flatten

Proof state:
α : Type u_1
l₁ l₂ : List (List α)
h : l₁ <:+ l₂
⊢ l₁.flatten <:+ l₂.flatten

Tactic:
rcases h with ⟨l, rfl⟩

Result:
case intro
α : Type u_1
l₁ l : List (List α)
⊢ l₁.flatten <:+ (l ++ l₁).flatten

Proof state:
case intro
α : Type u_1
l₁ l : List (List α)
⊢ l₁.flatten <:+ (l ++ l₁).flatten

Tactic:
simp

Result:
no goals
-- Mathlib/Algebra/Group/Int/Units.lean
lemma mul_eq_one_iff_eq_one_or_neg_one : u * v = 1 ↔ u = 1 ∧ v = 1 ∨ u = -1 ∧ v = -1

Proof state:
u v : ℤ
⊢ u * v = 1 ↔ u = 1 ∧ v = 1 ∨ u = -1 ∧ v = -1

Tactic:
refine ⟨eq_one_or_neg_one_of_mul_eq_one', fun h ↦ Or.elim h (fun H ↦ ?_) fun H ↦ ?_⟩ <;>
  obtain ⟨rfl, rfl⟩ := H <;> rfl

Result:
no goals
-- Mathlib/Analysis/Analytic/CPolynomialDef.lean
/-- If `p` is a formal multilinear series such that `p m = 0` for `n ≤ m`, then
`p.changeOriginSeriesTerm k l = 0` for `n ≤ k + l`. -/
lemma changeOriginSeriesTerm_bound (p : FormalMultilinearSeries 𝕜 E F) {n : ℕ}
    (hn : ∀ (m : ℕ), n ≤ m → p m = 0) (k l : ℕ) {s : Finset (Fin (k + l))}
    (hs : s.card = l) (hkl : n ≤ k + l) :
    p.changeOriginSeriesTerm k l s hs = 0

Proof state:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
n : ℕ
hn : ∀ (m : ℕ), n ≤ m → p m = 0
k l : ℕ
s : Finset (Fin (k + l))
hs : s.card = l
hkl : n ≤ k + l
⊢ p.changeOriginSeriesTerm k l s hs = 0

Tactic:
rw [changeOriginSeriesTerm, hn _ hkl, map_zero]

Result:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
n : ℕ
hn : ∀ (m : ℕ), n ≤ m → p m = 0
k l : ℕ
s : Finset (Fin (k + l))
hs : s.card = l
hkl : n ≤ k + l
⊢ ZeroHomClass
    (ContinuousMultilinearMap 𝕜 (fun i => E) F ≃ₗᵢ[𝕜]
      ContinuousMultilinearMap 𝕜 (fun i => E) (ContinuousMultilinearMap 𝕜 (fun i => E) F))
    (ContinuousMultilinearMap 𝕜 (fun i => E) F)
    (ContinuousMultilinearMap 𝕜 (fun i => E) (ContinuousMultilinearMap 𝕜 (fun i => E) F))
-- Mathlib/LinearAlgebra/Dimension/Constructions.lean
theorem rank_fun {M η : Type u} [Fintype η] [AddCommMonoid M] [Module R M] [Module.Free R M] :
    Module.rank R (η → M) = Fintype.card η * Module.rank R M

Proof state:
R : Type u
inst✝⁵ : Semiring R
inst✝⁴ : StrongRankCondition R
M η : Type u
inst✝³ : Fintype η
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Free R M
⊢ Module.rank R (η → M) = ↑(Fintype.card η) * Module.rank R M

Tactic:
rw [rank_pi, Cardinal.sum_const', Cardinal.mk_fintype]

Result:
no goals
-- Mathlib/RingTheory/Ideal/Maps.lean
theorem mem_annihilator {r} : r ∈ N.annihilator ↔ ∀ n ∈ N, r • n = (0 : M)

Proof state:
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
N : Submodule R M
r : R
⊢ (∀ (a : M) (b : a ∈ N), ↑(r • ⟨a, b⟩) = ↑0) ↔ ∀ n ∈ N, r • n = 0

Tactic:
rfl

Result:
no goals

Proof state:
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
N : Submodule R M
r : R
⊢ r ∈ N.annihilator ↔ ∀ n ∈ N, r • n = 0

Tactic:
simp_rw [annihilator, Module.mem_annihilator, Subtype.forall, Subtype.ext_iff]

Result:
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
N : Submodule R M
r : R
⊢ (∀ (a : M) (b : a ∈ N), ↑(r • ⟨a, b⟩) = ↑0) ↔ ∀ n ∈ N, r • n = 0
-- Mathlib/Order/Minimal.lean
theorem maximal_eq_iff : Maximal (· = y) x ↔ x = y

Proof state:
α : Type u_1
x y : α
inst✝ : LE α
⊢ Maximal (fun x => x = y) x ↔ x = y

Tactic:
simp (config := {contextual := true}) [Maximal]

Result:
no goals