harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/MapIdx.lean
theorem mapIdx_eq_mkArray_iff {l : Array α} {f : Nat → α → β} {b : β} :
    mapIdx f l = mkArray l.size b ↔ ∀ (i : Nat) (h : i < l.size), f i l[i] = b

Proof state:
case mk
α : Type u_1
β : Type u_2
f : Nat → α → β
b : β
l : List α
⊢ (mapIdx f { toList := l }).toList = (mkArray { toList := l }.size b).toList ↔
    ∀ (i : Nat) (h : i < { toList := l }.size), f i { toList := l }[i] = b

Tactic:
simp [List.mapIdx_eq_replicate_iff]

Result:
no goals

Proof state:
case mk
α : Type u_1
β : Type u_2
f : Nat → α → β
b : β
l : List α
⊢ mapIdx f { toList := l } = mkArray { toList := l }.size b ↔
    ∀ (i : Nat) (h : i < { toList := l }.size), f i { toList := l }[i] = b

Tactic:
rw [← toList_inj]

Result:
case mk
α : Type u_1
β : Type u_2
f : Nat → α → β
b : β
l : List α
⊢ (mapIdx f { toList := l }).toList = (mkArray { toList := l }.size b).toList ↔
    ∀ (i : Nat) (h : i < { toList := l }.size), f i { toList := l }[i] = b

Proof state:
α : Type u_1
β : Type u_2
l : Array α
f : Nat → α → β
b : β
⊢ mapIdx f l = mkArray l.size b ↔ ∀ (i : Nat) (h : i < l.size), f i l[i] = b

Tactic:
rcases l with ⟨l⟩

Result:
case mk
α : Type u_1
β : Type u_2
f : Nat → α → β
b : β
l : List α
⊢ mapIdx f { toList := l } = mkArray { toList := l }.size b ↔
    ∀ (i : Nat) (h : i < { toList := l }.size), f i { toList := l }[i] = b
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Bitblast.lean
theorem getLsbD_udiv (n d : BitVec w) (hy : 0#w < d)  (i : Nat) :
    (n / d).getLsbD i = (decide (i < w) && (divRec w {n, d} (DivModState.init w)).q.getLsbD i)

Proof state:
case neg
w : Nat
n d : BitVec w
hy : 0#w < d
i : Nat
hi : ¬i < w
⊢ (n / d).getLsbD i = (decide (i < w) && (divRec w { n := n, d := d } (DivModState.init w)).q.getLsbD i)

Tactic:
simp_all

Result:
no goals

Proof state:
case pos
w : Nat
n d : BitVec w
hy : 0#w < d
i : Nat
hi : i < w
⊢ (n / d).getLsbD i = (decide (i < w) && (divRec w { n := n, d := d } (DivModState.init w)).q.getLsbD i)

Tactic:
simp [udiv_eq_divRec (by assumption)]

Result:
case pos
w : Nat
n d : BitVec w
hy : 0#w < d
i : Nat
hi : i < w
⊢ (divRec w { n := n, d := d } (DivModState.init w)).q.getLsbD i = true → i < w

Proof state:
w : Nat
n d : BitVec w
hy : 0#w < d
i : Nat
hi : i < w
⊢ 0#?m.77374 < ?m.77375

Tactic:
assumption

Result:
no goals

Proof state:
w : Nat
n d : BitVec w
hy : 0#w < d
i : Nat
⊢ (n / d).getLsbD i = (decide (i < w) && (divRec w { n := n, d := d } (DivModState.init w)).q.getLsbD i)

Tactic:
by_cases hi : i < w

Result:
case pos
w : Nat
n d : BitVec w
hy : 0#w < d
i : Nat
hi : i < w
⊢ (n / d).getLsbD i = (decide (i < w) && (divRec w { n := n, d := d } (DivModState.init w)).q.getLsbD i)

case neg
w : Nat
n d : BitVec w
hy : 0#w < d
i : Nat
hi : ¬i < w
⊢ (n / d).getLsbD i = (decide (i < w) && (divRec w { n := n, d := d } (DivModState.init w)).q.getLsbD i)

Proof state:
case pos
w : Nat
n d : BitVec w
hy : 0#w < d
i : Nat
hi : i < w
⊢ (divRec w { n := n, d := d } (DivModState.init w)).q.getLsbD i = true → i < w

Tactic:
omega

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Lemmas.lean
theorem swap_swap (a : Vector α n) {i j : Nat} {hi hj} :
    (a.swap i j hi hj).swap i j hi hj = a

Proof state:
case mk
α : Type u_1
n i j : Nat
hi : i < n
hj : j < n
toArray✝ : Array α
size_toArray✝ : toArray✝.size = n
⊢ ({ toArray := toArray✝, size_toArray := size_toArray✝ }.swap i j hi hj).swap i j hi hj =
    { toArray := toArray✝, size_toArray := size_toArray✝ }

Tactic:
simp_all [Array.swap_swap]

Result:
no goals

Proof state:
α : Type u_1
n : Nat
a : Vector α n
i j : Nat
hi : i < n
hj : j < n
⊢ (a.swap i j hi hj).swap i j hi hj = a

Tactic:
cases a

Result:
case mk
α : Type u_1
n i j : Nat
hi : i < n
hj : j < n
toArray✝ : Array α
size_toArray✝ : toArray✝.size = n
⊢ ({ toArray := toArray✝, size_toArray := size_toArray✝ }.swap i j hi hj).swap i j hi hj =
    { toArray := toArray✝, size_toArray := size_toArray✝ }
-- Mathlib/Analysis/Seminorm.lean
theorem closedBall_eq_emptyset (p : Seminorm 𝕜 E) {x : E} {r : ℝ} (hr : r < 0) :
    p.closedBall x r = ∅

Proof state:
𝕜 : Type u_3
E : Type u_7
inst✝² : SeminormedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p : Seminorm 𝕜 E
x : E
r : ℝ
hr : r < 0
⊢ p.closedBall x r = ∅

Tactic:
ext

Result:
case h
𝕜 : Type u_3
E : Type u_7
inst✝² : SeminormedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p : Seminorm 𝕜 E
x : E
r : ℝ
hr : r < 0
x✝ : E
⊢ x✝ ∈ p.closedBall x r ↔ x✝ ∈ ∅

Proof state:
case h
𝕜 : Type u_3
E : Type u_7
inst✝² : SeminormedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p : Seminorm 𝕜 E
x : E
r : ℝ
hr : r < 0
x✝ : E
⊢ r < p (x✝ - x)

Tactic:
exact hr.trans_le (apply_nonneg _ _)

Result:
no goals

Proof state:
case h
𝕜 : Type u_3
E : Type u_7
inst✝² : SeminormedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p : Seminorm 𝕜 E
x : E
r : ℝ
hr : r < 0
x✝ : E
⊢ x✝ ∈ p.closedBall x r ↔ x✝ ∈ ∅

Tactic:
rw [Seminorm.mem_closedBall, Set.mem_empty_iff_false, iff_false, not_le]

Result:
case h
𝕜 : Type u_3
E : Type u_7
inst✝² : SeminormedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p : Seminorm 𝕜 E
x : E
r : ℝ
hr : r < 0
x✝ : E
⊢ r < p (x✝ - x)
-- Mathlib/Analysis/Calculus/ContDiff/FiniteDimension.lean
theorem contDiff_succ_iff_fderiv_apply [FiniteDimensional 𝕜 D] :
    ContDiff 𝕜 (n + 1) f ↔ Differentiable 𝕜 f ∧
      (n = ω → AnalyticOnNhd 𝕜 f Set.univ) ∧ ∀ y, ContDiff 𝕜 n fun x => fderiv 𝕜 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
n : WithTop ℕ∞
f : D → E
inst✝¹ : CompleteSpace 𝕜
inst✝ : FiniteDimensional 𝕜 D
⊢ ContDiff 𝕜 (n + 1) f ↔
    Differentiable 𝕜 f ∧ (n = ω → AnalyticOnNhd 𝕜 f Set.univ) ∧ ∀ (y : D), ContDiff 𝕜 n fun x => (fderiv 𝕜 f x) y

Tactic:
rw [contDiff_succ_iff_fderiv, contDiff_clm_apply_iff]

Result:
no goals
-- Mathlib/FieldTheory/IntermediateField/Adjoin/Defs.lean
theorem extendScalars_adjoin {K : IntermediateField F E} {S : Set E} (h : K ≤ adjoin F S) :
    extendScalars h = adjoin K S := restrictScalars_injective F <| by
  rw [extendScalars_restrictScalars, restrictScalars_adjoin]
  exact le_antisymm (adjoin.mono F S _ Set.subset_union_right) <| adjoin_le_iff.2 <|
    Set.union_subset h (subset_adjoin F S)

Proof state:
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
K : IntermediateField F E
S : Set E
h : K ≤ adjoin F S
⊢ restrictScalars F (extendScalars h) = restrictScalars F (adjoin (↥K) S)

Tactic:
rw [extendScalars_restrictScalars, restrictScalars_adjoin]

Result:
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
K : IntermediateField F E
S : Set E
h : K ≤ adjoin F S
⊢ adjoin F S = adjoin F (↑K ∪ S)

Proof state:
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
K : IntermediateField F E
S : Set E
h : K ≤ adjoin F S
⊢ adjoin F S = adjoin F (↑K ∪ S)

Tactic:
exact le_antisymm (adjoin.mono F S _ Set.subset_union_right) <| adjoin_le_iff.2 <|
  Set.union_subset h (subset_adjoin F S)

Result:
no goals
-- Mathlib/MeasureTheory/Constructions/Cylinders.lean
theorem union_cylinder (s₁ s₂ : Finset ι) (S₁ : Set (∀ i : s₁, α i)) (S₂ : Set (∀ i : s₂, α i))
    [DecidableEq ι] :
    cylinder s₁ S₁ ∪ cylinder s₂ S₂ =
      cylinder (s₁ ∪ s₂)
        (Finset.restrict₂ Finset.subset_union_left ⁻¹' S₁ ∪
          Finset.restrict₂ Finset.subset_union_right ⁻¹' S₂)

Proof state:
ι : Type u_1
α : ι → Type u_2
s₁ s₂ : Finset ι
S₁ : Set ((i : { x // x ∈ s₁ }) → α ↑i)
S₂ : Set ((i : { x // x ∈ s₂ }) → α ↑i)
inst✝ : DecidableEq ι
⊢ cylinder s₁ S₁ ∪ cylinder s₂ S₂ = cylinder (s₁ ∪ s₂) (Finset.restrict₂ ⋯ ⁻¹' S₁ ∪ Finset.restrict₂ ⋯ ⁻¹' S₂)

Tactic:
ext1 f

Result:
case h
ι : Type u_1
α : ι → Type u_2
s₁ s₂ : Finset ι
S₁ : Set ((i : { x // x ∈ s₁ }) → α ↑i)
S₂ : Set ((i : { x // x ∈ s₂ }) → α ↑i)
inst✝ : DecidableEq ι
f : (i : ι) → α i
⊢ f ∈ cylinder s₁ S₁ ∪ cylinder s₂ S₂ ↔ f ∈ cylinder (s₁ ∪ s₂) (Finset.restrict₂ ⋯ ⁻¹' S₁ ∪ Finset.restrict₂ ⋯ ⁻¹' S₂)

Proof state:
case h
ι : Type u_1
α : ι → Type u_2
s₁ s₂ : Finset ι
S₁ : Set ((i : { x // x ∈ s₁ }) → α ↑i)
S₂ : Set ((i : { x // x ∈ s₂ }) → α ↑i)
inst✝ : DecidableEq ι
f : (i : ι) → α i
⊢ s₁.restrict f ∈ S₁ ∨ s₂.restrict f ∈ S₂ ↔
    (s₁ ∪ s₂).restrict f ∈ Finset.restrict₂ ⋯ ⁻¹' S₁ ∨ (s₁ ∪ s₂).restrict f ∈ Finset.restrict₂ ⋯ ⁻¹' S₂

Tactic:
rfl

Result:
no goals

Proof state:
case h
ι : Type u_1
α : ι → Type u_2
s₁ s₂ : Finset ι
S₁ : Set ((i : { x // x ∈ s₁ }) → α ↑i)
S₂ : Set ((i : { x // x ∈ s₂ }) → α ↑i)
inst✝ : DecidableEq ι
f : (i : ι) → α i
⊢ f ∈ cylinder s₁ S₁ ∪ cylinder s₂ S₂ ↔ f ∈ cylinder (s₁ ∪ s₂) (Finset.restrict₂ ⋯ ⁻¹' S₁ ∪ Finset.restrict₂ ⋯ ⁻¹' S₂)

Tactic:
simp only [mem_union, mem_cylinder, mem_setOf_eq]

Result:
case h
ι : Type u_1
α : ι → Type u_2
s₁ s₂ : Finset ι
S₁ : Set ((i : { x // x ∈ s₁ }) → α ↑i)
S₂ : Set ((i : { x // x ∈ s₂ }) → α ↑i)
inst✝ : DecidableEq ι
f : (i : ι) → α i
⊢ s₁.restrict f ∈ S₁ ∨ s₂.restrict f ∈ S₂ ↔
    (s₁ ∪ s₂).restrict f ∈ Finset.restrict₂ ⋯ ⁻¹' S₁ ∨ (s₁ ∪ s₂).restrict f ∈ Finset.restrict₂ ⋯ ⁻¹' S₂
-- Mathlib/Combinatorics/SimpleGraph/Regularity/Equitabilise.lean
theorem exists_equipartition_card_eq (hn : n ≠ 0) (hs : n ≤ #s) :
    ∃ P : Finpartition s, P.IsEquipartition ∧ #P.parts = n

Proof state:
α : Type u_1
inst✝ : DecidableEq α
s : Finset α
n : ℕ
hn : 0 < n
hs : n ≤ #s
⊢ ∃ P, P.IsEquipartition ∧ #P.parts = n

Tactic:
have : (n - #s % n) * (#s / n) + #s % n * (#s / n + 1) = #s := by
  rw [tsub_mul, mul_add, ← add_assoc,
    tsub_add_cancel_of_le (Nat.mul_le_mul_right _ (mod_lt _ hn).le), mul_one, add_comm,
    mod_add_div]

Result:
α : Type u_1
inst✝ : DecidableEq α
s : Finset α
n : ℕ
hn : 0 < n
hs : n ≤ #s
this : (n - #s % n) * (#s / n) + #s % n * (#s / n + 1) = #s
⊢ ∃ P, P.IsEquipartition ∧ #P.parts = n

Proof state:
α : Type u_1
inst✝ : DecidableEq α
s : Finset α
n : ℕ
hn : 0 < n
hs : n ≤ #s
⊢ (n - #s % n) * (#s / n) + #s % n * (#s / n + 1) = #s

Tactic:
rw [tsub_mul, mul_add, ← add_assoc,
  tsub_add_cancel_of_le (Nat.mul_le_mul_right _ (mod_lt _ hn).le), mul_one, add_comm,
  mod_add_div]

Result:
no goals

Proof state:
α : Type u_1
inst✝ : DecidableEq α
s : Finset α
n : ℕ
hn : 0 < n
hs : n ≤ #s
this : (n - #s % n) * (#s / n) + #s % n * (#s / n + 1) = #s
⊢ ∃ P, P.IsEquipartition ∧ #P.parts = n

Tactic:
refine
  ⟨(indiscrete (card_pos.1 <| hn.trans_le hs).ne_empty).equitabilise this,
    equitabilise_isEquipartition, ?_⟩

Result:
α : Type u_1
inst✝ : DecidableEq α
s : Finset α
n : ℕ
hn : 0 < n
hs : n ≤ #s
this : (n - #s % n) * (#s / n) + #s % n * (#s / n + 1) = #s
⊢ #(equitabilise this).parts = n

Proof state:
α : Type u_1
inst✝ : DecidableEq α
s : Finset α
n : ℕ
hn : 0 < n
hs : n ≤ #s
this : (n - #s % n) * (#s / n) + #s % n * (#s / n + 1) = #s
⊢ #(equitabilise this).parts = n

Tactic:
rw [card_parts_equitabilise _ _ (Nat.div_pos hs hn).ne', tsub_add_cancel_of_le (mod_lt _ hn).le]

Result:
no goals

Proof state:
α : Type u_1
inst✝ : DecidableEq α
s : Finset α
n : ℕ
hn : n ≠ 0
hs : n ≤ #s
⊢ ∃ P, P.IsEquipartition ∧ #P.parts = n

Tactic:
rw [← pos_iff_ne_zero] at hn

Result:
α : Type u_1
inst✝ : DecidableEq α
s : Finset α
n : ℕ
hn : 0 < n
hs : n ≤ #s
⊢ ∃ P, P.IsEquipartition ∧ #P.parts = n
-- Mathlib/Analysis/Convex/Cone/Basic.lean
theorem Blunt.salient {S : ConvexCone 𝕜 E} : S.Blunt → S.Salient

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝² : OrderedSemiring 𝕜
inst✝¹ : AddCommGroup E
inst✝ : SMul 𝕜 E
S : ConvexCone 𝕜 E
⊢ ¬S.Pointed → ¬S.Flat

Tactic:
exact mt Flat.pointed

Result:
no goals

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝² : OrderedSemiring 𝕜
inst✝¹ : AddCommGroup E
inst✝ : SMul 𝕜 E
S : ConvexCone 𝕜 E
⊢ S.Blunt → S.Salient

Tactic:
rw [salient_iff_not_flat, blunt_iff_not_pointed]

Result:
𝕜 : Type u_1
E : Type u_2
inst✝² : OrderedSemiring 𝕜
inst✝¹ : AddCommGroup E
inst✝ : SMul 𝕜 E
S : ConvexCone 𝕜 E
⊢ ¬S.Pointed → ¬S.Flat
-- Mathlib/Data/Nat/Choose/Multinomial.lean
lemma multinomial_insert [DecidableEq α] (ha : a ∉ s) (f : α → ℕ) :
    multinomial (insert a s) f = (f a + ∑ i ∈ s, f i).choose (f a) * multinomial s f

Proof state:
α : Type u_1
s : Finset α
a : α
inst✝ : DecidableEq α
ha : a ∉ s
f : α → ℕ
⊢ multinomial (insert a s) f = (f a + ∑ i ∈ s, f i).choose (f a) * multinomial s f

Tactic:
rw [← cons_eq_insert _ _ ha, multinomial_cons]

Result:
no goals
-- Mathlib/Topology/Algebra/Algebra.lean
theorem coe_eq_id {f : A →A[R] A} :
    (f : A →ₐ[R] A) = AlgHom.id R A ↔ f = ContinuousAlgHom.id R A

Proof state:
R : Type u_1
inst✝³ : CommSemiring R
A : Type u_2
inst✝² : Semiring A
inst✝¹ : TopologicalSpace A
inst✝ : Algebra R A
f : A →A[R] A
⊢ ↑f = AlgHom.id R A ↔ f = ContinuousAlgHom.id R A

Tactic:
rw [← coe_id, coe_inj]

Result:
no goals
-- Mathlib/RingTheory/Flat/Equalizer.lean
@[simp]
lemma LinearMap.tensorKer_coe (x : M ⊗[R] (LinearMap.ker f)) :
    (tensorKer S M f x : M ⊗[R] N) = (ker f).subtype.lTensor M x

Proof state:
R : Type u_1
S : Type u_2
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing S
inst✝⁸ : Algebra R S
M : Type u_3
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : Module S M
inst✝⁴ : IsScalarTower R S M
N : Type u_4
P : Type u_5
inst✝³ : AddCommGroup N
inst✝² : AddCommGroup P
inst✝¹ : Module R N
inst✝ : Module R P
f : N →ₗ[R] P
x : M ⊗[R] ↥(ker f)
⊢ ↑((tensorKer S M f) x) = (lTensor M (ker f).subtype) x

Tactic:
induction x <;> simp_all

Result:
no goals
-- Mathlib/Algebra/Order/Ring/Unbundled/Basic.lean
lemma mul_self_nonneg [IsRightCancelAdd α]
    [ZeroLEOneClass α] [ExistsAddOfLE α] [PosMulMono α] [AddLeftStrictMono α]
    (a : α) : 0 ≤ a * a

Proof state:
α : Type u
inst✝⁶ : Semiring α
inst✝⁵ : LinearOrder α
inst✝⁴ : IsRightCancelAdd α
inst✝³ : ZeroLEOneClass α
inst✝² : ExistsAddOfLE α
inst✝¹ : PosMulMono α
inst✝ : AddLeftStrictMono α
a : α
⊢ 0 ≤ a * a

Tactic:
simpa only [sq] using sq_nonneg a

Result:
no goals
-- Mathlib/Analysis/Calculus/Deriv/Inv.lean
theorem HasDerivAt.inv (hc : HasDerivAt c c' x) (hx : c x ≠ 0) :
    HasDerivAt (fun y => (c y)⁻¹) (-c' / c x ^ 2) x

Proof state:
𝕜 : Type u
inst✝ : NontriviallyNormedField 𝕜
x : 𝕜
c : 𝕜 → 𝕜
c' : 𝕜
hc : HasDerivWithinAt c c' univ x
hx : c x ≠ 0
⊢ HasDerivWithinAt (fun y => (c y)⁻¹) (-c' / c x ^ 2) univ x

Tactic:
exact hc.inv hx

Result:
no goals

Proof state:
𝕜 : Type u
inst✝ : NontriviallyNormedField 𝕜
x : 𝕜
c : 𝕜 → 𝕜
c' : 𝕜
hc : HasDerivAt c c' x
hx : c x ≠ 0
⊢ HasDerivAt (fun y => (c y)⁻¹) (-c' / c x ^ 2) x

Tactic:
rw [← hasDerivWithinAt_univ] at *

Result:
𝕜 : Type u
inst✝ : NontriviallyNormedField 𝕜
x : 𝕜
c : 𝕜 → 𝕜
c' : 𝕜
hc : HasDerivWithinAt c c' univ x
hx : c x ≠ 0
⊢ HasDerivWithinAt (fun y => (c y)⁻¹) (-c' / c x ^ 2) univ x
-- Mathlib/Algebra/Group/Subsemigroup/Basic.lean
theorem mem_iInf {ι : Sort*} {S : ι → Subsemigroup M} {x : M} : (x ∈ ⨅ i, S i) ↔ ∀ i, x ∈ S i

Proof state:
M : Type u_1
inst✝ : Mul M
ι : Sort u_3
S : ι → Subsemigroup M
x : M
⊢ x ∈ ⨅ i, S i ↔ ∀ (i : ι), x ∈ S i

Tactic:
simp only [iInf, mem_sInf, Set.forall_mem_range]

Result:
no goals
-- Mathlib/Combinatorics/Additive/FreimanHom.lean
@[to_additive (attr := simp)]
lemma isMulFreimanHom_zero_iff : IsMulFreimanHom 0 A B f ↔ MapsTo f A B :=
  ⟨fun h => h.mapsTo, fun h => ⟨h, by aesop⟩⟩

Proof state:
α : Type u_2
β : Type u_3
inst✝¹ : CommMonoid α
inst✝ : CommMonoid β
A : Set α
B : Set β
f : α → β
h : MapsTo f A B
⊢ ∀ ⦃s t : Multiset α⦄,
    (∀ ⦃x : α⦄, x ∈ s → x ∈ A) →
      (∀ ⦃x : α⦄, x ∈ t → x ∈ A) → s.card = 0 → t.card = 0 → s.prod = t.prod → (map f s).prod = (map f t).prod

Tactic:
aesop

Result:
no goals
-- Mathlib/Algebra/Homology/HomologicalComplex.lean
@[reassoc (attr := simp)]
lemma XIsoOfEq_inv_comp_XIsoOfEq_inv (K : HomologicalComplex V c) {p₁ p₂ p₃ : ι}
    (h₂₁ : p₂ = p₁) (h₃₂ : p₃ = p₂) :
    (K.XIsoOfEq h₂₁).inv ≫ (K.XIsoOfEq h₃₂).inv = (K.XIsoOfEq (h₃₂.trans h₂₁).symm).hom

Proof state:
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
c : ComplexShape ι
K : HomologicalComplex V c
p₁ p₂ p₃ : ι
h₂₁ : p₂ = p₁
h₃₂ : p₃ = p₂
⊢ eqToHom ⋯ ≫ eqToHom ⋯ = eqToHom ⋯

Tactic:
simp only [eqToHom_trans]

Result:
no goals

Proof state:
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
c : ComplexShape ι
K : HomologicalComplex V c
p₁ p₂ p₃ : ι
h₂₁ : p₂ = p₁
h₃₂ : p₃ = p₂
⊢ (K.XIsoOfEq h₂₁).inv ≫ (K.XIsoOfEq h₃₂).inv = (K.XIsoOfEq ⋯).hom

Tactic:
dsimp [XIsoOfEq]

Result:
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
c : ComplexShape ι
K : HomologicalComplex V c
p₁ p₂ p₃ : ι
h₂₁ : p₂ = p₁
h₃₂ : p₃ = p₂
⊢ eqToHom ⋯ ≫ eqToHom ⋯ = eqToHom ⋯
-- Mathlib/Analysis/Normed/Lp/ProdLp.lean
theorem prod_nnnorm_eq_of_L2 (x : WithLp 2 (α × β)) :
    ‖x‖₊ = NNReal.sqrt (‖x.fst‖₊ ^ 2 + ‖x.snd‖₊ ^ 2) :=
  NNReal.eq <| by
    push_cast
    exact prod_norm_eq_of_L2 x

Proof state:
α : Type u_2
β : Type u_3
inst✝¹ : SeminormedAddCommGroup α
inst✝ : SeminormedAddCommGroup β
x : WithLp 2 (α × β)
⊢ ‖x‖ = √(‖x.1‖ ^ 2 + ‖x.2‖ ^ 2)

Tactic:
exact prod_norm_eq_of_L2 x

Result:
no goals

Proof state:
α : Type u_2
β : Type u_3
inst✝¹ : SeminormedAddCommGroup α
inst✝ : SeminormedAddCommGroup β
x : WithLp 2 (α × β)
⊢ ↑‖x‖₊ = ↑(NNReal.sqrt (‖x.1‖₊ ^ 2 + ‖x.2‖₊ ^ 2))

Tactic:
push_cast

Result:
α : Type u_2
β : Type u_3
inst✝¹ : SeminormedAddCommGroup α
inst✝ : SeminormedAddCommGroup β
x : WithLp 2 (α × β)
⊢ ‖x‖ = √(‖x.1‖ ^ 2 + ‖x.2‖ ^ 2)
-- Mathlib/FieldTheory/IntermediateField/Adjoin/Defs.lean
theorem lift_adjoin_simple (K : IntermediateField F E) (α : K) :
    lift (adjoin F {α}) = adjoin F {α.1}

Proof state:
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
K : IntermediateField F E
α : ↥K
⊢ lift (adjoin F {α}) = adjoin F {↑α}

Tactic:
simp only [lift_adjoin, Set.image_singleton]

Result:
no goals
-- Mathlib/Algebra/Algebra/Operations.lean
theorem bot_smul : (⊥ : Submodule R A) • N = ⊥ :=
  le_bot_iff.mp <| smul_le.mpr <| by rintro _ rfl _ _; rw [zero_smul]; exact zero_mem _

Proof state:
R : Type u
inst✝⁶ : Semiring R
A : Type v
inst✝⁵ : Semiring A
inst✝⁴ : Module R A
M : Type u_1
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : Module A M
inst✝ : IsScalarTower R A M
N : Submodule R M
n✝ : M
a✝ : n✝ ∈ N
⊢ 0 • n✝ ∈ ⊥

Tactic:
rw [zero_smul]

Result:
R : Type u
inst✝⁶ : Semiring R
A : Type v
inst✝⁵ : Semiring A
inst✝⁴ : Module R A
M : Type u_1
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : Module A M
inst✝ : IsScalarTower R A M
N : Submodule R M
n✝ : M
a✝ : n✝ ∈ N
⊢ 0 ∈ ⊥

Proof state:
R : Type u
inst✝⁶ : Semiring R
A : Type v
inst✝⁵ : Semiring A
inst✝⁴ : Module R A
M : Type u_1
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : Module A M
inst✝ : IsScalarTower R A M
N : Submodule R M
⊢ ∀ r ∈ ⊥, ∀ n ∈ N, r • n ∈ ⊥

Tactic:
rintro _ rfl _ _

Result:
R : Type u
inst✝⁶ : Semiring R
A : Type v
inst✝⁵ : Semiring A
inst✝⁴ : Module R A
M : Type u_1
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : Module A M
inst✝ : IsScalarTower R A M
N : Submodule R M
n✝ : M
a✝ : n✝ ∈ N
⊢ 0 • n✝ ∈ ⊥

Proof state:
R : Type u
inst✝⁶ : Semiring R
A : Type v
inst✝⁵ : Semiring A
inst✝⁴ : Module R A
M : Type u_1
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : Module A M
inst✝ : IsScalarTower R A M
N : Submodule R M
n✝ : M
a✝ : n✝ ∈ N
⊢ 0 ∈ ⊥

Tactic:
exact zero_mem _

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/RawLemmas.lean
theorem getKey?_modify [LawfulBEq α] {k k' : α} {f : β k → β k} (h : m.WF) :
    (m.modify k f).getKey? k' =
      if k == k' then
        if k ∈ m then some k else none
      else
        m.getKey? k'

Proof state:
α : Type u
β : α → Type v
inst✝² : BEq α
inst✝¹ : Hashable α
m : Raw α β
inst✝ : LawfulBEq α
k k' : α
f : β k → β k
h : m.WF
⊢ (m.modify k f).getKey? k' = if (k == k') = true then if m.contains k = true then some k else none else m.getKey? k'

Tactic:
simp_to_raw using Raw₀.getKey?_modify

Result:
no goals

Proof state:
α : Type u
β : α → Type v
inst✝² : BEq α
inst✝¹ : Hashable α
m : Raw α β
inst✝ : LawfulBEq α
k k' : α
f : β k → β k
h : m.WF
⊢ (m.modify k f).getKey? k' = if (k == k') = true then if k ∈ m then some k else none else m.getKey? k'

Tactic:
simp only [mem_iff_contains]

Result:
α : Type u
β : α → Type v
inst✝² : BEq α
inst✝¹ : Hashable α
m : Raw α β
inst✝ : LawfulBEq α
k k' : α
f : β k → β k
h : m.WF
⊢ (m.modify k f).getKey? k' = if (k == k') = true then if m.contains k = true then some k else none else m.getKey? k'
-- Mathlib/CategoryTheory/Quotient.lean
theorem comp_left {a b c : C} (f : a ⟶ b) :
    ∀ (g₁ g₂ : b ⟶ c) (_ : CompClosure r g₁ g₂), CompClosure r (f ≫ g₁) (f ≫ g₂)
  | _, _, ⟨x, m₁, m₂, y, h⟩ => by simpa using CompClosure.intro (f ≫ x) m₁ m₂ y h

Proof state:
C : Type u_2
inst✝ : Category.{u_1, u_2} C
r : HomRel C
a b c : C
f : a ⟶ b
a✝ b✝ : C
x : b ⟶ a✝
m₁ m₂ : a✝ ⟶ b✝
y : b✝ ⟶ c
h : r m₁ m₂
⊢ CompClosure r (f ≫ x ≫ m₁ ≫ y) (f ≫ x ≫ m₂ ≫ y)

Tactic:
simpa using CompClosure.intro (f ≫ x) m₁ m₂ y h

Result:
no goals
-- Mathlib/RingTheory/Ideal/Maps.lean
lemma Module.annihilator_eq_bot {R M} [Ring R] [AddCommGroup M] [Module R M] :
    Module.annihilator R M = ⊥ ↔ FaithfulSMul R M

Proof state:
R : Type u_4
M : Type u_5
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
⊢ annihilator R M ≤ ⊥ ↔ FaithfulSMul R M

Tactic:
refine ⟨fun H ↦ ⟨fun {r s} H' ↦ ?_⟩, fun ⟨H⟩ {a} ha ↦ ?_⟩

Result:
case refine_1
R : Type u_4
M : Type u_5
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
H : annihilator R M ≤ ⊥
r s : R
H' : ∀ (a : M), r • a = s • a
⊢ r = s

case refine_2
R : Type u_4
M : Type u_5
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x✝ : FaithfulSMul R M
a : R
ha : a ∈ annihilator R M
H : ∀ {m₁ m₂ : R}, (∀ (a : M), m₁ • a = m₂ • a) → m₁ = m₂
⊢ a ∈ ⊥

Proof state:
R : Type u_4
M : Type u_5
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x✝ : FaithfulSMul R M
a : R
ha : a ∈ annihilator R M
H : ∀ {m₁ m₂ : R}, (∀ (a : M), m₁ • a = m₂ • a) → m₁ = m₂
⊢ ∀ (a_1 : M), a • a_1 = 0 • a_1

Tactic:
simp [Module.mem_annihilator.mp ha]

Result:
no goals

Proof state:
R : Type u_4
M : Type u_5
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
⊢ annihilator R M = ⊥ ↔ FaithfulSMul R M

Tactic:
rw [← le_bot_iff]

Result:
R : Type u_4
M : Type u_5
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
⊢ annihilator R M ≤ ⊥ ↔ FaithfulSMul R M

Proof state:
case refine_1
R : Type u_4
M : Type u_5
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
H : annihilator R M ≤ ⊥
r s : R
H' : ∀ (a : M), r • a = s • a
⊢ r = s

Tactic:
rw [← sub_eq_zero]

Result:
case refine_1
R : Type u_4
M : Type u_5
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
H : annihilator R M ≤ ⊥
r s : R
H' : ∀ (a : M), r • a = s • a
⊢ r - s = 0

Proof state:
case refine_1
R : Type u_4
M : Type u_5
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
H : annihilator R M ≤ ⊥
r s : R
H' : ∀ (a : M), r • a = s • a
⊢ r - s = 0

Tactic:
exact H (Module.mem_annihilator (r := r - s).mpr
  (by simp only [sub_smul, H', sub_self, implies_true]))

Result:
no goals

Proof state:
R : Type u_4
M : Type u_5
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
H : annihilator R M ≤ ⊥
r s : R
H' : ∀ (a : M), r • a = s • a
⊢ ∀ (m : M), (r - s) • m = 0

Tactic:
simp only [sub_smul, H', sub_self, implies_true]

Result:
no goals

Proof state:
case refine_2
R : Type u_4
M : Type u_5
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x✝ : FaithfulSMul R M
a : R
ha : a ∈ annihilator R M
H : ∀ {m₁ m₂ : R}, (∀ (a : M), m₁ • a = m₂ • a) → m₁ = m₂
⊢ a ∈ ⊥

Tactic:
exact @H a 0 (by simp [Module.mem_annihilator.mp ha])

Result:
no goals
-- Mathlib/Algebra/Divisibility/Prod.lean
theorem pi_dvd_iff {x y : ∀ i, G i} : x ∣ y ↔ ∀ i, x i ∣ y i

Proof state:
ι : Type u_1
G : ι → Type u_4
inst✝ : (i : ι) → Semigroup (G i)
x y : (i : ι) → G i
⊢ (∃ c, ∀ (x_1 : ι), y x_1 = (x * c) x_1) ↔ ∃ f, ∀ (x_1 : ι), y x_1 = x x_1 * f x_1

Tactic:
rfl

Result:
no goals

Proof state:
ι : Type u_1
G : ι → Type u_4
inst✝ : (i : ι) → Semigroup (G i)
x y : (i : ι) → G i
⊢ x ∣ y ↔ ∀ (i : ι), x i ∣ y i

Tactic:
simp_rw [dvd_def, funext_iff, Classical.skolem]

Result:
ι : Type u_1
G : ι → Type u_4
inst✝ : (i : ι) → Semigroup (G i)
x y : (i : ι) → G i
⊢ (∃ c, ∀ (x_1 : ι), y x_1 = (x * c) x_1) ↔ ∃ f, ∀ (x_1 : ι), y x_1 = x x_1 * f x_1