harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/NumberTheory/Padics/PadicVal/Basic.lean
theorem padicValNat_choose' {n k b : ℕ} [hp : Fact p.Prime] (hnb : log p (n + k) < b) :
    padicValNat p (choose (n + k) k) =
    ((Finset.Ico 1 b).filter fun i => p ^ i ≤ k % p ^ i + n % p ^ i).card

Proof state:
p n k b : ℕ
hp : Fact (Nat.Prime p)
hnb : log p (n + k) < b
⊢ padicValNat p ((n + k).choose k) = (Finset.filter (fun i => p ^ i ≤ k % p ^ i + n % p ^ i) (Finset.Ico 1 b)).card

Tactic:
exact_mod_cast (padicValNat_eq_emultiplicity (p := p) <| choose_pos <|
  Nat.le_add_left k n)▸ Prime.emultiplicity_choose' hp.out hnb

Result:
no goals
-- Mathlib/Topology/Algebra/Group/Basic.lean
theorem map_mul_right_nhds_one (x : G) : map (· * x) (𝓝 1) = 𝓝 x

Proof state:
G : Type w
inst✝² : TopologicalSpace G
inst✝¹ : Group G
inst✝ : IsTopologicalGroup G
x : G
⊢ map (fun x_1 => x_1 * x) (𝓝 1) = 𝓝 x

Tactic:
simp

Result:
no goals
-- Mathlib/Analysis/Convex/EGauge.lean
lemma egauge_ball_one_le_of_one_lt_norm (hc : 1 < ‖c‖) (x : E) :
    egauge 𝕜 (ball 0 1) x ≤ ‖c‖ₑ * ‖x‖ₑ

Proof state:
𝕜 : Type u_1
inst✝² : NormedField 𝕜
E : Type u_2
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
c : 𝕜
hc : 1 < ‖c‖
x : E
⊢ egauge 𝕜 (ball 0 1) x ≤ ‖c‖ₑ * ‖x‖ₑ

Tactic:
simpa using egauge_ball_le_of_one_lt_norm hc (.inl one_ne_zero)

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Nat/Range.lean
theorem iota_ne_nil {n : Nat} : iota n ≠ [] ↔ n ≠ 0

Proof state:
n : Nat
⊢ iota n ≠ [] ↔ n ≠ 0

Tactic:
cases n <;> simp

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Pow/NNReal.lean
theorem rpow_inv_lt_iff {x y : ℝ≥0} {z : ℝ} (hz : 0 < z) : x ^ z⁻¹ < y ↔ x < y ^ z

Proof state:
x y : ℝ≥0
z : ℝ
hz : 0 < z
⊢ x ^ z⁻¹ < y ↔ x < y ^ z

Tactic:
simp only [← not_le, le_rpow_inv_iff hz]

Result:
no goals
-- Mathlib/Algebra/Ring/InjSurj.lean
theorem rightDistribClass [Mul α] [Add α] [RightDistribClass α] (add : ∀ x y, f (x + y) = f x + f y)
    (mul : ∀ x y, f (x * y) = f x * f y) : RightDistribClass β where
  right_distrib := hf.forall₃.2 fun x y z => by simp only [← add, ← mul, right_distrib]

Proof state:
α : Type u_1
β : Type u_2
f : α → β
hf : Surjective f
inst✝⁴ : Add β
inst✝³ : Mul β
inst✝² : Mul α
inst✝¹ : Add α
inst✝ : RightDistribClass α
add : ∀ (x y : α), f (x + y) = f x + f y
mul : ∀ (x y : α), f (x * y) = f x * f y
x y z : α
⊢ (f x + f y) * f z = f x * f z + f y * f z

Tactic:
simp only [← add, ← mul, right_distrib]

Result:
no goals
-- Mathlib/Algebra/Module/Torsion.lean
theorem isTorsionBy_iff_mem_annihilator {a : R} :
    IsTorsionBy R M a ↔ a ∈ annihilator R M

Proof state:
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
a : R
⊢ IsTorsionBy R M a ↔ a ∈ annihilator R M

Tactic:
rw [IsTorsionBy, mem_annihilator]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Bitblast.lean
theorem mod_two_pow_succ (x i : Nat) :
    x % 2^(i+1) = 2^i*(x.testBit i).toNat + x % (2 ^ i)

Proof state:
x i : Nat
⊢ x % 2 ^ (i + 1) = 2 ^ i * (x.testBit i).toNat + x % 2 ^ i

Tactic:
rw [Nat.mod_pow_succ, Nat.add_comm, Nat.toNat_testBit]

Result:
no goals
-- Mathlib/.lake/packages/batteries/Batteries/Data/AssocList.lean
theorem all_eq (p : α → β → Bool) (l : AssocList α β) :
    all p l = l.toList.all fun (a, b) => p a b

Proof state:
α : Type u_1
β : Type u_2
p : α → β → Bool
l : AssocList α β
⊢ all p l =
    l.toList.all fun x =>
      match x with
      | (a, b) => p a b

Tactic:
induction l <;> simp [all, *]

Result:
no goals
-- Mathlib/Algebra/Homology/ShortComplex/Homology.lean
@[reassoc]
lemma leftHomologyIso_hom_naturality :
    S₁.leftHomologyIso.hom ≫ homologyMap φ =
      leftHomologyMap φ ≫ S₂.leftHomologyIso.hom

Proof state:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroMorphisms C
S₁ S₂ : ShortComplex C
inst✝¹ : S₁.HasHomology
inst✝ : S₂.HasHomology
φ : S₁ ⟶ S₂
⊢ S₁.leftHomologyIso.hom ≫ homologyMap φ = leftHomologyMap φ ≫ S₂.leftHomologyIso.hom

Tactic:
simpa only [LeftHomologyData.homologyIso_leftHomologyData, Iso.symm_inv] using
  LeftHomologyData.leftHomologyIso_inv_naturality φ S₁.leftHomologyData S₂.leftHomologyData

Result:
no goals
-- Mathlib/Order/Irreducible.lean
theorem InfPrime.infIrred : InfPrime a → InfIrred a :=
  And.imp_right fun h b c ha => by simpa [← ha] using h ha.le

Proof state:
α : Type u_2
inst✝ : SemilatticeInf α
a : α
h : ∀ ⦃b c : α⦄, b ⊓ c ≤ a → b ≤ a ∨ c ≤ a
b c : α
ha : b ⊓ c = a
⊢ b = a ∨ c = a

Tactic:
simpa [← ha] using h ha.le

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Lemmas.lean
theorem map_eq_foldr (f : α → β) (l : List α) : map f l = foldr (fun a bs => f a :: bs) [] l

Proof state:
α : Type u_1
β : Type u_2
f : α → β
l : List α
⊢ map f l = foldr (fun a bs => f a :: bs) [] l

Tactic:
induction l <;> simp [*]

Result:
no goals
-- Mathlib/Tactic/CategoryTheory/Bicategory/Normalize.lean
theorem evalComp_nil_nil (α : f ≅ g) (β : g ≅ h) :
    (α ≪≫ β).hom = (α ≪≫ β).hom

Proof state:
B : Type u
inst✝ : Bicategory B
a b : B
f g h : a ⟶ b
α : f ≅ g
β : g ≅ h
⊢ (α ≪≫ β).hom = (α ≪≫ β).hom

Tactic:
simp

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Int/Lemmas.lean
theorem sub_right_inj {i j : Int} (k : Int) : (k - i = k - j) ↔ i = j

Proof state:
i j k : Int
⊢ k - i = k - j ↔ i = j

Tactic:
simp [Int.sub_eq_add_neg, Int.neg_inj]

Result:
no goals
-- Mathlib/Algebra/BigOperators/Balance.lean
@[simp] lemma balance_neg (f : ι → G) : balance (-f) = -balance f

Proof state:
ι : Type u_1
G : Type u_4
inst✝² : Fintype ι
inst✝¹ : AddCommGroup G
inst✝ : Module ℚ≥0 G
f : ι → G
⊢ balance (-f) = -balance f

Tactic:
simp only [balance, expect_neg_distrib, const_neg, neg_sub', Pi.neg_apply]

Result:
no goals
-- Mathlib/Order/SuccPred/Basic.lean
theorem succ_unbot :
    ∀ (a : WithBot α) (ha : a ≠ ⊥),
      succ (a.unbot ha) = (succ a).unbot (by induction a <;> simp)
  | ⊥, ha => (ha rfl).elim
  | (a : α), _ => rfl

Proof state:
α : Type u_1
β : Type u_2
inst✝² : Preorder α
inst✝¹ : OrderBot α
inst✝ : SuccOrder α
a : WithBot α
ha : a ≠ ⊥
⊢ succ a ≠ ⊥

Tactic:
induction a <;> simp

Result:
no goals
-- Mathlib/RingTheory/MvPowerSeries/Inverse.lean
theorem inv_mul_cancel (φ : MvPowerSeries σ k) (h : constantCoeff σ k φ ≠ 0) :
    φ⁻¹ * φ = 1

Proof state:
σ : Type u_1
k : Type u_3
inst✝ : Field k
φ : MvPowerSeries σ k
h : (constantCoeff σ k) φ ≠ 0
⊢ φ⁻¹ * φ = 1

Tactic:
rw [mul_comm, φ.mul_inv_cancel h]

Result:
no goals
-- Mathlib/Data/String/Lemmas.lean
/-- The length of the String returned by `String.leftpad n a c` is equal
  to the larger of `n` and `s.length` -/
@[simp] lemma leftpad_length (n : ℕ) (c : Char) :
    ∀ (s : String), (leftpad n c s).length = max n s.length
  | ⟨s⟩ => by simp only [leftpad, String.length, List.leftpad_length]

Proof state:
n : ℕ
c : Char
s : List Char
⊢ (leftpad n c { data := s }).length = max n { data := s }.length

Tactic:
simp only [leftpad, String.length, List.leftpad_length]

Result:
no goals
-- Mathlib/Algebra/Order/Module/Defs.lean
lemma smul_pos [PosSMulStrictMono α β] (ha : 0 < a) (hb : 0 < b) : 0 < a • b

Proof state:
α : Type u_1
β : Type u_2
a : α
b : β
inst✝⁵ : Zero α
inst✝⁴ : Zero β
inst✝³ : SMulZeroClass α β
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : PosSMulStrictMono α β
ha : 0 < a
hb : 0 < b
⊢ 0 < a • b

Tactic:
simpa only [smul_zero] using smul_lt_smul_of_pos_left hb ha

Result:
no goals
-- Mathlib/MeasureTheory/MeasurableSpace/Invariants.lean
theorem inf_le_invariants_comp (f g : α → α) :
    invariants f ⊓ invariants g ≤ invariants (f ∘ g) := fun s hs ↦
  ⟨hs.1.1, by rw [preimage_comp, hs.1.2, hs.2.2]⟩

Proof state:
α : Type u_1
inst✝ : MeasurableSpace α
f g : α → α
s : Set α
hs : MeasurableSet s
⊢ f ∘ g ⁻¹' s = s

Tactic:
rw [preimage_comp, hs.1.2, hs.2.2]

Result:
no goals
-- Mathlib/Algebra/Order/GroupWithZero/Unbundled.lean
theorem mul_lt_of_lt_one_right [PosMulStrictMono α] (ha : 0 < a) (h : b < 1) : a * b < a

Proof state:
α : Type u_3
a b : α
inst✝³ : MulOneClass α
inst✝² : Zero α
inst✝¹ : Preorder α
inst✝ : PosMulStrictMono α
ha : 0 < a
h : b < 1
⊢ a * b < a

Tactic:
simpa only [mul_one] using mul_lt_mul_of_pos_left h ha

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Log/NegMulLog.lean
lemma negMulLog_nonneg {x : ℝ} (h1 : 0 ≤ x) (h2 : x ≤ 1) : 0 ≤ negMulLog x

Proof state:
x : ℝ
h1 : 0 ≤ x
h2 : x ≤ 1
⊢ 0 ≤ x.negMulLog

Tactic:
simpa only [negMulLog_eq_neg, neg_nonneg] using mul_log_nonpos h1 h2

Result:
no goals
-- Mathlib/.lake/packages/batteries/Batteries/Data/Array/Lemmas.lean
theorem size_insertIdx (as : Array α) (i : Nat) (h : i ≤ as.size) (v : α) :
    (as.insertIdx i v).size = as.size + 1

Proof state:
α : Type u_1
as : Array α
i : Nat
h : i ≤ as.size
v : α
⊢ (as.insertIdx i v h).size = as.size + 1

Tactic:
rw [insertIdx, size_insertIdx_loop, size_push]

Result:
no goals
-- Mathlib/Order/Filter/AtTopBot/Archimedean.lean
theorem Tendsto.atTop_nsmul_neg_const {f : α → ℕ} (hr : r < 0) (hf : Tendsto f l atTop) :
    Tendsto (fun x => f x • r) l atBot

Proof state:
α : Type u_1
R : Type u_2
l : Filter α
r : R
inst✝¹ : LinearOrderedAddCommGroup R
inst✝ : Archimedean R
f : α → ℕ
hr : r < 0
hf : Tendsto f l atTop
⊢ Tendsto (fun x => f x • r) l atBot

Tactic:
simpa using hf.atTop_nsmul_const (neg_pos.2 hr)

Result:
no goals
-- Mathlib/Algebra/Order/GroupWithZero/Unbundled.lean
theorem mul_lt_of_lt_one_left [MulPosStrictMono α] (hb : 0 < b) (h : a < 1) : a * b < b

Proof state:
α : Type u_3
a b : α
inst✝³ : MulOneClass α
inst✝² : Zero α
inst✝¹ : Preorder α
inst✝ : MulPosStrictMono α
hb : 0 < b
h : a < 1
⊢ a * b < b

Tactic:
simpa only [one_mul] using mul_lt_mul_of_pos_right h hb

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Find.lean
theorem find?_cons_of_pos (l) (h : p a) : find? p (a :: l) = some a

Proof state:
α✝ : Type u_1
p : α✝ → Bool
a : α✝
l : List α✝
h : p a = true
⊢ find? p (a :: l) = some a

Tactic:
simp [find?, h]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/RawLemmas.lean
theorem getKey?_erase [EquivBEq α] [LawfulHashable α] (h : m.1.WF) {k a : α} :
    (m.erase k).getKey? a = if k == a then none else m.getKey? a

Proof state:
α : Type u
β : α → Type v
m : Raw₀ α β
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
h : m.val.WF
k a : α
⊢ (m.erase k).getKey? a = if (k == a) = true then none else m.getKey? a

Tactic:
simp_to_model [erase] using List.getKey?_eraseKey

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Attach.lean
theorem unattach_append {p : α → Prop} {l₁ l₂ : List { x // p x }} :
    (l₁ ++ l₂).unattach = l₁.unattach ++ l₂.unattach

Proof state:
α : Type u_1
p : α → Prop
l₁ l₂ : List { x // p x }
⊢ (l₁ ++ l₂).unattach = l₁.unattach ++ l₂.unattach

Tactic:
simp [unattach, -map_subtype]

Result:
no goals
-- Mathlib/NumberTheory/ArithmeticFunction.lean
theorem mul_apply_one [Semiring R] {f g : ArithmeticFunction R} : (f * g) 1 = f 1 * g 1

Proof state:
R : Type u_1
inst✝ : Semiring R
f g : ArithmeticFunction R
⊢ (f * g) 1 = f 1 * g 1

Tactic:
simp

Result:
no goals
-- Mathlib/Algebra/Group/Subgroup/Lattice.lean
theorem mem_sup' : x ∈ s ⊔ t ↔ ∃ (y : s) (z : t), (y : C) * z = x :=
  mem_sup.trans <| by simp only [SetLike.exists, coe_mk, exists_prop]

Proof state:
C : Type u_2
inst✝ : CommGroup C
s t : Subgroup C
x : C
⊢ (∃ y ∈ s, ∃ z ∈ t, y * z = x) ↔ ∃ y z, ↑y * ↑z = x

Tactic:
simp only [SetLike.exists, coe_mk, exists_prop]

Result:
no goals
-- Mathlib/Analysis/Normed/Affine/AddTorsor.lean
theorem dist_midpoint_midpoint_le (p₁ p₂ p₃ p₄ : V) :
    dist (midpoint ℝ p₁ p₂) (midpoint ℝ p₃ p₄) ≤ (dist p₁ p₃ + dist p₂ p₄) / 2

Proof state:
V : Type u_1
inst✝¹ : SeminormedAddCommGroup V
inst✝ : NormedSpace ℝ V
p₁ p₂ p₃ p₄ : V
⊢ dist (midpoint ℝ p₁ p₂) (midpoint ℝ p₃ p₄) ≤ (dist p₁ p₃ + dist p₂ p₄) / 2

Tactic:
simpa using dist_midpoint_midpoint_le' (𝕜 := ℝ) p₁ p₂ p₃ p₄

Result:
no goals
-- Mathlib/Data/Real/EReal.lean
theorem natCast_eq_iff {m n : ℕ} : (m : EReal) = (n : EReal) ↔ m = n

Proof state:
m n : ℕ
⊢ ↑m = ↑n ↔ m = n

Tactic:
rw [← coe_coe_eq_natCast n, ← coe_coe_eq_natCast m, EReal.coe_eq_coe_iff, Nat.cast_inj]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Zip.lean
theorem head?_zipWithAll {f : Option α → Option β → γ} :
    (zipWithAll f as bs).head? = match as.head?, bs.head? with
      | none, none => .none | a?, b? => some (f a? b?)

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
as : List α
bs : List β
f : Option α → Option β → γ
⊢ (zipWithAll f as bs).head? =
    match as.head?, bs.head? with
    | none, none => none
    | a?, b? => some (f a? b?)

Tactic:
simp [head?_eq_getElem?, getElem?_zipWithAll]

Result:
no goals
-- Mathlib/MeasureTheory/VectorMeasure/Basic.lean
theorem restrict_univ : v.restrict Set.univ = v :=
  ext fun i hi => by rw [restrict_apply v MeasurableSet.univ hi, Set.inter_univ]

Proof state:
α : Type u_1
inst✝² : MeasurableSpace α
M : Type u_3
inst✝¹ : AddCommMonoid M
inst✝ : TopologicalSpace M
v : VectorMeasure α M
i : Set α
hi : MeasurableSet i
⊢ ↑(v.restrict univ) i = ↑v i

Tactic:
rw [restrict_apply v MeasurableSet.univ hi, Set.inter_univ]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Option/Lemmas.lean
theorem ne_none_iff_exists : o ≠ none ↔ ∃ x, some x = o

Proof state:
α✝ : Type u_1
o : Option α✝
⊢ o ≠ none ↔ ∃ x, some x = o

Tactic:
cases o <;> simp

Result:
no goals
-- Mathlib/Probability/Martingale/BorelCantelli.lean
theorem Martingale.ae_not_tendsto_atTop_atTop [IsFiniteMeasure μ] (hf : Martingale f ℱ μ)
    (hbdd : ∀ᵐ ω ∂μ, ∀ i, |f (i + 1) ω - f i ω| ≤ R) :
    ∀ᵐ ω ∂μ, ¬Tendsto (fun n => f n ω) atTop atTop

Proof state:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
f : ℕ → Ω → ℝ
R : ℝ≥0
inst✝ : IsFiniteMeasure μ
hf : Martingale f ℱ μ
hbdd : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), |f (i + 1) ω - f i ω| ≤ ↑R
⊢ ∀ᵐ (ω : Ω) ∂μ, ¬Tendsto (fun n => f n ω) atTop atTop

Tactic:
filter_upwards [hf.bddAbove_range_iff_bddBelow_range hbdd] with ω hω htop using
  unbounded_of_tendsto_atTop htop (hω.2 <| bddBelow_range_of_tendsto_atTop_atTop htop)

Result:
no goals
-- Mathlib/Topology/MetricSpace/IsometricSMul.lean
theorem edist_div_left [PseudoEMetricSpace G] [IsometricSMul G G] [IsometricSMul Gᵐᵒᵖ G]
    (a b c : G) : edist (a / b) (a / c) = edist b c

Proof state:
G : Type v
inst✝³ : Group G
inst✝² : PseudoEMetricSpace G
inst✝¹ : IsometricSMul G G
inst✝ : IsometricSMul Gᵐᵒᵖ G
a b c : G
⊢ edist (a / b) (a / c) = edist b c

Tactic:
rw [div_eq_mul_inv, div_eq_mul_inv, edist_mul_left, edist_inv_inv]

Result:
no goals
-- Mathlib/CategoryTheory/Limits/Shapes/Pullback/Assoc.lean
theorem pullbackAssoc_inv_snd [HasPullback ((pullback.snd _ _ : Z₁ ⟶ X₂) ≫ f₃) f₄]
    [HasPullback f₁ ((pullback.fst _ _ : Z₂ ⟶ X₂) ≫ f₂)] :
    (pullbackAssoc f₁ f₂ f₃ f₄).inv ≫ pullback.snd _ _ = pullback.snd _ _ ≫ pullback.snd _ _

Proof state:
C : Type u
inst✝⁴ : Category.{v, u} C
X₁ X₂ X₃ Y₁ Y₂ : C
f₁ : X₁ ⟶ Y₁
f₂ : X₂ ⟶ Y₁
f₃ : X₂ ⟶ Y₂
f₄ : X₃ ⟶ Y₂
inst✝³ : HasPullback f₁ f₂
inst✝² : HasPullback f₃ f₄
inst✝¹ : HasPullback (pullback.snd f₁ f₂ ≫ f₃) f₄
inst✝ : HasPullback f₁ (pullback.fst f₃ f₄ ≫ f₂)
⊢ (pullbackAssoc f₁ f₂ f₃ f₄).inv ≫ pullback.snd (pullback.snd f₁ f₂ ≫ f₃) f₄ =
    pullback.snd f₁ (pullback.fst f₃ f₄ ≫ f₂) ≫ pullback.snd f₃ f₄

Tactic:
rw [Iso.inv_comp_eq, pullbackAssoc_hom_snd_snd]

Result:
no goals
-- Mathlib/Algebra/BigOperators/Expect.lean
lemma expect_dite_eq (i : ι) (f : ∀ j, i = j → M) :
    𝔼 j, (if h : i = j then f j h else 0) = f i rfl /ℚ card ι

Proof state:
ι : Type u_1
M : Type u_3
inst✝³ : Fintype ι
inst✝² : AddCommMonoid M
inst✝¹ : Module ℚ≥0 M
inst✝ : DecidableEq ι
i : ι
f : (j : ι) → i = j → M
⊢ (𝔼 j : ι, if h : i = j then f j h else 0) = (↑(card ι))⁻¹ • f i ⋯

Tactic:
simp

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Ord.lean
theorem isLE_of_eq_lt {o : Ordering} : o = .lt → o.isLE

Proof state:
⊢ lt.isLE = true

Tactic:
rfl

Result:
no goals

Proof state:
o : Ordering
⊢ o = lt → o.isLE = true

Tactic:
rintro rfl

Result:
⊢ lt.isLE = true
-- Mathlib/RingTheory/Flat/Basic.lean
/-- An `R`-module `M` is flat if for all finitely generated ideals `I` of `R`,
the canonical map `I ⊗ M →ₗ M` is injective. -/
lemma iff_lift_lsmul_comp_subtype_injective : Flat R M ↔ ∀ ⦃I : Ideal R⦄, I.FG →
    Function.Injective (TensorProduct.lift ((lsmul R M).comp I.subtype))

Proof state:
R : Type u
M : Type v
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
⊢ Flat R M ↔ ∀ ⦃I : Ideal R⦄, I.FG → Function.Injective ⇑(lift (lsmul R M ∘ₗ Submodule.subtype I))

Tactic:
simp [iff_rTensor_injective, ← lid_comp_rTensor]

Result:
no goals
-- Mathlib/Algebra/Homology/Embedding/ExtendHomology.lean
@[reassoc (attr := simp)]
lemma extendHomologyIso_hom_homologyι :
    (K.extendHomologyIso e hj').hom ≫ K.homologyι j =
      (K.extend e).homologyι j' ≫ (K.extendOpcyclesIso e hj').hom

Proof state:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst✝⁴ : Category.{u_4, u_3} C
inst✝³ : HasZeroMorphisms C
inst✝² : HasZeroObject C
K : HomologicalComplex C c
e : c.Embedding c'
j : ι
j' : ι'
hj' : e.f j = j'
inst✝¹ : K.HasHomology j
inst✝ : (K.extend e).HasHomology j'
⊢ (K.extendHomologyIso e hj').hom ≫ K.homologyι j = (K.extend e).homologyι j' ≫ (K.extendOpcyclesIso e hj').hom

Tactic:
simp only [← cancel_epi ((K.extend e).homologyπ j'),
  homologyπ_extendHomologyIso_hom_assoc, homology_π_ι, extendCyclesIso_hom_iCycles_assoc,
  homology_π_ι_assoc, pOpcycles_extendOpcyclesIso_hom]

Result:
no goals
-- Mathlib/Algebra/MvPolynomial/Basic.lean
lemma le_coeffsIn_pow : ∀ {n}, coeffsIn σ M ^ n ≤ coeffsIn σ (M ^ n)
  | 0 => by simpa using ⟨1, map_one _⟩
  | n + 1 => (coeffsIn_pow n.succ_ne_zero _).ge

Proof state:
R : Type u_2
S : Type u_3
σ : Type u_4
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
M : Submodule R S
⊢ coeffsIn σ M ^ 0 ≤ coeffsIn σ (M ^ 0)

Tactic:
simpa using ⟨1, map_one _⟩

Result:
no goals
-- Mathlib/RingTheory/MvPolynomial/MonomialOrder.lean
theorem leadingCoeff_prod_of_regular {ι : Type*}
    {P : ι → MvPolynomial σ R} {s : Finset ι} (H : ∀ i ∈ s, IsRegular (m.leadingCoeff (P i))) :
    m.leadingCoeff (∏ i ∈ s, P i) = ∏ i ∈ s, m.leadingCoeff (P i)

Proof state:
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
ι : Type u_3
P : ι → MvPolynomial σ R
s : Finset ι
H : ∀ i ∈ s, IsRegular (m.leadingCoeff (P i))
⊢ m.leadingCoeff (∏ i ∈ s, P i) = ∏ i ∈ s, m.leadingCoeff (P i)

Tactic:
simp only [leadingCoeff, degree_prod_of_regular H, coeff_prod_sum_degree]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem msb_fill {w : Nat} {v : Bool} :
    (fill w v).msb = (v && decide (0 < w))

Proof state:
w : Nat
v : Bool
⊢ (fill w v).msb = (v && decide (0 < w))

Tactic:
simp [BitVec.msb]

Result:
no goals
-- Mathlib/Analysis/Complex/IntegerCompl.lean
lemma integerComplement.ne_one {x : ℂ} (hx : x ∈ ℂ_ℤ): x ≠ 1 :=
  fun hx' ↦ hx ⟨1, by exact_mod_cast hx'.symm⟩

Proof state:
x : ℂ
hx : x ∈ ℂ_ℤ
hx' : x = 1
⊢ ↑1 = x

Tactic:
exact_mod_cast hx'.symm

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Tactic/BVDecide/LRAT/Internal/Formula/RupAddResult.lean
theorem ratUnits_performRupCheck {n : Nat} (f : DefaultFormula n) (rupHints : Array Nat) :
    (performRupCheck f rupHints).1.ratUnits = f.ratUnits

Proof state:
n : Nat
f : DefaultFormula n
rupHints : Array Nat
⊢ (f.performRupCheck rupHints).fst.ratUnits = f.ratUnits

Tactic:
simp only [performRupCheck]

Result:
no goals
-- Mathlib/Order/Filter/AtTopBot/Basic.lean
theorem frequently_atTop' [NoMaxOrder α] : (∃ᶠ x in atTop, p x) ↔ ∀ a, ∃ b > a, p b :=
  atTop_basis_Ioi.frequently_iff.trans <| by simp

Proof state:
α : Type u_3
inst✝³ : Preorder α
inst✝² : IsDirected α fun x1 x2 => x1 ≤ x2
p : α → Prop
inst✝¹ : Nonempty α
inst✝ : NoMaxOrder α
⊢ (∀ (i : α), True → ∃ x ∈ Ioi i, p x) ↔ ∀ (a : α), ∃ b > a, p b

Tactic:
simp

Result:
no goals
-- Mathlib/FieldTheory/RatFunc/Degree.lean
theorem intDegree_C (k : K) : intDegree (C k) = 0

Proof state:
K : Type u
inst✝ : Field K
k : K
⊢ (C k).intDegree = 0

Tactic:
rw [intDegree, num_C, natDegree_C, denom_C, natDegree_one, sub_self]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/List/Associative.lean
theorem getValue?_eraseKey [BEq α] [PartialEquivBEq α] {l : List ((_ : α) × β)} {k a : α}
    (hl : DistinctKeys l) :
    getValue? a (eraseKey k l) = if k == a then none else getValue? a l

Proof state:
α : Type u
β : Type v
inst✝¹ : BEq α
inst✝ : PartialEquivBEq α
l : List ((_ : α) × β)
k a : α
hl : DistinctKeys l
⊢ getValue? a (eraseKey k l) = if (k == a) = true then none else getValue? a l

Tactic:
simp [getValue?_eq_getEntry?, getEntry?_eraseKey hl, apply_ite (Option.map _)]

Result:
no goals
-- Mathlib/RingTheory/MvPolynomial/MonomialOrder.lean
theorem isUnit_leadingCoeff {f : MvPolynomial σ R} :
    IsUnit (m.leadingCoeff f) ↔ f ≠ 0

Proof state:
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : Field R
f : MvPolynomial σ R
⊢ IsUnit (m.leadingCoeff f) ↔ f ≠ 0

Tactic:
simp only [isUnit_iff_ne_zero, ne_eq, leadingCoeff_eq_zero_iff]

Result:
no goals
-- Mathlib/Order/Interval/Finset/Basic.lean
theorem Ico_inter_Ico {a b c d : α} : Ico a b ∩ Ico c d = Ico (max a c) (min b d)

Proof state:
α : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LocallyFiniteOrder α
a b c d : α
⊢ Ico a b ∩ Ico c d = Ico (a ⊔ c) (b ⊓ d)

Tactic:
rw [← coe_inj, coe_inter, coe_Ico, coe_Ico, coe_Ico, Set.Ico_inter_Ico]

Result:
no goals
-- Mathlib/Algebra/Category/ModuleCat/Presheaf.lean
@[simp]
lemma id_app (M : PresheafOfModules R) (X : Cᵒᵖ) : Hom.app (𝟙 M) X = 𝟙 _

Proof state:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
R : Cᵒᵖ ⥤ RingCat
M : PresheafOfModules R
X : Cᵒᵖ
⊢ (𝟙 M).app X = 𝟙 (M.obj X)

Tactic:
rfl

Result:
no goals
-- Mathlib/GroupTheory/FreeGroup/Reduce.lean
theorem norm_mul_le (x y : FreeGroup α) : norm (x * y) ≤ norm x + norm y :=
  calc
    norm (x * y) = norm (mk (x.toWord ++ y.toWord))

Proof state:
α : Type u_1
inst✝ : DecidableEq α
x y : FreeGroup α
⊢ (x * y).norm = (mk (x.toWord ++ y.toWord)).norm

Tactic:
rw [← mul_mk, mk_toWord, mk_toWord]

Result:
no goals
-- Mathlib/Order/SuccPred/Basic.lean
theorem le_succ_bot_iff : a ≤ succ ⊥ ↔ a = ⊥ ∨ a = succ ⊥

Proof state:
α : Type u_1
inst✝² : LinearOrder α
inst✝¹ : SuccOrder α
a : α
inst✝ : OrderBot α
⊢ a ≤ succ ⊥ ↔ a = ⊥ ∨ a = succ ⊥

Tactic:
rw [le_succ_iff_eq_or_le, le_bot_iff, or_comm]

Result:
no goals
-- Mathlib/Data/Finset/NAry.lean
theorem card_image₂_singleton_right (hf : Injective fun a => f a b) :
    #(image₂ f s {b}) = #s

Proof state:
α : Type u_1
β : Type u_3
γ : Type u_5
inst✝ : DecidableEq γ
f : α → β → γ
s : Finset α
b : β
hf : Injective fun a => f a b
⊢ #(image₂ f s {b}) = #s

Tactic:
rw [image₂_singleton_right, card_image_of_injective _ hf]

Result:
no goals
-- Mathlib/Topology/ContinuousOn.lean
theorem continuous_if {p : α → Prop} [∀ a, Decidable (p a)]
    (hp : ∀ a ∈ frontier { x | p x }, f a = g a) (hf : ContinuousOn f (closure { x | p x }))
    (hg : ContinuousOn g (closure { x | ¬p x })) :
    Continuous fun a => if p a then f a else g a

Proof state:
α : Type u_1
β : Type u_2
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
f g : α → β
p : α → Prop
inst✝ : (a : α) → Decidable (p a)
hp : ∀ a ∈ frontier {x | p x}, f a = g a
hf : ContinuousOn f (closure {x | p x})
hg : ContinuousOn g (closure {x | ¬p x})
⊢ Continuous fun a => if p a then f a else g a

Tactic:
rw [continuous_iff_continuousOn_univ]

Result:
α : Type u_1
β : Type u_2
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
f g : α → β
p : α → Prop
inst✝ : (a : α) → Decidable (p a)
hp : ∀ a ∈ frontier {x | p x}, f a = g a
hf : ContinuousOn f (closure {x | p x})
hg : ContinuousOn g (closure {x | ¬p x})
⊢ ContinuousOn (fun a => if p a then f a else g a) univ

Proof state:
α : Type u_1
β : Type u_2
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
f g : α → β
p : α → Prop
inst✝ : (a : α) → Decidable (p a)
hp : ∀ a ∈ frontier {x | p x}, f a = g a
hf : ContinuousOn f (closure {x | p x})
hg : ContinuousOn g (closure {x | ¬p x})
⊢ ContinuousOn (fun a => if p a then f a else g a) univ

Tactic:
apply ContinuousOn.if <;> simpa

Result:
no goals