harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Count.lean
theorem size_eq_countP_add_countP (l : Vector α n) : n = countP p l + countP (fun a => ¬p a) l

Proof state:
case mk
α : Type u_1
p : α → Bool
l : Array α
⊢ l.size =
    countP p { toArray := l, size_toArray := ⋯ } +
      countP (fun a => decide ¬p a = true) { toArray := l, size_toArray := ⋯ }

Tactic:
simp [List.length_eq_countP_add_countP (p := p)]

Result:
no goals

Proof state:
α : Type u_1
p : α → Bool
n : Nat
l : Vector α n
⊢ n = countP p l + countP (fun a => decide ¬p a = true) l

Tactic:
rcases l with ⟨l, rfl⟩

Result:
case mk
α : Type u_1
p : α → Bool
l : Array α
⊢ l.size =
    countP p { toArray := l, size_toArray := ⋯ } +
      countP (fun a => decide ¬p a = true) { toArray := l, size_toArray := ⋯ }
-- Mathlib/Order/SymmDiff.lean
theorem top_bihimp : ⊤ ⇔ a = a

Proof state:
α : Type u_2
inst✝ : GeneralizedHeytingAlgebra α
a : α
⊢ ⊤ ⇔ a = a

Tactic:
rw [bihimp_comm, bihimp_top]

Result:
no goals
-- Mathlib/AlgebraicGeometry/EllipticCurve/Affine.lean
lemma map_map (P : W'⟮F⟯) : map g (map f P) = map (g.comp f) P

Proof state:
R : Type r
S : Type s
F : Type u
K : Type v
L : Type w
inst✝¹⁴ : CommRing R
inst✝¹³ : CommRing S
inst✝¹² : Field F
inst✝¹¹ : Field K
inst✝¹⁰ : Field L
W' : Affine R
inst✝⁹ : Algebra R S
inst✝⁸ : Algebra R F
inst✝⁷ : Algebra S F
inst✝⁶ : IsScalarTower R S F
inst✝⁵ : Algebra R K
inst✝⁴ : Algebra S K
inst✝³ : IsScalarTower R S K
inst✝² : Algebra R L
inst✝¹ : Algebra S L
inst✝ : IsScalarTower R S L
f : F →ₐ[S] K
g : K →ₐ[S] L
P : W'⟮F⟯
⊢ (map g) ((map f) P) = (map (g.comp f)) P

Tactic:
cases P <;> rfl

Result:
no goals
-- Mathlib/Data/List/Chain.lean
theorem chain_append_cons_cons {a b c : α} {l₁ l₂ : List α} :
    Chain R a (l₁ ++ b :: c :: l₂) ↔ Chain R a (l₁ ++ [b]) ∧ R b c ∧ Chain R c l₂

Proof state:
α : Type u
R : α → α → Prop
a b c : α
l₁ l₂ : List α
⊢ Chain R a (l₁ ++ b :: c :: l₂) ↔ Chain R a (l₁ ++ [b]) ∧ R b c ∧ Chain R c l₂

Tactic:
rw [chain_split, chain_cons]

Result:
no goals
-- Mathlib/Topology/Separation/Regular.lean
theorem Topology.IsEmbedding.t5Space [TopologicalSpace Y] [T5Space Y] {e : X → Y}
    (he : IsEmbedding e) : T5Space X where
  __ := he.t1Space
  completely_normal

Proof state:
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : T5Space Y
e : X → Y
he : IsEmbedding e
this : CompletelyNormalSpace X
⊢ ∀ ⦃s t : Set X⦄, Disjoint (closure s) t → Disjoint s (closure t) → Disjoint (𝓝ˢ s) (𝓝ˢ t)

Tactic:
exact completely_normal

Result:
no goals

Proof state:
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : T5Space Y
e : X → Y
he : IsEmbedding e
⊢ ∀ ⦃s t : Set X⦄, Disjoint (closure s) t → Disjoint s (closure t) → Disjoint (𝓝ˢ s) (𝓝ˢ t)

Tactic:
have := he.completelyNormalSpace

Result:
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : T5Space Y
e : X → Y
he : IsEmbedding e
this : CompletelyNormalSpace X
⊢ ∀ ⦃s t : Set X⦄, Disjoint (closure s) t → Disjoint s (closure t) → Disjoint (𝓝ˢ s) (𝓝ˢ t)
-- Mathlib/Order/Bounded.lean
theorem unbounded_le_inter_lt [LinearOrder α] (a : α) :
    Unbounded (· ≤ ·) (s ∩ { b | a < b }) ↔ Unbounded (· ≤ ·) s

Proof state:
case h.e'_1.h.e'_3.h.e'_4.h.e'_2.h.a
α : Type u_1
s : Set α
inst✝ : LinearOrder α
a x✝ : α
⊢ a < x✝ ↔ ¬x✝ ≤ a

Tactic:
exact lt_iff_not_le

Result:
no goals

Proof state:
α : Type u_1
s : Set α
inst✝ : LinearOrder α
a : α
⊢ Unbounded (fun x1 x2 => x1 ≤ x2) (s ∩ {b | a < b}) ↔ Unbounded (fun x1 x2 => x1 ≤ x2) s

Tactic:
convert @unbounded_le_inter_not_le _ s _ a

Result:
case h.e'_1.h.e'_3.h.e'_4.h.e'_2.h.a
α : Type u_1
s : Set α
inst✝ : LinearOrder α
a x✝ : α
⊢ a < x✝ ↔ ¬x✝ ≤ a
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Nat/Basic.lean
theorem sub_one_eq_self {n : Nat} : n - 1 = n ↔ n = 0

Proof state:
n : Nat
⊢ n - 1 = n ↔ n = 0

Tactic:
cases n <;> simp [ne_add_one]

Result:
no goals
-- Mathlib/Algebra/Order/Group/Pointwise/Interval.lean
theorem image_sub_const_Iic : (fun x => x - a) '' Iic b = Iic (b - a)

Proof state:
α : Type u_1
inst✝ : OrderedAddCommGroup α
a b : α
⊢ (fun x => x - a) '' Iic b = Iic (b - a)

Tactic:
simp [sub_eq_neg_add]

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Path.lean
theorem isBridge_iff_adj_and_forall_cycle_not_mem {v w : V} : G.IsBridge s(v, w) ↔
    G.Adj v w ∧ ∀ ⦃u : V⦄ (p : G.Walk u u), p.IsCycle → s(v, w) ∉ p.edges

Proof state:
V : Type u
G : SimpleGraph V
v w : V
⊢ G.Adj v w → (¬(G \ fromEdgeSet {s(v, w)}).Reachable v w ↔ ∀ ⦃u : V⦄ (p : G.Walk u u), p.IsCycle → s(v, w) ∉ p.edges)

Tactic:
intro h

Result:
V : Type u
G : SimpleGraph V
v w : V
h : G.Adj v w
⊢ ¬(G \ fromEdgeSet {s(v, w)}).Reachable v w ↔ ∀ ⦃u : V⦄ (p : G.Walk u u), p.IsCycle → s(v, w) ∉ p.edges

Proof state:
V : Type u
G : SimpleGraph V
v w : V
h : G.Adj v w
⊢ (G \ fromEdgeSet {s(v, w)}).Reachable v w ↔ ∃ u p, p.IsCycle ∧ s(v, w) ∈ p.edges

Tactic:
rw [← adj_and_reachable_delete_edges_iff_exists_cycle]

Result:
V : Type u
G : SimpleGraph V
v w : V
h : G.Adj v w
⊢ (G \ fromEdgeSet {s(v, w)}).Reachable v w ↔ G.Adj v w ∧ (G \ fromEdgeSet {s(v, w)}).Reachable v w

Proof state:
V : Type u
G : SimpleGraph V
v w : V
h : G.Adj v w
⊢ ¬¬(G \ fromEdgeSet {s(v, w)}).Reachable v w ↔ ¬∀ ⦃u : V⦄ (p : G.Walk u u), p.IsCycle → s(v, w) ∉ p.edges

Tactic:
push_neg

Result:
V : Type u
G : SimpleGraph V
v w : V
h : G.Adj v w
⊢ (G \ fromEdgeSet {s(v, w)}).Reachable v w ↔ ∃ u p, p.IsCycle ∧ s(v, w) ∈ p.edges

Proof state:
V : Type u
G : SimpleGraph V
v w : V
⊢ G.IsBridge s(v, w) ↔ G.Adj v w ∧ ∀ ⦃u : V⦄ (p : G.Walk u u), p.IsCycle → s(v, w) ∉ p.edges

Tactic:
rw [isBridge_iff, and_congr_right_iff]

Result:
V : Type u
G : SimpleGraph V
v w : V
⊢ G.Adj v w → (¬(G \ fromEdgeSet {s(v, w)}).Reachable v w ↔ ∀ ⦃u : V⦄ (p : G.Walk u u), p.IsCycle → s(v, w) ∉ p.edges)

Proof state:
V : Type u
G : SimpleGraph V
v w : V
h : G.Adj v w
⊢ (G \ fromEdgeSet {s(v, w)}).Reachable v w ↔ G.Adj v w ∧ (G \ fromEdgeSet {s(v, w)}).Reachable v w

Tactic:
simp only [h, true_and]

Result:
no goals

Proof state:
V : Type u
G : SimpleGraph V
v w : V
h : G.Adj v w
⊢ ¬(G \ fromEdgeSet {s(v, w)}).Reachable v w ↔ ∀ ⦃u : V⦄ (p : G.Walk u u), p.IsCycle → s(v, w) ∉ p.edges

Tactic:
rw [← not_iff_not]

Result:
V : Type u
G : SimpleGraph V
v w : V
h : G.Adj v w
⊢ ¬¬(G \ fromEdgeSet {s(v, w)}).Reachable v w ↔ ¬∀ ⦃u : V⦄ (p : G.Walk u u), p.IsCycle → s(v, w) ∉ p.edges
-- Mathlib/Topology/Algebra/Module/Multilinear/Basic.lean
theorem mkPiRing_zero : ContinuousMultilinearMap.mkPiRing R ι (0 : M) = 0

Proof state:
case H
R : Type u
ι : Type v
M : Type u_1
inst✝⁷ : Fintype ι
inst✝⁶ : CommRing R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : TopologicalSpace R
inst✝² : TopologicalSpace M
inst✝¹ : ContinuousMul R
inst✝ : ContinuousSMul R M
x✝ : ι → R
⊢ (ContinuousMultilinearMap.mkPiRing R ι 0) x✝ = 0 x✝

Tactic:
rw [mkPiRing_apply, smul_zero, ContinuousMultilinearMap.zero_apply]

Result:
no goals

Proof state:
R : Type u
ι : Type v
M : Type u_1
inst✝⁷ : Fintype ι
inst✝⁶ : CommRing R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : TopologicalSpace R
inst✝² : TopologicalSpace M
inst✝¹ : ContinuousMul R
inst✝ : ContinuousSMul R M
⊢ ContinuousMultilinearMap.mkPiRing R ι 0 = 0

Tactic:
ext

Result:
case H
R : Type u
ι : Type v
M : Type u_1
inst✝⁷ : Fintype ι
inst✝⁶ : CommRing R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : TopologicalSpace R
inst✝² : TopologicalSpace M
inst✝¹ : ContinuousMul R
inst✝ : ContinuousSMul R M
x✝ : ι → R
⊢ (ContinuousMultilinearMap.mkPiRing R ι 0) x✝ = 0 x✝
-- Mathlib/CategoryTheory/Category/Basic.lean
theorem whisker_eq (f : X ⟶ Y) {g h : Y ⟶ Z} (w : g = h) : f ≫ g = f ≫ h

Proof state:
C : Type u
inst✝ : Category.{v, u} C
X Y Z : C
f : X ⟶ Y
g h : Y ⟶ Z
w : g = h
⊢ f ≫ g = f ≫ h

Tactic:
rw [w]

Result:
no goals
-- Mathlib/.lake/packages/batteries/Batteries/Data/AssocList.lean
theorem length_mapKey : (mapKey f l).length = l.length

Proof state:
α✝¹ : Type u_1
α✝ : Type u_2
f : α✝¹ → α✝
β✝ : Type u_3
l : AssocList α✝¹ β✝
⊢ (mapKey f l).length = l.length

Tactic:
induction l <;> simp_all

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/RawLemmas.lean
theorem getD_erase [EquivBEq α] [LawfulHashable α] (h : m.WF) {k a : α} {fallback : β} :
    getD (m.erase k) a fallback = if k == a then fallback else getD m a fallback

Proof state:
α : Type u
inst✝³ : BEq α
inst✝² : Hashable α
β : Type v
m : Raw α fun x => β
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
h : m.WF
k a : α
fallback : β
⊢ getD (m.erase k) a fallback = if (k == a) = true then fallback else getD m a fallback

Tactic:
simp_to_raw using Raw₀.Const.getD_erase

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/List/Associative.lean
theorem length_alterKey_eq_self {k : α} {f : Option β → Option β} {l : List ((_ : α) × β)}
    (h : containsKey k l) (h' : (f (getValue? k l)).isSome) :
    (alterKey k f l).length = l.length

Proof state:
α : Type u
inst✝ : BEq α
β : Type v
k : α
f : Option β → Option β
l : List ((_ : α) × β)
h : containsKey k l = true
h' : (f (getValue? k l)).isSome = true
⊢ (alterKey k f l).length = l.length

Tactic:
simp [length_alterKey', h, Option.isSome_iff_ne_none.mp h']

Result:
no goals
-- Mathlib/RingTheory/Localization/Defs.lean
theorem mk'_eq_zero_iff (x : R) (s : M) : mk' S x s = 0 ↔ ∃ m : M, ↑m * x = 0

Proof state:
R : Type u_1
inst✝³ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
x : R
s : ↥M
⊢ mk' S x s = 0 ↔ ∃ m, ↑m * x = 0

Tactic:
rw [← (map_units S s).mul_left_inj, mk'_spec, zero_mul, map_eq_zero_iff M]

Result:
no goals
-- Mathlib/CategoryTheory/Limits/Shapes/Products.lean
lemma Pi.map'_eq {f : α → C} {g : β → C} [HasProduct f] [HasProduct g] {p p' : β → α}
    {q : ∀ (b : β), f (p b) ⟶ g b} {q' : ∀ (b : β), f (p' b) ⟶ g b} (hp : p = p')
    (hq : ∀ (b : β), eqToHom (hp ▸ rfl) ≫ q b = q' b) : Pi.map' p q = Pi.map' p' q'

Proof state:
β : Type w
α : Type w₂
C : Type u
inst✝² : Category.{v, u} C
f : α → C
g : β → C
inst✝¹ : HasProduct f
inst✝ : HasProduct g
p p' : β → α
q : (b : β) → f (p b) ⟶ g b
q' : (b : β) → f (p' b) ⟶ g b
hp : p = p'
hq : ∀ (b : β), eqToHom ⋯ ≫ q b = q' b
⊢ map' p q = map' p' q'

Tactic:
aesop_cat

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/WF.lean
theorem get!ₘ_eq_getValueCast! [BEq α] [Hashable α] [LawfulBEq α] {m : Raw₀ α β}
    (hm : Raw.WFImp m.1) {a : α} [Inhabited (β a)] :
    m.get!ₘ a = getValueCast! a (toListModel m.1.buckets)

Proof state:
α : Type u
β : α → Type v
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : LawfulBEq α
m : Raw₀ α β
hm : Raw.WFImp m.val
a : α
inst✝ : Inhabited (β a)
⊢ m.get!ₘ a = getValueCast! a (toListModel m.val.buckets)

Tactic:
rw [get!ₘ, get?ₘ_eq_getValueCast? hm, List.getValueCast!_eq_getValueCast?]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/RawLemmas.lean
theorem getKeyD_insertMany_list_of_mem [EquivBEq α] [LawfulHashable α] (h : m.1.WF)
    {l : List (α × β)}
    {k k' fallback : α} (k_beq : k == k')
    (distinct : l.Pairwise (fun a b => (a.1 == b.1) = false))
    (mem : k ∈ l.map Prod.fst) :
    (insertMany m l).1.getKeyD k' fallback = k

Proof state:
α : Type u
inst✝³ : BEq α
inst✝² : Hashable α
β : Type v
m : Raw₀ α fun x => β
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
h : m.val.WF
l : List (α × β)
k k' fallback : α
k_beq : (k == k') = true
distinct : List.Pairwise (fun a b => (a.fst == b.fst) = false) l
mem : k ∈ List.map Prod.fst l
⊢ (insertMany m l).val.getKeyD k' fallback = k

Tactic:
simp_to_model [Const.insertMany] using List.getKeyD_insertListConst_of_mem

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Int/DivModLemmas.lean
theorem tdiv_neg : ∀ a b : Int, a.tdiv (-b) = -(a.tdiv b)
  | ofNat m, 0 => show ofNat (m / 0) = -↑(m / 0) by rw [Nat.div_zero]; rfl
  | ofNat _, -[_+1] | -[_+1], succ _ => (Int.neg_neg _).symm
  | ofNat _, succ _ | -[_+1], 0 | -[_+1], -[_+1] => rfl

Proof state:
m : Nat
⊢ ofNat 0 = -↑0

Tactic:
rfl

Result:
no goals

Proof state:
m : Nat
⊢ ofNat (m / 0) = -↑(m / 0)

Tactic:
rw [Nat.div_zero]

Result:
m : Nat
⊢ ofNat 0 = -↑0
-- Mathlib/Algebra/Order/Floor.lean
theorem floor_eq_iff (ha : 0 ≤ a) : ⌊a⌋₊ = n ↔ ↑n ≤ a ∧ a < ↑n + 1

Proof state:
α : Type u_2
inst✝¹ : LinearOrderedSemiring α
inst✝ : FloorSemiring α
a : α
n : ℕ
ha : 0 ≤ a
⊢ ⌊a⌋₊ = n ↔ ↑n ≤ a ∧ a < ↑n + 1

Tactic:
rw [← le_floor_iff ha, ← Nat.cast_one, ← Nat.cast_add, ← floor_lt ha, Nat.lt_add_one_iff,
  le_antisymm_iff, and_comm]

Result:
no goals
-- Mathlib/RingTheory/MvPowerSeries/Order.lean
theorem exists_coeff_ne_zero_and_weightedOrder
    (h : (toNat (f.weightedOrder w) : ℕ∞) = f.weightedOrder w) :
    ∃ d, coeff R d f ≠ 0 ∧ weight w d = f.weightedOrder w

Proof state:
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
w : σ → ℕ
f : MvPowerSeries σ R
h : ↑(weightedOrder w f).toNat = weightedOrder w f
⊢ ∃ d, (coeff R d) f ≠ 0 ∧ (weight w) d = Nat.find ⋯

Tactic:
generalize_proofs h1

Result:
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
w : σ → ℕ
f : MvPowerSeries σ R
h : ↑(weightedOrder w f).toNat = weightedOrder w f
h1 : ∃ n d, (coeff R d) f ≠ 0 ∧ (weight w) d = n
⊢ ∃ d, (coeff R d) f ≠ 0 ∧ (weight w) d = Nat.find h1

Proof state:
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
w : σ → ℕ
f : MvPowerSeries σ R
h : ↑(weightedOrder w f).toNat = weightedOrder w f
⊢ ∃ d, (coeff R d) f ≠ 0 ∧ ↑((weight w) d) = weightedOrder w f

Tactic:
classical
simp_rw [weightedOrder, dif_neg ((ne_zero_iff_weightedOrder_finite w).mpr h), Nat.cast_inj]
generalize_proofs h1
exact Nat.find_spec h1

Result:
no goals

Proof state:
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
w : σ → ℕ
f : MvPowerSeries σ R
h : ↑(weightedOrder w f).toNat = weightedOrder w f
h1 : ∃ n d, (coeff R d) f ≠ 0 ∧ (weight w) d = n
⊢ ∃ d, (coeff R d) f ≠ 0 ∧ (weight w) d = Nat.find h1

Tactic:
exact Nat.find_spec h1

Result:
no goals

Proof state:
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
w : σ → ℕ
f : MvPowerSeries σ R
h : ↑(weightedOrder w f).toNat = weightedOrder w f
⊢ ∃ d, (coeff R d) f ≠ 0 ∧ ↑((weight w) d) = weightedOrder w f

Tactic:
simp_rw [weightedOrder, dif_neg ((ne_zero_iff_weightedOrder_finite w).mpr h), Nat.cast_inj]

Result:
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
w : σ → ℕ
f : MvPowerSeries σ R
h : ↑(weightedOrder w f).toNat = weightedOrder w f
⊢ ∃ d, (coeff R d) f ≠ 0 ∧ (weight w) d = Nat.find ⋯
-- Mathlib/RingTheory/TensorProduct/Basic.lean
lemma baseChange_comp (g : N →ₗ[R] P) :
    (g ∘ₗ f).baseChange A = g.baseChange A ∘ₗ f.baseChange A

Proof state:
R : Type u_1
A : Type u_2
M : Type u_4
N : Type u_5
P : Type u_6
inst✝⁸ : CommSemiring R
inst✝⁷ : Semiring A
inst✝⁶ : Algebra R A
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid N
inst✝³ : AddCommMonoid P
inst✝² : Module R M
inst✝¹ : Module R N
inst✝ : Module R P
f : M →ₗ[R] N
g : N →ₗ[R] P
⊢ baseChange A (g ∘ₗ f) = baseChange A g ∘ₗ baseChange A f

Tactic:
ext

Result:
case a.h.h
R : Type u_1
A : Type u_2
M : Type u_4
N : Type u_5
P : Type u_6
inst✝⁸ : CommSemiring R
inst✝⁷ : Semiring A
inst✝⁶ : Algebra R A
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid N
inst✝³ : AddCommMonoid P
inst✝² : Module R M
inst✝¹ : Module R N
inst✝ : Module R P
f : M →ₗ[R] N
g : N →ₗ[R] P
x✝ : M
⊢ ((AlgebraTensorModule.curry (baseChange A (g ∘ₗ f))) 1) x✝ =
    ((AlgebraTensorModule.curry (baseChange A g ∘ₗ baseChange A f)) 1) x✝

Proof state:
case a.h.h
R : Type u_1
A : Type u_2
M : Type u_4
N : Type u_5
P : Type u_6
inst✝⁸ : CommSemiring R
inst✝⁷ : Semiring A
inst✝⁶ : Algebra R A
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid N
inst✝³ : AddCommMonoid P
inst✝² : Module R M
inst✝¹ : Module R N
inst✝ : Module R P
f : M →ₗ[R] N
g : N →ₗ[R] P
x✝ : M
⊢ ((AlgebraTensorModule.curry (baseChange A (g ∘ₗ f))) 1) x✝ =
    ((AlgebraTensorModule.curry (baseChange A g ∘ₗ baseChange A f)) 1) x✝

Tactic:
simp

Result:
no goals
-- Mathlib/Data/Semiquot.lean
theorem blur_eq_blur' (q : Semiquot α) (s : Set α) (h : q.s ⊆ s) : blur s q = blur' q h

Proof state:
α : Type u_1
q : Semiquot α
s : Set α
h : q.s ⊆ s
⊢ q.blur' ⋯ = q.blur' h

Tactic:
congr

Result:
case e_s
α : Type u_1
q : Semiquot α
s : Set α
h : q.s ⊆ s
⊢ s ∪ q.s = s

Proof state:
case e_s
α : Type u_1
q : Semiquot α
s : Set α
h : q.s ⊆ s
⊢ s ∪ q.s = s

Tactic:
exact Set.union_eq_self_of_subset_right h

Result:
no goals

Proof state:
α : Type u_1
q : Semiquot α
s : Set α
h : q.s ⊆ s
⊢ blur s q = q.blur' h

Tactic:
unfold blur

Result:
α : Type u_1
q : Semiquot α
s : Set α
h : q.s ⊆ s
⊢ q.blur' ⋯ = q.blur' h
-- Mathlib/Topology/Semicontinuous.lean
theorem lowerSemicontinuousWithinAt_iSup {f : ι → α → δ}
    (h : ∀ i, LowerSemicontinuousWithinAt (f i) s x) :
    LowerSemicontinuousWithinAt (fun x' => ⨆ i, f i x') s x :=
  lowerSemicontinuousWithinAt_ciSup (by simp) h

Proof state:
α : Type u_1
inst✝¹ : TopologicalSpace α
x : α
s : Set α
ι : Sort u_3
δ : Type u_4
inst✝ : CompleteLinearOrder δ
f : ι → α → δ
h : ∀ (i : ι), LowerSemicontinuousWithinAt (f i) s x
⊢ ∀ᶠ (y : α) in 𝓝[s] x, BddAbove (range fun i => f i y)

Tactic:
simp

Result:
no goals
-- Mathlib/Algebra/BigOperators/Expect.lean
@[simp] lemma expect_apply {α : Type*} {π : α → Type*} [∀ a, CommSemiring (π a)]
    [∀ a, Module ℚ≥0 (π a)] (s : Finset ι) (f : ι → ∀ a, π a) (a : α) :
    (𝔼 i ∈ s, f i) a = 𝔼 i ∈ s, f i a

Proof state:
ι : Type u_1
α : Type u_5
π : α → Type u_6
inst✝¹ : (a : α) → CommSemiring (π a)
inst✝ : (a : α) → Module ℚ≥0 (π a)
s : Finset ι
f : ι → (a : α) → π a
a : α
⊢ (𝔼 i ∈ s, f i) a = 𝔼 i ∈ s, f i a

Tactic:
simp [expect]

Result:
no goals
-- Mathlib/RingTheory/Spectrum/Prime/Topology.lean
theorem vanishingIdeal_strict_anti_mono_iff {s t : Set (PrimeSpectrum R)} (hs : IsClosed s)
    (ht : IsClosed t) : s ⊂ t ↔ vanishingIdeal t < vanishingIdeal s

Proof state:
R : Type u
inst✝ : CommSemiring R
s t : Set (PrimeSpectrum R)
hs : IsClosed s
ht : IsClosed t
⊢ s ⊂ t ↔ vanishingIdeal t < vanishingIdeal s

Tactic:
rw [Set.ssubset_def, vanishingIdeal_anti_mono_iff hs, vanishingIdeal_anti_mono_iff ht,
  lt_iff_le_not_le]

Result:
no goals
-- Mathlib/CategoryTheory/ConcreteCategory/Basic.lean
theorem forget_eq_ConcreteCategory_hom [HasForget C] {X Y : C} (f : X ⟶ Y) :
    (forget C).map f = @ConcreteCategory.hom _ _ _ _ _ (HasForget.toConcreteCategory C) _ _ f

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasForget C
X Y : C
f : X ⟶ Y
⊢ (forget C).map f = ⇑(ConcreteCategory.hom f)

Tactic:
with_reducible_and_instances rfl

Result:
no goals

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasForget C
X Y : C
f : X ⟶ Y
⊢ (forget C).map f = ⇑(ConcreteCategory.hom f)

Tactic:
rfl

Result:
no goals
-- Mathlib/Data/Set/Function.lean
theorem bijOn_range (h : Semiconj f fa fb) (ha : Bijective fa) (hf : Injective f) :
    BijOn fb (range f) (range f)

Proof state:
α : Type u_1
β : Type u_2
fa : α → α
fb : β → β
f : α → β
h : Semiconj f fa fb
ha : Bijective fa
hf : Injective f
⊢ BijOn fb (range f) (range f)

Tactic:
rw [← image_univ]

Result:
α : Type u_1
β : Type u_2
fa : α → α
fb : β → β
f : α → β
h : Semiconj f fa fb
ha : Bijective fa
hf : Injective f
⊢ BijOn fb (f '' univ) (f '' univ)

Proof state:
α : Type u_1
β : Type u_2
fa : α → α
fb : β → β
f : α → β
h : Semiconj f fa fb
ha : Bijective fa
hf : Injective f
⊢ BijOn fb (f '' univ) (f '' univ)

Tactic:
exact h.bijOn_image (bijective_iff_bijOn_univ.1 ha) hf.injOn

Result:
no goals
-- Mathlib/Analysis/Asymptotics/Defs.lean
theorem IsBigO.of_bound' (h : ∀ᶠ x in l, ‖f x‖ ≤ ‖g x‖) : f =O[l] g :=
  .of_bound 1 <| by simpa only [one_mul] using h

Proof state:
α : Type u_1
E : Type u_3
F : Type u_4
inst✝¹ : Norm E
inst✝ : Norm F
f : α → E
g : α → F
l : Filter α
h : ∀ᶠ (x : α) in l, ‖f x‖ ≤ ‖g x‖
⊢ ∀ᶠ (x : α) in l, ‖f x‖ ≤ 1 * ‖g x‖

Tactic:
simpa only [one_mul] using h

Result:
no goals
-- Mathlib/Topology/Algebra/Module/LinearMap.lean
theorem add_comp [ContinuousAdd M₃] (g₁ g₂ : M₂ →SL[σ₂₃] M₃) (f : M₁ →SL[σ₁₂] M₂) :
    (g₁ + g₂).comp f = g₁.comp f + g₂.comp f

Proof state:
R₁ : Type u_1
R₂ : Type u_2
R₃ : Type u_3
inst✝¹³ : Semiring R₁
inst✝¹² : Semiring R₂
inst✝¹¹ : Semiring R₃
σ₁₂ : R₁ →+* R₂
σ₂₃ : R₂ →+* R₃
σ₁₃ : R₁ →+* R₃
M₁ : Type u_4
inst✝¹⁰ : TopologicalSpace M₁
inst✝⁹ : AddCommMonoid M₁
M₂ : Type u_6
inst✝⁸ : TopologicalSpace M₂
inst✝⁷ : AddCommMonoid M₂
M₃ : Type u_7
inst✝⁶ : TopologicalSpace M₃
inst✝⁵ : AddCommMonoid M₃
inst✝⁴ : Module R₁ M₁
inst✝³ : Module R₂ M₂
inst✝² : Module R₃ M₃
inst✝¹ : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
inst✝ : ContinuousAdd M₃
g₁ g₂ : M₂ →SL[σ₂₃] M₃
f : M₁ →SL[σ₁₂] M₂
⊢ (g₁ + g₂).comp f = g₁.comp f + g₂.comp f

Tactic:
ext

Result:
case h
R₁ : Type u_1
R₂ : Type u_2
R₃ : Type u_3
inst✝¹³ : Semiring R₁
inst✝¹² : Semiring R₂
inst✝¹¹ : Semiring R₃
σ₁₂ : R₁ →+* R₂
σ₂₃ : R₂ →+* R₃
σ₁₃ : R₁ →+* R₃
M₁ : Type u_4
inst✝¹⁰ : TopologicalSpace M₁
inst✝⁹ : AddCommMonoid M₁
M₂ : Type u_6
inst✝⁸ : TopologicalSpace M₂
inst✝⁷ : AddCommMonoid M₂
M₃ : Type u_7
inst✝⁶ : TopologicalSpace M₃
inst✝⁵ : AddCommMonoid M₃
inst✝⁴ : Module R₁ M₁
inst✝³ : Module R₂ M₂
inst✝² : Module R₃ M₃
inst✝¹ : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
inst✝ : ContinuousAdd M₃
g₁ g₂ : M₂ →SL[σ₂₃] M₃
f : M₁ →SL[σ₁₂] M₂
x✝ : M₁
⊢ ((g₁ + g₂).comp f) x✝ = (g₁.comp f + g₂.comp f) x✝

Proof state:
case h
R₁ : Type u_1
R₂ : Type u_2
R₃ : Type u_3
inst✝¹³ : Semiring R₁
inst✝¹² : Semiring R₂
inst✝¹¹ : Semiring R₃
σ₁₂ : R₁ →+* R₂
σ₂₃ : R₂ →+* R₃
σ₁₃ : R₁ →+* R₃
M₁ : Type u_4
inst✝¹⁰ : TopologicalSpace M₁
inst✝⁹ : AddCommMonoid M₁
M₂ : Type u_6
inst✝⁸ : TopologicalSpace M₂
inst✝⁷ : AddCommMonoid M₂
M₃ : Type u_7
inst✝⁶ : TopologicalSpace M₃
inst✝⁵ : AddCommMonoid M₃
inst✝⁴ : Module R₁ M₁
inst✝³ : Module R₂ M₂
inst✝² : Module R₃ M₃
inst✝¹ : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
inst✝ : ContinuousAdd M₃
g₁ g₂ : M₂ →SL[σ₂₃] M₃
f : M₁ →SL[σ₁₂] M₂
x✝ : M₁
⊢ ((g₁ + g₂).comp f) x✝ = (g₁.comp f + g₂.comp f) x✝

Tactic:
simp

Result:
no goals
-- Mathlib/Data/Multiset/Sum.lean
theorem inl_mem_disjSum : inl a ∈ s.disjSum t ↔ a ∈ s

Proof state:
α : Type u_1
β : Type u_2
s : Multiset α
t : Multiset β
a : α
⊢ (∃ a_1 ∈ s, inl a_1 = inl a) ↔ a ∈ s

Tactic:
simp only [inl.injEq, exists_eq_right]

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
s : Multiset α
t : Multiset β
a : α
⊢ inl a ∈ s.disjSum t ↔ a ∈ s

Tactic:
rw [mem_disjSum, or_iff_left]

Result:
α : Type u_1
β : Type u_2
s : Multiset α
t : Multiset β
a : α
⊢ (∃ a_1 ∈ s, inl a_1 = inl a) ↔ a ∈ s

α : Type u_1
β : Type u_2
s : Multiset α
t : Multiset β
a : α
⊢ ¬∃ b ∈ t, inr b = inl a

Proof state:
α : Type u_1
β : Type u_2
s : Multiset α
t : Multiset β
a : α
⊢ ¬∃ b ∈ t, inr b = inl a

Tactic:
rintro ⟨b, _, hb⟩

Result:
case intro.intro
α : Type u_1
β : Type u_2
s : Multiset α
t : Multiset β
a : α
b : β
left✝ : b ∈ t
hb : inr b = inl a
⊢ False

Proof state:
case intro.intro
α : Type u_1
β : Type u_2
s : Multiset α
t : Multiset β
a : α
b : β
left✝ : b ∈ t
hb : inr b = inl a
⊢ False

Tactic:
exact inr_ne_inl hb

Result:
no goals
-- Mathlib/Data/Finset/NAry.lean
theorem image₂_image_right (f : α → γ → δ) (g : β → γ) :
    image₂ f s (t.image g) = image₂ (fun a b => f a (g b)) s t :=
  coe_injective <| by
    push_cast
    exact image2_image_right _ _

Proof state:
α : Type u_1
β : Type u_3
γ : Type u_5
δ : Type u_7
inst✝¹ : DecidableEq γ
s : Finset α
t : Finset β
inst✝ : DecidableEq δ
f : α → γ → δ
g : β → γ
⊢ image2 f (↑s) (g '' ↑t) = image2 (fun a b => f a (g b)) ↑s ↑t

Tactic:
exact image2_image_right _ _

Result:
no goals

Proof state:
α : Type u_1
β : Type u_3
γ : Type u_5
δ : Type u_7
inst✝¹ : DecidableEq γ
s : Finset α
t : Finset β
inst✝ : DecidableEq δ
f : α → γ → δ
g : β → γ
⊢ ↑(image₂ f s (image g t)) = ↑(image₂ (fun a b => f a (g b)) s t)

Tactic:
push_cast

Result:
α : Type u_1
β : Type u_3
γ : Type u_5
δ : Type u_7
inst✝¹ : DecidableEq γ
s : Finset α
t : Finset β
inst✝ : DecidableEq δ
f : α → γ → δ
g : β → γ
⊢ image2 f (↑s) (g '' ↑t) = image2 (fun a b => f a (g b)) ↑s ↑t