harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/MeasureTheory/Measure/Portmanteau.lean
/-- One implication of the portmanteau theorem:
Assuming that for all Borel sets E whose boundary ∂E carries no probability mass under a
candidate limit probability measure μ we have convergence of the measures μsᵢ(E) to μ(E),
then for all open sets G we have the limsup condition μ(G) ≤ liminf μsᵢ(G). -/
lemma le_liminf_measure_open_of_forall_tendsto_measure
    {Ω ι : Type*} {L : Filter ι}
    [MeasurableSpace Ω] [PseudoEMetricSpace Ω] [OpensMeasurableSpace Ω]
    {μ : Measure Ω} [IsProbabilityMeasure μ] {μs : ι → Measure Ω} [∀ i, IsProbabilityMeasure (μs i)]
    (h : ∀ {E}, MeasurableSet E → μ (frontier E) = 0 → Tendsto (fun i ↦ μs i E) L (𝓝 (μ E)))
    (G : Set Ω) (G_open : IsOpen G) :
    μ G ≤ L.liminf (fun i ↦ μs i G)

Proof state:
Ω : Type u_2
ι : Type u_3
L : Filter ι
inst✝⁴ : MeasurableSpace Ω
inst✝³ : PseudoEMetricSpace Ω
inst✝² : OpensMeasurableSpace Ω
μ : Measure Ω
inst✝¹ : IsProbabilityMeasure μ
μs : ι → Measure Ω
inst✝ : ∀ (i : ι), IsProbabilityMeasure (μs i)
h : ∀ {E : Set Ω}, MeasurableSet E → μ (frontier E) = 0 → Tendsto (fun i => (μs i) E) L (𝓝 (μ E))
G : Set Ω
G_open : IsOpen G
⊢ μ G ≤ liminf (fun i => (μs i) G) L

Tactic:
apply le_measure_liminf_of_limsup_measure_compl_le G_open.measurableSet

Result:
Ω : Type u_2
ι : Type u_3
L : Filter ι
inst✝⁴ : MeasurableSpace Ω
inst✝³ : PseudoEMetricSpace Ω
inst✝² : OpensMeasurableSpace Ω
μ : Measure Ω
inst✝¹ : IsProbabilityMeasure μ
μs : ι → Measure Ω
inst✝ : ∀ (i : ι), IsProbabilityMeasure (μs i)
h : ∀ {E : Set Ω}, MeasurableSet E → μ (frontier E) = 0 → Tendsto (fun i => (μs i) E) L (𝓝 (μ E))
G : Set Ω
G_open : IsOpen G
⊢ limsup (fun i => (μs i) Gᶜ) L ≤ μ Gᶜ

Proof state:
Ω : Type u_2
ι : Type u_3
L : Filter ι
inst✝⁴ : MeasurableSpace Ω
inst✝³ : PseudoEMetricSpace Ω
inst✝² : OpensMeasurableSpace Ω
μ : Measure Ω
inst✝¹ : IsProbabilityMeasure μ
μs : ι → Measure Ω
inst✝ : ∀ (i : ι), IsProbabilityMeasure (μs i)
h : ∀ {E : Set Ω}, MeasurableSet E → μ (frontier E) = 0 → Tendsto (fun i => (μs i) E) L (𝓝 (μ E))
G : Set Ω
G_open : IsOpen G
⊢ limsup (fun i => (μs i) Gᶜ) L ≤ μ Gᶜ

Tactic:
exact limsup_measure_closed_le_of_forall_tendsto_measure h _ (isClosed_compl_iff.mpr G_open)

Result:
no goals
-- Mathlib/Data/Int/Init.lean
protected lemma le_iff_lt_or_eq : a ≤ b ↔ a < b ∨ a = b

Proof state:
a b : ℤ
⊢ a ≤ b ↔ a < b ∨ a = b

Tactic:
rw [Int.le_iff_eq_or_lt, or_comm]

Result:
no goals
-- Mathlib/NumberTheory/ZetaValues.lean
theorem bernoulli_zero_fourier_coeff {n : ℤ} (hn : n ≠ 0) : bernoulliFourierCoeff 0 n = 0

Proof state:
n : ℤ
hn : n ≠ 0
⊢ bernoulliFourierCoeff 0 n = 0

Tactic:
simpa using bernoulliFourierCoeff_recurrence 0 hn

Result:
no goals
-- Mathlib/Algebra/Group/Basic.lean
@[to_additive (attr := simp) neg_zsmul]
lemma zpow_neg (a : α) : ∀ n : ℤ, a ^ (-n) = (a ^ n)⁻¹
  | (_ + 1 : ℕ) => DivInvMonoid.zpow_neg' _ _
  | 0 => by simp
  | Int.negSucc n => by
    rw [zpow_negSucc, inv_inv, ← zpow_natCast]
    rfl

Proof state:
α : Type u_1
inst✝ : DivisionMonoid α
a : α
⊢ a ^ (-0) = (a ^ 0)⁻¹

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
inst✝ : DivisionMonoid α
a : α
n : ℕ
⊢ a ^ (-Int.negSucc n) = (a ^ Int.negSucc n)⁻¹

Tactic:
rw [zpow_negSucc, inv_inv, ← zpow_natCast]

Result:
α : Type u_1
inst✝ : DivisionMonoid α
a : α
n : ℕ
⊢ a ^ (-Int.negSucc n) = a ^ ↑(n + 1)

Proof state:
α : Type u_1
inst✝ : DivisionMonoid α
a : α
n : ℕ
⊢ a ^ (-Int.negSucc n) = a ^ ↑(n + 1)

Tactic:
rfl

Result:
no goals
-- Mathlib/CategoryTheory/Limits/Opposites.lean
theorem op_inr {X Y Z : C} {f : X ⟶ Z} {g : Y ⟶ Z} (c : PullbackCone f g) :
    c.op.inr = c.snd.op

Proof state:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
c : PullbackCone f g
⊢ c.op.inr = c.snd.op

Tactic:
simp

Result:
no goals
-- Mathlib/CategoryTheory/EqToHom.lean
theorem NatTrans.congr {F G : C ⥤ D} (α : F ⟶ G) {X Y : C} (h : X = Y) :
    α.app X = F.map (eqToHom h) ≫ α.app Y ≫ G.map (eqToHom h.symm)

Proof state:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F G : C ⥤ D
α : F ⟶ G
X Y : C
h : X = Y
⊢ α.app X = α.app X ≫ G.map (eqToHom h) ≫ G.map (eqToHom ⋯)

Tactic:
simp [eqToHom_map]

Result:
no goals

Proof state:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F G : C ⥤ D
α : F ⟶ G
X Y : C
h : X = Y
⊢ α.app X = F.map (eqToHom h) ≫ α.app Y ≫ G.map (eqToHom ⋯)

Tactic:
rw [α.naturality_assoc]

Result:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F G : C ⥤ D
α : F ⟶ G
X Y : C
h : X = Y
⊢ α.app X = α.app X ≫ G.map (eqToHom h) ≫ G.map (eqToHom ⋯)
-- Mathlib/Algebra/Quandle.lean
lemma act_idem (x : S) : (x ◃ x) = x

Proof state:
S : Type u_1
inst✝ : UnitalShelf S
x : S
⊢ x ◃ x = x

Tactic:
rw [← act_one x, ← Shelf.self_distrib, act_one]

Result:
no goals
-- Mathlib/Data/Nat/Log.lean
theorem log_mul_base {b n : ℕ} (hb : 1 < b) (hn : n ≠ 0) : log b (n * b) = log b n + 1

Proof state:
b n : ℕ
hb : 1 < b
hn : n ≠ 0
⊢ log b (n * b) = log b n + 1

Tactic:
apply log_eq_of_pow_le_of_lt_pow <;> rw [pow_succ', Nat.mul_comm b]

Result:
case h₁
b n : ℕ
hb : 1 < b
hn : n ≠ 0
⊢ b ^ log b n * b ≤ n * b

case h₂
b n : ℕ
hb : 1 < b
hn : n ≠ 0
⊢ n * b < b ^ (log b n + 1) * b

Proof state:
case h₁
b n : ℕ
hb : 1 < b
hn : n ≠ 0
⊢ b ^ log b n * b ≤ n * b

case h₂
b n : ℕ
hb : 1 < b
hn : n ≠ 0
⊢ n * b < b ^ (log b n + 1) * b

Tactic:
exacts [Nat.mul_le_mul_right _ (pow_log_le_self _ hn),
  (Nat.mul_lt_mul_right (Nat.zero_lt_one.trans hb)).2 (lt_pow_succ_log_self hb _)]

Result:
no goals
-- Mathlib/Data/Finset/NAry.lean
@[simp (default + 1)] -- otherwise `simp` doesn't use `forall_mem_image₂`
lemma sup'_image₂_le {g : γ → δ} {a : δ} (h : (image₂ f s t).Nonempty) :
    sup' (image₂ f s t) h g ≤ a ↔ ∀ x ∈ s, ∀ y ∈ t, g (f x y) ≤ a

Proof state:
α : Type u_1
β : Type u_3
γ : Type u_5
δ : Type u_7
inst✝¹ : DecidableEq γ
f : α → β → γ
s : Finset α
t : Finset β
inst✝ : SemilatticeSup δ
g : γ → δ
a : δ
h : (image₂ f s t).Nonempty
⊢ (image₂ f s t).sup' h g ≤ a ↔ ∀ x ∈ s, ∀ y ∈ t, g (f x y) ≤ a

Tactic:
rw [sup'_le_iff, forall_mem_image₂]

Result:
no goals
-- Mathlib/LinearAlgebra/AffineSpace/Independent.lean
@[simp] lemma affineIndependent_smul {G : Type*} [Group G] [DistribMulAction G V]
    [SMulCommClass G k V] {p : ι → V} {a : G} :
    AffineIndependent k (a • p) ↔ AffineIndependent k p

Proof state:
k : Type u_1
V : Type u_2
inst✝⁵ : Ring k
inst✝⁴ : AddCommGroup V
inst✝³ : Module k V
ι : Type u_4
G : Type u_5
inst✝² : Group G
inst✝¹ : DistribMulAction G V
inst✝ : SMulCommClass G k V
p : ι → V
a : G
⊢ AffineIndependent k (a • p) ↔ AffineIndependent k p

Tactic:
simp +contextual [AffineIndependent, weightedVSub_smul,
  ← smul_comm (α := V) a, ← smul_sum, smul_eq_zero_iff_eq]

Result:
no goals
-- Mathlib/Algebra/Group/Defs.lean
@[to_additive three'_nsmul]
lemma pow_three' (a : M) : a ^ 3 = a * a * a

Proof state:
M : Type u_2
inst✝ : Monoid M
a : M
⊢ a ^ 3 = a * a * a

Tactic:
rw [pow_succ, pow_two]

Result:
no goals
-- Mathlib/MeasureTheory/Integral/Lebesgue.lean
theorem ae_lt_top' {f : α → ℝ≥0∞} (hf : AEMeasurable f μ) (h2f : ∫⁻ x, f x ∂μ ≠ ∞) :
    ∀ᵐ x ∂μ, f x < ∞

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : AEMeasurable f μ
h2f : ∫⁻ (x : α), f x ∂μ ≠ ⊤
⊢ ∀ᵐ (x : α) ∂μ, f x < ⊤

Tactic:
simp_rw [ae_iff, ENNReal.not_lt_top]

Result:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : AEMeasurable f μ
h2f : ∫⁻ (x : α), f x ∂μ ≠ ⊤
⊢ μ {a | f a = ⊤} = 0

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : AEMeasurable f μ
h2f : ∫⁻ (x : α), f x ∂μ ≠ ⊤
⊢ μ {a | f a = ⊤} = 0

Tactic:
exact measure_eq_top_of_lintegral_ne_top hf h2f

Result:
no goals
-- Mathlib/Topology/MetricSpace/Isometry.lean
theorem image_closedBall (h : α ≃ᵢ β) (x : α) (r : ℝ) :
    h '' Metric.closedBall x r = Metric.closedBall (h x) r

Proof state:
α : Type u
β : Type v
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
h : α ≃ᵢ β
x : α
r : ℝ
⊢ ⇑h '' Metric.closedBall x r = Metric.closedBall (h x) r

Tactic:
rw [← h.preimage_symm, h.symm.preimage_closedBall, symm_symm]

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Path.lean
theorem cons_isCycle_iff {u v : V} (p : G.Walk v u) (h : G.Adj u v) :
    (Walk.cons h p).IsCycle ↔ p.IsPath ∧ ¬s(u, v) ∈ p.edges

Proof state:
V : Type u
G : SimpleGraph V
u v : V
p : G.Walk v u
h : G.Adj u v
this : p.support.Nodup → p.edges.Nodup
⊢ (s(u, v) ∉ p.edges ∧ p.edges.Nodup) ∧ cons h p ≠ nil ∧ p.support.Nodup ↔ p.support.Nodup ∧ s(u, v) ∉ p.edges

Tactic:
tauto

Result:
no goals

Proof state:
V : Type u
G : SimpleGraph V
u v : V
p : G.Walk v u
h : G.Adj u v
⊢ (s(u, v) ∉ p.edges ∧ p.edges.Nodup) ∧ cons h p ≠ nil ∧ p.support.Nodup ↔ p.support.Nodup ∧ s(u, v) ∉ p.edges

Tactic:
have : p.support.Nodup → p.edges.Nodup := edges_nodup_of_support_nodup

Result:
V : Type u
G : SimpleGraph V
u v : V
p : G.Walk v u
h : G.Adj u v
this : p.support.Nodup → p.edges.Nodup
⊢ (s(u, v) ∉ p.edges ∧ p.edges.Nodup) ∧ cons h p ≠ nil ∧ p.support.Nodup ↔ p.support.Nodup ∧ s(u, v) ∉ p.edges

Proof state:
V : Type u
G : SimpleGraph V
u v : V
p : G.Walk v u
h : G.Adj u v
⊢ (cons h p).IsCycle ↔ p.IsPath ∧ s(u, v) ∉ p.edges

Tactic:
simp only [Walk.isCycle_def, Walk.isPath_def, Walk.isTrail_def, edges_cons, List.nodup_cons,
  support_cons, List.tail_cons]

Result:
V : Type u
G : SimpleGraph V
u v : V
p : G.Walk v u
h : G.Adj u v
⊢ (s(u, v) ∉ p.edges ∧ p.edges.Nodup) ∧ cons h p ≠ nil ∧ p.support.Nodup ↔ p.support.Nodup ∧ s(u, v) ∉ p.edges
-- Mathlib/LinearAlgebra/Lagrange.lean
theorem nodal_ne_zero [Nontrivial R] : nodal s v ≠ 0

Proof state:
case inr
R : Type u_1
inst✝¹ : CommRing R
ι : Type u_2
s : Finset ι
v : ι → R
inst✝ : Nontrivial R
h : s.Nonempty
⊢ nodal s v ≠ 0

Tactic:
apply ne_zero_of_natDegree_gt (n := 0)

Result:
case inr
R : Type u_1
inst✝¹ : CommRing R
ι : Type u_2
s : Finset ι
v : ι → R
inst✝ : Nontrivial R
h : s.Nonempty
⊢ 0 < (nodal s v).natDegree

Proof state:
case inr
R : Type u_1
inst✝¹ : CommRing R
ι : Type u_2
s : Finset ι
v : ι → R
inst✝ : Nontrivial R
h : s.Nonempty
⊢ 0 < (nodal s v).natDegree

Tactic:
simp only [natDegree_nodal, h.card_pos]

Result:
no goals

Proof state:
R : Type u_1
inst✝¹ : CommRing R
ι : Type u_2
s : Finset ι
v : ι → R
inst✝ : Nontrivial R
⊢ nodal s v ≠ 0

Tactic:
rcases s.eq_empty_or_nonempty with (rfl | h)

Result:
case inl
R : Type u_1
inst✝¹ : CommRing R
ι : Type u_2
v : ι → R
inst✝ : Nontrivial R
⊢ nodal ∅ v ≠ 0

case inr
R : Type u_1
inst✝¹ : CommRing R
ι : Type u_2
s : Finset ι
v : ι → R
inst✝ : Nontrivial R
h : s.Nonempty
⊢ nodal s v ≠ 0

Proof state:
case inl
R : Type u_1
inst✝¹ : CommRing R
ι : Type u_2
v : ι → R
inst✝ : Nontrivial R
⊢ nodal ∅ v ≠ 0

Tactic:
exact one_ne_zero

Result:
no goals
-- Mathlib/ModelTheory/Basic.lean
theorem card_relations_sum (i : ℕ) :
    #((L.sum L').Relations i) =
      Cardinal.lift.{v'} #(L.Relations i) + Cardinal.lift.{v} #(L'.Relations i)

Proof state:
L : Language
L' : Language
i : ℕ
⊢ #((L.sum L').Relations i) = lift.{v', v} #(L.Relations i) + lift.{v, v'} #(L'.Relations i)

Tactic:
simp [Language.sum]

Result:
no goals
-- Mathlib/Data/List/Rotate.lean
theorem isRotated_iff_mem_map_range : l ~r l' ↔ l' ∈ (List.range (l.length + 1)).map l.rotate

Proof state:
α : Type u
l l' : List α
⊢ l ~r l' ↔ l' ∈ map l.rotate (range (l.length + 1))

Tactic:
simp_rw [mem_map, mem_range, isRotated_iff_mod]

Result:
α : Type u
l l' : List α
⊢ (∃ n ≤ l.length, l.rotate n = l') ↔ ∃ a < l.length + 1, l.rotate a = l'

Proof state:
α : Type u
l l' : List α
⊢ (∃ n ≤ l.length, l.rotate n = l') ↔ ∃ a < l.length + 1, l.rotate a = l'

Tactic:
exact
  ⟨fun ⟨n, hn, h⟩ => ⟨n, Nat.lt_succ_of_le hn, h⟩,
    fun ⟨n, hn, h⟩ => ⟨n, Nat.le_of_lt_succ hn, h⟩⟩

Result:
no goals
-- Mathlib/NumberTheory/LSeries/HurwitzZetaEven.lean
lemma cosKernel_def (a x : ℝ) : ↑(cosKernel ↑a x) = jacobiTheta₂ a (I * x)

Proof state:
a x : ℝ
⊢ ↑(cosKernel (↑a) x) = jacobiTheta₂ (↑a) (I * ↑x)

Tactic:
simp [cosKernel, re_eq_add_conj, jacobiTheta₂_conj, ← mul_two,
  mul_div_cancel_right₀ _ (two_ne_zero' ℂ)]

Result:
no goals
-- Mathlib/RingTheory/Flat/FaithfullyFlat/Basic.lean
lemma iff_exact_iff_rTensor_exact :
    FaithfullyFlat R M ↔
    (∀ {N1 : Type max u v} [AddCommGroup N1] [Module R N1]
      {N2 : Type max u v} [AddCommGroup N2] [Module R N2]
      {N3 : Type max u v} [AddCommGroup N3] [Module R N3]
      (l12 : N1 →ₗ[R] N2) (l23 : N2 →ₗ[R] N3),
        Function.Exact l12 l23 ↔ Function.Exact (l12.rTensor M) (l23.rTensor M)) :=
  ⟨fun fl _ _ _ _ _ _ _ _ _ l12 l23 => (rTensor_exact_iff_exact R M l12 l23).symm, fun iff_exact =>
    iff_flat_and_rTensor_reflects_triviality _ _ |>.2
      ⟨Flat.iff_rTensor_exact.2 <| fun _ _ _ => iff_exact .. |>.1,
    fun N _ _ h => subsingleton_iff_forall_eq 0 |>.2 <| fun y => by
      simpa [eq_comm] using (iff_exact (0 : PUnit →ₗ[R] N) (0 : N →ₗ[R] PUnit) |>.2 fun x => by
        simpa using Subsingleton.elim _ _) y⟩⟩

Proof state:
R : Type u
M : Type v
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
iff_exact :
  ∀ {N1 : Type (max u v)} [inst : AddCommGroup N1] [inst_1 : Module R N1] {N2 : Type (max u v)}
    [inst_2 : AddCommGroup N2] [inst_3 : Module R N2] {N3 : Type (max u v)} [inst_4 : AddCommGroup N3]
    [inst_5 : Module R N3] (l12 : N1 →ₗ[R] N2) (l23 : N2 →ₗ[R] N3),
    Function.Exact ⇑l12 ⇑l23 ↔ Function.Exact ⇑(LinearMap.rTensor M l12) ⇑(LinearMap.rTensor M l23)
N : Type (max u v)
x✝¹ : AddCommGroup N
x✝ : Module R N
h : Subsingleton (N ⊗[R] M)
y : N
⊢ y = 0

Tactic:
simpa [eq_comm] using (iff_exact (0 : PUnit →ₗ[R] N) (0 : N →ₗ[R] PUnit) |>.2 fun x => by
  simpa using Subsingleton.elim _ _) y

Result:
no goals

Proof state:
R : Type u
M : Type v
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
iff_exact :
  ∀ {N1 : Type (max u v)} [inst : AddCommGroup N1] [inst_1 : Module R N1] {N2 : Type (max u v)}
    [inst_2 : AddCommGroup N2] [inst_3 : Module R N2] {N3 : Type (max u v)} [inst_4 : AddCommGroup N3]
    [inst_5 : Module R N3] (l12 : N1 →ₗ[R] N2) (l23 : N2 →ₗ[R] N3),
    Function.Exact ⇑l12 ⇑l23 ↔ Function.Exact ⇑(LinearMap.rTensor M l12) ⇑(LinearMap.rTensor M l23)
N : Type (max u v)
x✝¹ : AddCommGroup N
x✝ : Module R N
h : Subsingleton (N ⊗[R] M)
y : N
x : N ⊗[R] M
⊢ (LinearMap.rTensor M 0) x = 0 ↔ x ∈ Set.range ⇑(LinearMap.rTensor M 0)

Tactic:
simpa using Subsingleton.elim _ _

Result:
no goals
-- Mathlib/Logic/Basic.lean
theorem heq_rec_iff_heq {α β : Sort _} {a b : α} {C : α → Sort*} {x : β} {y : C a} {e : a = b} :
    HEq x (e ▸ y) ↔ HEq x y

Proof state:
α : Sort u_2
β : Sort u_1
a b : α
C : α → Sort u_1
x : β
y : C a
e : a = b
⊢ HEq x (e ▸ y) ↔ HEq x y

Tactic:
subst e

Result:
α : Sort u_2
β : Sort u_1
a : α
C : α → Sort u_1
x : β
y : C a
⊢ HEq x (⋯ ▸ y) ↔ HEq x y

Proof state:
α : Sort u_2
β : Sort u_1
a : α
C : α → Sort u_1
x : β
y : C a
⊢ HEq x (⋯ ▸ y) ↔ HEq x y

Tactic:
rfl

Result:
no goals
-- Mathlib/Data/Stream/Init.lean
@[simp] lemma take_prefix : a.take m <+: a.take n ↔ m ≤ n :=
  ⟨fun h ↦ by simpa using h.length_le, take_prefix_take_left m n a⟩

Proof state:
α : Type u
m n : ℕ
a : Stream' α
h : take m a <+: take n a
⊢ m ≤ n

Tactic:
simpa using h.length_le

Result:
no goals
-- Mathlib/Order/Filter/Lift.lean
theorem mem_lift_sets (hg : Monotone g) {s : Set β} : s ∈ f.lift g ↔ ∃ t ∈ f, s ∈ g t :=
  (f.basis_sets.mem_lift_iff (fun s => (g s).basis_sets) hg).trans <| by
    simp only [id, exists_mem_subset_iff]

Proof state:
α : Type u_1
β : Type u_2
f : Filter α
g : Set α → Filter β
hg : Monotone g
s : Set β
⊢ (∃ i ∈ f, ∃ x ∈ g i, id x ⊆ s) ↔ ∃ t ∈ f, s ∈ g t

Tactic:
simp only [id, exists_mem_subset_iff]

Result:
no goals
-- Mathlib/Data/Finset/Prod.lean
theorem singleton_product_singleton {a : α} {b : β} :
    ({a} ×ˢ {b} : Finset _) = {(a, b)}

Proof state:
α : Type u_1
β : Type u_2
a : α
b : β
⊢ {a} ×ˢ {b} = {(a, b)}

Tactic:
simp only [product_singleton, Function.Embedding.coeFn_mk, map_singleton]

Result:
no goals
-- Mathlib/Order/Heyting/Regular.lean
theorem IsRegular.himp (ha : IsRegular a) (hb : IsRegular b) : IsRegular (a ⇨ b)

Proof state:
α : Type u_1
inst✝ : HeytingAlgebra α
a b : α
ha : IsRegular a
hb : IsRegular b
⊢ IsRegular (a ⇨ b)

Tactic:
rw [IsRegular, compl_compl_himp_distrib, ha.eq, hb.eq]

Result:
no goals
-- Mathlib/LinearAlgebra/TensorProduct/RightExactness.lean
lemma rTensor.inverse_comp_rTensor :
    (rTensor.inverse Q hfg hg).comp (rTensor Q g) =
      Submodule.mkQ (p := LinearMap.range (rTensor Q f))

Proof state:
R : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
inst✝⁸ : CommRing R
inst✝⁷ : AddCommGroup M
inst✝⁶ : AddCommGroup N
inst✝⁵ : AddCommGroup P
inst✝⁴ : Module R M
inst✝³ : Module R N
inst✝² : Module R P
f : M →ₗ[R] N
g : N →ₗ[R] P
Q : Type u_5
inst✝¹ : AddCommGroup Q
inst✝ : Module R Q
hfg : Exact ⇑f ⇑g
hg : Surjective ⇑g
⊢ inverse Q hfg hg ∘ₗ rTensor Q g = (range (rTensor Q f)).mkQ

Tactic:
rw [rTensor.inverse, rTensor.inverse_of_rightInverse_comp_rTensor]

Result:
no goals
-- Mathlib/Algebra/Group/Subgroup/Finite.lean
@[to_additive] lemma eq_bot_iff_card : H = ⊥ ↔ Nat.card H = 1 :=
  ⟨by rintro rfl; exact card_bot, eq_bot_of_card_eq _⟩

Proof state:
G : Type u_1
inst✝ : Group G
H : Subgroup G
⊢ H = ⊥ → Nat.card ↥H = 1

Tactic:
rintro rfl

Result:
G : Type u_1
inst✝ : Group G
⊢ Nat.card ↥⊥ = 1

Proof state:
G : Type u_1
inst✝ : Group G
⊢ Nat.card ↥⊥ = 1

Tactic:
exact card_bot

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

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

Tactic:
simp_to_raw using Raw₀.getKeyD_erase

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/WF.lean
theorem getKey?_eq_getKey? [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] {m : Raw₀ α β}
    (hm : Raw.WFImp m.1) {a : α} :
    m.getKey? a = List.getKey? a (toListModel m.1.buckets)

Proof state:
α : Type u
β : α → Type v
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
m : Raw₀ α β
hm : Raw.WFImp m.val
a : α
⊢ m.getKey? a = List.getKey? a (toListModel m.val.buckets)

Tactic:
rw [getKey?_eq_getKey?ₘ, getKey?ₘ_eq_getKey? hm]

Result:
no goals
-- Mathlib/Geometry/Euclidean/Angle/Oriented/RightAngle.lean
theorem cos_oangle_sub_left_mul_norm_of_oangle_eq_pi_div_two {x y : V}
    (h : o.oangle x y = ↑(π / 2)) : Real.Angle.cos (o.oangle (x - y) x) * ‖x - y‖ = ‖x‖

Proof state:
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
hd2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
h : (-o).oangle y x = ↑(π / 2)
⊢ ((-o).oangle x (x - y)).cos * ‖x - y‖ = ‖x‖

Tactic:
exact (-o).cos_oangle_sub_right_mul_norm_of_oangle_eq_pi_div_two h

Result:
no goals

Proof state:
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
hd2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
h : o.oangle x y = ↑(π / 2)
⊢ (o.oangle (x - y) x).cos * ‖x - y‖ = ‖x‖

Tactic:
rw [← neg_inj, oangle_rev, ← oangle_neg_orientation_eq_neg, neg_inj] at h ⊢

Result:
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
hd2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
h : (-o).oangle y x = ↑(π / 2)
⊢ ((-o).oangle x (x - y)).cos * ‖x - y‖ = ‖x‖
-- Mathlib/.lake/packages/lean4/src/lean/Std/Tactic/BVDecide/Normalize/BitVec.lean
theorem BitVec.not_neg'' (x : BitVec w) : ~~~(1#w + x) = ~~~x + -1#w

Proof state:
w : Nat
x : BitVec w
⊢ ~~~(1#w + x) = ~~~x + -1#w

Tactic:
rw [BitVec.add_comm 1#w x]

Result:
w : Nat
x : BitVec w
⊢ ~~~(x + 1#w) = ~~~x + -1#w

Proof state:
w : Nat
x : BitVec w
⊢ ~~~(x + 1#w) = ~~~x + -1#w

Tactic:
rw [BitVec.not_neg']

Result:
no goals
-- Mathlib/RingTheory/Adjoin/Tower.lean
theorem adjoin_res_eq_adjoin_res (C D E F : Type*) [CommSemiring C] [CommSemiring D]
    [CommSemiring E] [CommSemiring F] [Algebra C D] [Algebra C E] [Algebra C F] [Algebra D F]
    [Algebra E F] [IsScalarTower C D F] [IsScalarTower C E F] {S : Set D} {T : Set E}
    (hS : Algebra.adjoin C S = ⊤) (hT : Algebra.adjoin C T = ⊤) :
    (Algebra.adjoin E (algebraMap D F '' S)).restrictScalars C =
      (Algebra.adjoin D (algebraMap E F '' T)).restrictScalars C

Proof state:
C : Type u_1
D : Type u_2
E : Type u_3
F : Type u_4
inst✝¹⁰ : CommSemiring C
inst✝⁹ : CommSemiring D
inst✝⁸ : CommSemiring E
inst✝⁷ : CommSemiring F
inst✝⁶ : Algebra C D
inst✝⁵ : Algebra C E
inst✝⁴ : Algebra C F
inst✝³ : Algebra D F
inst✝² : Algebra E F
inst✝¹ : IsScalarTower C D F
inst✝ : IsScalarTower C E F
S : Set D
T : Set E
hS : adjoin C S = ⊤
hT : adjoin C T = ⊤
⊢ Subalgebra.restrictScalars C (adjoin E (⇑(algebraMap D F) '' S)) =
    Subalgebra.restrictScalars C (adjoin D (⇑(algebraMap E F) '' T))

Tactic:
rw [adjoin_restrictScalars C E, adjoin_restrictScalars C D, ← hS, ← hT, ← Algebra.adjoin_image,
  ← Algebra.adjoin_image, ← AlgHom.coe_toRingHom, ← AlgHom.coe_toRingHom,
  IsScalarTower.coe_toAlgHom, IsScalarTower.coe_toAlgHom, ← adjoin_union_eq_adjoin_adjoin, ←
  adjoin_union_eq_adjoin_adjoin, Set.union_comm]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/List/Associative.lean
theorem containsKey_eraseKey_self [BEq α] [PartialEquivBEq α] {l : List ((a : α) × β a)} {k : α}
    (h : DistinctKeys l) : containsKey k (eraseKey k l) = false

Proof state:
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : PartialEquivBEq α
l : List ((a : α) × β a)
k : α
h : DistinctKeys l
⊢ containsKey k (eraseKey k l) = false

Tactic:
simp [containsKey_eq_isSome_getEntry?, getEntry?_eraseKey_self h]

Result:
no goals
-- Mathlib/Data/ENNReal/Inv.lean
theorem ofReal_div_of_pos {x y : ℝ} (hy : 0 < y) :
    ENNReal.ofReal (x / y) = ENNReal.ofReal x / ENNReal.ofReal y

Proof state:
x y : ℝ
hy : 0 < y
⊢ ENNReal.ofReal (x / y) = ENNReal.ofReal x / ENNReal.ofReal y

Tactic:
rw [div_eq_mul_inv, div_eq_mul_inv, ofReal_mul' (inv_nonneg.2 hy.le), ofReal_inv_of_pos hy]

Result:
no goals
-- Mathlib/Algebra/Module/LocalizedModule/Basic.lean
theorem fromLocalizedModule.surj : Function.Surjective <| fromLocalizedModule S f := fun x =>
  let ⟨⟨m, s⟩, eq1⟩ := IsLocalizedModule.surj S f x
  ⟨LocalizedModule.mk m s, by
    rw [fromLocalizedModule_mk, Module.End_algebraMap_isUnit_inv_apply_eq_iff, ← eq1,
      Submonoid.smul_def]⟩

Proof state:
R : Type u_1
inst✝⁵ : CommSemiring R
S : Submonoid R
M : Type u_2
M' : Type u_3
inst✝⁴ : AddCommMonoid M
inst✝³ : AddCommMonoid M'
inst✝² : Module R M
inst✝¹ : Module R M'
f : M →ₗ[R] M'
inst✝ : IsLocalizedModule S f
x : M'
m : M
s : ↥S
eq1 : (m, s).2 • x = f (m, s).1
⊢ (fromLocalizedModule S f) (LocalizedModule.mk m s) = x

Tactic:
rw [fromLocalizedModule_mk, Module.End_algebraMap_isUnit_inv_apply_eq_iff, ← eq1,
  Submonoid.smul_def]

Result:
no goals
-- Mathlib/Topology/Category/TopCat/Limits/Pullbacks.lean
lemma snd_isEmbedding_of_left {X Y S : TopCat} {f : X ⟶ S} (H : IsEmbedding f) (g : Y ⟶ S) :
    IsEmbedding <| ⇑(pullback.snd f g)

Proof state:
X Y S : TopCat
f : X ⟶ S
H : IsEmbedding ⇑(ConcreteCategory.hom f)
g : Y ⟶ S
⊢ g ≫ 𝟙 S = 𝟙 Y ≫ g

Tactic:
simp

Result:
no goals

Proof state:
X Y S : TopCat
f : X ⟶ S
H : IsEmbedding ⇑(ConcreteCategory.hom f)
g : Y ⟶ S
⊢ IsEmbedding ⇑(ConcreteCategory.hom (pullback.snd f g))

Tactic:
convert (homeoOfIso (asIso (pullback.snd (𝟙 S) g))).isEmbedding.comp
    (pullback_map_isEmbedding (i₂ := 𝟙 Y)
      f g (𝟙 S) g H (homeoOfIso (Iso.refl _)).isEmbedding (𝟙 _) rfl (by simp))

Result:
case h.e'_5
X Y S : TopCat
f : X ⟶ S
H : IsEmbedding ⇑(ConcreteCategory.hom f)
g : Y ⟶ S
⊢ ⇑(ConcreteCategory.hom (pullback.snd f g)) =
    ⇑(homeoOfIso (asIso (pullback.snd (𝟙 S) g))) ∘ ⇑(ConcreteCategory.hom (pullback.map f g (𝟙 S) g f (𝟙 Y) (𝟙 S) ⋯ ⋯))

Proof state:
case h.e'_5
X Y S : TopCat
f : X ⟶ S
H : IsEmbedding ⇑(ConcreteCategory.hom f)
g : Y ⟶ S
⊢ ⇑(ConcreteCategory.hom (pullback.snd f g)) =
    ⇑(homeoOfIso (asIso (pullback.snd (𝟙 S) g))) ∘ ⇑(ConcreteCategory.hom (pullback.map f g (𝟙 S) g f (𝟙 Y) (𝟙 S) ⋯ ⋯))

Tactic:
simp [homeoOfIso, ← coe_comp]

Result:
no goals