harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Data/Set/Pairwise/Lattice.lean
lemma Set.pairwiseDisjoint_pair_insert {s : Set α} {a : α} (ha : a ∉ s) :
    s.powerset.PairwiseDisjoint fun t ↦ ({t, insert a t} : Set (Set α))

Proof state:
α : Type u_1
s : Set α
a : α
ha : a ∉ s
i : Set α
hi : i ∈ 𝒫 s
j : Set α
hj : j ∈ 𝒫 s
⊢ ({i, insert a i} ∩ {j, insert a j}).Nonempty → i = j

Tactic:
have := insert_erase_invOn.2.injOn (not_mem_subset hi ha) (not_mem_subset hj ha)

Result:
α : Type u_1
s : Set α
a : α
ha : a ∉ s
i : Set α
hi : i ∈ 𝒫 s
j : Set α
hj : j ∈ 𝒫 s
this : insert a i = insert a j → i = j
⊢ ({i, insert a i} ∩ {j, insert a j}).Nonempty → i = j

Proof state:
α : Type u_1
s : Set α
a : α
ha : a ∉ s
i : Set α
hi : i ∈ 𝒫 s
j : Set α
hj : j ∈ 𝒫 s
this : insert a i = insert a j → i = j
⊢ ({i, insert a i} ∩ {j, insert a j}).Nonempty → i = j

Tactic:
aesop (add simp [Set.Nonempty, Set.subset_def])

Result:
no goals

Proof state:
α : Type u_1
s : Set α
a : α
ha : a ∉ s
⊢ (𝒫 s).PairwiseDisjoint fun t => {t, insert a t}

Tactic:
rw [pairwiseDisjoint_iff]

Result:
α : Type u_1
s : Set α
a : α
ha : a ∉ s
⊢ ∀ ⦃i : Set α⦄, i ∈ 𝒫 s → ∀ ⦃j : Set α⦄, j ∈ 𝒫 s → ({i, insert a i} ∩ {j, insert a j}).Nonempty → i = j

Proof state:
α : Type u_1
s : Set α
a : α
ha : a ∉ s
⊢ ∀ ⦃i : Set α⦄, i ∈ 𝒫 s → ∀ ⦃j : Set α⦄, j ∈ 𝒫 s → ({i, insert a i} ∩ {j, insert a j}).Nonempty → i = j

Tactic:
rintro i hi j hj

Result:
α : Type u_1
s : Set α
a : α
ha : a ∉ s
i : Set α
hi : i ∈ 𝒫 s
j : Set α
hj : j ∈ 𝒫 s
⊢ ({i, insert a i} ∩ {j, insert a j}).Nonempty → i = j
-- Mathlib/CategoryTheory/Subpresheaf/Basic.lean
lemma iSup_min {ι : Type*} (S : ι → Subpresheaf F) (T : Subpresheaf F) :
    (⨆ i, S i) ⊓ T = ⨆ i, S i ⊓ T

Proof state:
C : Type u
inst✝ : Category.{v, u} C
F : Cᵒᵖ ⥤ Type w
ι : Type u_1
S : ι → Subpresheaf F
T : Subpresheaf F
⊢ (⨆ i, S i) ⊓ T = ⨆ i, S i ⊓ T

Tactic:
aesop

Result:
no goals
-- Mathlib/Probability/Process/PartitionFiltration.lean
lemma iSup_partitionFiltration_eq_generateFrom_range (ht : ∀ n, MeasurableSet (t n)) :
    ⨆ n, partitionFiltration ht n = generateFrom (Set.range t)

Proof state:
α : Type u_1
m : MeasurableSpace α
t : ℕ → Set α
ht : ∀ (n : ℕ), MeasurableSet (t n)
⊢ ⨆ n, ↑(partitionFiltration ht) n = generateFrom (Set.range t)

Tactic:
conv_rhs => rw [← generateFrom_iUnion_memPartition t, ← iSup_generateFrom]

Result:
α : Type u_1
m : MeasurableSpace α
t : ℕ → Set α
ht : ∀ (n : ℕ), MeasurableSet (t n)
⊢ ⨆ n, ↑(partitionFiltration ht) n = ⨆ i, generateFrom (memPartition t i)

Proof state:
α : Type u_1
m : MeasurableSpace α
t : ℕ → Set α
ht : ∀ (n : ℕ), MeasurableSet (t n)
⊢ ⨆ n, ↑(partitionFiltration ht) n = ⨆ i, generateFrom (memPartition t i)

Tactic:
rfl

Result:
no goals
-- Mathlib/Data/Nat/GCD/Basic.lean
theorem gcd_self_add_left (m n : ℕ) : gcd (m + n) m = gcd n m

Proof state:
m n : ℕ
⊢ (m + n).gcd m = n.gcd m

Tactic:
rw [add_comm, gcd_add_self_left]

Result:
no goals
-- Mathlib/MeasureTheory/Measure/AEMeasurable.lean
lemma aemeasurable_of_map_neZero {μ : Measure α}
    {f : α → β} (h : NeZero (μ.map f)) :
    AEMeasurable f μ

Proof state:
α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
inst✝ : MeasurableSpace β
μ : Measure α
f : α → β
h : NeZero (Measure.map f μ)
⊢ AEMeasurable f μ

Tactic:
by_contra h'

Result:
α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
inst✝ : MeasurableSpace β
μ : Measure α
f : α → β
h : NeZero (Measure.map f μ)
h' : ¬AEMeasurable f μ
⊢ False

Proof state:
α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
inst✝ : MeasurableSpace β
μ : Measure α
f : α → β
h : NeZero (Measure.map f μ)
h' : ¬AEMeasurable f μ
⊢ False

Tactic:
simp [h'] at h

Result:
no goals
-- Mathlib/LinearAlgebra/Dimension/Finrank.lean
theorem finrank_eq_of_rank_eq {n : ℕ} (h : Module.rank R M = ↑n) : finrank R M = n

Proof state:
R : Type u
M : Type v
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
n : ℕ
h : toNat (Module.rank R M) = toNat ↑n
⊢ finrank R M = n

Tactic:
rw [toNat_natCast] at h

Result:
R : Type u
M : Type v
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
n : ℕ
h : toNat (Module.rank R M) = n
⊢ finrank R M = n

Proof state:
R : Type u
M : Type v
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
n : ℕ
h : Module.rank R M = ↑n
⊢ finrank R M = n

Tactic:
apply_fun toNat at h

Result:
R : Type u
M : Type v
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
n : ℕ
h : toNat (Module.rank R M) = toNat ↑n
⊢ finrank R M = n

Proof state:
R : Type u
M : Type v
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
n : ℕ
h : toNat (Module.rank R M) = n
⊢ finrank R M = n

Tactic:
exact mod_cast h

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Lemmas.lean
theorem foldl_assoc {op : α → α → α} [ha : Std.Associative op] :
    ∀ {l : List α} {a₁ a₂}, l.foldl op (op a₁ a₂) = op a₁ (l.foldl op a₂)
  | [], a₁, a₂ => rfl
  | a :: l, a₁, a₂ => by
    simp only [foldl_cons, ha.assoc]
    rw [foldl_assoc]

Proof state:
α : Type u_1
op : α → α → α
ha : Std.Associative op
a : α
l : List α
a₁ a₂ : α
⊢ foldl op (op a₁ a₂) (a :: l) = op a₁ (foldl op a₂ (a :: l))

Tactic:
simp only [foldl_cons, ha.assoc]

Result:
α : Type u_1
op : α → α → α
ha : Std.Associative op
a : α
l : List α
a₁ a₂ : α
⊢ foldl op (op a₁ (op a₂ a)) l = op a₁ (foldl op (op a₂ a) l)

Proof state:
α : Type u_1
op : α → α → α
ha : Std.Associative op
a : α
l : List α
a₁ a₂ : α
⊢ foldl op (op a₁ (op a₂ a)) l = op a₁ (foldl op (op a₂ a) l)

Tactic:
rw [foldl_assoc]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/RawLemmas.lean
theorem mem_of_mem_insertMany_list [EquivBEq α] [LawfulHashable α] (h : m.WF)
    {l : List (α × β)} {k : α} :
    k ∈ insertMany m l → (l.map Prod.fst).contains k = false → k ∈ m

Proof state:
α : Type u
inst✝³ : BEq α
inst✝² : Hashable α
β : Type v
m : Raw α fun x => β
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
h : m.WF
l : List (α × β)
k : α
⊢ k ∈ insertMany m l → (List.map Prod.fst l).contains k = false → k ∈ m

Tactic:
simp only [mem_iff_contains]

Result:
α : Type u
inst✝³ : BEq α
inst✝² : Hashable α
β : Type v
m : Raw α fun x => β
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
h : m.WF
l : List (α × β)
k : α
⊢ (insertMany m l).contains k = true → (List.map Prod.fst l).contains k = false → m.contains k = true

Proof state:
α : Type u
inst✝³ : BEq α
inst✝² : Hashable α
β : Type v
m : Raw α fun x => β
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
h : m.WF
l : List (α × β)
k : α
⊢ (insertMany m l).contains k = true → (List.map Prod.fst l).contains k = false → m.contains k = true

Tactic:
simp_to_raw using Raw₀.Const.contains_of_contains_insertMany_list

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Sat/AIG/Relabel.lean
theorem relabel_const {aig : AIG α} {r : α → β} {hidx : idx < (relabel r aig).decls.size}
    (h : (relabel r aig).decls[idx]'hidx = .const b) :
    aig.decls[idx]'(by rw [← relabel_size_eq_size (r := r)]; omega) = .const b

Proof state:
α : Type
inst✝³ : Hashable α
inst✝² : DecidableEq α
β : Type
inst✝¹ : Hashable β
inst✝ : DecidableEq β
idx : Nat
b : Bool
aig : AIG α
r : α → β
hidx : idx < (relabel r aig).decls.size
h : (relabel r aig).decls[idx] = Decl.const b
⊢ idx < (relabel r aig).decls.size

Tactic:
omega

Result:
no goals

Proof state:
α : Type
inst✝³ : Hashable α
inst✝² : DecidableEq α
β : Type
inst✝¹ : Hashable β
inst✝ : DecidableEq β
idx : Nat
b : Bool
aig : AIG α
r : α → β
hidx : idx < (relabel r aig).decls.size
h : (relabel r aig).decls[idx] = Decl.const b
⊢ idx < aig.decls.size

Tactic:
rw [← relabel_size_eq_size (r := r)]

Result:
α : Type
inst✝³ : Hashable α
inst✝² : DecidableEq α
β : Type
inst✝¹ : Hashable β
inst✝ : DecidableEq β
idx : Nat
b : Bool
aig : AIG α
r : α → β
hidx : idx < (relabel r aig).decls.size
h : (relabel r aig).decls[idx] = Decl.const b
⊢ idx < (relabel r aig).decls.size

Proof state:
case h
α : Type
inst✝³ : Hashable α
inst✝² : DecidableEq α
β : Type
inst✝¹ : Hashable β
inst✝ : DecidableEq β
idx : Nat
b : Bool
aig : AIG α
r : α → β
hidx : idx < (relabel r aig).decls.size
h : (relabel r aig).decls[idx] = Decl.const b
⊢ Decl.relabel ?r aig.decls[idx] = Decl.const b

case β
α : Type
inst✝³ : Hashable α
inst✝² : DecidableEq α
β : Type
inst✝¹ : Hashable β
inst✝ : DecidableEq β
idx : Nat
b : Bool
aig : AIG α
r : α → β
hidx : idx < (relabel r aig).decls.size
h : (relabel r aig).decls[idx] = Decl.const b
⊢ Type

case r
α : Type
inst✝³ : Hashable α
inst✝² : DecidableEq α
β : Type
inst✝¹ : Hashable β
inst✝ : DecidableEq β
idx : Nat
b : Bool
aig : AIG α
r : α → β
hidx : idx < (relabel r aig).decls.size
h : (relabel r aig).decls[idx] = Decl.const b
⊢ α → ?β

Tactic:
simpa [relabel] using h

Result:
no goals

Proof state:
α : Type
inst✝³ : Hashable α
inst✝² : DecidableEq α
β : Type
inst✝¹ : Hashable β
inst✝ : DecidableEq β
idx : Nat
b : Bool
aig : AIG α
r : α → β
hidx : idx < (relabel r aig).decls.size
h : (relabel r aig).decls[idx] = Decl.const b
⊢ aig.decls[idx] = Decl.const b

Tactic:
apply Decl.relabel_const

Result:
case h
α : Type
inst✝³ : Hashable α
inst✝² : DecidableEq α
β : Type
inst✝¹ : Hashable β
inst✝ : DecidableEq β
idx : Nat
b : Bool
aig : AIG α
r : α → β
hidx : idx < (relabel r aig).decls.size
h : (relabel r aig).decls[idx] = Decl.const b
⊢ Decl.relabel ?r aig.decls[idx] = Decl.const b

case β
α : Type
inst✝³ : Hashable α
inst✝² : DecidableEq α
β : Type
inst✝¹ : Hashable β
inst✝ : DecidableEq β
idx : Nat
b : Bool
aig : AIG α
r : α → β
hidx : idx < (relabel r aig).decls.size
h : (relabel r aig).decls[idx] = Decl.const b
⊢ Type

case r
α : Type
inst✝³ : Hashable α
inst✝² : DecidableEq α
β : Type
inst✝¹ : Hashable β
inst✝ : DecidableEq β
idx : Nat
b : Bool
aig : AIG α
r : α → β
hidx : idx < (relabel r aig).decls.size
h : (relabel r aig).decls[idx] = Decl.const b
⊢ α → ?β
-- Mathlib/MeasureTheory/Function/ConditionalExpectation/CondexpL2.lean
theorem eLpNorm_condExpL2_le (hm : m ≤ m0) (f : α →₂[μ] E) :
    eLpNorm (ε := E) (condExpL2 E 𝕜 hm f) 2 μ ≤ eLpNorm f 2 μ

Proof state:
α : Type u_1
E : Type u_2
𝕜 : Type u_7
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : CompleteSpace E
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
f : ↥(Lp E 2 μ)
⊢ eLpNorm (↑↑↑((condExpL2 E 𝕜 hm) f)) 2 μ ≤ eLpNorm (↑↑f) 2 μ

Tactic:
rw [← ENNReal.toReal_le_toReal (Lp.eLpNorm_ne_top _) (Lp.eLpNorm_ne_top _), ←
  Lp.norm_def, ← Lp.norm_def, Submodule.norm_coe]

Result:
α : Type u_1
E : Type u_2
𝕜 : Type u_7
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : CompleteSpace E
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
f : ↥(Lp E 2 μ)
⊢ ‖(condExpL2 E 𝕜 hm) f‖ ≤ ‖f‖

Proof state:
α : Type u_1
E : Type u_2
𝕜 : Type u_7
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : CompleteSpace E
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
f : ↥(Lp E 2 μ)
⊢ ‖(condExpL2 E 𝕜 hm) f‖ ≤ ‖f‖

Tactic:
exact norm_condExpL2_le hm f

Result:
no goals
-- Mathlib/NumberTheory/VonMangoldt.lean
theorem vonMangoldt_le_log : ∀ {n : ℕ}, Λ n ≤ Real.log (n : ℝ)
  | 0 => by simp
  | n + 1 => by
    rw [← vonMangoldt_sum]
    exact single_le_sum (by exact fun _ _ => vonMangoldt_nonneg)
      (mem_divisors_self _ n.succ_ne_zero)

Proof state:
⊢ Λ 0 ≤ Real.log ↑0

Tactic:
simp

Result:
no goals

Proof state:
n : ℕ
⊢ Λ (n + 1) ≤ ∑ i ∈ (n + 1).divisors, Λ i

Tactic:
exact single_le_sum (by exact fun _ _ => vonMangoldt_nonneg)
  (mem_divisors_self _ n.succ_ne_zero)

Result:
no goals

Proof state:
n : ℕ
⊢ Λ (n + 1) ≤ Real.log ↑(n + 1)

Tactic:
rw [← vonMangoldt_sum]

Result:
n : ℕ
⊢ Λ (n + 1) ≤ ∑ i ∈ (n + 1).divisors, Λ i

Proof state:
n : ℕ
⊢ ∀ i ∈ (n + 1).divisors, 0 ≤ Λ i

Tactic:
exact fun _ _ => vonMangoldt_nonneg

Result:
no goals
-- Mathlib/Analysis/Convex/Join.lean
theorem convexJoin_union_right (s t₁ t₂ : Set E) :
    convexJoin 𝕜 s (t₁ ∪ t₂) = convexJoin 𝕜 s t₁ ∪ convexJoin 𝕜 s t₂

Proof state:
𝕜 : Type u_2
E : Type u_3
inst✝² : OrderedSemiring 𝕜
inst✝¹ : AddCommMonoid E
inst✝ : Module 𝕜 E
s t₁ t₂ : Set E
⊢ convexJoin 𝕜 s (t₁ ∪ t₂) = convexJoin 𝕜 s t₁ ∪ convexJoin 𝕜 s t₂

Tactic:
simp_rw [convexJoin_comm s, convexJoin_union_left]

Result:
no goals
-- Mathlib/MeasureTheory/Measure/QuasiMeasurePreserving.lean
theorem smul_ae_eq_of_ae_eq {G α : Type*} [Group G] [MulAction G α] {_ : MeasurableSpace α}
    {s t : Set α} {μ : Measure α} (g : G)
    (h_qmp : QuasiMeasurePreserving (g⁻¹ • · : α → α) μ μ)
    (h_ae_eq : s =ᵐ[μ] t) : (g • s : Set α) =ᵐ[μ] (g • t : Set α)

Proof state:
G : Type u_5
α : Type u_6
inst✝¹ : Group G
inst✝ : MulAction G α
x✝ : MeasurableSpace α
s t : Set α
μ : Measure α
g : G
h_qmp : QuasiMeasurePreserving (fun x => g⁻¹ • x) μ μ
h_ae_eq : s =ᵐ[μ] t
⊢ g • s =ᵐ[μ] g • t

Tactic:
simpa only [← preimage_smul_inv] using h_qmp.ae_eq h_ae_eq

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Lemmas.lean
theorem filterMap_reverse (f : α → Option β) (l : List α) : (l.reverse.filterMap f) = (l.filterMap f).reverse

Proof state:
case cons
α : Type u_1
β : Type u_2
f : α → Option β
a : α
l : List α
ih : filterMap f l.reverse = (filterMap f l).reverse
⊢ ((filterMap f l).reverse ++
      match f a with
      | none => filterMap f []
      | some b => b :: filterMap f []) =
    (match f a with
      | none => filterMap f l
      | some b => b :: filterMap f l).reverse

Tactic:
split <;> simp_all

Result:
no goals

Proof state:
case cons
α : Type u_1
β : Type u_2
f : α → Option β
a : α
l : List α
ih : filterMap f l.reverse = (filterMap f l).reverse
⊢ filterMap f (a :: l).reverse = (filterMap f (a :: l)).reverse

Tactic:
simp only [reverse_cons, filterMap_append, filterMap_cons, ih]

Result:
case cons
α : Type u_1
β : Type u_2
f : α → Option β
a : α
l : List α
ih : filterMap f l.reverse = (filterMap f l).reverse
⊢ ((filterMap f l).reverse ++
      match f a with
      | none => filterMap f []
      | some b => b :: filterMap f []) =
    (match f a with
      | none => filterMap f l
      | some b => b :: filterMap f l).reverse

Proof state:
case nil
α : Type u_1
β : Type u_2
f : α → Option β
⊢ filterMap f [].reverse = (filterMap f []).reverse

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
f : α → Option β
l : List α
⊢ filterMap f l.reverse = (filterMap f l).reverse

Tactic:
induction l with
| nil => simp
| cons a l ih =>
  simp only [reverse_cons, filterMap_append, filterMap_cons, ih]
  split <;> simp_all

Result:
no goals
-- Mathlib/LinearAlgebra/Quotient/Basic.lean
theorem Quotient.equiv_trans {N O : Type*} [AddCommGroup N] [Module R N] [AddCommGroup O]
    [Module R O] (P : Submodule R M) (Q : Submodule R N) (S : Submodule R O) (e : M ≃ₗ[R] N)
    (f : N ≃ₗ[R] O) (he : P.map e = Q) (hf : Q.map f = S) (hef : P.map (e.trans f) = S) :
    Quotient.equiv P S (e.trans f) hef =
      (Quotient.equiv P Q e he).trans (Quotient.equiv Q S f hf)

Proof state:
R : Type u_1
M : Type u_2
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
N : Type u_5
O : Type u_6
inst✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : AddCommGroup O
inst✝ : Module R O
P : Submodule R M
Q : Submodule R N
S : Submodule R O
e : M ≃ₗ[R] N
f : N ≃ₗ[R] O
he : map e P = Q
hf : map f Q = S
hef : map (e ≪≫ₗ f) P = S
⊢ equiv P S (e ≪≫ₗ f) hef = equiv P Q e he ≪≫ₗ equiv Q S f hf

Tactic:
ext

Result:
case h
R : Type u_1
M : Type u_2
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
N : Type u_5
O : Type u_6
inst✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : AddCommGroup O
inst✝ : Module R O
P : Submodule R M
Q : Submodule R N
S : Submodule R O
e : M ≃ₗ[R] N
f : N ≃ₗ[R] O
he : map e P = Q
hf : map f Q = S
hef : map (e ≪≫ₗ f) P = S
x✝ : M ⧸ P
⊢ (equiv P S (e ≪≫ₗ f) hef) x✝ = (equiv P Q e he ≪≫ₗ equiv Q S f hf) x✝

Proof state:
case h
R : Type u_1
M : Type u_2
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
N : Type u_5
O : Type u_6
inst✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : AddCommGroup O
inst✝ : Module R O
P : Submodule R M
Q : Submodule R N
S : Submodule R O
e : M ≃ₗ[R] N
f : N ≃ₗ[R] O
he : map e P = Q
hf : map f Q = S
hef : map (e ≪≫ₗ f) P = S
x✝ : M ⧸ P
⊢ (equiv P S (e ≪≫ₗ f) hef) x✝ = (equiv P Q e he ≪≫ₗ equiv Q S f hf) x✝

Tactic:
simp only [Quotient.equiv_apply, LinearEquiv.trans_apply, LinearEquiv.coe_trans]

Result:
case h
R : Type u_1
M : Type u_2
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
N : Type u_5
O : Type u_6
inst✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : AddCommGroup O
inst✝ : Module R O
P : Submodule R M
Q : Submodule R N
S : Submodule R O
e : M ≃ₗ[R] N
f : N ≃ₗ[R] O
he : map e P = Q
hf : map f Q = S
hef : map (e ≪≫ₗ f) P = S
x✝ : M ⧸ P
⊢ (P.mapQ S (↑f ∘ₗ ↑e) ⋯) x✝ = (Q.mapQ S ↑f ⋯) ((P.mapQ Q ↑e ⋯) x✝)

Proof state:
case h
R : Type u_1
M : Type u_2
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
N : Type u_5
O : Type u_6
inst✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : AddCommGroup O
inst✝ : Module R O
P : Submodule R M
Q : Submodule R N
S : Submodule R O
e : M ≃ₗ[R] N
f : N ≃ₗ[R] O
he : map e P = Q
hf : map f Q = S
hef : map (e ≪≫ₗ f) P = S
x✝ : M ⧸ P
⊢ (P.mapQ S (↑f ∘ₗ ↑e) ⋯) x✝ = (Q.mapQ S ↑f ⋯) ((P.mapQ Q ↑e ⋯) x✝)

Tactic:
rw [mapQ_comp, LinearMap.comp_apply]

Result:
no goals
-- Mathlib/LinearAlgebra/Matrix/Charpoly/Basic.lean
theorem charmatrix_apply_ne (h : i ≠ j) : charmatrix M i j = -C (M i j)

Proof state:
R : Type u_1
inst✝² : CommRing R
n : Type u_4
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : Matrix n n R
i j : n
h : i ≠ j
⊢ M.charmatrix i j = -C (M i j)

Tactic:
simp only [charmatrix, RingHom.mapMatrix_apply, sub_apply, scalar_apply, diagonal_apply_ne _ h,
  map_apply, sub_eq_neg_self]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/SizeOfLemmas.lean
theorem UInt64.sizeOf (a : UInt64) : sizeOf a = a.toNat + 3

Proof state:
a : UInt64
⊢ sizeOf a = a.toNat + 3

Tactic:
cases a

Result:
case mk
toBitVec✝ : BitVec 64
⊢ sizeOf { toBitVec := toBitVec✝ } = { toBitVec := toBitVec✝ }.toNat + 3

Proof state:
case mk
toBitVec✝ : BitVec 64
⊢ sizeOf { toBitVec := toBitVec✝ } = { toBitVec := toBitVec✝ }.toNat + 3

Tactic:
simp_arith [UInt64.toNat, BitVec.toNat]

Result:
no goals
-- Mathlib/LinearAlgebra/AffineSpace/Independent.lean
theorem affineCombination_mem_affineSpan_pair {p : ι → P} (h : AffineIndependent k p)
    {w w₁ w₂ : ι → k} {s : Finset ι} (_ : ∑ i ∈ s, w i = 1) (hw₁ : ∑ i ∈ s, w₁ i = 1)
    (hw₂ : ∑ i ∈ s, w₂ i = 1) :
    s.affineCombination k p w ∈ line[k, s.affineCombination k p w₁, s.affineCombination k p w₂] ↔
      ∃ r : k, ∀ i ∈ s, w i = r * (w₂ i - w₁ i) + w₁ i

Proof state:
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
ι : Type u_4
p : ι → P
h : AffineIndependent k p
w w₁ w₂ : ι → k
s : Finset ι
x✝ : ∑ i ∈ s, w i = 1
hw₁ : ∑ i ∈ s, w₁ i = 1
hw₂ : ∑ i ∈ s, w₂ i = 1
⊢ (affineCombination k s p) w ∈ affineSpan k {(affineCombination k s p) w₁, (affineCombination k s p) w₂} ↔
    ∃ r, ∀ i ∈ s, w i = r * (w₂ i - w₁ i) + w₁ i

Tactic:
rw [← vsub_vadd (s.affineCombination k p w) (s.affineCombination k p w₁),
  AffineSubspace.vadd_mem_iff_mem_direction _ (left_mem_affineSpan_pair _ _ _),
  direction_affineSpan, s.affineCombination_vsub, Set.pair_comm,
  weightedVSub_mem_vectorSpan_pair h _ hw₂ hw₁]

Result:
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
ι : Type u_4
p : ι → P
h : AffineIndependent k p
w w₁ w₂ : ι → k
s : Finset ι
x✝ : ∑ i ∈ s, w i = 1
hw₁ : ∑ i ∈ s, w₁ i = 1
hw₂ : ∑ i ∈ s, w₂ i = 1
⊢ (∃ r, ∀ i ∈ s, (w - w₁) i = r * (w₂ i - w₁ i)) ↔ ∃ r, ∀ i ∈ s, w i = r * (w₂ i - w₁ i) + w₁ i

k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
ι : Type u_4
p : ι → P
h : AffineIndependent k p
w w₁ w₂ : ι → k
s : Finset ι
x✝ : ∑ i ∈ s, w i = 1
hw₁ : ∑ i ∈ s, w₁ i = 1
hw₂ : ∑ i ∈ s, w₂ i = 1
⊢ ∑ i ∈ s, (w - w₁) i = 0

Proof state:
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
ι : Type u_4
p : ι → P
h : AffineIndependent k p
w w₁ w₂ : ι → k
s : Finset ι
x✝ : ∑ i ∈ s, w i = 1
hw₁ : ∑ i ∈ s, w₁ i = 1
hw₂ : ∑ i ∈ s, w₂ i = 1
⊢ ∑ i ∈ s, (w - w₁) i = 0

Tactic:
simp_all only [Pi.sub_apply, Finset.sum_sub_distrib, sub_self]

Result:
no goals

Proof state:
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
ι : Type u_4
p : ι → P
h : AffineIndependent k p
w w₁ w₂ : ι → k
s : Finset ι
x✝ : ∑ i ∈ s, w i = 1
hw₁ : ∑ i ∈ s, w₁ i = 1
hw₂ : ∑ i ∈ s, w₂ i = 1
⊢ (∃ r, ∀ i ∈ s, (w - w₁) i = r * (w₂ i - w₁ i)) ↔ ∃ r, ∀ i ∈ s, w i = r * (w₂ i - w₁ i) + w₁ i

Tactic:
simp only [Pi.sub_apply, sub_eq_iff_eq_add]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Lemmas.lean
theorem eq_replicate_of_mem {a : α} :
    ∀ {l : List α}, (∀ (b) (_ : b ∈ l), b = a) → l = replicate l.length a
  | [], _ => rfl
  | b :: l, H => by
    let ⟨rfl, H₂⟩ := forall_mem_cons (l := l).1 H
    rw [length_cons, replicate, ← eq_replicate_of_mem H₂]

Proof state:
α : Type u_1
b : α
l : List α
H₂ : ∀ (x : α), x ∈ l → x = b
H : ∀ (b_1 : α), b_1 ∈ b :: l → b_1 = b
⊢ b :: l = replicate (b :: l).length b

Tactic:
rw [length_cons, replicate, ← eq_replicate_of_mem H₂]

Result:
no goals

Proof state:
α : Type u_1
a b : α
l : List α
H : ∀ (b_1 : α), b_1 ∈ b :: l → b_1 = a
⊢ b :: l = replicate (b :: l).length a

Tactic:
let ⟨rfl, H₂⟩ := forall_mem_cons (l := l).1 H

Result:
α : Type u_1
b : α
l : List α
H₂ : ∀ (x : α), x ∈ l → x = b
H : ∀ (b_1 : α), b_1 ∈ b :: l → b_1 = b
⊢ b :: l = replicate (b :: l).length b
-- Mathlib/Algebra/Order/Field/Defs.lean
/-- Equality holds when `b ≠ 0`. See `mul_inv_cancel_right`. -/
lemma mul_inv_right_le (ha : 0 ≤ a) : a * b * b⁻¹ ≤ a

Proof state:
α : Type u_1
inst✝ : LinearOrderedSemifield α
a b : α
ha : 0 ≤ a
⊢ a * b * b⁻¹ ≤ a

Tactic:
obtain rfl | hb := eq_or_ne b 0 <;> simp [*]

Result:
no goals
-- Mathlib/NumberTheory/NumberField/Embeddings.lean
lemma isReal_infinitePlace : InfinitePlace.IsReal (infinitePlace) :=
  ⟨Rat.castHom ℂ, by ext; simp, rfl⟩

Proof state:
⊢ ComplexEmbedding.IsReal (castHom ℂ)

Tactic:
ext

Result:
case a
x✝ : ℚ
⊢ (star (castHom ℂ)) x✝ = (castHom ℂ) x✝

Proof state:
case a
x✝ : ℚ
⊢ (star (castHom ℂ)) x✝ = (castHom ℂ) x✝

Tactic:
simp

Result:
no goals
-- Mathlib/RingTheory/Localization/Module.lean
theorem LinearIndependent.localization [Module Rₛ M] [IsScalarTower R Rₛ M]
    {ι : Type*} {b : ι → M} (hli : LinearIndependent R b) :
    LinearIndependent Rₛ b

Proof state:
R : Type u_1
Rₛ : Type u_2
inst✝⁷ : CommSemiring R
S : Submonoid R
inst✝⁶ : CommSemiring Rₛ
inst✝⁵ : Algebra R Rₛ
inst✝⁴ : IsLocalization S Rₛ
M : Type u_3
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : Module Rₛ M
inst✝ : IsScalarTower R Rₛ M
ι : Type u_5
b : ι → M
hli : LinearIndependent R b
this : IsLocalizedModule S LinearMap.id
⊢ LinearIndependent Rₛ b

Tactic:
exact hli.of_isLocalizedModule Rₛ S .id

Result:
no goals

Proof state:
R : Type u_1
Rₛ : Type u_2
inst✝⁷ : CommSemiring R
S : Submonoid R
inst✝⁶ : CommSemiring Rₛ
inst✝⁵ : Algebra R Rₛ
inst✝⁴ : IsLocalization S Rₛ
M : Type u_3
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : Module Rₛ M
inst✝ : IsScalarTower R Rₛ M
ι : Type u_5
b : ι → M
hli : LinearIndependent R b
⊢ LinearIndependent Rₛ b

Tactic:
have := isLocalizedModule_id S M Rₛ

Result:
R : Type u_1
Rₛ : Type u_2
inst✝⁷ : CommSemiring R
S : Submonoid R
inst✝⁶ : CommSemiring Rₛ
inst✝⁵ : Algebra R Rₛ
inst✝⁴ : IsLocalization S Rₛ
M : Type u_3
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : Module Rₛ M
inst✝ : IsScalarTower R Rₛ M
ι : Type u_5
b : ι → M
hli : LinearIndependent R b
this : IsLocalizedModule S LinearMap.id
⊢ LinearIndependent Rₛ b