harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/RingTheory/Ideal/Operations.lean
theorem mul_sup_eq_of_coprime_left (h : I ⊔ J = ⊤) : I * K ⊔ J = K ⊔ J

Proof state:
R : Type u
inst✝ : CommSemiring R
I J K : Ideal R
h : I ⊔ J = ⊤
⊢ I * K ⊔ J = K ⊔ J

Tactic:
rw [sup_comm] at h

Result:
R : Type u
inst✝ : CommSemiring R
I J K : Ideal R
h : J ⊔ I = ⊤
⊢ I * K ⊔ J = K ⊔ J

Proof state:
R : Type u
inst✝ : CommSemiring R
I J K : Ideal R
h : J ⊔ I = ⊤
⊢ I * K ⊔ J = K ⊔ J

Tactic:
rw [sup_comm, sup_mul_eq_of_coprime_left h, sup_comm]

Result:
no goals
-- Mathlib/Algebra/Order/ToIntervalMod.lean
theorem iUnion_Ico_intCast : ⋃ n : ℤ, Ico (n : α) (n + 1) = Set.univ

Proof state:
α : Type u_1
inst✝¹ : LinearOrderedRing α
inst✝ : Archimedean α
⊢ ⋃ n, Ico (↑n) (↑n + 1) = univ

Tactic:
simpa only [zero_add] using iUnion_Ico_add_intCast (0 : α)

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem getElem_fill {w i : Nat} {v : Bool} (h : i < w) :
    (fill w v)[i] = v

Proof state:
w i : Nat
v : Bool
h : i < w
⊢ (fill w v)[i] = v

Tactic:
by_cases h : v
<;> simp [h, BitVec.fill, BitVec.negOne_eq_allOnes]

Result:
no goals
-- Mathlib/Data/Nat/Cast/Order/Basic.lean
theorem NeZero.nat_of_injective {n : ℕ} [NeZero (n : R)] [RingHomClass F R S] {f : F}
    (hf : Function.Injective f) : NeZero (n : S) :=
  ⟨fun h ↦ NeZero.natCast_ne n R <| hf <| by simpa only [map_natCast, map_zero f]⟩

Proof state:
R : Type u_2
S : Type u_3
F : Type u_4
inst✝⁴ : NonAssocSemiring R
inst✝³ : NonAssocSemiring S
inst✝² : FunLike F R S
n : ℕ
inst✝¹ : NeZero ↑n
inst✝ : RingHomClass F R S
f : F
hf : Function.Injective ⇑f
h : ↑n = 0
⊢ f ↑n = f 0

Tactic:
simpa only [map_natCast, map_zero f]

Result:
no goals
-- Mathlib/.lake/packages/batteries/Batteries/Data/UnionFind/Lemmas.lean
theorem rankMax_push {m : UnionFind} : m.push.rankMax = m.rankMax

Proof state:
m : UnionFind
⊢ m.push.rankMax = m.rankMax

Tactic:
simp [rankMax]

Result:
no goals
-- Mathlib/Data/Set/Card.lean
theorem ncard_diff_singleton_add_one {a : α} (h : a ∈ s)
    (hs : s.Finite

Proof state:
α : Type u_1
s : Set α
a : α
h : a ∈ s
hs : autoParam s.Finite _auto✝
⊢ (s \ {a}).ncard + 1 = s.ncard

Tactic:
to_encard_tac

Result:
α : Type u_1
s : Set α
a : α
h : a ∈ s
hs : autoParam s.Finite _auto✝
⊢ ↑(s \ {a}).ncard + 1 = ↑s.ncard

Proof state:
α : Type u_1
s : Set α
a : α
h : a ∈ s
hs : autoParam s.Finite _auto✝
⊢ ↑(s \ {a}).ncard + 1 = ↑s.ncard

Tactic:
rw [hs.cast_ncard_eq, hs.diff.cast_ncard_eq,
encard_diff_singleton_add_one h]

Result:
no goals
-- Mathlib/Dynamics/BirkhoffSum/Average.lean
theorem birkhoffAverage_one (f : α → α) (g : α → M) (x : α) :
    birkhoffAverage R f g 1 x = g x

Proof state:
R : Type u_1
α : Type u_2
M : Type u_3
inst✝² : DivisionSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
f : α → α
g : α → M
x : α
⊢ birkhoffAverage R f g 1 x = g x

Tactic:
simp [birkhoffAverage]

Result:
no goals
-- Mathlib/Analysis/Normed/Module/Convex.lean
theorem convexOn_norm (hs : Convex ℝ s) : ConvexOn ℝ s norm :=
  ⟨hs, fun x _ y _ a b ha hb _ =>
    calc
      ‖a • x + b • y‖ ≤ ‖a • x‖ + ‖b • y‖ := norm_add_le _ _
      _ = a * ‖x‖ + b * ‖y‖

Proof state:
E : Type u_1
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
s : Set E
hs : Convex ℝ s
x : E
x✝² : x ∈ s
y : E
x✝¹ : y ∈ s
a b : ℝ
ha : 0 ≤ a
hb : 0 ≤ b
x✝ : a + b = 1
⊢ ‖a • x‖ + ‖b • y‖ = a * ‖x‖ + b * ‖y‖

Tactic:
rw [norm_smul, norm_smul, Real.norm_of_nonneg ha, Real.norm_of_nonneg hb]

Result:
no goals
-- Mathlib/Data/Set/Function.lean
lemma graphOn_comp (s : Set α) (f : α → β) (g : β → γ) :
    s.graphOn (g ∘ f) = (fun x ↦ (x.1, g x.2)) '' s.graphOn f

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
s : Set α
f : α → β
g : β → γ
⊢ graphOn (g ∘ f) s = (fun x => (x.1, g x.2)) '' graphOn f s

Tactic:
simpa using image_comp (fun x ↦ (x.1, g x.2)) (fun x ↦ (x, f x)) _

Result:
no goals
-- Mathlib/Algebra/MonoidAlgebra/Grading.lean
theorem single_mem_gradeBy {R} [CommSemiring R] (f : M → ι) (m : M) (r : R) :
    Finsupp.single m r ∈ gradeBy R f (f m)

Proof state:
M : Type u_1
ι : Type u_2
R : Type u_4
inst✝ : CommSemiring R
f : M → ι
m : M
r : R
⊢ Finsupp.single m r ∈ gradeBy R f (f m)

Tactic:
intro x hx

Result:
M : Type u_1
ι : Type u_2
R : Type u_4
inst✝ : CommSemiring R
f : M → ι
m : M
r : R
x : M
hx : x ∈ (Finsupp.single m r).support
⊢ f x = f m

Proof state:
M : Type u_1
ι : Type u_2
R : Type u_4
inst✝ : CommSemiring R
f : M → ι
m : M
r : R
x : M
hx : x ∈ (Finsupp.single m r).support
⊢ f x = f m

Tactic:
rw [Finset.mem_singleton.mp (Finsupp.support_single_subset hx)]

Result:
no goals
-- Mathlib/RingTheory/WittVector/Truncated.lean
theorem coeff_zero (i : Fin n) : (0 : TruncatedWittVector p n R).coeff i = 0

Proof state:
p n : ℕ
R : Type u_1
inst✝¹ : CommRing R
inst✝ : Fact (Nat.Prime p)
i : Fin n
⊢ coeff i 0 = 0

Tactic:
show coeff i (truncateFun _ 0 : TruncatedWittVector p n R) = 0

Result:
p n : ℕ
R : Type u_1
inst✝¹ : CommRing R
inst✝ : Fact (Nat.Prime p)
i : Fin n
⊢ coeff i (truncateFun n 0) = 0

Proof state:
p n : ℕ
R : Type u_1
inst✝¹ : CommRing R
inst✝ : Fact (Nat.Prime p)
i : Fin n
⊢ coeff i (truncateFun n 0) = 0

Tactic:
rw [coeff_truncateFun, WittVector.zero_coeff]

Result:
no goals
-- Mathlib/MeasureTheory/Integral/Lebesgue.lean
theorem lintegral_singleton [MeasurableSingletonClass α] (f : α → ℝ≥0∞) (a : α) :
    ∫⁻ x in {a}, f x ∂μ = f a * μ {a}

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
inst✝ : MeasurableSingletonClass α
f : α → ℝ≥0∞
a : α
⊢ ∫⁻ (x : α) in {a}, f x ∂μ = f a * μ {a}

Tactic:
simp only [restrict_singleton, lintegral_smul_measure, lintegral_dirac, mul_comm]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem reverse_eq_push_iff {xs : Array α} {ys : Array α} {a : α} :
    xs.reverse = ys.push a ↔ xs = #[a] ++ ys.reverse

Proof state:
α : Type u_1
xs ys : Array α
a : α
⊢ xs.reverse = ys.push a ↔ xs = #[a] ++ ys.reverse

Tactic:
rw [reverse_eq_iff, reverse_push]

Result:
no goals
-- Mathlib/Algebra/GCDMonoid/Basic.lean
theorem gcd_eq_of_dvd_sub_left {a b c : α} (h : a ∣ b - c) : gcd b a = gcd c a

Proof state:
α : Type u_1
inst✝² : CommRing α
inst✝¹ : IsDomain α
inst✝ : NormalizedGCDMonoid α
a b c : α
h : a ∣ b - c
⊢ gcd b a = gcd c a

Tactic:
rw [gcd_comm _ a, gcd_comm _ a, gcd_eq_of_dvd_sub_right h]

Result:
no goals
-- Mathlib/Order/Partition/Equipartition.lean
theorem IsEquipartition.card_part_le_average_add_one (hP : P.IsEquipartition) (ht : t ∈ P.parts) :
    #t ≤ #s / #P.parts + 1

Proof state:
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
P : Finpartition s
hP : P.IsEquipartition
ht : t ∈ P.parts
⊢ #t ≤ (∑ i ∈ P.parts, #i) / #P.parts + 1

Tactic:
exact Finset.EquitableOn.le_add_one hP ht

Result:
no goals

Proof state:
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
P : Finpartition s
hP : P.IsEquipartition
ht : t ∈ P.parts
⊢ #t ≤ #s / #P.parts + 1

Tactic:
rw [← P.sum_card_parts]

Result:
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
P : Finpartition s
hP : P.IsEquipartition
ht : t ∈ P.parts
⊢ #t ≤ (∑ i ∈ P.parts, #i) / #P.parts + 1
-- Mathlib/Algebra/Order/ToIntervalMod.lean
theorem toIcoMod_add_zsmul (a b : α) (m : ℤ) : toIcoMod hp a (b + m • p) = toIcoMod hp a b

Proof state:
α : Type u_1
inst✝ : LinearOrderedAddCommGroup α
hα : Archimedean α
p : α
hp : 0 < p
a b : α
m : ℤ
⊢ toIcoMod hp a (b + m • p) = toIcoMod hp a b

Tactic:
rw [toIcoMod, toIcoDiv_add_zsmul, toIcoMod, add_smul]

Result:
α : Type u_1
inst✝ : LinearOrderedAddCommGroup α
hα : Archimedean α
p : α
hp : 0 < p
a b : α
m : ℤ
⊢ b + m • p - (toIcoDiv hp a b • p + m • p) = b - toIcoDiv hp a b • p

Proof state:
α : Type u_1
inst✝ : LinearOrderedAddCommGroup α
hα : Archimedean α
p : α
hp : 0 < p
a b : α
m : ℤ
⊢ b + m • p - (toIcoDiv hp a b • p + m • p) = b - toIcoDiv hp a b • p

Tactic:
abel

Result:
no goals
-- Mathlib/Combinatorics/Additive/AP/Three/Defs.lean
@[to_additive] lemma threeGPFree_smul_set : ThreeGPFree (a • s) ↔ ThreeGPFree s where
  mp hs b hb c hc d hd h := mul_left_cancel
      (hs (mem_image_of_mem _ hb) (mem_image_of_mem _ hc) (mem_image_of_mem _ hd) <| by
        rw [mul_mul_mul_comm, smul_eq_mul, smul_eq_mul, mul_mul_mul_comm, h])
  mpr := ThreeGPFree.smul_set

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

Tactic:
rw [mul_mul_mul_comm, smul_eq_mul, smul_eq_mul, mul_mul_mul_comm, h]

Result:
no goals
-- Mathlib/MeasureTheory/Measure/Lebesgue/Basic.lean
theorem volume_closedBall (a r : ℝ) : volume (Metric.closedBall a r) = ofReal (2 * r)

Proof state:
a r : ℝ
⊢ volume (Metric.closedBall a r) = ofReal (2 * r)

Tactic:
rw [closedBall_eq_Icc, volume_Icc, ← sub_add, add_sub_cancel_left, two_mul]

Result:
no goals
-- Mathlib/CategoryTheory/MorphismProperty/Representable.lean
@[reassoc (attr := simp)]
lemma lift'_snd [Full F] [Faithful F] : hf'.lift' i h hi ≫ hf'.snd g = h

Proof state:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
F : C ⥤ D
Y : D
b : C
f' : F.obj b ⟶ Y
hf' : F.relativelyRepresentable f'
a : C
g : F.obj a ⟶ Y
c : C
i : c ⟶ b
h : c ⟶ a
hi : F.map i ≫ f' = F.map h ≫ g
inst✝¹ : F.Full
inst✝ : F.Faithful
⊢ hf'.lift' i h hi ≫ hf'.snd g = h

Tactic:
simp [lift']

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Nat/Basic.lean
theorem leftpad_length (n : Nat) (a : α) (l : List α) :
    (leftpad n a l).length = max n l.length

Proof state:
α : Type u_1
n : Nat
a : α
l : List α
⊢ (leftpad n a l).length = max n l.length

Tactic:
simp only [leftpad, length_append, length_replicate, Nat.sub_add_eq_max]

Result:
no goals
-- Mathlib/Analysis/InnerProductSpace/OfNorm.lean
theorem add_left_aux5 (x y z : E) :
    ‖(I : 𝕜) • (2 • x + y)‖ * ‖(I : 𝕜) • (2 • x + y)‖
    + ‖(I : 𝕜) • y + 2 • z‖ * ‖(I : 𝕜) • y + 2 • z‖
    = 2 * (‖(I : 𝕜) • (x + y) + z‖ * ‖(I : 𝕜) • (x + y) + z‖
    + ‖(I : 𝕜) • x - z‖ * ‖(I : 𝕜) • x - z‖)

Proof state:
𝕜 : Type u_1
inst✝³ : RCLike 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : InnerProductSpaceable E
x y z : E
⊢ ‖I • (2 • x + y)‖ * ‖I • (2 • x + y)‖ + ‖I • y + 2 • z‖ * ‖I • y + 2 • z‖ =
    2 * (‖I • (x + y) + z‖ * ‖I • (x + y) + z‖ + ‖I • x - z‖ * ‖I • x - z‖)

Tactic:
convert parallelogram_identity ((I : 𝕜) • (x + y) + z) ((I : 𝕜) • x - z) using 4 <;> module

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Int/DivModLemmas.lean
theorem bmod_neg (x : Int) (m : Nat) (p : x % m ≥ (m + 1) / 2) : bmod x m = (x % m) - m

Proof state:
x : Int
m : Nat
p : x % ↑m ≥ (↑m + 1) / 2
⊢ x.bmod m = x % ↑m - ↑m

Tactic:
simp [bmod_def, Int.not_lt.mpr p]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem flatten_toArray_map (l : List (List α)) :
    (l.map List.toArray).toArray.flatten = l.flatten.toArray

Proof state:
α : Type u_1
l : List (List α)
⊢ (List.map List.toArray l).toArray.flatten = l.flatten.toArray

Tactic:
rw [← flatten_map_toArray]

Result:
α : Type u_1
l : List (List α)
⊢ (List.map List.toArray l).toArray.flatten = (map List.toArray l.toArray).flatten

Proof state:
α : Type u_1
l : List (List α)
⊢ (List.map List.toArray l).toArray.flatten = (map List.toArray l.toArray).flatten

Tactic:
simp

Result:
no goals
-- Mathlib/Analysis/Convex/Segment.lean
theorem segment_eq_image₂ (x y : E) :
    [x -[𝕜] y] =
      (fun p : 𝕜 × 𝕜 => p.1 • x + p.2 • y) '' { p | 0 ≤ p.1 ∧ 0 ≤ p.2 ∧ p.1 + p.2 = 1 }

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝² : OrderedSemiring 𝕜
inst✝¹ : AddCommMonoid E
inst✝ : SMul 𝕜 E
x y : E
⊢ [x-[𝕜]y] = (fun p => p.1 • x + p.2 • y) '' {p | 0 ≤ p.1 ∧ 0 ≤ p.2 ∧ p.1 + p.2 = 1}

Tactic:
simp only [segment, image, Prod.exists, mem_setOf_eq, exists_prop, and_assoc]

Result:
no goals
-- Mathlib/MeasureTheory/Integral/Lebesgue.lean
theorem lintegral_biUnion_finset₀ {s : Finset β} {t : β → Set α}
    (hd : Set.Pairwise (↑s) (AEDisjoint μ on t)) (hm : ∀ b ∈ s, NullMeasurableSet (t b) μ)
    (f : α → ℝ≥0∞) : ∫⁻ a in ⋃ b ∈ s, t b, f a ∂μ = ∑ b ∈ s, ∫⁻ a in t b, f a ∂μ

Proof state:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
s : Finset β
t : β → Set α
hd : (↑s).Pairwise (AEDisjoint μ on t)
hm : ∀ b ∈ s, NullMeasurableSet (t b) μ
f : α → ℝ≥0∞
⊢ ∫⁻ (a : α) in ⋃ b ∈ s, t b, f a ∂μ = ∑ b ∈ s, ∫⁻ (a : α) in t b, f a ∂μ

Tactic:
simp only [← Finset.mem_coe, lintegral_biUnion₀ s.countable_toSet hm hd, ← Finset.tsum_subtype']

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/List/Associative.lean
theorem containsKey_of_containsKey_cons [BEq α] {l : List ((a : α) × β a)} {k a : α} {v : β k}
    (h₁ : containsKey a (⟨k, v⟩ :: l)) (h₂ : (k == a) = false) : containsKey a l

Proof state:
case inr
α : Type u
β : α → Type v
inst✝ : BEq α
l : List ((a : α) × β a)
k a : α
v : β k
h₁ : containsKey a (⟨k, v⟩ :: l) = true
h₂ : (k == a) = false
h : containsKey a l = true
⊢ containsKey a l = true

Tactic:
exact h

Result:
no goals

Proof state:
case inl
α : Type u
β : α → Type v
inst✝ : BEq α
l : List ((a : α) × β a)
k a : α
v : β k
h₁ : containsKey a (⟨k, v⟩ :: l) = true
h₂ : (k == a) = false
h : (k == a) = true
⊢ containsKey a l = true

Tactic:
exact False.elim (Bool.eq_false_iff.1 h₂ h)

Result:
no goals

Proof state:
α : Type u
β : α → Type v
inst✝ : BEq α
l : List ((a : α) × β a)
k a : α
v : β k
h₁ : containsKey a (⟨k, v⟩ :: l) = true
h₂ : (k == a) = false
⊢ containsKey a l = true

Tactic:
rcases (containsKey_cons_eq_true.1 h₁) with (h|h)

Result:
case inl
α : Type u
β : α → Type v
inst✝ : BEq α
l : List ((a : α) × β a)
k a : α
v : β k
h₁ : containsKey a (⟨k, v⟩ :: l) = true
h₂ : (k == a) = false
h : (k == a) = true
⊢ containsKey a l = true

case inr
α : Type u
β : α → Type v
inst✝ : BEq α
l : List ((a : α) × β a)
k a : α
v : β k
h₁ : containsKey a (⟨k, v⟩ :: l) = true
h₂ : (k == a) = false
h : containsKey a l = true
⊢ containsKey a l = true
-- Mathlib/Order/Max.lean
theorem IsTop.isMax_iff {α} [PartialOrder α] {i j : α} (h : IsTop i) : IsMax j ↔ j = i

Proof state:
α : Type u_3
inst✝ : PartialOrder α
i j : α
h : IsTop i
⊢ IsMax j ↔ j = i

Tactic:
simp_rw [le_antisymm_iff, h j, true_and]

Result:
α : Type u_3
inst✝ : PartialOrder α
i j : α
h : IsTop i
⊢ IsMax j ↔ i ≤ j
-- Mathlib/.lake/packages/lean4/src/lean/Init/Grind/Lemmas.lean
theorem eq_true_of_and_eq_true_left {a b : Prop} (h : (a ∧ b) = True) : a = True

Proof state:
a b : Prop
h : (a ∧ b) = True
⊢ a = True

Tactic:
simp_all

Result:
no goals
-- Mathlib/NumberTheory/NumberField/CanonicalEmbedding/Basic.lean
theorem normAtPlace_apply_of_isReal {w : InfinitePlace K} (hw : IsReal w) (x : mixedSpace K) :
    normAtPlace w x = ‖x.1 ⟨w, hw⟩‖

Proof state:
K : Type u_1
inst✝ : Field K
w : InfinitePlace K
hw : w.IsReal
x : mixedSpace K
⊢ (normAtPlace w) x = ‖x.1 ⟨w, hw⟩‖

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

Result:
no goals
-- Mathlib/Data/List/Flatten.lean
/-- See `List.countP_flatten` for the corresponding statement using `List.sum`. -/
@[deprecated countP_flatten (since := "2024-10-17")]
lemma countP_flatten' (p : α → Bool) :
    ∀ L : List (List α), countP p L.flatten = Nat.sum (L.map (countP p))
  | [] => rfl
  | a :: l => by rw [flatten, countP_append, map_cons, Nat.sum_cons, countP_flatten' _ l]

Proof state:
α : Type u_1
p : α → Bool
a : List α
l : List (List α)
⊢ countP p (a :: l).flatten = Nat.sum (map (countP p) (a :: l))

Tactic:
rw [flatten, countP_append, map_cons, Nat.sum_cons, countP_flatten' _ l]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Trigonometric/Angle.lean
theorem sign_coe_nonneg_of_nonneg_of_le_pi {θ : ℝ} (h0 : 0 ≤ θ) (hpi : θ ≤ π) :
    0 ≤ (θ : Angle).sign

Proof state:
θ : ℝ
h0 : 0 ≤ θ
hpi : θ ≤ π
⊢ 0 ≤ (↑θ).sign

Tactic:
rw [sign, sign_nonneg_iff]

Result:
θ : ℝ
h0 : 0 ≤ θ
hpi : θ ≤ π
⊢ 0 ≤ (↑θ).sin

Proof state:
θ : ℝ
h0 : 0 ≤ θ
hpi : θ ≤ π
⊢ 0 ≤ (↑θ).sin

Tactic:
exact sin_nonneg_of_nonneg_of_le_pi h0 hpi

Result:
no goals
-- Mathlib/Topology/Bases.lean
theorem IsTopologicalBasis.inf_induced {γ} [s : TopologicalSpace β] {B₁ : Set (Set α)}
    {B₂ : Set (Set β)} (h₁ : IsTopologicalBasis B₁) (h₂ : IsTopologicalBasis B₂) (f₁ : γ → α)
    (f₂ : γ → β) :
    IsTopologicalBasis (t := induced f₁ t ⊓ induced f₂ s) (image2 (f₁ ⁻¹' · ∩ f₂ ⁻¹' ·) B₁ B₂)

Proof state:
α : Type u
β : Type u_1
t : TopologicalSpace α
γ : Type u_2
s : TopologicalSpace β
B₁ : Set (Set α)
B₂ : Set (Set β)
h₁ : IsTopologicalBasis B₁
h₂ : IsTopologicalBasis B₂
f₁ : γ → α
f₂ : γ → β
⊢ IsTopologicalBasis (image2 (fun x1 x2 => f₁ ⁻¹' x1 ∩ f₂ ⁻¹' x2) B₁ B₂)

Tactic:
simpa only [image2_image_left, image2_image_right] using (h₁.induced f₁).inf (h₂.induced f₂)

Result:
no goals
-- Mathlib/Data/Multiset/Bind.lean
@[simp] lemma mem_product : ∀ {p : α × β}, p ∈ @product α β s t ↔ p.1 ∈ s ∧ p.2 ∈ t
  | (a, b) => by simp [product, and_left_comm]

Proof state:
α : Type u_1
β : Type v
s : Multiset α
t : Multiset β
a : α
b : β
⊢ (a, b) ∈ s.product t ↔ (a, b).1 ∈ s ∧ (a, b).2 ∈ t

Tactic:
simp [product, and_left_comm]

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Regularity/Chunk.lean
theorem card_le_m_add_one_of_mem_chunk_parts (hs : s ∈ (chunk hP G ε hU).parts) : #s ≤ m + 1 :=
  (card_eq_of_mem_parts_chunk hs).elim (fun i => by simp [i]) fun i => i.le

Proof state:
α : Type u_1
inst✝² : Fintype α
inst✝¹ : DecidableEq α
P : Finpartition univ
hP : P.IsEquipartition
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : ℝ
U : Finset α
hU : U ∈ P.parts
s : Finset α
hs : s ∈ (chunk hP G ε hU).parts
i : #s = m
⊢ #s ≤ m + 1

Tactic:
simp [i]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Nat/Basic.lean
theorem add_sub_cancel_left (n m : Nat) : n + m - n = m :=
  show n + m - (n + 0) = m from
  by rw [Nat.add_sub_add_left, Nat.sub_zero]

Proof state:
n m : Nat
⊢ n + m - (n + 0) = m

Tactic:
rw [Nat.add_sub_add_left, Nat.sub_zero]

Result:
no goals
-- Mathlib/Logic/Encodable/Basic.lean
theorem surjective_decode_iget (α : Type*) [Encodable α] [Inhabited α] :
    Surjective fun n => ((Encodable.decode n).iget : α) := fun x =>
  ⟨Encodable.encode x, by simp_rw [Encodable.encodek]⟩

Proof state:
α : Type u_3
inst✝¹ : Encodable α
inst✝ : Inhabited α
x : α
⊢ (fun n => (decode n).iget) (encode x) = x

Tactic:
simp_rw [Encodable.encodek]

Result:
no goals
-- Mathlib/Algebra/BigOperators/Group/List/Lemmas.lean
lemma ranges_flatten : ∀ (l : List ℕ), l.ranges.flatten = range l.sum
  | [] => rfl
  | a :: l => by simp [ranges, ← map_flatten, ranges_flatten, range_add]

Proof state:
a : ℕ
l : List ℕ
⊢ (a :: l).ranges.flatten = range (a :: l).sum

Tactic:
simp [ranges, ← map_flatten, ranges_flatten, range_add]

Result:
no goals
-- Mathlib/Data/Finset/Sups.lean
@[simp] lemma powerset_infs_powerset_self (s : Finset α) :
    s.powerset ⊼ s.powerset = s.powerset

Proof state:
α : Type u_2
inst✝ : DecidableEq α
s : Finset α
⊢ s.powerset ⊼ s.powerset = s.powerset

Tactic:
simp [← powerset_inter]

Result:
no goals
-- Mathlib/Data/Nat/Init.lean
@[simp]
protected lemma div_left_inj (hda : d ∣ a) (hdb : d ∣ b) : a / d = b / d ↔ a = b

Proof state:
a b d : ℕ
hda : d ∣ a
hdb : d ∣ b
⊢ a / d = b / d ↔ a = b

Tactic:
refine ⟨fun h ↦ ?_, congrArg fun b ↦ b / d⟩

Result:
a b d : ℕ
hda : d ∣ a
hdb : d ∣ b
h : a / d = b / d
⊢ a = b

Proof state:
a b d : ℕ
hda : d ∣ a
hdb : d ∣ b
h : a / d = b / d
⊢ a = b

Tactic:
rw [← Nat.mul_div_cancel' hda, ← Nat.mul_div_cancel' hdb, h]

Result:
no goals
-- Mathlib/Algebra/Order/Chebyshev.lean
theorem MonovaryOn.sum_mul_sum_le_card_mul_sum (hfg : MonovaryOn f g s) :
    (∑ i ∈ s, f i) * ∑ i ∈ s, g i ≤ #s * ∑ i ∈ s, f i * g i

Proof state:
ι : Type u_1
α : Type u_2
inst✝¹ : LinearOrderedSemiring α
inst✝ : ExistsAddOfLE α
s : Finset ι
f g : ι → α
hfg : MonovaryOn f g ↑s
⊢ (∑ i ∈ s, f i) * ∑ i ∈ s, g i ≤ ↑(#s) * ∑ i ∈ s, f i * g i

Tactic:
rw [← nsmul_eq_mul]

Result:
ι : Type u_1
α : Type u_2
inst✝¹ : LinearOrderedSemiring α
inst✝ : ExistsAddOfLE α
s : Finset ι
f g : ι → α
hfg : MonovaryOn f g ↑s
⊢ (∑ i ∈ s, f i) * ∑ i ∈ s, g i ≤ #s • ∑ i ∈ s, f i * g i

Proof state:
ι : Type u_1
α : Type u_2
inst✝¹ : LinearOrderedSemiring α
inst✝ : ExistsAddOfLE α
s : Finset ι
f g : ι → α
hfg : MonovaryOn f g ↑s
⊢ (∑ i ∈ s, f i) * ∑ i ∈ s, g i ≤ #s • ∑ i ∈ s, f i * g i

Tactic:
exact hfg.sum_smul_sum_le_card_smul_sum

Result:
no goals
-- Mathlib/LinearAlgebra/TensorProduct/Vanishing.lean
theorem _root_.Equiv.vanishesTrivially_comp {κ} [Fintype κ] (e : κ ≃ ι) :
    VanishesTrivially R (m ∘ e) (n ∘ e) ↔ VanishesTrivially R m n

Proof state:
R : Type u_1
inst✝⁶ : CommRing R
M : Type u_2
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
N : Type u_3
inst✝³ : AddCommGroup N
inst✝² : Module R N
ι : Type u_4
inst✝¹ : Fintype ι
m : ι → M
n : ι → N
κ : Type u_5
inst✝ : Fintype κ
e : κ ≃ ι
⊢ VanishesTrivially R (m ∘ ⇑e) (n ∘ ⇑e) ↔ VanishesTrivially R m n

Tactic:
simp [VanishesTrivially, ← e.forall_congr_right,
  ← (e.arrowCongr (.refl _)).exists_congr_right, ← e.sum_comp]

Result:
no goals
-- Mathlib/FieldTheory/IntermediateField/Adjoin/Basic.lean
lemma algHomAdjoinIntegralEquiv_symm_apply_gen (h : IsIntegral F α)
    (x : { x // x ∈ (minpoly F α).aroots K }) :
    (algHomAdjoinIntegralEquiv F h).symm x (AdjoinSimple.gen F α) = x :=
  (adjoin.powerBasis h).lift_gen x.val <| by
    rw [adjoin.powerBasis_gen, minpoly_gen]; exact (mem_aroots.mp x.2).2

Proof state:
F : Type u_1
inst✝⁴ : Field F
E : Type u_2
inst✝³ : Field E
inst✝² : Algebra F E
α : E
K : Type u
inst✝¹ : Field K
inst✝ : Algebra F K
h : IsIntegral F α
x : { x // x ∈ (minpoly F α).aroots K }
⊢ (aeval ↑x) (minpoly F α) = 0

Tactic:
exact (mem_aroots.mp x.2).2

Result:
no goals

Proof state:
F : Type u_1
inst✝⁴ : Field F
E : Type u_2
inst✝³ : Field E
inst✝² : Algebra F E
α : E
K : Type u
inst✝¹ : Field K
inst✝ : Algebra F K
h : IsIntegral F α
x : { x // x ∈ (minpoly F α).aroots K }
⊢ (aeval ↑x) (minpoly F (adjoin.powerBasis h).gen) = 0

Tactic:
rw [adjoin.powerBasis_gen, minpoly_gen]

Result:
F : Type u_1
inst✝⁴ : Field F
E : Type u_2
inst✝³ : Field E
inst✝² : Algebra F E
α : E
K : Type u
inst✝¹ : Field K
inst✝ : Algebra F K
h : IsIntegral F α
x : { x // x ∈ (minpoly F α).aroots K }
⊢ (aeval ↑x) (minpoly F α) = 0
-- Mathlib/MeasureTheory/Measure/Tilted.lean
@[simp]
lemma tilted_zero_measure (f : α → ℝ) : (0 : Measure α).tilted f = 0

Proof state:
α : Type u_1
mα : MeasurableSpace α
f : α → ℝ
⊢ Measure.tilted 0 f = 0

Tactic:
simp [Measure.tilted]

Result:
no goals
-- Mathlib/Computability/Ackermann.lean
theorem ack_zero (n : ℕ) : ack 0 n = n + 1

Proof state:
n : ℕ
⊢ ack 0 n = n + 1

Tactic:
rw [ack]

Result:
no goals
-- Mathlib/Algebra/Order/Monoid/Unbundled/WithTop.lean
lemma add_coe_eq_top_iff : x + b = ⊤ ↔ x = ⊤

Proof state:
α : Type u
inst✝ : Add α
x : WithTop α
b : α
⊢ x + ↑b = ⊤ ↔ x = ⊤

Tactic:
simp

Result:
no goals
-- Mathlib/Analysis/Complex/UpperHalfPlane/Basic.lean
@[simp]
lemma coe_mk_subtype {z : ℂ} (hz : 0 < z.im) :
    UpperHalfPlane.coe ⟨z, hz⟩ = z

Proof state:
z : ℂ
hz : 0 < z.im
⊢ ↑⟨z, hz⟩ = z

Tactic:
rfl

Result:
no goals
-- Mathlib/Logic/Relation.lean
@[simp] lemma reflGen_transGen : ReflGen (TransGen r) = ReflTransGen r

Proof state:
case h.h.a
α : Type u_1
r : α → α → Prop
x y : α
⊢ ReflGen (TransGen r) x y ↔ ReflTransGen r x y

Tactic:
simp_rw [reflTransGen_iff_eq_or_transGen, reflGen_iff]

Result:
no goals

Proof state:
α : Type u_1
r : α → α → Prop
⊢ ReflGen (TransGen r) = ReflTransGen r

Tactic:
ext x y

Result:
case h.h.a
α : Type u_1
r : α → α → Prop
x y : α
⊢ ReflGen (TransGen r) x y ↔ ReflTransGen r x y