harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Algebra/Order/Floor/Div.lean
lemma floorDiv_le_ceilDiv : b ⌊/⌋ a ≤ b ⌈/⌉ a

Proof state:
α : Type u_2
β : Type u_3
inst✝⁵ : LinearOrderedAddCommMonoid α
inst✝⁴ : OrderedAddCommMonoid β
inst✝³ : SMulZeroClass α β
inst✝² : PosSMulReflectLE α β
inst✝¹ : FloorDiv α β
inst✝ : CeilDiv α β
a : α
b : β
⊢ b ⌊/⌋ a ≤ b ⌈/⌉ a

Tactic:
obtain ha | ha := le_or_lt a 0

Result:
case inl
α : Type u_2
β : Type u_3
inst✝⁵ : LinearOrderedAddCommMonoid α
inst✝⁴ : OrderedAddCommMonoid β
inst✝³ : SMulZeroClass α β
inst✝² : PosSMulReflectLE α β
inst✝¹ : FloorDiv α β
inst✝ : CeilDiv α β
a : α
b : β
ha : a ≤ 0
⊢ b ⌊/⌋ a ≤ b ⌈/⌉ a

case inr
α : Type u_2
β : Type u_3
inst✝⁵ : LinearOrderedAddCommMonoid α
inst✝⁴ : OrderedAddCommMonoid β
inst✝³ : SMulZeroClass α β
inst✝² : PosSMulReflectLE α β
inst✝¹ : FloorDiv α β
inst✝ : CeilDiv α β
a : α
b : β
ha : 0 < a
⊢ b ⌊/⌋ a ≤ b ⌈/⌉ a

Proof state:
case inl
α : Type u_2
β : Type u_3
inst✝⁵ : LinearOrderedAddCommMonoid α
inst✝⁴ : OrderedAddCommMonoid β
inst✝³ : SMulZeroClass α β
inst✝² : PosSMulReflectLE α β
inst✝¹ : FloorDiv α β
inst✝ : CeilDiv α β
a : α
b : β
ha : a ≤ 0
⊢ b ⌊/⌋ a ≤ b ⌈/⌉ a

Tactic:
simp [ha]

Result:
no goals

Proof state:
case inr
α : Type u_2
β : Type u_3
inst✝⁵ : LinearOrderedAddCommMonoid α
inst✝⁴ : OrderedAddCommMonoid β
inst✝³ : SMulZeroClass α β
inst✝² : PosSMulReflectLE α β
inst✝¹ : FloorDiv α β
inst✝ : CeilDiv α β
a : α
b : β
ha : 0 < a
⊢ b ⌊/⌋ a ≤ b ⌈/⌉ a

Tactic:
exact le_of_smul_le_smul_left ((smul_floorDiv_le ha).trans <| le_smul_ceilDiv ha) ha

Result:
no goals
-- Mathlib/Data/Nat/PartENat.lean
theorem toWithTop_natCast (n : ℕ) {_ : Decidable (n : PartENat).Dom} : toWithTop n = n

Proof state:
n : ℕ
x✝ : Decidable (↑n).Dom
⊢ (↑n).toWithTop = (↑n).toWithTop

Tactic:
congr

Result:
no goals

Proof state:
n : ℕ
x✝ : Decidable (↑n).Dom
⊢ (↑n).toWithTop = ↑n

Tactic:
simp only [← toWithTop_some]

Result:
n : ℕ
x✝ : Decidable (↑n).Dom
⊢ (↑n).toWithTop = (↑n).toWithTop
-- Mathlib/Data/Fin/Basic.lean
lemma predAbove_succ_of_le (p i : Fin n) (h : p ≤ i) : p.predAbove (succ i) = i

Proof state:
n : ℕ
p i : Fin n
h : p ≤ i
⊢ p.predAbove i.succ = i

Tactic:
rw [predAbove_of_succ_le _ _ (succ_le_succ_iff.mpr h), pred_succ]

Result:
no goals
-- Mathlib/Data/Finset/Image.lean
theorem map_singleton (f : α ↪ β) (a : α) : map f {a} = {f a} :=
  coe_injective <| by simp only [coe_map, coe_singleton, Set.image_singleton]

Proof state:
α : Type u_1
β : Type u_2
f : α ↪ β
a : α
⊢ ↑(map f {a}) = ↑{f a}

Tactic:
simp only [coe_map, coe_singleton, Set.image_singleton]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem getMsbD_ofBoolListBE : (ofBoolListBE bs).getMsbD i = bs.getD i false

Proof state:
bs : List Bool
i : Nat
⊢ (ofBoolListBE bs).getMsbD i = bs.getD i false

Tactic:
induction bs generalizing i <;> cases i <;> simp_all [ofBoolListBE]

Result:
no goals
-- Mathlib/Topology/EMetricSpace/Defs.lean
theorem edist_triangle_left (x y z : α) : edist x y ≤ edist z x + edist z y

Proof state:
α : Type u
inst✝ : PseudoEMetricSpace α
x y z : α
⊢ edist x y ≤ edist x z + edist z y

Tactic:
apply edist_triangle

Result:
no goals

Proof state:
α : Type u
inst✝ : PseudoEMetricSpace α
x y z : α
⊢ edist x y ≤ edist z x + edist z y

Tactic:
rw [edist_comm z]

Result:
α : Type u
inst✝ : PseudoEMetricSpace α
x y z : α
⊢ edist x y ≤ edist x z + edist z y
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Int/DivModLemmas.lean
theorem mul_ediv_cancel_of_emod_eq_zero {a b : Int} (H : a % b = 0) : b * (a / b) = a

Proof state:
a b : Int
H : a % b = 0
this : a % b + b * (a / b) = a
⊢ b * (a / b) = a

Tactic:
rwa [H, Int.zero_add] at this

Result:
no goals

Proof state:
a b : Int
H : a % b = 0
⊢ b * (a / b) = a

Tactic:
have := emod_add_ediv a b

Result:
a b : Int
H : a % b = 0
this : a % b + b * (a / b) = a
⊢ b * (a / b) = a
-- Mathlib/LinearAlgebra/Quotient/Basic.lean
theorem mapQ_comp {R₃ M₃ : Type*} [Ring R₃] [AddCommGroup M₃] [Module R₃ M₃] (p₂ : Submodule R₂ M₂)
    (p₃ : Submodule R₃ M₃) {τ₂₃ : R₂ →+* R₃} {τ₁₃ : R →+* R₃} [RingHomCompTriple τ₁₂ τ₂₃ τ₁₃]
    (f : M →ₛₗ[τ₁₂] M₂) (g : M₂ →ₛₗ[τ₂₃] M₃) (hf : p ≤ p₂.comap f) (hg : p₂ ≤ p₃.comap g)
    (h := hf.trans (comap_mono hg)) :
    p.mapQ p₃ (g.comp f) h = (p₂.mapQ p₃ g hg).comp (p.mapQ p₂ f hf)

Proof state:
R : Type u_1
M : Type u_2
inst✝⁹ : Ring R
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
p : Submodule R M
R₂ : Type u_3
M₂ : Type u_4
inst✝⁶ : Ring R₂
inst✝⁵ : AddCommGroup M₂
inst✝⁴ : Module R₂ M₂
τ₁₂ : R →+* R₂
R₃ : Type u_5
M₃ : Type u_6
inst✝³ : Ring R₃
inst✝² : AddCommGroup M₃
inst✝¹ : Module R₃ M₃
p₂ : Submodule R₂ M₂
p₃ : Submodule R₃ M₃
τ₂₃ : R₂ →+* R₃
τ₁₃ : R →+* R₃
inst✝ : RingHomCompTriple τ₁₂ τ₂₃ τ₁₃
f : M →ₛₗ[τ₁₂] M₂
g : M₂ →ₛₗ[τ₂₃] M₃
hf : p ≤ comap f p₂
hg : p₂ ≤ comap g p₃
h : optParam (p ≤ comap f (comap g p₃)) ⋯
⊢ p.mapQ p₃ (g.comp f) h = (p₂.mapQ p₃ g hg).comp (p.mapQ p₂ f hf)

Tactic:
ext

Result:
case h.h
R : Type u_1
M : Type u_2
inst✝⁹ : Ring R
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
p : Submodule R M
R₂ : Type u_3
M₂ : Type u_4
inst✝⁶ : Ring R₂
inst✝⁵ : AddCommGroup M₂
inst✝⁴ : Module R₂ M₂
τ₁₂ : R →+* R₂
R₃ : Type u_5
M₃ : Type u_6
inst✝³ : Ring R₃
inst✝² : AddCommGroup M₃
inst✝¹ : Module R₃ M₃
p₂ : Submodule R₂ M₂
p₃ : Submodule R₃ M₃
τ₂₃ : R₂ →+* R₃
τ₁₃ : R →+* R₃
inst✝ : RingHomCompTriple τ₁₂ τ₂₃ τ₁₃
f : M →ₛₗ[τ₁₂] M₂
g : M₂ →ₛₗ[τ₂₃] M₃
hf : p ≤ comap f p₂
hg : p₂ ≤ comap g p₃
h : optParam (p ≤ comap f (comap g p₃)) ⋯
x✝ : M
⊢ ((p.mapQ p₃ (g.comp f) h).comp p.mkQ) x✝ = (((p₂.mapQ p₃ g hg).comp (p.mapQ p₂ f hf)).comp p.mkQ) x✝

Proof state:
case h.h
R : Type u_1
M : Type u_2
inst✝⁹ : Ring R
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
p : Submodule R M
R₂ : Type u_3
M₂ : Type u_4
inst✝⁶ : Ring R₂
inst✝⁵ : AddCommGroup M₂
inst✝⁴ : Module R₂ M₂
τ₁₂ : R →+* R₂
R₃ : Type u_5
M₃ : Type u_6
inst✝³ : Ring R₃
inst✝² : AddCommGroup M₃
inst✝¹ : Module R₃ M₃
p₂ : Submodule R₂ M₂
p₃ : Submodule R₃ M₃
τ₂₃ : R₂ →+* R₃
τ₁₃ : R →+* R₃
inst✝ : RingHomCompTriple τ₁₂ τ₂₃ τ₁₃
f : M →ₛₗ[τ₁₂] M₂
g : M₂ →ₛₗ[τ₂₃] M₃
hf : p ≤ comap f p₂
hg : p₂ ≤ comap g p₃
h : optParam (p ≤ comap f (comap g p₃)) ⋯
x✝ : M
⊢ ((p.mapQ p₃ (g.comp f) h).comp p.mkQ) x✝ = (((p₂.mapQ p₃ g hg).comp (p.mapQ p₂ f hf)).comp p.mkQ) x✝

Tactic:
simp

Result:
no goals
-- Mathlib/NumberTheory/Padics/PadicVal/Basic.lean
theorem padicValInt_mul_eq_succ (a : ℤ) (ha : a ≠ 0) :
    padicValInt p (a * p) = padicValInt p a + 1

Proof state:
p : ℕ
hp : Fact (Nat.Prime p)
a : ℤ
ha : a ≠ 0
⊢ padicValInt p (a * ↑p) = padicValInt p a + 1

Tactic:
rw [padicValInt.mul ha (Int.natCast_ne_zero.mpr hp.out.ne_zero)]

Result:
p : ℕ
hp : Fact (Nat.Prime p)
a : ℤ
ha : a ≠ 0
⊢ padicValInt p a + padicValInt p ↑p = padicValInt p a + 1

Proof state:
p : ℕ
hp : Fact (Nat.Prime p)
a : ℤ
ha : a ≠ 0
⊢ padicValInt p a + padicValInt p ↑p = padicValInt p a + 1

Tactic:
simp only [eq_self_iff_true, padicValInt.of_nat, padicValNat_self]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Bootstrap.lean
theorem empty_append (as : Array α) : #[] ++ as = as

Proof state:
α : Type u_1
as : Array α
⊢ #[] ++ as = as

Tactic:
apply ext'

Result:
case h
α : Type u_1
as : Array α
⊢ (#[] ++ as).toList = as.toList

Proof state:
case h
α : Type u_1
as : Array α
⊢ (#[] ++ as).toList = as.toList

Tactic:
simp only [toList_append, toList_empty, List.nil_append]

Result:
no goals
-- Mathlib/Analysis/Calculus/UniformLimitsDeriv.lean
theorem uniformCauchySeqOnFilter_of_deriv (hf' : UniformCauchySeqOnFilter f' l (𝓝 x))
    (hf : ∀ᶠ n : ι × 𝕜 in l ×ˢ 𝓝 x, HasDerivAt (f n.1) (f' n.1 n.2) n.2)
    (hfg : Cauchy (map (fun n => f n x) l)) : UniformCauchySeqOnFilter f l (𝓝 x)

Proof state:
ι : Type u_1
l : Filter ι
𝕜 : Type u_2
inst✝³ : NontriviallyNormedField 𝕜
G : Type u_3
inst✝² : NormedAddCommGroup G
inst✝¹ : NormedSpace 𝕜 G
f f' : ι → 𝕜 → G
x : 𝕜
inst✝ : IsRCLikeNormedField 𝕜
hf' : UniformCauchySeqOnFilter f' l (𝓝 x)
hfg : Cauchy (map (fun n => f n x) l)
hf : ∀ᶠ (n : ι × 𝕜) in l ×ˢ 𝓝 x, HasFDerivAt (f n.1) (ContinuousLinearMap.smulRight 1 (f' n.1 n.2)) n.2
⊢ UniformCauchySeqOnFilter f l (𝓝 x)

Tactic:
exact uniformCauchySeqOnFilter_of_fderiv hf'.one_smulRight hf hfg

Result:
no goals

Proof state:
ι : Type u_1
l : Filter ι
𝕜 : Type u_2
inst✝³ : NontriviallyNormedField 𝕜
G : Type u_3
inst✝² : NormedAddCommGroup G
inst✝¹ : NormedSpace 𝕜 G
f f' : ι → 𝕜 → G
x : 𝕜
inst✝ : IsRCLikeNormedField 𝕜
hf' : UniformCauchySeqOnFilter f' l (𝓝 x)
hf : ∀ᶠ (n : ι × 𝕜) in l ×ˢ 𝓝 x, HasDerivAt (f n.1) (f' n.1 n.2) n.2
hfg : Cauchy (map (fun n => f n x) l)
⊢ UniformCauchySeqOnFilter f l (𝓝 x)

Tactic:
simp_rw [hasDerivAt_iff_hasFDerivAt] at hf

Result:
ι : Type u_1
l : Filter ι
𝕜 : Type u_2
inst✝³ : NontriviallyNormedField 𝕜
G : Type u_3
inst✝² : NormedAddCommGroup G
inst✝¹ : NormedSpace 𝕜 G
f f' : ι → 𝕜 → G
x : 𝕜
inst✝ : IsRCLikeNormedField 𝕜
hf' : UniformCauchySeqOnFilter f' l (𝓝 x)
hfg : Cauchy (map (fun n => f n x) l)
hf : ∀ᶠ (n : ι × 𝕜) in l ×ˢ 𝓝 x, HasFDerivAt (f n.1) (ContinuousLinearMap.smulRight 1 (f' n.1 n.2)) n.2
⊢ UniformCauchySeqOnFilter f l (𝓝 x)
-- Mathlib/Analysis/Matrix.lean
theorem frobenius_norm_def (A : Matrix m n α) :
    ‖A‖ = (∑ i, ∑ j, ‖A i j‖ ^ (2 : ℝ)) ^ (1 / 2 : ℝ) :=
  (congr_arg ((↑) : ℝ≥0 → ℝ) (frobenius_nnnorm_def A)).trans <| by simp [NNReal.coe_sum]

Proof state:
m : Type u_3
n : Type u_4
α : Type u_5
inst✝² : Fintype m
inst✝¹ : Fintype n
inst✝ : SeminormedAddCommGroup α
A : Matrix m n α
⊢ ↑((∑ i : m, ∑ j : n, ‖A i j‖₊ ^ 2) ^ (1 / 2)) = (∑ i : m, ∑ j : n, ‖A i j‖ ^ 2) ^ (1 / 2)

Tactic:
simp [NNReal.coe_sum]

Result:
no goals
-- Mathlib/Combinatorics/Additive/AP/Three/Defs.lean
theorem ThreeGPFree.smul_set (hs : ThreeGPFree s) : ThreeGPFree (a • s)

Proof state:
α : Type u_2
inst✝ : CancelCommMonoid α
s : Set α
a : α
hs : ThreeGPFree s
⊢ ThreeGPFree (a • s)

Tactic:
rintro _ ⟨b, hb, rfl⟩ _ ⟨c, hc, rfl⟩ _ ⟨d, hd, rfl⟩ h

Result:
case intro.intro.intro.intro.intro.intro
α : Type u_2
inst✝ : CancelCommMonoid α
s : Set α
a : α
hs : ThreeGPFree s
b : α
hb : b ∈ s
c : α
hc : c ∈ s
d : α
hd : d ∈ s
h : (fun x => a • x) b * (fun x => a • x) d = (fun x => a • x) c * (fun x => a • x) c
⊢ (fun x => a • x) b = (fun x => a • x) c

Proof state:
α : Type u_2
inst✝ : CancelCommMonoid α
s : Set α
a : α
hs : ThreeGPFree s
b : α
hb : b ∈ s
c : α
hc : c ∈ s
d : α
hd : d ∈ s
h : (fun x => a • x) b * (fun x => a • x) d = (fun x => a • x) c * (fun x => a • x) c
⊢ b * d = c * c

Tactic:
simpa [mul_mul_mul_comm _ _ a] using h

Result:
no goals
-- Mathlib/NumberTheory/NumberField/CanonicalEmbedding/Basic.lean
theorem normAtPlace_neg (w : InfinitePlace K) (x : mixedSpace K)  :
    normAtPlace w (- x) = normAtPlace w x

Proof state:
K : Type u_1
inst✝ : Field K
w : InfinitePlace K
x : mixedSpace K
⊢ (normAtPlace w) (-x) = (normAtPlace w) x

Tactic:
rw [normAtPlace, MonoidWithZeroHom.coe_mk, ZeroHom.coe_mk]

Result:
K : Type u_1
inst✝ : Field K
w : InfinitePlace K
x : mixedSpace K
⊢ (if hw : w.IsReal then ‖(-x).1 ⟨w, hw⟩‖ else ‖(-x).2 ⟨w, ⋯⟩‖) = if hw : w.IsReal then ‖x.1 ⟨w, hw⟩‖ else ‖x.2 ⟨w, ⋯⟩‖

Proof state:
K : Type u_1
inst✝ : Field K
w : InfinitePlace K
x : mixedSpace K
⊢ (if hw : w.IsReal then ‖(-x).1 ⟨w, hw⟩‖ else ‖(-x).2 ⟨w, ⋯⟩‖) = if hw : w.IsReal then ‖x.1 ⟨w, hw⟩‖ else ‖x.2 ⟨w, ⋯⟩‖

Tactic:
split_ifs <;> simp

Result:
no goals
-- Mathlib/LinearAlgebra/Matrix/Charpoly/LinearMap.lean
theorem Matrix.Represents.smul {A : Matrix ι ι R} {f : Module.End R M} (h : A.Represents b f)
    (r : R) : (r • A).Represents b (r • f)

Proof state:
ι : Type u_1
inst✝⁴ : Fintype ι
M : Type u_2
inst✝³ : AddCommGroup M
R : Type u_3
inst✝² : CommRing R
inst✝¹ : Module R M
b : ι → M
inst✝ : DecidableEq ι
A : Matrix ι ι R
f : Module.End R M
h : (PiToModule.fromMatrix R b) A = (PiToModule.fromEnd R b) f
r : R
⊢ (PiToModule.fromMatrix R b) (r • A) = (PiToModule.fromEnd R b) (r • f)

Tactic:
rw [_root_.map_smul, _root_.map_smul, h]

Result:
no goals

Proof state:
ι : Type u_1
inst✝⁴ : Fintype ι
M : Type u_2
inst✝³ : AddCommGroup M
R : Type u_3
inst✝² : CommRing R
inst✝¹ : Module R M
b : ι → M
inst✝ : DecidableEq ι
A : Matrix ι ι R
f : Module.End R M
h : Represents b A f
r : R
⊢ Represents b (r • A) (r • f)

Tactic:
delta Matrix.Represents at h ⊢

Result:
ι : Type u_1
inst✝⁴ : Fintype ι
M : Type u_2
inst✝³ : AddCommGroup M
R : Type u_3
inst✝² : CommRing R
inst✝¹ : Module R M
b : ι → M
inst✝ : DecidableEq ι
A : Matrix ι ι R
f : Module.End R M
h : (PiToModule.fromMatrix R b) A = (PiToModule.fromEnd R b) f
r : R
⊢ (PiToModule.fromMatrix R b) (r • A) = (PiToModule.fromEnd R b) (r • f)
-- Mathlib/NumberTheory/Pell.lean
theorem zpow_eq_one_iff {a : Solution₁ d} (h : IsFundamental a) (n : ℤ) : a ^ n = 1 ↔ n = 0

Proof state:
d : ℤ
a : Solution₁ d
h : IsFundamental a
n : ℤ
⊢ a ^ n = 1 ↔ n = 0

Tactic:
rw [← zpow_zero a]

Result:
d : ℤ
a : Solution₁ d
h : IsFundamental a
n : ℤ
⊢ a ^ n = a ^ 0 ↔ n = 0

Proof state:
d : ℤ
a : Solution₁ d
h : IsFundamental a
n : ℤ
⊢ a ^ n = a ^ 0 ↔ n = 0

Tactic:
exact ⟨fun H => h.y_strictMono.injective (congr_arg Solution₁.y H), fun H => H ▸ rfl⟩

Result:
no goals
-- Mathlib/RingTheory/UniqueFactorizationDomain/Defs.lean
theorem exists_prime_factors (a : α) :
    a ≠ 0 → ∃ f : Multiset α, (∀ b ∈ f, Prime b) ∧ f.prod ~ᵤ a

Proof state:
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
a : α
⊢ a ≠ 0 → ∃ f, (∀ b ∈ f, Prime b) ∧ f.prod ~ᵤ a

Tactic:
simp_rw [← UniqueFactorizationMonoid.irreducible_iff_prime]

Result:
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
a : α
⊢ a ≠ 0 → ∃ f, (∀ b ∈ f, Irreducible b) ∧ f.prod ~ᵤ a

Proof state:
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
a : α
⊢ a ≠ 0 → ∃ f, (∀ b ∈ f, Irreducible b) ∧ f.prod ~ᵤ a

Tactic:
apply WfDvdMonoid.exists_factors a

Result:
no goals
-- Mathlib/Order/ConditionallyCompleteLattice/Indexed.lean
theorem le_ciSup_iff' {s : ι → α} {a : α} (h : BddAbove (range s)) :
    a ≤ iSup s ↔ ∀ b, (∀ i, s i ≤ b) → a ≤ b

Proof state:
α : Type u_1
ι : Sort u_4
inst✝ : ConditionallyCompleteLinearOrderBot α
s : ι → α
a : α
h : BddAbove (range s)
⊢ a ≤ iSup s ↔ ∀ (b : α), (∀ (i : ι), s i ≤ b) → a ≤ b

Tactic:
simp [iSup, h, le_csSup_iff', upperBounds]

Result:
no goals
-- Mathlib/Analysis/Convex/Gauge.lean
theorem gauge_unit_ball (x : E) : gauge (ball (0 : E) 1) x = ‖x‖

Proof state:
E : Type u_2
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x : E
⊢ gauge (ball 0 1) x = ‖x‖

Tactic:
rw [← ball_normSeminorm ℝ, Seminorm.gauge_ball, coe_normSeminorm]

Result:
no goals
-- Mathlib/Data/Matrix/Mul.lean
theorem smul_eq_diagonal_mul [Fintype m] [DecidableEq m] (M : Matrix m n α) (a : α) :
    a • M = (diagonal fun _ => a) * M

Proof state:
case a
m : Type u_2
n : Type u_3
α : Type v
inst✝² : NonUnitalNonAssocSemiring α
inst✝¹ : Fintype m
inst✝ : DecidableEq m
M : Matrix m n α
a : α
i✝ : m
j✝ : n
⊢ (a • M) i✝ j✝ = ((diagonal fun x => a) * M) i✝ j✝

Tactic:
simp

Result:
no goals

Proof state:
m : Type u_2
n : Type u_3
α : Type v
inst✝² : NonUnitalNonAssocSemiring α
inst✝¹ : Fintype m
inst✝ : DecidableEq m
M : Matrix m n α
a : α
⊢ a • M = (diagonal fun x => a) * M

Tactic:
ext

Result:
case a
m : Type u_2
n : Type u_3
α : Type v
inst✝² : NonUnitalNonAssocSemiring α
inst✝¹ : Fintype m
inst✝ : DecidableEq m
M : Matrix m n α
a : α
i✝ : m
j✝ : n
⊢ (a • M) i✝ j✝ = ((diagonal fun x => a) * M) i✝ j✝
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lex/Lemmas.lean
theorem lex_eq_true_iff_lt [DecidableEq α] [LT α] [DecidableLT α]
    {l₁ l₂ : Array α} : lex l₁ l₂ = true ↔ l₁ < l₂

Proof state:
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : LT α
inst✝ : DecidableLT α
l₁ l₂ : Array α
⊢ (l₁.lex l₂ fun x1 x2 => decide (x1 < x2)) = true ↔ l₁ < l₂

Tactic:
cases l₁

Result:
case mk
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : LT α
inst✝ : DecidableLT α
l₂ : Array α
toList✝ : List α
⊢ ({ toList := toList✝ }.lex l₂ fun x1 x2 => decide (x1 < x2)) = true ↔ { toList := toList✝ } < l₂

Proof state:
case mk.mk
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : LT α
inst✝ : DecidableLT α
toList✝¹ toList✝ : List α
⊢ ({ toList := toList✝¹ }.lex { toList := toList✝ } fun x1 x2 => decide (x1 < x2)) = true ↔
    { toList := toList✝¹ } < { toList := toList✝ }

Tactic:
simp

Result:
no goals

Proof state:
case mk
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : LT α
inst✝ : DecidableLT α
l₂ : Array α
toList✝ : List α
⊢ ({ toList := toList✝ }.lex l₂ fun x1 x2 => decide (x1 < x2)) = true ↔ { toList := toList✝ } < l₂

Tactic:
cases l₂

Result:
case mk.mk
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : LT α
inst✝ : DecidableLT α
toList✝¹ toList✝ : List α
⊢ ({ toList := toList✝¹ }.lex { toList := toList✝ } fun x1 x2 => decide (x1 < x2)) = true ↔
    { toList := toList✝¹ } < { toList := toList✝ }
-- Mathlib/Data/Finsupp/Single.lean
theorem support_subset_singleton' {f : α →₀ M} {a : α} : f.support ⊆ {a} ↔ ∃ b, f = single a b :=
  ⟨fun h => ⟨f a, support_subset_singleton.mp h⟩, fun ⟨b, hb⟩ => by
    rw [hb, support_subset_singleton, single_eq_same]⟩

Proof state:
α : Type u_1
M : Type u_5
inst✝ : Zero M
f : α →₀ M
a : α
x✝ : ∃ b, f = single a b
b : M
hb : f = single a b
⊢ f.support ⊆ {a}

Tactic:
rw [hb, support_subset_singleton, single_eq_same]

Result:
no goals
-- Mathlib/Order/Interval/Set/SurjOn.lean
theorem surjOn_Ioi_of_monotone_surjective (h_mono : Monotone f) (h_surj : Function.Surjective f)
    (a : α) : SurjOn f (Ioi a) (Ioi (f a))

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : PartialOrder β
f : α → β
h_mono : Monotone f
h_surj : Surjective f
a : α
⊢ MapsTo f (Iic a) (Ioi (f a))ᶜ

Tactic:
exact fun x hx => (h_mono hx).not_lt

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : PartialOrder β
f : α → β
h_mono : Monotone f
h_surj : Surjective f
a : α
⊢ SurjOn f (Ioi a) (Ioi (f a))

Tactic:
rw [← compl_Iic, ← compl_compl (Ioi (f a))]

Result:
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : PartialOrder β
f : α → β
h_mono : Monotone f
h_surj : Surjective f
a : α
⊢ SurjOn f (Iic a)ᶜ (Ioi (f a))ᶜᶜ

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : PartialOrder β
f : α → β
h_mono : Monotone f
h_surj : Surjective f
a : α
⊢ SurjOn f (Iic a)ᶜ (Ioi (f a))ᶜᶜ

Tactic:
refine MapsTo.surjOn_compl ?_ h_surj

Result:
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : PartialOrder β
f : α → β
h_mono : Monotone f
h_surj : Surjective f
a : α
⊢ MapsTo f (Iic a) (Ioi (f a))ᶜ
-- Mathlib/.lake/packages/lean4/src/lean/Init/ByCases.lean
theorem dite_some_none_eq_some [Decidable P] {x : P → α} {y : α} :
    (if h : P then some (x h) else none) = some y ↔ ∃ h : P, x h = y

Proof state:
P : Prop
α : Type u_1
inst✝ : Decidable P
x : P → α
y : α
⊢ (if h : P then some (x h) else none) = some y ↔ ∃ h, x h = y

Tactic:
by_cases h : P <;> simp [h]

Result:
no goals
-- Mathlib/Algebra/Order/Floor.lean
theorem ceil_intCast (z : ℤ) : ⌈(z : α)⌉ = z :=
  eq_of_forall_ge_iff fun a => by rw [ceil_le, Int.cast_le]

Proof state:
α : Type u_2
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
z a : ℤ
⊢ ⌈↑z⌉ ≤ a ↔ z ≤ a

Tactic:
rw [ceil_le, Int.cast_le]

Result:
no goals
-- Mathlib/Algebra/Group/Basic.lean
theorem mul_left_comm (a b c : G) : a * (b * c) = b * (a * c)

Proof state:
G : Type u_3
inst✝ : CommSemigroup G
a b c : G
⊢ a * (b * c) = b * (a * c)

Tactic:
rw [← mul_assoc, mul_comm a, mul_assoc]

Result:
no goals
-- Mathlib/Analysis/Convex/Side.lean
theorem not_sOppSide_self (s : AffineSubspace R P) (x : P) : ¬s.SOppSide x x

Proof state:
R : Type u_1
V : Type u_2
P : Type u_4
inst✝³ : LinearOrderedField R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
s : AffineSubspace R P
x : P
⊢ ¬s.SOppSide x x

Tactic:
rw [SOppSide]

Result:
R : Type u_1
V : Type u_2
P : Type u_4
inst✝³ : LinearOrderedField R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
s : AffineSubspace R P
x : P
⊢ ¬(s.WOppSide x x ∧ x ∉ s ∧ x ∉ s)

Proof state:
R : Type u_1
V : Type u_2
P : Type u_4
inst✝³ : LinearOrderedField R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
s : AffineSubspace R P
x : P
⊢ ¬(s.WOppSide x x ∧ x ∉ s ∧ x ∉ s)

Tactic:
simp

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/Model.lean
theorem insert_eq_insertₘ [BEq α] [Hashable α] (m : Raw₀ α β) (a : α) (b : β a) :
    m.insert a b = m.insertₘ a b

Proof state:
case isTrue
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : Hashable α
m : Raw₀ α β
a : α
b : β a
h✝ : AssocList.contains a m.1.buckets[(mkIdx m.1.buckets.size ⋯ (hash a)).val.toNat] = true
⊢ m.1.buckets.set (mkIdx m.1.buckets.size ⋯ (hash a)).val.toNat
      (AssocList.replace a b m.1.buckets[(mkIdx m.1.buckets.size ⋯ (hash a)).val.toNat]) ⋯ =
    match mkIdx m.val.buckets.size ⋯ (hash a) with
    | ⟨i, h⟩ => m.val.buckets.uset i (AssocList.replace a b m.val.buckets[i]) h

Tactic:
simp only [Array.uset, Array.ugetElem_eq_getElem]

Result:
no goals
-- Mathlib/Data/Matroid/Basic.lean
/-- If every base of `M₁` is independent in `M₂` and vice versa, then `M₁ = M₂`. -/
lemma ext_isBase_indep {M₁ M₂ : Matroid α} (hE : M₁.E = M₂.E)
    (hM₁ : ∀ ⦃B⦄, M₁.IsBase B → M₂.Indep B) (hM₂ : ∀ ⦃B⦄, M₂.IsBase B → M₁.Indep B) : M₁ = M₂

Proof state:
case refine_1
α : Type u_1
M₁ M₂ : Matroid α
hE : M₁.E = M₂.E
hM₁ : ∀ ⦃B : Set α⦄, M₁.IsBase B → M₂.Indep B
hM₂ : ∀ ⦃B : Set α⦄, M₂.IsBase B → M₁.Indep B
I : Set α
hIE : I ⊆ M₁.E
hI : M₁.Indep I
⊢ M₂.Indep I

Tactic:
obtain ⟨B, hB, hIB⟩ := hI.exists_isBase_superset

Result:
case refine_1.intro.intro
α : Type u_1
M₁ M₂ : Matroid α
hE : M₁.E = M₂.E
hM₁ : ∀ ⦃B : Set α⦄, M₁.IsBase B → M₂.Indep B
hM₂ : ∀ ⦃B : Set α⦄, M₂.IsBase B → M₁.Indep B
I : Set α
hIE : I ⊆ M₁.E
hI : M₁.Indep I
B : Set α
hB : M₁.IsBase B
hIB : I ⊆ B
⊢ M₂.Indep I

Proof state:
α : Type u_1
M₁ M₂ : Matroid α
hE : M₁.E = M₂.E
hM₁ : ∀ ⦃B : Set α⦄, M₁.IsBase B → M₂.Indep B
hM₂ : ∀ ⦃B : Set α⦄, M₂.IsBase B → M₁.Indep B
⊢ M₁ = M₂

Tactic:
refine ext_indep hE fun I hIE ↦ ⟨fun hI ↦ ?_, fun hI ↦ ?_⟩

Result:
case refine_1
α : Type u_1
M₁ M₂ : Matroid α
hE : M₁.E = M₂.E
hM₁ : ∀ ⦃B : Set α⦄, M₁.IsBase B → M₂.Indep B
hM₂ : ∀ ⦃B : Set α⦄, M₂.IsBase B → M₁.Indep B
I : Set α
hIE : I ⊆ M₁.E
hI : M₁.Indep I
⊢ M₂.Indep I

case refine_2
α : Type u_1
M₁ M₂ : Matroid α
hE : M₁.E = M₂.E
hM₁ : ∀ ⦃B : Set α⦄, M₁.IsBase B → M₂.Indep B
hM₂ : ∀ ⦃B : Set α⦄, M₂.IsBase B → M₁.Indep B
I : Set α
hIE : I ⊆ M₁.E
hI : M₂.Indep I
⊢ M₁.Indep I

Proof state:
case refine_2
α : Type u_1
M₁ M₂ : Matroid α
hE : M₁.E = M₂.E
hM₁ : ∀ ⦃B : Set α⦄, M₁.IsBase B → M₂.Indep B
hM₂ : ∀ ⦃B : Set α⦄, M₂.IsBase B → M₁.Indep B
I : Set α
hIE : I ⊆ M₁.E
hI : M₂.Indep I
⊢ M₁.Indep I

Tactic:
obtain ⟨B, hB, hIB⟩ := hI.exists_isBase_superset

Result:
case refine_2.intro.intro
α : Type u_1
M₁ M₂ : Matroid α
hE : M₁.E = M₂.E
hM₁ : ∀ ⦃B : Set α⦄, M₁.IsBase B → M₂.Indep B
hM₂ : ∀ ⦃B : Set α⦄, M₂.IsBase B → M₁.Indep B
I : Set α
hIE : I ⊆ M₁.E
hI : M₂.Indep I
B : Set α
hB : M₂.IsBase B
hIB : I ⊆ B
⊢ M₁.Indep I

Proof state:
case refine_2.intro.intro
α : Type u_1
M₁ M₂ : Matroid α
hE : M₁.E = M₂.E
hM₁ : ∀ ⦃B : Set α⦄, M₁.IsBase B → M₂.Indep B
hM₂ : ∀ ⦃B : Set α⦄, M₂.IsBase B → M₁.Indep B
I : Set α
hIE : I ⊆ M₁.E
hI : M₂.Indep I
B : Set α
hB : M₂.IsBase B
hIB : I ⊆ B
⊢ M₁.Indep I

Tactic:
exact (hM₂ hB).subset hIB

Result:
no goals

Proof state:
case refine_1.intro.intro
α : Type u_1
M₁ M₂ : Matroid α
hE : M₁.E = M₂.E
hM₁ : ∀ ⦃B : Set α⦄, M₁.IsBase B → M₂.Indep B
hM₂ : ∀ ⦃B : Set α⦄, M₂.IsBase B → M₁.Indep B
I : Set α
hIE : I ⊆ M₁.E
hI : M₁.Indep I
B : Set α
hB : M₁.IsBase B
hIB : I ⊆ B
⊢ M₂.Indep I

Tactic:
exact (hM₁ hB).subset hIB

Result:
no goals
-- Mathlib/Algebra/Homology/HomotopyCategory/HomComplexShift.lean
@[simp]
lemma leftShift_comp_zero_cochain (a n' : ℤ) (hn' : n + a = n') (γ' : Cochain L M 0) :
    (γ.comp γ' (add_zero n)).leftShift a n' hn' =
      (γ.leftShift a n' hn').comp γ' (add_zero n')

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
K L M : CochainComplex C ℤ
n : ℤ
γ : Cochain K L n
a n' : ℤ
hn' : n + a = n'
γ' : Cochain L M 0
⊢ (γ.comp γ' ⋯).leftShift a n' hn' = (γ.leftShift a n' hn').comp γ' ⋯

Tactic:
rw [leftShift_comp γ a n' hn' γ' (add_zero _) hn', mul_zero, Int.negOnePow_zero, one_smul]

Result:
no goals