harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Topology/ContinuousOn.lean
theorem isOpenMap_prod_of_discrete_left [DiscreteTopology α] {f : α × β → γ} :
    IsOpenMap f ↔ ∀ a, IsOpenMap (f ⟨a, ·⟩)

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : DiscreteTopology α
f : α × β → γ
⊢ (∀ (a : α) (b : β), 𝓝 (f (a, b)) ≤ map (f ∘ Prod.mk a) (𝓝 b)) ↔
    ∀ (a : α) (x : β), 𝓝 (f (a, x)) ≤ map (fun x => f (a, x)) (𝓝 x)

Tactic:
rfl

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : DiscreteTopology α
f : α × β → γ
⊢ IsOpenMap f ↔ ∀ (a : α), IsOpenMap fun x => f (a, x)

Tactic:
simp_rw [isOpenMap_iff_nhds_le, Prod.forall, nhds_prod_eq, nhds_discrete, pure_prod, map_map]

Result:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : DiscreteTopology α
f : α × β → γ
⊢ (∀ (a : α) (b : β), 𝓝 (f (a, b)) ≤ map (f ∘ Prod.mk a) (𝓝 b)) ↔
    ∀ (a : α) (x : β), 𝓝 (f (a, x)) ≤ map (fun x => f (a, x)) (𝓝 x)
-- Mathlib/Data/DFinsupp/Sigma.lean
theorem sigmaCurry_add [∀ i j, AddZeroClass (δ i j)] (f g : Π₀ (i : Σ _, _), δ i.1 i.2) :
    #adaptation_note /-- https://github.com/leanprover/lean4/pull/6024
    we needed to add the `(_ : Π₀ (i) (j), δ i j)` type annotation. -/
    sigmaCurry (f + g) = (sigmaCurry f + sigmaCurry g : Π₀ (i) (j), δ i j)

Proof state:
case h.h
ι : Type u
α : ι → Type u_2
δ : (i : ι) → α i → Type v
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → (j : α i) → AddZeroClass (δ i j)
f g : Π₀ (i : (x : ι) × α x), δ i.fst i.snd
i : ι
j : α i
⊢ ((f + g).sigmaCurry i) j = ((f.sigmaCurry + g.sigmaCurry) i) j

Tactic:
rfl

Result:
no goals

Proof state:
ι : Type u
α : ι → Type u_2
δ : (i : ι) → α i → Type v
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → (j : α i) → AddZeroClass (δ i j)
f g : Π₀ (i : (x : ι) × α x), δ i.fst i.snd
⊢ (f + g).sigmaCurry = f.sigmaCurry + g.sigmaCurry

Tactic:
ext (i j)

Result:
case h.h
ι : Type u
α : ι → Type u_2
δ : (i : ι) → α i → Type v
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → (j : α i) → AddZeroClass (δ i j)
f g : Π₀ (i : (x : ι) × α x), δ i.fst i.snd
i : ι
j : α i
⊢ ((f + g).sigmaCurry i) j = ((f.sigmaCurry + g.sigmaCurry) i) j
-- Mathlib/Topology/EMetricSpace/Lipschitz.lean
lemma lipschitzOnWith_restrict {t : Set s} :
    LipschitzOnWith K (s.restrict f) t ↔ LipschitzOnWith K f (s ∩ Subtype.val '' t)

Proof state:
α : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
K : ℝ≥0
s : Set α
f : α → β
t : Set ↑s
⊢ LipschitzOnWith K (s.restrict f) t ↔ LipschitzOnWith K f (s ∩ Subtype.val '' t)

Tactic:
simp [LipschitzOnWith, LipschitzWith]

Result:
no goals
-- Mathlib/GroupTheory/PGroup.lean
theorem map {H : Subgroup G} (hH : IsPGroup p H) {K : Type*} [Group K] (ϕ : G →* K) :
    IsPGroup p (H.map ϕ)

Proof state:
p : ℕ
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
hH : IsPGroup p ↥H
K : Type u_2
inst✝ : Group K
ϕ : G →* K
⊢ IsPGroup p ↥(ϕ.comp H.subtype).range

Tactic:
exact hH.of_surjective (ϕ.restrict H).rangeRestrict (ϕ.restrict H).rangeRestrict_surjective

Result:
no goals

Proof state:
p : ℕ
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
hH : IsPGroup p ↥H
K : Type u_2
inst✝ : Group K
ϕ : G →* K
⊢ IsPGroup p ↥(Subgroup.map ϕ H)

Tactic:
rw [← H.range_subtype, MonoidHom.map_range]

Result:
p : ℕ
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
hH : IsPGroup p ↥H
K : Type u_2
inst✝ : Group K
ϕ : G →* K
⊢ IsPGroup p ↥(ϕ.comp H.subtype).range
-- Mathlib/Algebra/Polynomial/FieldDivision.lean
theorem mem_roots_map [CommRing k] [IsDomain k] {f : R →+* k} {x : k} (hp : p ≠ 0) :
    x ∈ (p.map f).roots ↔ p.eval₂ f x = 0

Proof state:
R : Type u
k : Type y
inst✝² : Field R
p : R[X]
inst✝¹ : CommRing k
inst✝ : IsDomain k
f : R →+* k
x : k
hp : p ≠ 0
⊢ x ∈ (map f p).roots ↔ eval₂ f x p = 0

Tactic:
rw [mem_roots (map_ne_zero hp), IsRoot, Polynomial.eval_map]

Result:
no goals
-- Mathlib/MeasureTheory/Measure/MeasureSpace.lean
theorem sum_comm {ι' : Type*} (μ : ι → ι' → Measure α) :
    (sum fun n => sum (μ n)) = sum fun m => sum fun n => μ n m

Proof state:
case h
α : Type u_1
ι : Type u_5
m0 : MeasurableSpace α
ι' : Type u_8
μ : ι → ι' → Measure α
s : Set α
hs : MeasurableSet s
⊢ ∑' (i : ι) (i_1 : ι'), (μ i i_1) s = ∑' (i : ι') (i_1 : ι), (μ i_1 i) s

Tactic:
rw [ENNReal.tsum_comm]

Result:
no goals

Proof state:
α : Type u_1
ι : Type u_5
m0 : MeasurableSpace α
ι' : Type u_8
μ : ι → ι' → Measure α
⊢ (sum fun n => sum (μ n)) = sum fun m => sum fun n => μ n m

Tactic:
ext1 s hs

Result:
case h
α : Type u_1
ι : Type u_5
m0 : MeasurableSpace α
ι' : Type u_8
μ : ι → ι' → Measure α
s : Set α
hs : MeasurableSet s
⊢ (sum fun n => sum (μ n)) s = (sum fun m => sum fun n => μ n m) s

Proof state:
case h
α : Type u_1
ι : Type u_5
m0 : MeasurableSpace α
ι' : Type u_8
μ : ι → ι' → Measure α
s : Set α
hs : MeasurableSet s
⊢ (sum fun n => sum (μ n)) s = (sum fun m => sum fun n => μ n m) s

Tactic:
simp_rw [sum_apply _ hs]

Result:
case h
α : Type u_1
ι : Type u_5
m0 : MeasurableSpace α
ι' : Type u_8
μ : ι → ι' → Measure α
s : Set α
hs : MeasurableSet s
⊢ ∑' (i : ι) (i_1 : ι'), (μ i i_1) s = ∑' (i : ι') (i_1 : ι), (μ i_1 i) s
-- Mathlib/LinearAlgebra/AffineSpace/FiniteDimensional.lean
theorem coplanar_insert_iff_of_mem_affineSpan {s : Set P} {p : P} (h : p ∈ affineSpan k s) :
    Coplanar k (insert p s) ↔ Coplanar k s

Proof state:
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : Set P
p : P
h : p ∈ affineSpan k s
⊢ Coplanar k (insert p s) ↔ Coplanar k s

Tactic:
rw [Coplanar, Coplanar, vectorSpan_insert_eq_vectorSpan h]

Result:
no goals
-- Mathlib/Algebra/Order/Antidiag/Nat.lean
theorem card_pair_lcm_eq {n : ℕ} (hn : Squarefree n) :
    #{p ∈ (n.divisors ×ˢ n.divisors) | p.1.lcm p.2 = n} = 3 ^ ω n

Proof state:
n : ℕ
hn : Squarefree n
⊢ #(finMulAntidiag 3 n) = #(filter (fun p => p.1.lcm p.2 = n) (n.divisors ×ˢ n.divisors))

Tactic:
apply Finset.card_bij f (f_img hn) (f_inj) (f_surj hn.ne_zero)

Result:
no goals

Proof state:
n : ℕ
hn : Squarefree n
⊢ #(filter (fun p => p.1.lcm p.2 = n) (n.divisors ×ˢ n.divisors)) = 3 ^ ω n

Tactic:
rw [← card_finMulAntidiag_of_squarefree hn, eq_comm]

Result:
n : ℕ
hn : Squarefree n
⊢ #(finMulAntidiag 3 n) = #(filter (fun p => p.1.lcm p.2 = n) (n.divisors ×ˢ n.divisors))
-- Mathlib/Algebra/Order/BigOperators/Group/LocallyFinite.lean
@[to_additive]
lemma left_mul_prod_Ioi (a : α) : f a * ∏ x ∈ Ioi a, f x = ∏ x ∈ Ici a, f x

Proof state:
α : Type u_1
β : Type u_2
inst✝² : PartialOrder α
inst✝¹ : CommMonoid β
f : α → β
inst✝ : LocallyFiniteOrderTop α
a : α
⊢ f a * ∏ x ∈ Ioi a, f x = ∏ x ∈ Ici a, f x

Tactic:
rw [Ici_eq_cons_Ioi, prod_cons]

Result:
no goals
-- Mathlib/CategoryTheory/Limits/Shapes/BinaryBiproducts.lean
theorem biprod.braiding'_eq_braiding {P Q : C} : biprod.braiding' P Q = biprod.braiding P Q

Proof state:
C : Type uC
inst✝² : Category.{uC', uC} C
inst✝¹ : HasZeroMorphisms C
inst✝ : HasBinaryBiproducts C
P Q : C
⊢ braiding' P Q = braiding P Q

Tactic:
aesop_cat

Result:
no goals
-- Mathlib/Order/Filter/Partial.lean
theorem rmap_rmap (r : Rel α β) (s : Rel β γ) (l : Filter α) :
    rmap s (rmap r l) = rmap (r.comp s) l :=
  filter_eq <| by simp [rmap_sets, Set.preimage, Rel.core_comp]

Proof state:
α : Type u
β : Type v
γ : Type w
r : Rel α β
s : Rel β γ
l : Filter α
⊢ (rmap s (rmap r l)).sets = (rmap (r.comp s) l).sets

Tactic:
simp [rmap_sets, Set.preimage, Rel.core_comp]

Result:
no goals
-- Mathlib/RingTheory/Ideal/Prime.lean
theorem bot_prime [Nontrivial α] [NoZeroDivisors α] : (⊥ : Ideal α).IsPrime :=
  ⟨fun h => one_ne_zero (α := α) (by rwa [Ideal.eq_top_iff_one, Submodule.mem_bot] at h), fun h =>
    mul_eq_zero.mp (by simpa only [Submodule.mem_bot] using h)⟩

Proof state:
α : Type u
inst✝² : Semiring α
inst✝¹ : Nontrivial α
inst✝ : NoZeroDivisors α
x✝ y✝ : α
h : x✝ * y✝ ∈ ⊥
⊢ x✝ * y✝ = 0

Tactic:
simpa only [Submodule.mem_bot] using h

Result:
no goals

Proof state:
α : Type u
inst✝² : Semiring α
inst✝¹ : Nontrivial α
inst✝ : NoZeroDivisors α
h : ⊥ = ⊤
⊢ 1 = 0

Tactic:
rwa [Ideal.eq_top_iff_one, Submodule.mem_bot] at h

Result:
no goals
-- Mathlib/FieldTheory/SeparableDegree.lean
theorem natSepDegree_le_natDegree : f.natSepDegree ≤ f.natDegree

Proof state:
F : Type u
inst✝ : Field F
f : F[X]
⊢ f.natSepDegree ≤ f.natDegree

Tactic:
have := f.map (algebraMap F f.SplittingField) |>.card_roots'

Result:
F : Type u
inst✝ : Field F
f : F[X]
this : (map (algebraMap F f.SplittingField) f).roots.card ≤ (map (algebraMap F f.SplittingField) f).natDegree
⊢ f.natSepDegree ≤ f.natDegree

Proof state:
F : Type u
inst✝ : Field F
f : F[X]
this : (map (algebraMap F f.SplittingField) f).roots.card ≤ (map (algebraMap F f.SplittingField) f).natDegree
⊢ f.natSepDegree ≤ f.natDegree

Tactic:
rw [← aroots_def, natDegree_map] at this

Result:
F : Type u
inst✝ : Field F
f : F[X]
this : (f.aroots f.SplittingField).card ≤ f.natDegree
⊢ f.natSepDegree ≤ f.natDegree

Proof state:
F : Type u
inst✝ : Field F
f : F[X]
this : (f.aroots f.SplittingField).card ≤ f.natDegree
⊢ f.natSepDegree ≤ f.natDegree

Tactic:
exact (f.aroots f.SplittingField).toFinset_card_le.trans this

Result:
no goals

Proof state:
F : Type u
inst✝ : Field F
f : F[X]
this : (f.aroots f.SplittingField).card ≤ f.natDegree
⊢ f.natSepDegree ≤ f.natDegree

Tactic:
classical
exact (f.aroots f.SplittingField).toFinset_card_le.trans this

Result:
no goals
-- Mathlib/AlgebraicGeometry/EllipticCurve/Jacobian.lean
lemma add_of_Y_eq {P Q : Fin 3 → F} (hPz : P z ≠ 0) (hQz : Q z ≠ 0)
    (hx : P x * Q z ^ 2 = Q x * P z ^ 2) (hy : P y * Q z ^ 3 = Q y * P z ^ 3)
    (hy' : P y * Q z ^ 3 = W.negY Q * P z ^ 3) : W.add P Q = W.dblU P • ![1, 1, 0]

Proof state:
F : Type u
inst✝ : Field F
W : Jacobian F
P Q : Fin 3 → F
hPz : P z ≠ 0
hQz : Q z ≠ 0
hx : P x * Q z ^ 2 = Q x * P z ^ 2
hy : P y * Q z ^ 3 = Q y * P z ^ 3
hy' : P y * Q z ^ 3 = W.negY Q * P z ^ 3
⊢ W.add P Q = W.dblU P • ![1, 1, 0]

Tactic:
rw [add, if_pos <| equiv_of_X_eq_of_Y_eq hPz hQz hx hy, dblXYZ_of_Y_eq hQz hx hy hy']

Result:
no goals
-- Mathlib/MeasureTheory/Function/StronglyMeasurable/AEStronglyMeasurable.lean
lemma of_trim {m₀' : MeasurableSpace α} (hm₀ : m₀' ≤ m₀)
    (hf : AEStronglyMeasurable[m] f (μ.trim hm₀)) : AEStronglyMeasurable[m] f μ

Proof state:
α : Type u_1
β : Type u_2
inst✝ : TopologicalSpace β
m m₀ : MeasurableSpace α
μ : Measure α
f : α → β
m₀' : MeasurableSpace α
hm₀ : m₀' ≤ m₀
hf : AEStronglyMeasurable f (μ.trim hm₀)
⊢ AEStronglyMeasurable f μ

Tactic:
obtain ⟨g, hg_meas, hfg⟩ := hf

Result:
case intro.intro
α : Type u_1
β : Type u_2
inst✝ : TopologicalSpace β
m m₀ : MeasurableSpace α
μ : Measure α
f : α → β
m₀' : MeasurableSpace α
hm₀ : m₀' ≤ m₀
g : α → β
hg_meas : StronglyMeasurable g
hfg : f =ᶠ[ae (μ.trim hm₀)] g
⊢ AEStronglyMeasurable f μ

Proof state:
case intro.intro
α : Type u_1
β : Type u_2
inst✝ : TopologicalSpace β
m m₀ : MeasurableSpace α
μ : Measure α
f : α → β
m₀' : MeasurableSpace α
hm₀ : m₀' ≤ m₀
g : α → β
hg_meas : StronglyMeasurable g
hfg : f =ᶠ[ae (μ.trim hm₀)] g
⊢ AEStronglyMeasurable f μ

Tactic:
exact ⟨g, hg_meas, ae_eq_of_ae_eq_trim hfg⟩

Result:
no goals
-- Mathlib/MeasureTheory/Integral/SetIntegral.lean
theorem norm_setIntegral_le_of_norm_le_const_ae {C : ℝ} (hs : μ s < ∞)
    (hC : ∀ᵐ x ∂μ.restrict s, ‖f x‖ ≤ C) : ‖∫ x in s, f x ∂μ‖ ≤ C * (μ s).toReal

Proof state:
X : Type u_1
E : Type u_3
mX : MeasurableSpace X
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : X → E
s : Set X
μ : Measure X
C : ℝ
hs : μ s < ⊤
hC : ∀ᵐ (x : X) ∂μ.restrict s, ‖f x‖ ≤ C
⊢ ‖∫ (x : X) in s, f x ∂μ‖ ≤ C * (μ s).toReal

Tactic:
rw [← Measure.restrict_apply_univ] at *

Result:
X : Type u_1
E : Type u_3
mX : MeasurableSpace X
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : X → E
s : Set X
μ : Measure X
C : ℝ
hs : (μ.restrict s) univ < ⊤
hC : ∀ᵐ (x : X) ∂μ.restrict s, ‖f x‖ ≤ C
⊢ ‖∫ (x : X) in s, f x ∂μ‖ ≤ C * ((μ.restrict s) univ).toReal

Proof state:
X : Type u_1
E : Type u_3
mX : MeasurableSpace X
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : X → E
s : Set X
μ : Measure X
C : ℝ
hs : (μ.restrict s) univ < ⊤
hC : ∀ᵐ (x : X) ∂μ.restrict s, ‖f x‖ ≤ C
this : IsFiniteMeasure (μ.restrict s)
⊢ ‖∫ (x : X) in s, f x ∂μ‖ ≤ C * ((μ.restrict s) univ).toReal

Tactic:
exact norm_integral_le_of_norm_le_const hC

Result:
no goals

Proof state:
X : Type u_1
E : Type u_3
mX : MeasurableSpace X
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : X → E
s : Set X
μ : Measure X
C : ℝ
hs : (μ.restrict s) univ < ⊤
hC : ∀ᵐ (x : X) ∂μ.restrict s, ‖f x‖ ≤ C
⊢ ‖∫ (x : X) in s, f x ∂μ‖ ≤ C * ((μ.restrict s) univ).toReal

Tactic:
haveI : IsFiniteMeasure (μ.restrict s) := ⟨hs⟩

Result:
X : Type u_1
E : Type u_3
mX : MeasurableSpace X
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : X → E
s : Set X
μ : Measure X
C : ℝ
hs : (μ.restrict s) univ < ⊤
hC : ∀ᵐ (x : X) ∂μ.restrict s, ‖f x‖ ≤ C
this : IsFiniteMeasure (μ.restrict s)
⊢ ‖∫ (x : X) in s, f x ∂μ‖ ≤ C * ((μ.restrict s) univ).toReal
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Lemmas.lean
theorem getElem?_insert (l : List α) (a : α) (i : Nat) :
    (l.insert a)[i]? = if a ∈ l then l[i]? else if i = 0 then some a else l[i-1]?

Proof state:
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
l : List α
a : α
i : Nat
⊢ (List.insert a l)[i]? = if a ∈ l then l[i]? else if i = 0 then some a else l[i - 1]?

Tactic:
cases i

Result:
case zero
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
l : List α
a : α
⊢ (List.insert a l)[0]? = if a ∈ l then l[0]? else if 0 = 0 then some a else l[0 - 1]?

case succ
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
l : List α
a : α
n✝ : Nat
⊢ (List.insert a l)[n✝ + 1]? = if a ∈ l then l[n✝ + 1]? else if n✝ + 1 = 0 then some a else l[n✝ + 1 - 1]?

Proof state:
case zero
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
l : List α
a : α
⊢ (List.insert a l)[0]? = if a ∈ l then l[0]? else if 0 = 0 then some a else l[0 - 1]?

Tactic:
simp [getElem?_insert_zero]

Result:
no goals

Proof state:
case succ
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
l : List α
a : α
n✝ : Nat
⊢ (List.insert a l)[n✝ + 1]? = if a ∈ l then l[n✝ + 1]? else if n✝ + 1 = 0 then some a else l[n✝ + 1 - 1]?

Tactic:
simp [getElem?_insert_succ]

Result:
no goals
-- Mathlib/Tactic/PNatToNat.lean
@[pnat_to_nat_coe]
lemma coe_lt_coe (m n : PNat) : m < n ↔ (m : ℕ) < (n : ℕ)

Proof state:
m n : ℕ+
⊢ m < n ↔ ↑m < ↑n

Tactic:
simp

Result:
no goals
-- Mathlib/Data/Matroid/Map.lean
@[simp] lemma restrictSubtype_indep_iff {I : Set X} :
    (M.restrictSubtype X).Indep I ↔ M.Indep ((↑) '' I)

Proof state:
α : Type u_1
X : Set α
M : Matroid α
I : Set ↑X
⊢ (M.restrictSubtype X).Indep I ↔ M.Indep ↑I

Tactic:
simp [restrictSubtype, Subtype.val_injective.injOn]

Result:
no goals
-- Mathlib/Logic/Equiv/Fin.lean
theorem finRotate_of_lt {k : ℕ} (h : k < n) :
    finRotate (n + 1) ⟨k, h.trans_le n.le_succ⟩ = ⟨k + 1, Nat.succ_lt_succ h⟩

Proof state:
n k : ℕ
h : k < n
⊢ (finRotate (n + 1)) ⟨k, ⋯⟩ = ⟨k + 1, ⋯⟩

Tactic:
ext

Result:
case h
n k : ℕ
h : k < n
⊢ ↑((finRotate (n + 1)) ⟨k, ⋯⟩) = ↑⟨k + 1, ⋯⟩

Proof state:
case h
n k : ℕ
h : k < n
⊢ ↑(finAddFlip ⟨k, ⋯⟩) = k + 1

Tactic:
simp [finAddFlip_apply_mk_left h, Nat.add_comm]

Result:
no goals

Proof state:
case h
n k : ℕ
h : k < n
⊢ ↑((finRotate (n + 1)) ⟨k, ⋯⟩) = ↑⟨k + 1, ⋯⟩

Tactic:
dsimp [finRotate_succ]

Result:
case h
n k : ℕ
h : k < n
⊢ ↑(finAddFlip ⟨k, ⋯⟩) = k + 1
-- Mathlib/LinearAlgebra/CliffordAlgebra/Prod.lean
@[simp]
lemma toProd_ι_tmul_one (m₁ : M₁) : toProd Q₁ Q₂ (ι _ m₁ ᵍ⊗ₜ 1) = ι _ (m₁, 0)

Proof state:
R : Type u_1
M₁ : Type u_2
M₂ : Type u_3
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M₁
inst✝² : AddCommGroup M₂
inst✝¹ : Module R M₁
inst✝ : Module R M₂
Q₁ : QuadraticForm R M₁
Q₂ : QuadraticForm R M₂
m₁ : M₁
⊢ (toProd Q₁ Q₂) ((ι Q₁) m₁ ᵍ⊗ₜ[R] 1) = (ι (QuadraticMap.prod Q₁ Q₂)) (m₁, 0)

Tactic:
rw [toProd, GradedTensorProduct.lift_tmul, map_one, mul_one, map_apply_ι,
  QuadraticMap.Isometry.inl_apply]

Result:
no goals
-- Mathlib/Algebra/GroupWithZero/Action/Defs.lean
lemma smul_ite_zero (p : Prop) [Decidable p] (a : M) (b : A) :
    (a • if p then b else 0) = if p then a • b else 0

Proof state:
M : Type u_1
A : Type u_3
inst✝² : Zero A
inst✝¹ : SMulZeroClass M A
p : Prop
inst✝ : Decidable p
a : M
b : A
⊢ (a • if p then b else 0) = if p then a • b else 0

Tactic:
split_ifs <;> simp

Result:
no goals
-- Mathlib/Data/Seq/Computation.lean
theorem LiftRelAux.swap (R : α → β → Prop) (C) (a b) :
    LiftRelAux (swap R) (swap C) b a = LiftRelAux R C a b

Proof state:
α : Type u
β : Type v
R : α → β → Prop
C : Computation α → Computation β → Prop
a : α ⊕ Computation α
b : β ⊕ Computation β
⊢ LiftRelAux (Function.swap R) (Function.swap C) b a = LiftRelAux R C a b

Tactic:
rcases a with a | ca <;> rcases b with b | cb <;> simp only [LiftRelAux]

Result:
no goals
-- Mathlib/Data/List/Sort.lean
theorem orderedInsert_count [DecidableEq α] (L : List α) (a b : α) :
    count a (L.orderedInsert r b) = count a L + if b = a then 1 else 0

Proof state:
α : Type u
r : α → α → Prop
inst✝¹ : DecidableRel r
inst✝ : DecidableEq α
L : List α
a b : α
⊢ count a (orderedInsert r b L) = count a L + if b = a then 1 else 0

Tactic:
rw [(L.perm_orderedInsert r b).count_eq, count_cons]

Result:
α : Type u
r : α → α → Prop
inst✝¹ : DecidableRel r
inst✝ : DecidableEq α
L : List α
a b : α
⊢ (count a L + if (b == a) = true then 1 else 0) = count a L + if b = a then 1 else 0

Proof state:
α : Type u
r : α → α → Prop
inst✝¹ : DecidableRel r
inst✝ : DecidableEq α
L : List α
a b : α
⊢ (count a L + if (b == a) = true then 1 else 0) = count a L + if b = a then 1 else 0

Tactic:
simp

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/TakeDrop.lean
theorem head?_takeWhile (p : α → Bool) (l : List α) : (l.takeWhile p).head? = l.head?.filter p

Proof state:
case nil
α : Type u_1
p : α → Bool
⊢ (takeWhile p []).head? = Option.filter p [].head?

Tactic:
rfl

Result:
no goals

Proof state:
case cons
α : Type u_1
p : α → Bool
x : α
xs : List α
⊢ (takeWhile p (x :: xs)).head? = Option.filter p (x :: xs).head?

Tactic:
simp only [takeWhile_cons, head?_cons, Option.filter_some]

Result:
case cons
α : Type u_1
p : α → Bool
x : α
xs : List α
⊢ (if p x = true then x :: takeWhile p xs else []).head? = if p x = true then some x else none

Proof state:
α : Type u_1
p : α → Bool
l : List α
⊢ (takeWhile p l).head? = Option.filter p l.head?

Tactic:
cases l with
| nil => rfl
| cons x xs =>
  simp only [takeWhile_cons, head?_cons, Option.filter_some]
  split <;> simp

Result:
no goals

Proof state:
case cons
α : Type u_1
p : α → Bool
x : α
xs : List α
⊢ (if p x = true then x :: takeWhile p xs else []).head? = if p x = true then some x else none

Tactic:
split <;> simp

Result:
no goals
-- Mathlib/Topology/Maps/Basic.lean
theorem isOpenMap_iff (hg : IsOpenEmbedding g) :
    IsOpenMap f ↔ IsOpenMap (g ∘ f)

Proof state:
X : Type u_1
Y : Type u_2
Z : Type u_3
f : X → Y
g : Y → Z
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
hg : IsOpenEmbedding g
⊢ IsOpenMap f ↔ IsOpenMap (g ∘ f)

Tactic:
simp_rw [isOpenMap_iff_nhds_le, ← map_map, comp, ← hg.map_nhds_eq, map_le_map_iff hg.injective]

Result:
no goals
-- Mathlib/Algebra/Polynomial/Basic.lean
theorem support_erase (p : R[X]) (n : ℕ) : support (p.erase n) = (support p).erase n

Proof state:
case ofFinsupp
R : Type u
inst✝ : Semiring R
n : ℕ
toFinsupp✝ : R[ℕ]
⊢ (erase n { toFinsupp := toFinsupp✝ }).support = { toFinsupp := toFinsupp✝ }.support.erase n

Tactic:
simp only [support, erase_def, Finsupp.support_erase]

Result:
no goals

Proof state:
R : Type u
inst✝ : Semiring R
p : R[X]
n : ℕ
⊢ (erase n p).support = p.support.erase n

Tactic:
rcases p with ⟨⟩

Result:
case ofFinsupp
R : Type u
inst✝ : Semiring R
n : ℕ
toFinsupp✝ : R[ℕ]
⊢ (erase n { toFinsupp := toFinsupp✝ }).support = { toFinsupp := toFinsupp✝ }.support.erase n
-- Mathlib/.lake/packages/lean4/src/lean/Init/ByCases.lean
theorem dite_some_none_eq_none [Decidable P] {x : P → α} :
    (if h : P then some (x h) else none) = none ↔ ¬P

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

Tactic:
simp

Result:
no goals
-- Mathlib/Analysis/InnerProductSpace/Calculus.lean
theorem contDiff_univBall : ContDiff ℝ n (univBall c r)

Proof state:
n : ℕ∞
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
c : E
r : ℝ
⊢ ContDiff ℝ ↑n
    ↑(if h : 0 < r then univUnitBall.trans' (unitBallBall c r h) ⋯
      else (IsometryEquiv.vaddConst c).toHomeomorph.toPartialHomeomorph)

Tactic:
split_ifs with h

Result:
case pos
n : ℕ∞
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
c : E
r : ℝ
h : 0 < r
⊢ ContDiff ℝ ↑n ↑(univUnitBall.trans' (unitBallBall c r h) ⋯)

case neg
n : ℕ∞
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
c : E
r : ℝ
h : ¬0 < r
⊢ ContDiff ℝ ↑n ↑(IsometryEquiv.vaddConst c).toHomeomorph.toPartialHomeomorph

Proof state:
n : ℕ∞
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
c : E
r : ℝ
⊢ ContDiff ℝ ↑n ↑(univBall c r)

Tactic:
unfold univBall

Result:
n : ℕ∞
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
c : E
r : ℝ
⊢ ContDiff ℝ ↑n
    ↑(if h : 0 < r then univUnitBall.trans' (unitBallBall c r h) ⋯
      else (IsometryEquiv.vaddConst c).toHomeomorph.toPartialHomeomorph)

Proof state:
case neg
n : ℕ∞
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
c : E
r : ℝ
h : ¬0 < r
⊢ ContDiff ℝ ↑n ↑(IsometryEquiv.vaddConst c).toHomeomorph.toPartialHomeomorph

Tactic:
exact contDiff_id.add contDiff_const

Result:
no goals

Proof state:
case pos
n : ℕ∞
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
c : E
r : ℝ
h : 0 < r
⊢ ContDiff ℝ ↑n ↑(univUnitBall.trans' (unitBallBall c r h) ⋯)

Tactic:
exact (contDiff_unitBallBall h).comp contDiff_univUnitBall

Result:
no goals
-- Mathlib/Data/Nat/Choose/Basic.lean
theorem multichoose_succ_succ (n k : ℕ) :
    multichoose (n + 1) (k + 1) = multichoose n (k + 1) + multichoose (n + 1) k

Proof state:
n k : ℕ
⊢ (n + 1).multichoose (k + 1) = n.multichoose (k + 1) + (n + 1).multichoose k

Tactic:
simp [multichoose]

Result:
no goals
-- Mathlib/Data/Matroid/Dual.lean
theorem dual_dual (M : Matroid α) : M✶✶ = M :=
  ext_isBase rfl (fun B (h : B ⊆ M.E) ↦
    by rw [dual_isBase_iff, dual_isBase_iff, dual_ground, diff_diff_cancel_left h])

Proof state:
α : Type u_1
M : Matroid α
B : Set α
h : B ⊆ M.E
⊢ M✶✶.IsBase B ↔ M.IsBase B

Tactic:
rw [dual_isBase_iff, dual_isBase_iff, dual_ground, diff_diff_cancel_left h]

Result:
no goals
-- Mathlib/FieldTheory/IntermediateField/Adjoin/Defs.lean
theorem extendScalars_top : extendScalars (le_top : F ≤ ⊤) = ⊤ :=
  restrictScalars_injective K (by simp)

Proof state:
K : Type u_1
inst✝² : Field K
L : Type u_2
inst✝¹ : Field L
inst✝ : Algebra K L
F : IntermediateField K L
⊢ restrictScalars K (extendScalars ⋯) = restrictScalars K ⊤

Tactic:
simp

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Int/Order.lean
theorem add_lt_of_lt_neg_add {a b c : Int} (h : b < -a + c) : a + b < c

Proof state:
a b c : Int
h✝ : b < -a + c
h : a + b < a + (-a + c)
⊢ a + b < c

Tactic:
rwa [Int.add_neg_cancel_left] at h

Result:
no goals

Proof state:
a b c : Int
h : b < -a + c
⊢ a + b < c

Tactic:
have h := Int.add_lt_add_left h a

Result:
a b c : Int
h✝ : b < -a + c
h : a + b < a + (-a + c)
⊢ a + b < c
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Int/DivModLemmas.lean
theorem dvd_add : ∀ {a b c : Int}, a ∣ b → a ∣ c → a ∣ b + c
  | _, _, _, ⟨d, rfl⟩, ⟨e, rfl⟩ => ⟨d + e, by rw [Int.mul_add]⟩

Proof state:
a✝ d e : Int
⊢ a✝ * d + a✝ * e = a✝ * (d + e)

Tactic:
rw [Int.mul_add]

Result:
no goals