harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/MeasureTheory/Measure/Comap.lean
lemma MeasurableEmbedding.comap_add {f : α → β} (hf : MeasurableEmbedding f) (μ ν : Measure β) :
    (μ + ν).comap f = μ.comap f + ν.comap f

Proof state:
case h
α : Type u_1
β : Type u_2
ma : MeasurableSpace α
mb : MeasurableSpace β
f : α → β
hf : MeasurableEmbedding f
μ ν : Measure β
s : Set α
hs : MeasurableSet s
⊢ (Measure.comap f (μ + ν)) s = (Measure.comap f μ + Measure.comap f ν) s

Tactic:
simp only [← comapₗ_eq_comap _ hf.injective (fun _ ↦ hf.measurableSet_image.mpr) _ hs,
  _root_.map_add, add_apply]

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
ma : MeasurableSpace α
mb : MeasurableSpace β
f : α → β
hf : MeasurableEmbedding f
μ ν : Measure β
⊢ Measure.comap f (μ + ν) = Measure.comap f μ + Measure.comap f ν

Tactic:
ext s hs

Result:
case h
α : Type u_1
β : Type u_2
ma : MeasurableSpace α
mb : MeasurableSpace β
f : α → β
hf : MeasurableEmbedding f
μ ν : Measure β
s : Set α
hs : MeasurableSet s
⊢ (Measure.comap f (μ + ν)) s = (Measure.comap f μ + Measure.comap f ν) s
-- Mathlib/Topology/Instances/ENNReal/Lemmas.lean
theorem Tendsto.div_const {f : Filter α} {m : α → ℝ≥0∞} {a b : ℝ≥0∞}
    (hm : Tendsto m f (𝓝 a)) (ha : a ≠ 0 ∨ b ≠ 0) : Tendsto (fun x => m x / b) f (𝓝 (a / b))

Proof state:
α : Type u_1
f : Filter α
m : α → ℝ≥0∞
a b : ℝ≥0∞
hm : Tendsto m f (𝓝 a)
ha : a ≠ 0 ∨ b ≠ 0
⊢ Tendsto (fun x => m x / b) f (𝓝 (a / b))

Tactic:
apply Tendsto.mul_const hm

Result:
α : Type u_1
f : Filter α
m : α → ℝ≥0∞
a b : ℝ≥0∞
hm : Tendsto m f (𝓝 a)
ha : a ≠ 0 ∨ b ≠ 0
⊢ a ≠ 0 ∨ b⁻¹ ≠ ⊤

Proof state:
α : Type u_1
f : Filter α
m : α → ℝ≥0∞
a b : ℝ≥0∞
hm : Tendsto m f (𝓝 a)
ha : a ≠ 0 ∨ b ≠ 0
⊢ a ≠ 0 ∨ b⁻¹ ≠ ⊤

Tactic:
simp [ha]

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

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

Tactic:
subst e

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

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

Tactic:
rfl

Result:
no goals
-- Mathlib/Geometry/Euclidean/Triangle.lean
theorem norm_sub_sq_eq_norm_sq_add_norm_sq_sub_two_mul_norm_mul_norm_mul_cos_angle (x y : V) :
    ‖x - y‖ * ‖x - y‖ = ‖x‖ * ‖x‖ + ‖y‖ * ‖y‖ - 2 * ‖x‖ * ‖y‖ * Real.cos (angle x y)

Proof state:
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
⊢ ‖x - y‖ * ‖x - y‖ = ‖x‖ * ‖x‖ + ‖y‖ * ‖y‖ - 2 * ‖x‖ * ‖y‖ * Real.cos (angle x y)

Tactic:
rw [show 2 * ‖x‖ * ‖y‖ * Real.cos (angle x y) = 2 * (Real.cos (angle x y) * (‖x‖ * ‖y‖)) by ring,
  cos_angle_mul_norm_mul_norm, ← real_inner_self_eq_norm_mul_norm, ←
  real_inner_self_eq_norm_mul_norm, ← real_inner_self_eq_norm_mul_norm, real_inner_sub_sub_self,
  sub_add_eq_add_sub]

Result:
no goals

Proof state:
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
⊢ 2 * ‖x‖ * ‖y‖ * Real.cos (angle x y) = 2 * (Real.cos (angle x y) * (‖x‖ * ‖y‖))

Tactic:
ring

Result:
no goals
-- Mathlib/SetTheory/Cardinal/Cofinality.lean
theorem iSup_lt_of_isRegular {ι} {f : ι → Cardinal} {c} (hc : IsRegular c) (hι : #ι < c) :
    (∀ i, f i < c) → iSup f < c :=
  iSup_lt (by rwa [hc.cof_eq])

Proof state:
ι : Type u_1
f : ι → Cardinal.{u_1}
c : Cardinal.{u_1}
hc : c.IsRegular
hι : #ι < c
⊢ #ι < c.ord.cof

Tactic:
rwa [hc.cof_eq]

Result:
no goals
-- Mathlib/Order/Heyting/Boundary.lean
theorem boundary_idem (a : α) : ∂ ∂ a = ∂ a

Proof state:
α : Type u_1
inst✝ : CoheytingAlgebra α
a : α
⊢ ∂ ∂ a = ∂ a

Tactic:
rw [boundary, hnot_boundary, inf_top_eq]

Result:
no goals
-- Mathlib/RepresentationTheory/GroupCohomology/LowDegree.lean
theorem twoCocycles_map_one_snd (f : twoCocycles A) (g : G) :
    f (g, 1) = A.ρ g (f (1, 1))

Proof state:
k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A : Rep k G
f : ↥(twoCocycles A)
g : G
⊢ f (g, 1) = (A.ρ g) (f (1, 1))

Tactic:
have := (mem_twoCocycles_iff f).1 f.2 g 1 1

Result:
k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A : Rep k G
f : ↥(twoCocycles A)
g : G
this : f (g * 1, 1) + f (g, 1) = (A.ρ g) (f (1, 1)) + f (g, 1 * 1)
⊢ f (g, 1) = (A.ρ g) (f (1, 1))

Proof state:
k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A : Rep k G
f : ↥(twoCocycles A)
g : G
this : f (g * 1, 1) + f (g, 1) = (A.ρ g) (f (1, 1)) + f (g, 1 * 1)
⊢ f (g, 1) = (A.ρ g) (f (1, 1))

Tactic:
simpa only [mul_one, add_left_inj, this]

Result:
no goals
-- Mathlib/LinearAlgebra/FiniteDimensional.lean
theorem finrank_lt [FiniteDimensional K V] {s : Submodule K V} (h : s < ⊤) :
    finrank K s < finrank K V

Proof state:
K : Type u
V : Type v
inst✝³ : DivisionRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
s : Submodule K V
h : s < ⊤
⊢ finrank K ↥s < finrank K ↥s + finrank K (V ⧸ s)

Tactic:
exact Nat.lt_add_of_pos_right (finrank_pos_iff.mpr (Quotient.nontrivial_of_lt_top _ h))

Result:
no goals

Proof state:
K : Type u
V : Type v
inst✝³ : DivisionRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
s : Submodule K V
h : s < ⊤
⊢ finrank K ↥s < finrank K V

Tactic:
rw [← s.finrank_quotient_add_finrank, add_comm]

Result:
K : Type u
V : Type v
inst✝³ : DivisionRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
s : Submodule K V
h : s < ⊤
⊢ finrank K ↥s < finrank K ↥s + finrank K (V ⧸ s)
-- Mathlib/MeasureTheory/Group/AEStabilizer.lean
@[to_additive]
lemma aestabilizer_congr (h : s =ᵐ[μ] t) : aestabilizer G μ s = aestabilizer G μ t

Proof state:
case h
G : Type u_1
α : Type u_2
inst✝² : Group G
inst✝¹ : MulAction G α
x✝ : MeasurableSpace α
μ : Measure α
inst✝ : SMulInvariantMeasure G α μ
s t : Set α
h : s =ᶠ[ae μ] t
g : G
⊢ g ∈ aestabilizer G μ s ↔ g ∈ aestabilizer G μ t

Tactic:
rw [mem_aestabilizer, mem_aestabilizer, h.congr_right, ((smul_set_ae_eq g).2 h).congr_left]

Result:
no goals

Proof state:
G : Type u_1
α : Type u_2
inst✝² : Group G
inst✝¹ : MulAction G α
x✝ : MeasurableSpace α
μ : Measure α
inst✝ : SMulInvariantMeasure G α μ
s t : Set α
h : s =ᶠ[ae μ] t
⊢ aestabilizer G μ s = aestabilizer G μ t

Tactic:
ext g

Result:
case h
G : Type u_1
α : Type u_2
inst✝² : Group G
inst✝¹ : MulAction G α
x✝ : MeasurableSpace α
μ : Measure α
inst✝ : SMulInvariantMeasure G α μ
s t : Set α
h : s =ᶠ[ae μ] t
g : G
⊢ g ∈ aestabilizer G μ s ↔ g ∈ aestabilizer G μ t
-- Mathlib/Data/List/Intervals.lean
theorem filter_lt_of_succ_bot {n m : ℕ} (hnm : n < m) :
    ((Ico n m).filter fun x => x < n + 1) = [n]

Proof state:
n m : ℕ
hnm : n < m
r : m ⊓ (n + 1) = n + 1
⊢ filter (fun x => decide (x < n + 1)) (Ico n m) = [n]

Tactic:
simp [filter_lt n m (n + 1), r]

Result:
no goals

Proof state:
n m : ℕ
hnm : n < m
⊢ filter (fun x => decide (x < n + 1)) (Ico n m) = [n]

Tactic:
have r : min m (n + 1) = n + 1 := (@inf_eq_right _ _ m (n + 1)).mpr hnm

Result:
n m : ℕ
hnm : n < m
r : m ⊓ (n + 1) = n + 1
⊢ filter (fun x => decide (x < n + 1)) (Ico n m) = [n]
-- Mathlib/LinearAlgebra/Span/Defs.lean
theorem span_zero : span R (0 : Set M) = ⊥

Proof state:
R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
⊢ span R 0 = ⊥

Tactic:
rw [← singleton_zero, span_singleton_eq_bot]

Result:
no goals
-- Mathlib/Data/Nat/PartENat.lean
theorem coe_add_get {x : ℕ} {y : PartENat} (h : ((x : PartENat) + y).Dom) :
    get ((x : PartENat) + y) h = x + get y h.2

Proof state:
x : ℕ
y : PartENat
h : (↑x + y).Dom
⊢ (↑x + y).get h = x + y.get ⋯

Tactic:
rfl

Result:
no goals
-- Mathlib/CategoryTheory/Sites/Sieves.lean
theorem le_pullback_bind (S : Presieve X) (R : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, S f → Sieve Y) (f : Y ⟶ X)
    (h : S f) : R h ≤ (bind S R).pullback f

Proof state:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y : C
S : Presieve X
R : ⦃Y : C⦄ → ⦃f : Y ⟶ X⦄ → S f → Sieve Y
f : Y ⟶ X
h : S f
⊢ pushforward f (R h) ≤ bind S R

Tactic:
apply pushforward_le_bind_of_mem

Result:
no goals

Proof state:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y : C
S : Presieve X
R : ⦃Y : C⦄ → ⦃f : Y ⟶ X⦄ → S f → Sieve Y
f : Y ⟶ X
h : S f
⊢ R h ≤ pullback f (bind S R)

Tactic:
rw [← galoisConnection f]

Result:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y : C
S : Presieve X
R : ⦃Y : C⦄ → ⦃f : Y ⟶ X⦄ → S f → Sieve Y
f : Y ⟶ X
h : S f
⊢ pushforward f (R h) ≤ bind S R
-- Mathlib/MeasureTheory/Measure/Stieltjes.lean
lemma measure_univ_of_tendsto_atTop_atTop (hf : Tendsto f atTop atTop) :
    f.measure univ = ∞

Proof state:
f : StieltjesFunction
hf : Tendsto (↑f) atTop atTop
⊢ f.measure univ = ⊤

Tactic:
rw [← top_le_iff, ← f.measure_Ioi_of_tendsto_atTop_atTop hf 0]

Result:
f : StieltjesFunction
hf : Tendsto (↑f) atTop atTop
⊢ f.measure (Ioi 0) ≤ f.measure univ

Proof state:
f : StieltjesFunction
hf : Tendsto (↑f) atTop atTop
⊢ f.measure (Ioi 0) ≤ f.measure univ

Tactic:
exact measure_mono (subset_univ _)

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/RawLemmas.lean
theorem getKey!_ofList_of_mem [EquivBEq α] [LawfulHashable α] [Inhabited α]
    {l : List ((a : α) × β a)}
    {k k' : α} (k_beq : k == k')
    (distinct : l.Pairwise (fun a b => (a.1 == b.1) = false))
    (mem : k ∈ l.map Sigma.fst) :
    (ofList l).getKey! k' = k

Proof state:
α : Type u
β : α → Type v
inst✝⁴ : BEq α
inst✝³ : Hashable α
inst✝² : EquivBEq α
inst✝¹ : LawfulHashable α
inst✝ : Inhabited α
l : List ((a : α) × β a)
k k' : α
k_beq : (k == k') = true
distinct : List.Pairwise (fun a b => (a.fst == b.fst) = false) l
mem : k ∈ List.map Sigma.fst l
⊢ (ofList l).getKey! k' = k

Tactic:
simp_to_raw using Raw₀.getKey!_insertMany_empty_list_of_mem

Result:
no goals
-- Mathlib/.lake/packages/batteries/Batteries/Data/RBMap/Lemmas.lean
theorem upperBound?_reverse (t : RBNode α) (cut ub) :
    t.reverse.upperBound? cut ub = t.lowerBound? (cut · |>.swap) ub

Proof state:
α : Type u_1
t : RBNode α
cut : α → Ordering
ub : Option α
⊢ upperBound? cut t.reverse ub = lowerBound? (fun x => (cut x).swap) t ub

Tactic:
induction t generalizing ub <;> simp [lowerBound?, upperBound?]

Result:
case node
α : Type u_1
cut : α → Ordering
c✝ : RBColor
l✝ : RBNode α
v✝ : α
r✝ : RBNode α
l_ih✝ : ∀ (ub : Option α), upperBound? cut l✝.reverse ub = lowerBound? (fun x => (cut x).swap) l✝ ub
r_ih✝ : ∀ (ub : Option α), upperBound? cut r✝.reverse ub = lowerBound? (fun x => (cut x).swap) r✝ ub
ub : Option α
⊢ (match cut v✝ with
    | Ordering.lt => upperBound? cut r✝.reverse (some v✝)
    | Ordering.gt => upperBound? cut l✝.reverse ub
    | Ordering.eq => some v✝) =
    match (cut v✝).swap with
    | Ordering.lt => lowerBound? (fun x => (cut x).swap) l✝ ub
    | Ordering.gt => lowerBound? (fun x => (cut x).swap) r✝ (some v✝)
    | Ordering.eq => some v✝

Proof state:
case node
α : Type u_1
cut : α → Ordering
c✝ : RBColor
l✝ : RBNode α
v✝ : α
r✝ : RBNode α
l_ih✝ : ∀ (ub : Option α), upperBound? cut l✝.reverse ub = lowerBound? (fun x => (cut x).swap) l✝ ub
r_ih✝ : ∀ (ub : Option α), upperBound? cut r✝.reverse ub = lowerBound? (fun x => (cut x).swap) r✝ ub
ub : Option α
⊢ (match cut v✝ with
    | Ordering.lt => upperBound? cut r✝.reverse (some v✝)
    | Ordering.gt => upperBound? cut l✝.reverse ub
    | Ordering.eq => some v✝) =
    match (cut v✝).swap with
    | Ordering.lt => lowerBound? (fun x => (cut x).swap) l✝ ub
    | Ordering.gt => lowerBound? (fun x => (cut x).swap) r✝ (some v✝)
    | Ordering.eq => some v✝

Tactic:
split <;> simp [*, Ordering.swap]

Result:
no goals
-- Mathlib/Data/ZMod/Basic.lean
theorem natCast_zmod_val {n : ℕ} [NeZero n] (a : ZMod n) : (a.val : ZMod n) = a

Proof state:
case succ
n✝ : ℕ
inst✝ : NeZero (n✝ + 1)
a : ZMod (n✝ + 1)
⊢ ↑a.val = a

Tactic:
apply Fin.cast_val_eq_self

Result:
no goals

Proof state:
case zero
inst✝ : NeZero 0
a : ZMod 0
⊢ ↑a.val = a

Tactic:
cases NeZero.ne 0 rfl

Result:
no goals

Proof state:
n : ℕ
inst✝ : NeZero n
a : ZMod n
⊢ ↑a.val = a

Tactic:
cases n

Result:
case zero
inst✝ : NeZero 0
a : ZMod 0
⊢ ↑a.val = a

case succ
n✝ : ℕ
inst✝ : NeZero (n✝ + 1)
a : ZMod (n✝ + 1)
⊢ ↑a.val = a
-- Mathlib/Analysis/Analytic/Basic.lean
theorem radius_unshift (p : FormalMultilinearSeries 𝕜 E (E →L[𝕜] F)) (z : F) :
    (p.unshift z).radius = p.radius

Proof state:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E (E →L[𝕜] F)
z : F
⊢ (p.unshift z).radius = p.radius

Tactic:
rw [← radius_shift, unshift_shift]

Result:
no goals
-- Mathlib/Topology/Algebra/GroupWithZero.lean
lemma tendsto_inv_iff₀ {l : Filter α} {f : α → G₀} (hx : x ≠ 0) :
    Tendsto (fun x ↦ (f x)⁻¹) l (𝓝 x⁻¹) ↔ Tendsto f l (𝓝 x)

Proof state:
α : Type u_1
G₀ : Type u_3
inst✝² : GroupWithZero G₀
inst✝¹ : TopologicalSpace G₀
inst✝ : HasContinuousInv₀ G₀
x : G₀
l : Filter α
f : α → G₀
hx : x ≠ 0
⊢ Tendsto (fun x => (f x)⁻¹) l (𝓝 x⁻¹) ↔ Tendsto f l (𝓝 x)

Tactic:
simp only [nhds_inv₀ hx, ← Filter.comap_inv, tendsto_comap_iff, Function.comp_def, inv_inv]

Result:
no goals
-- Mathlib/Data/Finset/NAry.lean
theorem card_image₂_iff :
    #(image₂ f s t) = #s * #t ↔ (s ×ˢ t : Set (α × β)).InjOn fun x => f x.1 x.2

Proof state:
α : Type u_1
β : Type u_3
γ : Type u_5
inst✝ : DecidableEq γ
f : α → β → γ
s : Finset α
t : Finset β
⊢ #(image₂ f s t) = #(s ×ˢ t) ↔ InjOn (fun x => f x.1 x.2) ↑(s ×ˢ t)

Tactic:
exact card_image_iff

Result:
no goals

Proof state:
α : Type u_1
β : Type u_3
γ : Type u_5
inst✝ : DecidableEq γ
f : α → β → γ
s : Finset α
t : Finset β
⊢ #(image₂ f s t) = #s * #t ↔ InjOn (fun x => f x.1 x.2) (↑s ×ˢ ↑t)

Tactic:
rw [← card_product, ← coe_product]

Result:
α : Type u_1
β : Type u_3
γ : Type u_5
inst✝ : DecidableEq γ
f : α → β → γ
s : Finset α
t : Finset β
⊢ #(image₂ f s t) = #(s ×ˢ t) ↔ InjOn (fun x => f x.1 x.2) ↑(s ×ˢ t)
-- Mathlib/Analysis/InnerProductSpace/Defs.lean
theorem inner_zero_left (x : F) : ⟪0, x⟫ = 0

Proof state:
𝕜 : Type u_1
F : Type u_3
inst✝² : RCLike 𝕜
inst✝¹ : AddCommGroup F
inst✝ : Module 𝕜 F
c : PreInnerProductSpace.Core 𝕜 F
x : F
⊢ (starRingEnd 𝕜) 0 * ⟪0, x⟫_𝕜 = 0

Tactic:
simp only [zero_mul, RingHom.map_zero]

Result:
no goals

Proof state:
𝕜 : Type u_1
F : Type u_3
inst✝² : RCLike 𝕜
inst✝¹ : AddCommGroup F
inst✝ : Module 𝕜 F
c : PreInnerProductSpace.Core 𝕜 F
x : F
⊢ ⟪0, x⟫_𝕜 = 0

Tactic:
rw [← zero_smul 𝕜 (0 : F), inner_smul_left]

Result:
𝕜 : Type u_1
F : Type u_3
inst✝² : RCLike 𝕜
inst✝¹ : AddCommGroup F
inst✝ : Module 𝕜 F
c : PreInnerProductSpace.Core 𝕜 F
x : F
⊢ (starRingEnd 𝕜) 0 * ⟪0, x⟫_𝕜 = 0
-- Mathlib/Data/Matroid/Map.lean
@[simp] lemma comapOn_indep_iff :
    (N.comapOn E f).Indep I ↔ (N.Indep (f '' I) ∧ InjOn f I ∧ I ⊆ E)

Proof state:
α : Type u_1
β : Type u_2
f : α → β
N : Matroid β
E I : Set α
⊢ (N.comapOn E f).Indep I ↔ N.Indep (f '' I) ∧ InjOn f I ∧ I ⊆ E

Tactic:
simp [comapOn, and_assoc]

Result:
no goals
-- Mathlib/Algebra/Order/Hom/Ring.lean
theorem refl_apply (x : α) : OrderRingIso.refl α x = x

Proof state:
α : Type u_2
inst✝² : Mul α
inst✝¹ : Add α
inst✝ : LE α
x : α
⊢ (OrderRingIso.refl α) x = x

Tactic:
rfl

Result:
no goals
-- Mathlib/GroupTheory/Perm/Support.lean
theorem disjoint_prod_right (l : List (Perm α)) (h : ∀ g ∈ l, Disjoint f g) :
    Disjoint f l.prod

Proof state:
α : Type u_1
f : Perm α
l : List (Perm α)
h : ∀ g ∈ l, f.Disjoint g
⊢ f.Disjoint l.prod

Tactic:
induction' l with g l ih

Result:
case nil
α : Type u_1
f : Perm α
h : ∀ g ∈ [], f.Disjoint g
⊢ f.Disjoint [].prod

case cons
α : Type u_1
f g : Perm α
l : List (Perm α)
ih : (∀ g ∈ l, f.Disjoint g) → f.Disjoint l.prod
h : ∀ g_1 ∈ g :: l, f.Disjoint g_1
⊢ f.Disjoint (g :: l).prod

Proof state:
case nil
α : Type u_1
f : Perm α
h : ∀ g ∈ [], f.Disjoint g
⊢ f.Disjoint [].prod

Tactic:
exact disjoint_one_right _

Result:
no goals

Proof state:
case cons
α : Type u_1
f g : Perm α
l : List (Perm α)
ih : (∀ g ∈ l, f.Disjoint g) → f.Disjoint l.prod
h : ∀ g_1 ∈ g :: l, f.Disjoint g_1
⊢ f.Disjoint (g :: l).prod

Tactic:
rw [List.prod_cons]

Result:
case cons
α : Type u_1
f g : Perm α
l : List (Perm α)
ih : (∀ g ∈ l, f.Disjoint g) → f.Disjoint l.prod
h : ∀ g_1 ∈ g :: l, f.Disjoint g_1
⊢ f.Disjoint (g * l.prod)

Proof state:
case cons
α : Type u_1
f g : Perm α
l : List (Perm α)
ih : (∀ g ∈ l, f.Disjoint g) → f.Disjoint l.prod
h : ∀ g_1 ∈ g :: l, f.Disjoint g_1
⊢ f.Disjoint (g * l.prod)

Tactic:
exact (h _ (List.mem_cons_self _ _)).mul_right (ih fun g hg => h g (List.mem_cons_of_mem _ hg))

Result:
no goals
-- Mathlib/Algebra/Order/Interval/Finset/SuccPred.lean
lemma Ioo_add_one_right_eq_Ioc (a b : α) : Ioo a (b + 1) = Ioc a b

Proof state:
α : Type u_2
inst✝⁵ : LinearOrder α
inst✝⁴ : One α
inst✝³ : LocallyFiniteOrder α
inst✝² : Add α
inst✝¹ : SuccAddOrder α
inst✝ : NoMaxOrder α
a b : α
⊢ Ioo a (b + 1) = Ioc a b

Tactic:
simpa [succ_eq_add_one] using Ioo_succ_right_eq_Ioc a b

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Subgraph.lean
theorem neighborSet_snd_subgraphOfAdj {v w : V} (hvw : G.Adj v w) :
    (G.subgraphOfAdj hvw).neighborSet w = {v}

Proof state:
V : Type u
G : SimpleGraph V
v w : V
hvw : G.Adj v w
⊢ (G.subgraphOfAdj hvw).neighborSet w = {v}

Tactic:
rw [subgraphOfAdj_symm hvw.symm]

Result:
V : Type u
G : SimpleGraph V
v w : V
hvw : G.Adj v w
⊢ (G.subgraphOfAdj ⋯).neighborSet w = {v}

Proof state:
V : Type u
G : SimpleGraph V
v w : V
hvw : G.Adj v w
⊢ (G.subgraphOfAdj ⋯).neighborSet w = {v}

Tactic:
exact neighborSet_fst_subgraphOfAdj hvw.symm

Result:
no goals
-- Mathlib/Algebra/MvPolynomial/Eval.lean
theorem eval₂_comp (f : R →+* S₁) (g : σ → R) (p : MvPolynomial σ R) :
    f (eval g p) = eval₂ f (f ∘ g) p

Proof state:
R : Type u
S₁ : Type v
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S₁
f : R →+* S₁
g : σ → R
p : MvPolynomial σ R
⊢ f ((eval g) p) = eval₂ f (⇑f ∘ g) p

Tactic:
rw [← p.map_id, eval_map, eval₂_comp_right]

Result:
no goals
-- Mathlib/Algebra/Order/Interval/Set/SuccPred.lean
lemma Ioc_sub_one_sub_one_eq_Ico_of_not_isMin (ha : ¬ IsMin a) (b : α) :
    Ioc (a - 1) (b - 1) = Ico a b

Proof state:
α : Type u_2
inst✝³ : LinearOrder α
inst✝² : One α
inst✝¹ : Sub α
inst✝ : PredSubOrder α
a : α
ha : ¬IsMin a
b : α
⊢ Ioc (a - 1) (b - 1) = Ico a b

Tactic:
simpa [pred_eq_sub_one] using Ioc_pred_pred_eq_Ico_of_not_isMin ha b

Result:
no goals
-- Mathlib/Order/PrimeIdeal.lean
theorem PrimePair.I_isPrime (IF : PrimePair P) : IsPrime IF.I :=
  { IF.I_isProper with
    compl_filter

Proof state:
P : Type u_1
inst✝ : Preorder P
IF : PrimePair P
⊢ IsPFilter ↑IF.F

Tactic:
exact IF.F.isPFilter

Result:
no goals

Proof state:
P : Type u_1
inst✝ : Preorder P
IF : PrimePair P
⊢ IsPFilter (↑IF.I)ᶜ

Tactic:
rw [IF.compl_I_eq_F]

Result:
P : Type u_1
inst✝ : Preorder P
IF : PrimePair P
⊢ IsPFilter ↑IF.F
-- Mathlib/CategoryTheory/Limits/Shapes/FunctorToTypes.lean
@[simp]
lemma prodMk_snd {a : C} (x : F.obj a) (y : G.obj a) :
    (Limits.prod.snd (X := F)).app a (prodMk x y) = y

Proof state:
C : Type u
inst✝ : Category.{v, u} C
F G : C ⥤ Type w
a : C
x : F.obj a
y : G.obj a
⊢ Limits.prod.snd.app a (prodMk x y) = y

Tactic:
simp only [prodMk, binaryProductIso_inv_comp_snd_apply]

Result:
no goals
-- Mathlib/Probability/Independence/Basic.lean
theorem indepFun_iff_indepSet_preimage {mβ : MeasurableSpace β} {mβ' : MeasurableSpace β'}
    [IsZeroOrProbabilityMeasure μ] (hf : Measurable f) (hg : Measurable g) :
    IndepFun f g μ ↔
      ∀ s t, MeasurableSet s → MeasurableSet t → IndepSet (f ⁻¹' s) (g ⁻¹' t) μ

Proof state:
Ω : Type u_1
β : Type u_6
β' : Type u_7
_mΩ : MeasurableSpace Ω
μ : Measure Ω
f : Ω → β
g : Ω → β'
mβ : MeasurableSpace β
mβ' : MeasurableSpace β'
inst✝ : IsZeroOrProbabilityMeasure μ
hf : Measurable f
hg : Measurable g
⊢ IndepFun f g μ ↔ ∀ (s : Set β) (t : Set β'), MeasurableSet s → MeasurableSet t → IndepSet (f ⁻¹' s) (g ⁻¹' t) μ

Tactic:
simp only [IndepFun, IndepSet, Kernel.indepFun_iff_indepSet_preimage hf hg, ae_dirac_eq,
  Filter.eventually_pure, Kernel.const_apply]

Result:
no goals
-- Mathlib/RingTheory/PowerSeries/Trunc.lean
theorem coeff_trunc (m) (n) (φ : R⟦X⟧) :
    (trunc n φ).coeff m = if m < n then coeff R m φ else 0

Proof state:
R : Type u_1
inst✝ : Semiring R
m n : ℕ
φ : R⟦X⟧
⊢ (trunc n φ).coeff m = if m < n then (coeff R m) φ else 0

Tactic:
simp [trunc, Polynomial.coeff_sum, Polynomial.coeff_monomial, Nat.lt_succ_iff]

Result:
no goals
-- Mathlib/Data/Finset/Powerset.lean
lemma powersetCard_empty_subsingleton (n : ℕ) :
    (powersetCard n (∅ : Finset α) : Set <| Finset α).Subsingleton

Proof state:
α : Type u_1
n : ℕ
⊢ (↑(powersetCard n ∅)).Subsingleton

Tactic:
simp [Set.Subsingleton, subset_empty]

Result:
no goals
-- Mathlib/Algebra/Group/End.lean
theorem mul_swap_mul_self (i j : α) (σ : Perm α) : σ * Equiv.swap i j * Equiv.swap i j = σ

Proof state:
α : Type u_4
inst✝ : DecidableEq α
i j : α
σ : Perm α
⊢ σ * swap i j * swap i j = σ

Tactic:
rw [mul_assoc, swap_mul_self, mul_one]

Result:
no goals
-- Mathlib/NumberTheory/NumberField/ClassNumber.lean
theorem classNumber_eq : NumberField.classNumber ℚ = 1 :=
  classNumber_eq_one_iff.mpr <| by
    convert IsPrincipalIdealRing.of_surjective
      (Rat.ringOfIntegersEquiv.symm : ℤ →+* 𝓞 ℚ) Rat.ringOfIntegersEquiv.symm.surjective

Proof state:
⊢ IsPrincipalIdealRing (𝓞 ℚ)

Tactic:
convert IsPrincipalIdealRing.of_surjective
  (Rat.ringOfIntegersEquiv.symm : ℤ →+* 𝓞 ℚ) Rat.ringOfIntegersEquiv.symm.surjective

Result:
no goals
-- Mathlib/Algebra/Lie/Nilpotent.lean
theorem isNilpotent_iff_exists_self_le_ucs :
    LieModule.IsNilpotent L N ↔ ∃ k, N ≤ (⊥ : LieSubmodule R L M).ucs k

Proof state:
R : Type u
L : Type v
M : Type w
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
N : LieSubmodule R L M
inst✝ : LieModule R L M
⊢ LieModule.IsNilpotent L ↥N ↔ ∃ k, N ≤ ucs k ⊥

Tactic:
simp_rw [LieModule.isNilpotent_iff_exists_ucs_eq_top R, ← ucs_comap_incl, comap_incl_eq_top]

Result:
no goals
-- Mathlib/Algebra/Homology/HomotopyCategory/MappingCone.lean
lemma decomp_from {j : ℤ} {A : C} (f : (mappingCone φ).X j ⟶ A) (i : ℤ) (hij : j + 1 = i) :
    ∃ (a : F.X i ⟶ A) (b : G.X j ⟶ A),
      f = (fst φ).1.v j i hij ≫ a + (snd φ).v j j (add_zero j) ≫ b :=
  ⟨(inl φ).v i j (by omega) ≫ f, (inr φ).f j ≫ f,
    by apply ext_from φ i j hij <;> simp⟩

Proof state:
C : Type u_1
inst✝² : Category.{u_3, u_1} C
inst✝¹ : Preadditive C
F G : CochainComplex C ℤ
φ : F ⟶ G
inst✝ : HasHomotopyCofiber φ
j : ℤ
A : C
f : (mappingCone φ).X j ⟶ A
i : ℤ
hij : j + 1 = i
⊢ f = (↑(fst φ)).v j i hij ≫ (inl φ).v i j ⋯ ≫ f + (snd φ).v j j ⋯ ≫ (inr φ).f j ≫ f

Tactic:
apply ext_from φ i j hij <;> simp

Result:
no goals

Proof state:
C : Type u_1
inst✝² : Category.{u_3, u_1} C
inst✝¹ : Preadditive C
F G : CochainComplex C ℤ
φ : F ⟶ G
inst✝ : HasHomotopyCofiber φ
j : ℤ
A : C
f : (mappingCone φ).X j ⟶ A
i : ℤ
hij : j + 1 = i
⊢ i + -1 = j

Tactic:
omega

Result:
no goals