harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/RingTheory/UniqueFactorizationDomain/Basic.lean
theorem of_existsUnique_irreducible_factors [CancelCommMonoidWithZero α]
    (eif : ∀ a : α, a ≠ 0 → ∃ f : Multiset α, (∀ b ∈ f, Irreducible b) ∧ f.prod ~ᵤ a)
    (uif :
      ∀ f g : Multiset α,
        (∀ x ∈ f, Irreducible x) →
          (∀ x ∈ g, Irreducible x) → f.prod ~ᵤ g.prod → Multiset.Rel Associated f g) :
    UniqueFactorizationMonoid α :=
  UniqueFactorizationMonoid.of_exists_prime_factors
    (by
      convert eif using 7
      simp_rw [irreducible_iff_prime_of_existsUnique_irreducible_factors eif uif])

Proof state:
case h.h'.h.e'_2.h.h.e'_1.h.h'.a
α : Type u_1
inst✝ : CancelCommMonoidWithZero α
eif : ∀ (a : α), a ≠ 0 → ∃ f, (∀ b ∈ f, Irreducible b) ∧ f.prod ~ᵤ a
uif :
  ∀ (f g : Multiset α),
    (∀ x ∈ f, Irreducible x) → (∀ x ∈ g, Irreducible x) → f.prod ~ᵤ g.prod → Multiset.Rel Associated f g
a✝³ : α
a✝² : a✝³ ≠ 0
x✝ : Multiset α
a✝¹ : α
a✝ : a✝¹ ∈ x✝
⊢ Prime a✝¹ ↔ Irreducible a✝¹

Tactic:
simp_rw [irreducible_iff_prime_of_existsUnique_irreducible_factors eif uif]

Result:
no goals

Proof state:
α : Type u_1
inst✝ : CancelCommMonoidWithZero α
eif : ∀ (a : α), a ≠ 0 → ∃ f, (∀ b ∈ f, Irreducible b) ∧ f.prod ~ᵤ a
uif :
  ∀ (f g : Multiset α),
    (∀ x ∈ f, Irreducible x) → (∀ x ∈ g, Irreducible x) → f.prod ~ᵤ g.prod → Multiset.Rel Associated f g
⊢ ∀ (a : α), a ≠ 0 → ∃ f, (∀ b ∈ f, Prime b) ∧ f.prod ~ᵤ a

Tactic:
convert eif using 7

Result:
case h.h'.h.e'_2.h.h.e'_1.h.h'.a
α : Type u_1
inst✝ : CancelCommMonoidWithZero α
eif : ∀ (a : α), a ≠ 0 → ∃ f, (∀ b ∈ f, Irreducible b) ∧ f.prod ~ᵤ a
uif :
  ∀ (f g : Multiset α),
    (∀ x ∈ f, Irreducible x) → (∀ x ∈ g, Irreducible x) → f.prod ~ᵤ g.prod → Multiset.Rel Associated f g
a✝³ : α
a✝² : a✝³ ≠ 0
x✝ : Multiset α
a✝¹ : α
a✝ : a✝¹ ∈ x✝
⊢ Prime a✝¹ ↔ Irreducible a✝¹
-- Mathlib/Algebra/Order/ToIntervalMod.lean
theorem toIcoDiv_apply_right (a : α) : toIcoDiv hp a (a + p) = 1 :=
  toIcoDiv_eq_of_sub_zsmul_mem_Ico hp <| by simp [hp]

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

Tactic:
simp [hp]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Trigonometric/Bounds.lean
/-- Half of **Jordan's inequality** for `cos`. -/
lemma one_sub_mul_le_cos (hx₀ : 0 ≤ x) (hx : x ≤ π / 2) : 1 - 2 / π * x ≤ cos x

Proof state:
x : ℝ
hx₀ : 0 ≤ x
hx : x ≤ π / 2
⊢ 0 ≤ π / 2 - x

Tactic:
simpa

Result:
no goals

Proof state:
x : ℝ
hx₀ : 0 ≤ x
hx : x ≤ π / 2
⊢ 1 - 2 / π * x ≤ cos x

Tactic:
simpa [sin_pi_div_two_sub, mul_sub, div_mul_div_comm, mul_comm π, pi_pos.ne']
  using mul_le_sin (x := π / 2 - x) (by simpa) (by simpa)

Result:
no goals

Proof state:
x : ℝ
hx₀ : 0 ≤ x
hx : x ≤ π / 2
⊢ π / 2 - x ≤ π / 2

Tactic:
simpa

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Attach.lean
theorem foldr_attachWith
    (l : Array α) {q : α → Prop} (H : ∀ a, a ∈ l → q a) {f : { x // q x} → β → β} {b} (w : start = l.size) :
    (l.attachWith q H).foldr f b start 0 = l.attach.foldr (fun a acc => f ⟨a.1, H _ a.2⟩ acc) b

Proof state:
α : Type u_1
β : Type u_2
l : Array α
q : α → Prop
H : ∀ (a : α), a ∈ l → q a
f : { x // q x } → β → β
b : β
⊢ foldr f b (l.attachWith q H) l.size = foldr (fun a acc => f ⟨a.val, ⋯⟩ acc) b l.attach

Tactic:
rcases l with ⟨l⟩

Result:
case mk
α : Type u_1
β : Type u_2
q : α → Prop
f : { x // q x } → β → β
b : β
l : List α
H : ∀ (a : α), a ∈ { toList := l } → q a
⊢ foldr f b ({ toList := l }.attachWith q H) { toList := l }.size =
    foldr (fun a acc => f ⟨a.val, ⋯⟩ acc) b { toList := l }.attach

Proof state:
α : Type u_1
β : Type u_2
start : Nat
l : Array α
q : α → Prop
H : ∀ (a : α), a ∈ l → q a
f : { x // q x } → β → β
b : β
w : start = l.size
⊢ foldr f b (l.attachWith q H) start = foldr (fun a acc => f ⟨a.val, ⋯⟩ acc) b l.attach

Tactic:
subst w

Result:
α : Type u_1
β : Type u_2
l : Array α
q : α → Prop
H : ∀ (a : α), a ∈ l → q a
f : { x // q x } → β → β
b : β
⊢ foldr f b (l.attachWith q H) l.size = foldr (fun a acc => f ⟨a.val, ⋯⟩ acc) b l.attach

Proof state:
case mk
α : Type u_1
β : Type u_2
q : α → Prop
f : { x // q x } → β → β
b : β
l : List α
H : ∀ (a : α), a ∈ { toList := l } → q a
⊢ foldr f b ({ toList := l }.attachWith q H) { toList := l }.size =
    foldr (fun a acc => f ⟨a.val, ⋯⟩ acc) b { toList := l }.attach

Tactic:
simp [List.foldr_attachWith, List.foldr_map]

Result:
no goals
-- Mathlib/MeasureTheory/Function/L1Space/HasFiniteIntegral.lean
theorem hasFiniteIntegral_iff_norm (f : α → β) :
    HasFiniteIntegral f μ ↔ (∫⁻ a, ENNReal.ofReal ‖f a‖ ∂μ) < ∞

Proof state:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
f : α → β
⊢ HasFiniteIntegral f μ ↔ ∫⁻ (a : α), ENNReal.ofReal ‖f a‖ ∂μ < ⊤

Tactic:
simp only [hasFiniteIntegral_iff_enorm, ofReal_norm_eq_enorm]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Lemmas.lean
theorem head_tail (l : List α) (h : l.tail ≠ []) :
    (tail l).head h = l[1]'(one_lt_length_of_tail_ne_nil h)

Proof state:
case cons
α : Type u_1
head✝ : α
l : List α
h : (head✝ :: l).tail ≠ []
⊢ (head✝ :: l).tail.head h = (head✝ :: l)[1]

Tactic:
simp [head_eq_getElem]

Result:
no goals

Proof state:
α : Type u_1
l : List α
h : l.tail ≠ []
⊢ l.tail.head h = l[1]

Tactic:
cases l with
| nil => simp at h
| cons _ l => simp [head_eq_getElem]

Result:
no goals

Proof state:
case nil
α : Type u_1
h : [].tail ≠ []
⊢ [].tail.head h = [][1]

Tactic:
simp at h

Result:
no goals
-- Mathlib/Topology/Constructions.lean
theorem IsOpenMap.prodMap {f : X → Y} {g : Z → W} (hf : IsOpenMap f) (hg : IsOpenMap g) :
    IsOpenMap (Prod.map f g)

Proof state:
X : Type u
Y : Type v
Z : Type u_1
W : Type u_2
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : TopologicalSpace Z
inst✝ : TopologicalSpace W
f : X → Y
g : Z → W
hf : IsOpenMap f
hg : IsOpenMap g
⊢ IsOpenMap (Prod.map f g)

Tactic:
rw [isOpenMap_iff_nhds_le]

Result:
X : Type u
Y : Type v
Z : Type u_1
W : Type u_2
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : TopologicalSpace Z
inst✝ : TopologicalSpace W
f : X → Y
g : Z → W
hf : IsOpenMap f
hg : IsOpenMap g
⊢ ∀ (x : X × Z), 𝓝 (Prod.map f g x) ≤ map (Prod.map f g) (𝓝 x)

Proof state:
X : Type u
Y : Type v
Z : Type u_1
W : Type u_2
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : TopologicalSpace Z
inst✝ : TopologicalSpace W
f : X → Y
g : Z → W
hf : IsOpenMap f
hg : IsOpenMap g
⊢ ∀ (x : X × Z), 𝓝 (Prod.map f g x) ≤ map (Prod.map f g) (𝓝 x)

Tactic:
rintro ⟨a, b⟩

Result:
case mk
X : Type u
Y : Type v
Z : Type u_1
W : Type u_2
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : TopologicalSpace Z
inst✝ : TopologicalSpace W
f : X → Y
g : Z → W
hf : IsOpenMap f
hg : IsOpenMap g
a : X
b : Z
⊢ 𝓝 (Prod.map f g (a, b)) ≤ map (Prod.map f g) (𝓝 (a, b))

Proof state:
case mk
X : Type u
Y : Type v
Z : Type u_1
W : Type u_2
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : TopologicalSpace Z
inst✝ : TopologicalSpace W
f : X → Y
g : Z → W
hf : IsOpenMap f
hg : IsOpenMap g
a : X
b : Z
⊢ 𝓝 (Prod.map f g (a, b)).1 ×ˢ 𝓝 (Prod.map f g (a, b)).2 ≤ map f (𝓝 a) ×ˢ map g (𝓝 b)

Tactic:
exact Filter.prod_mono (hf.nhds_le a) (hg.nhds_le b)

Result:
no goals

Proof state:
case mk
X : Type u
Y : Type v
Z : Type u_1
W : Type u_2
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : TopologicalSpace Z
inst✝ : TopologicalSpace W
f : X → Y
g : Z → W
hf : IsOpenMap f
hg : IsOpenMap g
a : X
b : Z
⊢ 𝓝 (Prod.map f g (a, b)) ≤ map (Prod.map f g) (𝓝 (a, b))

Tactic:
rw [nhds_prod_eq, nhds_prod_eq, ← Filter.prod_map_map_eq']

Result:
case mk
X : Type u
Y : Type v
Z : Type u_1
W : Type u_2
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : TopologicalSpace Z
inst✝ : TopologicalSpace W
f : X → Y
g : Z → W
hf : IsOpenMap f
hg : IsOpenMap g
a : X
b : Z
⊢ 𝓝 (Prod.map f g (a, b)).1 ×ˢ 𝓝 (Prod.map f g (a, b)).2 ≤ map f (𝓝 a) ×ˢ map g (𝓝 b)
-- Mathlib/RingTheory/Multiplicity.lean
theorem not_pow_dvd_of_emultiplicity_lt {m : ℕ} (hm : emultiplicity a b < m) :
    ¬a ^ m ∣ b := fun nh => by
  unfold emultiplicity at hm
  split at hm
  · simp only [cast_lt, find_lt_iff] at hm
    obtain ⟨n, hn1, hn2⟩ := hm
    exact hn2 ((pow_dvd_pow _ hn1).trans nh)
  · simp at hm

Proof state:
case isTrue
α : Type u_1
inst✝ : Monoid α
a b : α
m : ℕ
nh : a ^ m ∣ b
h✝ : FiniteMultiplicity a b
hm : ∃ m_1 < m, ¬a ^ (m_1 + 1) ∣ b
⊢ False

Tactic:
obtain ⟨n, hn1, hn2⟩ := hm

Result:
case isTrue.intro.intro
α : Type u_1
inst✝ : Monoid α
a b : α
m : ℕ
nh : a ^ m ∣ b
h✝ : FiniteMultiplicity a b
n : ℕ
hn1 : n < m
hn2 : ¬a ^ (n + 1) ∣ b
⊢ False

Proof state:
case isTrue.intro.intro
α : Type u_1
inst✝ : Monoid α
a b : α
m : ℕ
nh : a ^ m ∣ b
h✝ : FiniteMultiplicity a b
n : ℕ
hn1 : n < m
hn2 : ¬a ^ (n + 1) ∣ b
⊢ False

Tactic:
exact hn2 ((pow_dvd_pow _ hn1).trans nh)

Result:
no goals

Proof state:
case isTrue
α : Type u_1
inst✝ : Monoid α
a b : α
m : ℕ
nh : a ^ m ∣ b
h✝ : FiniteMultiplicity a b
hm : ↑(Nat.find h✝) < ↑m
⊢ False

Tactic:
simp only [cast_lt, find_lt_iff] at hm

Result:
case isTrue
α : Type u_1
inst✝ : Monoid α
a b : α
m : ℕ
nh : a ^ m ∣ b
h✝ : FiniteMultiplicity a b
hm : ∃ m_1 < m, ¬a ^ (m_1 + 1) ∣ b
⊢ False

Proof state:
α : Type u_1
inst✝ : Monoid α
a b : α
m : ℕ
hm : (if h : FiniteMultiplicity a b then ↑(Nat.find h) else ⊤) < ↑m
nh : a ^ m ∣ b
⊢ False

Tactic:
split at hm

Result:
case isTrue
α : Type u_1
inst✝ : Monoid α
a b : α
m : ℕ
nh : a ^ m ∣ b
h✝ : FiniteMultiplicity a b
hm : ↑(Nat.find h✝) < ↑m
⊢ False

case isFalse
α : Type u_1
inst✝ : Monoid α
a b : α
m : ℕ
nh : a ^ m ∣ b
h✝ : ¬FiniteMultiplicity a b
hm : ⊤ < ↑m
⊢ False

Proof state:
α : Type u_1
inst✝ : Monoid α
a b : α
m : ℕ
hm : emultiplicity a b < ↑m
nh : a ^ m ∣ b
⊢ False

Tactic:
unfold emultiplicity at hm

Result:
α : Type u_1
inst✝ : Monoid α
a b : α
m : ℕ
hm : (if h : FiniteMultiplicity a b then ↑(Nat.find h) else ⊤) < ↑m
nh : a ^ m ∣ b
⊢ False

Proof state:
case isFalse
α : Type u_1
inst✝ : Monoid α
a b : α
m : ℕ
nh : a ^ m ∣ b
h✝ : ¬FiniteMultiplicity a b
hm : ⊤ < ↑m
⊢ False

Tactic:
simp at hm

Result:
no goals
-- Mathlib/Tactic/ReduceModChar.lean
lemma CharP.intCast_eq_mod (R : Type _) [Ring R] (p : ℕ) [CharP R p] (k : ℤ) :
    (k : R) = (k % p : ℤ)

Proof state:
R : Type u_1
inst✝¹ : Ring R
p : ℕ
inst✝ : CharP R p
k : ℤ
⊢ ↑(k % ↑p + ↑p * (k / ↑p)) = ↑(k % ↑p)

Tactic:
simp [CharP.cast_eq_zero R]

Result:
no goals

Proof state:
R : Type u_1
inst✝¹ : Ring R
p : ℕ
inst✝ : CharP R p
k : ℤ
⊢ ↑k = ↑(k % ↑p + ↑p * (k / ↑p))

Tactic:
rw [Int.emod_add_ediv]

Result:
no goals

Proof state:
R : Type u_1
inst✝¹ : Ring R
p : ℕ
inst✝ : CharP R p
k : ℤ
⊢ ↑k = ↑(k % ↑p)

Tactic:
calc
  (k : R) = ↑(k % p + p * (k / p)) := by rw [Int.emod_add_ediv]
  _ = ↑(k % p) := by simp [CharP.cast_eq_zero R]

Result:
no goals
-- Mathlib/Analysis/Fourier/AddCircle.lean
theorem hasSum_fourier_series_L2 (f : Lp ℂ 2 <| @haarAddCircle T hT) :
    HasSum (fun i => fourierCoeff f i • fourierLp 2 i) f

Proof state:
T : ℝ
hT : Fact (0 < T)
f : ↥(Lp ℂ 2 haarAddCircle)
⊢ HasSum (fun i => ↑(fourierBasis.repr f) i • fourierBasis i) f

Tactic:
exact HilbertBasis.hasSum_repr fourierBasis f

Result:
no goals

Proof state:
T : ℝ
hT : Fact (0 < T)
f : ↥(Lp ℂ 2 haarAddCircle)
⊢ HasSum (fun i => ↑(fourierBasis.repr f) i • fourierLp 2 i) f

Tactic:
rw [← coe_fourierBasis]

Result:
T : ℝ
hT : Fact (0 < T)
f : ↥(Lp ℂ 2 haarAddCircle)
⊢ HasSum (fun i => ↑(fourierBasis.repr f) i • fourierBasis i) f

Proof state:
T : ℝ
hT : Fact (0 < T)
f : ↥(Lp ℂ 2 haarAddCircle)
⊢ HasSum (fun i => fourierCoeff (↑↑f) i • fourierLp 2 i) f

Tactic:
simp_rw [← fourierBasis_repr]

Result:
T : ℝ
hT : Fact (0 < T)
f : ↥(Lp ℂ 2 haarAddCircle)
⊢ HasSum (fun i => ↑(fourierBasis.repr f) i • fourierLp 2 i) f
-- Mathlib/Algebra/Module/Defs.lean
theorem Convex.combo_eq_smul_sub_add [Module R M] {x y : M} {a b : R} (h : a + b = 1) :
    a • x + b • y = b • (y - x) + x :=
  calc
    a • x + b • y = b • y - b • x + (a • x + b • x)

Proof state:
R : Type u_1
M : Type u_3
inst✝² : Semiring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x y : M
a b : R
h : a + b = 1
⊢ a • x + b • y = b • y - b • x + (a • x + b • x)

Tactic:
rw [sub_add_add_cancel, add_comm]

Result:
no goals

Proof state:
R : Type u_1
M : Type u_3
inst✝² : Semiring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x y : M
a b : R
h : a + b = 1
⊢ b • y - b • x + (a • x + b • x) = b • (y - x) + x

Tactic:
rw [smul_sub, Convex.combo_self h]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Fin/Lemmas.lean
theorem reverseInduction_last {n : Nat} {motive : Fin (n + 1) → Sort _} {zero succ} :
    (reverseInduction zero succ (Fin.last n) : motive (Fin.last n)) = zero

Proof state:
n : Nat
motive : Fin (n + 1) → Sort u_1
zero : motive (last n)
succ : (i : Fin n) → motive i.succ → motive i.castSucc
⊢ reverseInduction zero succ (last n) = zero

Tactic:
rw [reverseInduction]

Result:
n : Nat
motive : Fin (n + 1) → Sort u_1
zero : motive (last n)
succ : (i : Fin n) → motive i.succ → motive i.castSucc
⊢ (if hi : last n = last n then cast ⋯ zero
    else
      let j := ⟨↑(last n), ⋯⟩;
      succ j (reverseInduction zero succ j.succ)) =
    zero

Proof state:
n : Nat
motive : Fin (n + 1) → Sort u_1
zero : motive (last n)
succ : (i : Fin n) → motive i.succ → motive i.castSucc
⊢ (if hi : last n = last n then cast ⋯ zero
    else
      let j := ⟨↑(last n), ⋯⟩;
      succ j (reverseInduction zero succ j.succ)) =
    zero

Tactic:
simp

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Int/DivModLemmas.lean
theorem mul_tdiv_assoc (a : Int) : ∀ {b c : Int}, c ∣ b → (a * b).tdiv c = a * (b.tdiv c)
  | _, c, ⟨d, rfl⟩ =>
    if cz : c = 0 then by simp [cz, Int.mul_zero] else by
      rw [Int.mul_left_comm, Int.mul_tdiv_cancel_left _ cz, Int.mul_tdiv_cancel_left _ cz]

Proof state:
a c d : Int
cz : ¬c = 0
⊢ (a * (c * d)).tdiv c = a * (c * d).tdiv c

Tactic:
rw [Int.mul_left_comm, Int.mul_tdiv_cancel_left _ cz, Int.mul_tdiv_cancel_left _ cz]

Result:
no goals

Proof state:
a c d : Int
cz : c = 0
⊢ (a * (c * d)).tdiv c = a * (c * d).tdiv c

Tactic:
simp [cz, Int.mul_zero]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/RawLemmas.lean
theorem get?_insertMany_empty_list_of_mem [LawfulBEq α]
    {l : List ((a : α) × β a)} {k k' : α} (k_beq : k == k') {v : β k}
    (distinct : l.Pairwise (fun a b => (a.1 == b.1) = false))
    (mem : ⟨k, v⟩ ∈ l) :
    (insertMany empty l).1.get? k' = some (cast (by congr; apply LawfulBEq.eq_of_beq k_beq) v)

Proof state:
case e_a
α : Type u
β : α → Type v
m : Raw₀ α β
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : LawfulBEq α
l : List ((a : α) × β a)
k k' : α
k_beq : (k == k') = true
v : β k
distinct : List.Pairwise (fun a b => (a.fst == b.fst) = false) l
mem : ⟨k, v⟩ ∈ l
⊢ k = k'

Tactic:
apply LawfulBEq.eq_of_beq k_beq

Result:
no goals

Proof state:
α : Type u
β : α → Type v
m : Raw₀ α β
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : LawfulBEq α
l : List ((a : α) × β a)
k k' : α
k_beq : (k == k') = true
v : β k
distinct : List.Pairwise (fun a b => (a.fst == b.fst) = false) l
mem : ⟨k, v⟩ ∈ l
⊢ β k = β k'

Tactic:
congr

Result:
case e_a
α : Type u
β : α → Type v
m : Raw₀ α β
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : LawfulBEq α
l : List ((a : α) × β a)
k k' : α
k_beq : (k == k') = true
v : β k
distinct : List.Pairwise (fun a b => (a.fst == b.fst) = false) l
mem : ⟨k, v⟩ ∈ l
⊢ k = k'

Proof state:
α : Type u
β : α → Type v
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : LawfulBEq α
l : List ((a : α) × β a)
k k' : α
k_beq : (k == k') = true
v : β k
distinct : List.Pairwise (fun a b => (a.fst == b.fst) = false) l
mem : ⟨k, v⟩ ∈ l
⊢ (empty.insertMany l).val.get? k' = some (cast ⋯ v)

Tactic:
rw [get?_insertMany_list_of_mem _ Raw.WF.empty₀ k_beq distinct mem]

Result:
no goals
-- Mathlib/Order/Part.lean
lemma Antitone.partBind (hf : Antitone f) (hg : Antitone g) :
    Antitone fun x ↦ (f x).bind (g x)

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : Preorder α
f : α → Part β
g : α → β → Part γ
hf : Antitone f
hg : Antitone g
x y : α
h : x ≤ y
a : γ
⊢ a ∈ (fun x => (f x).bind (g x)) y → a ∈ (fun x => (f x).bind (g x)) x

Tactic:
simp only [and_imp, exists_prop, Part.bind_eq_bind, Part.mem_bind_iff, exists_imp]

Result:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : Preorder α
f : α → Part β
g : α → β → Part γ
hf : Antitone f
hg : Antitone g
x y : α
h : x ≤ y
a : γ
⊢ ∀ x_1 ∈ f y, a ∈ g y x_1 → ∃ a_3 ∈ f x, a ∈ g x a_3

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : Preorder α
f : α → Part β
g : α → β → Part γ
hf : Antitone f
hg : Antitone g
x y : α
h : x ≤ y
a : γ
⊢ ∀ x_1 ∈ f y, a ∈ g y x_1 → ∃ a_3 ∈ f x, a ∈ g x a_3

Tactic:
exact fun b hb ha ↦ ⟨b, hf h _ hb, hg h _ _ ha⟩

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : Preorder α
f : α → Part β
g : α → β → Part γ
hf : Antitone f
hg : Antitone g
⊢ Antitone fun x => (f x).bind (g x)

Tactic:
rintro x y h a

Result:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : Preorder α
f : α → Part β
g : α → β → Part γ
hf : Antitone f
hg : Antitone g
x y : α
h : x ≤ y
a : γ
⊢ a ∈ (fun x => (f x).bind (g x)) y → a ∈ (fun x => (f x).bind (g x)) x
-- Mathlib/LinearAlgebra/Basis/Basic.lean
theorem mk_coord_apply [DecidableEq ι] {i j : ι} :
    (Basis.mk hli hsp).coord i (v j) = if j = i then 1 else 0

Proof state:
case inl
ι : Type u_1
R : Type u_3
M : Type u_5
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
v : ι → M
hli : LinearIndependent R v
hsp : ⊤ ≤ span R (range v)
inst✝ : DecidableEq ι
i j : ι
h : j = i
⊢ ((Basis.mk hli hsp).coord i) (v j) = if j = i then 1 else 0

Tactic:
simp only [h, if_true, eq_self_iff_true, mk_coord_apply_eq i]

Result:
no goals

Proof state:
case inr
ι : Type u_1
R : Type u_3
M : Type u_5
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
v : ι → M
hli : LinearIndependent R v
hsp : ⊤ ≤ span R (range v)
inst✝ : DecidableEq ι
i j : ι
h : j ≠ i
⊢ ((Basis.mk hli hsp).coord i) (v j) = if j = i then 1 else 0

Tactic:
simp only [h, if_false, mk_coord_apply_ne h]

Result:
no goals

Proof state:
ι : Type u_1
R : Type u_3
M : Type u_5
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
v : ι → M
hli : LinearIndependent R v
hsp : ⊤ ≤ span R (range v)
inst✝ : DecidableEq ι
i j : ι
⊢ ((Basis.mk hli hsp).coord i) (v j) = if j = i then 1 else 0

Tactic:
rcases eq_or_ne j i with h | h

Result:
case inl
ι : Type u_1
R : Type u_3
M : Type u_5
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
v : ι → M
hli : LinearIndependent R v
hsp : ⊤ ≤ span R (range v)
inst✝ : DecidableEq ι
i j : ι
h : j = i
⊢ ((Basis.mk hli hsp).coord i) (v j) = if j = i then 1 else 0

case inr
ι : Type u_1
R : Type u_3
M : Type u_5
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
v : ι → M
hli : LinearIndependent R v
hsp : ⊤ ≤ span R (range v)
inst✝ : DecidableEq ι
i j : ι
h : j ≠ i
⊢ ((Basis.mk hli hsp).coord i) (v j) = if j = i then 1 else 0
-- Mathlib/LinearAlgebra/Dimension/RankNullity.lean
/-- Rank-nullity theorem using `finrank`. -/
lemma Submodule.finrank_quotient_add_finrank [Module.Finite R M] (N : Submodule R M) :
    finrank R (M ⧸ N) + finrank R N = finrank R M

Proof state:
R : Type u_1
M : Type u
inst✝⁵ : Ring R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : HasRankNullity.{u, u_1} R
inst✝¹ : StrongRankCondition R
inst✝ : Module.Finite R M
N : Submodule R M
⊢ finrank R (M ⧸ N) + finrank R ↥N = finrank R M

Tactic:
rw [← Nat.cast_inj (R := Cardinal), Module.finrank_eq_rank, Nat.cast_add, Module.finrank_eq_rank,
  Submodule.finrank_eq_rank]

Result:
R : Type u_1
M : Type u
inst✝⁵ : Ring R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : HasRankNullity.{u, u_1} R
inst✝¹ : StrongRankCondition R
inst✝ : Module.Finite R M
N : Submodule R M
⊢ Module.rank R (M ⧸ N) + Module.rank R ↥N = Module.rank R M

Proof state:
R : Type u_1
M : Type u
inst✝⁵ : Ring R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : HasRankNullity.{u, u_1} R
inst✝¹ : StrongRankCondition R
inst✝ : Module.Finite R M
N : Submodule R M
⊢ Module.rank R (M ⧸ N) + Module.rank R ↥N = Module.rank R M

Tactic:
exact HasRankNullity.rank_quotient_add_rank _

Result:
no goals
-- Mathlib/Geometry/Euclidean/Angle/Oriented/RightAngle.lean
theorem oangle_sub_left_eq_arccos_of_oangle_eq_pi_div_two {x y : V} (h : o.oangle x y = ↑(π / 2)) :
    o.oangle (x - y) x = Real.arccos (‖x‖ / ‖x - y‖)

Proof state:
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
hd2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
h : o.oangle x y = ↑(π / 2)
⊢ o.oangle (x - y) x = ↑(Real.arccos (‖x‖ / ‖x - y‖))

Tactic:
rw [← neg_inj, oangle_rev, ← oangle_neg_orientation_eq_neg, neg_inj] at h ⊢

Result:
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
hd2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
h : (-o).oangle y x = ↑(π / 2)
⊢ (-o).oangle x (x - y) = ↑(Real.arccos (‖x‖ / ‖x - y‖))

Proof state:
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
hd2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
h : (-o).oangle y x = ↑(π / 2)
⊢ (-o).oangle x (x - y) = ↑(Real.arccos (‖x‖ / ‖x - y‖))

Tactic:
exact (-o).oangle_sub_right_eq_arccos_of_oangle_eq_pi_div_two h

Result:
no goals
-- Mathlib/MeasureTheory/Measure/MeasureSpace.lean
theorem measure_iUnion_eq_iSup_accumulate [Preorder ι] [IsDirected ι (· ≤ ·)]
    [(atTop : Filter ι).IsCountablyGenerated] {f : ι → Set α} :
    μ (⋃ i, f i) = ⨆ i, μ (Accumulate f i)

Proof state:
α : Type u_1
ι : Type u_5
m : MeasurableSpace α
μ : Measure α
inst✝² : Preorder ι
inst✝¹ : IsDirected ι fun x1 x2 => x1 ≤ x2
inst✝ : atTop.IsCountablyGenerated
f : ι → Set α
⊢ μ (⋃ x, Accumulate f x) = ⨆ i, μ (Accumulate f i)

Tactic:
exact monotone_accumulate.measure_iUnion

Result:
no goals

Proof state:
α : Type u_1
ι : Type u_5
m : MeasurableSpace α
μ : Measure α
inst✝² : Preorder ι
inst✝¹ : IsDirected ι fun x1 x2 => x1 ≤ x2
inst✝ : atTop.IsCountablyGenerated
f : ι → Set α
⊢ μ (⋃ i, f i) = ⨆ i, μ (Accumulate f i)

Tactic:
rw [← iUnion_accumulate]

Result:
α : Type u_1
ι : Type u_5
m : MeasurableSpace α
μ : Measure α
inst✝² : Preorder ι
inst✝¹ : IsDirected ι fun x1 x2 => x1 ≤ x2
inst✝ : atTop.IsCountablyGenerated
f : ι → Set α
⊢ μ (⋃ x, Accumulate f x) = ⨆ i, μ (Accumulate f i)