harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/MeasureTheory/Measure/AEMeasurable.lean
theorem _root_.aemeasurable_union_iff {s t : Set α} :
    AEMeasurable f (μ.restrict (s ∪ t)) ↔
      AEMeasurable f (μ.restrict s) ∧ AEMeasurable f (μ.restrict t)

Proof state:
α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
inst✝ : MeasurableSpace β
f : α → β
μ : Measure α
s t : Set α
⊢ AEMeasurable f (μ.restrict (s ∪ t)) ↔ AEMeasurable f (μ.restrict s) ∧ AEMeasurable f (μ.restrict t)

Tactic:
simp only [union_eq_iUnion, aemeasurable_iUnion_iff, Bool.forall_bool, cond, and_comm]

Result:
no goals
-- Mathlib/AlgebraicGeometry/EllipticCurve/NormalForms.lean
theorem b₄_of_isCharNeTwoNF : W.b₄ = 2 * W.a₄

Proof state:
R : Type u_1
inst✝¹ : CommRing R
W : WeierstrassCurve R
inst✝ : W.IsCharNeTwoNF
⊢ W.b₄ = 2 * W.a₄

Tactic:
rw [b₄, a₃_of_isCharNeTwoNF]

Result:
R : Type u_1
inst✝¹ : CommRing R
W : WeierstrassCurve R
inst✝ : W.IsCharNeTwoNF
⊢ 2 * W.a₄ + W.a₁ * 0 = 2 * W.a₄

Proof state:
R : Type u_1
inst✝¹ : CommRing R
W : WeierstrassCurve R
inst✝ : W.IsCharNeTwoNF
⊢ 2 * W.a₄ + W.a₁ * 0 = 2 * W.a₄

Tactic:
ring1

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/CompareExp.lean
theorem isLittleO_zpow_mul_exp {b₁ b₂ : ℝ} (hl : IsExpCmpFilter l) (hb : b₁ < b₂) (m n : ℤ) :
    (fun z => z ^ m * exp (b₁ * z)) =o[l] fun z => z ^ n * exp (b₂ * z)

Proof state:
l : Filter ℂ
b₁ b₂ : ℝ
hl : IsExpCmpFilter l
hb : b₁ < b₂
m n : ℤ
⊢ (fun z => z ^ m * cexp (↑b₁ * z)) =o[l] fun z => z ^ n * cexp (↑b₂ * z)

Tactic:
simpa only [cpow_intCast] using hl.isLittleO_cpow_mul_exp hb m n

Result:
no goals
-- Mathlib/Data/Seq/Computation.lean
theorem results_think_iff {s : Computation α} {a n} : Results (think s) a (n + 1) ↔ Results s a n :=
  ⟨fun h => by
    let ⟨n', r, e⟩ := of_results_think h
    injection e with h'; rwa [h'], results_think⟩

Proof state:
α : Type u
s : Computation α
a : α
n : ℕ
h : s.think.Results a (n + 1)
n' : ℕ
r : s.Results a n'
e : n + 1 = n' + 1
⊢ s.Results a n

Tactic:
injection e with h'

Result:
α : Type u
s : Computation α
a : α
n : ℕ
h : s.think.Results a (n + 1)
n' : ℕ
r : s.Results a n'
h' : n = n'
⊢ s.Results a n

Proof state:
α : Type u
s : Computation α
a : α
n : ℕ
h : s.think.Results a (n + 1)
⊢ s.Results a n

Tactic:
let ⟨n', r, e⟩ := of_results_think h

Result:
α : Type u
s : Computation α
a : α
n : ℕ
h : s.think.Results a (n + 1)
n' : ℕ
r : s.Results a n'
e : n + 1 = n' + 1
⊢ s.Results a n

Proof state:
α : Type u
s : Computation α
a : α
n : ℕ
h : s.think.Results a (n + 1)
n' : ℕ
r : s.Results a n'
h' : n = n'
⊢ s.Results a n

Tactic:
rwa [h']

Result:
no goals
-- Mathlib/GroupTheory/FreeGroup/IsFreeGroup.lean
@[simp] lemma repr_apply_coe (b : FreeGroupBasis ι G) (i : ι) : b.repr (b i) = FreeGroup.of i

Proof state:
ι : Type u_1
G : Type u_3
inst✝ : Group G
b : FreeGroupBasis ι G
i : ι
⊢ b.repr (b i) = FreeGroup.of i

Tactic:
change b.repr (b.repr.symm (FreeGroup.of i)) = FreeGroup.of i

Result:
ι : Type u_1
G : Type u_3
inst✝ : Group G
b : FreeGroupBasis ι G
i : ι
⊢ b.repr (b.repr.symm (FreeGroup.of i)) = FreeGroup.of i

Proof state:
ι : Type u_1
G : Type u_3
inst✝ : Group G
b : FreeGroupBasis ι G
i : ι
⊢ b.repr (b.repr.symm (FreeGroup.of i)) = FreeGroup.of i

Tactic:
simp

Result:
no goals
-- Mathlib/Analysis/BoxIntegral/Partition/Basic.lean
theorem biUnion_top : (π.biUnion fun _ => ⊤) = π

Proof state:
ι : Type u_1
I : Box ι
π : Prepartition I
⊢ (π.biUnion fun x => ⊤) = π

Tactic:
ext

Result:
case h
ι : Type u_1
I : Box ι
π : Prepartition I
J✝ : Box ι
⊢ (J✝ ∈ π.biUnion fun x => ⊤) ↔ J✝ ∈ π

Proof state:
case h
ι : Type u_1
I : Box ι
π : Prepartition I
J✝ : Box ι
⊢ (J✝ ∈ π.biUnion fun x => ⊤) ↔ J✝ ∈ π

Tactic:
simp

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Control/Lawful/Basic.lean
theorem LawfulMonad.map_map {m} [Monad m] [LawfulMonad m] {x : m α} :
    g <$> f <$> x = (fun a => g (f a)) <$> x

Proof state:
α α✝ a✝ : Type u_1
g : α✝ → a✝
f : α → α✝
m : Type u_1 → Type u_2
inst✝¹ : Monad m
inst✝ : LawfulMonad m
x : m α
⊢ g <$> f <$> x = (fun a => g (f a)) <$> x

Tactic:
simp only [Functor.map_map]

Result:
no goals
-- Mathlib/Analysis/Calculus/VectorField.lean
theorem _root_.Filter.EventuallyEq.lieBracketWithin_vectorField'
    (hV : V₁ =ᶠ[𝓝[s] x] V) (hW : W₁ =ᶠ[𝓝[s] x] W) (ht : t ⊆ s) :
    lieBracketWithin 𝕜 V₁ W₁ t =ᶠ[𝓝[s] x] lieBracketWithin 𝕜 V W t

Proof state:
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
V W V₁ W₁ : E → E
s t : Set E
x : E
hV : V₁ =ᶠ[𝓝[s] x] V
hW : W₁ =ᶠ[𝓝[s] x] W
ht : t ⊆ s
⊢ lieBracketWithin 𝕜 V₁ W₁ t =ᶠ[𝓝[s] x] lieBracketWithin 𝕜 V W t

Tactic:
filter_upwards [hV.fderivWithin' ht (𝕜 := 𝕜), hW.fderivWithin' ht (𝕜 := 𝕜), hV, hW]
  with x hV' hW' hV hW

Result:
case h
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
V W V₁ W₁ : E → E
s t : Set E
x✝ : E
hV✝ : V₁ =ᶠ[𝓝[s] x✝] V
hW✝ : W₁ =ᶠ[𝓝[s] x✝] W
ht : t ⊆ s
x : E
hV' : fderivWithin 𝕜 V₁ t x = fderivWithin 𝕜 V t x
hW' : fderivWithin 𝕜 W₁ t x = fderivWithin 𝕜 W t x
hV : V₁ x = V x
hW : W₁ x = W x
⊢ lieBracketWithin 𝕜 V₁ W₁ t x = lieBracketWithin 𝕜 V W t x

Proof state:
case h
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
V W V₁ W₁ : E → E
s t : Set E
x✝ : E
hV✝ : V₁ =ᶠ[𝓝[s] x✝] V
hW✝ : W₁ =ᶠ[𝓝[s] x✝] W
ht : t ⊆ s
x : E
hV' : fderivWithin 𝕜 V₁ t x = fderivWithin 𝕜 V t x
hW' : fderivWithin 𝕜 W₁ t x = fderivWithin 𝕜 W t x
hV : V₁ x = V x
hW : W₁ x = W x
⊢ lieBracketWithin 𝕜 V₁ W₁ t x = lieBracketWithin 𝕜 V W t x

Tactic:
simp [lieBracketWithin, hV', hW', hV, hW]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Var.lean
theorem denote_blastVar (aig : AIG BVBit) (var : BVVar w) (assign : Assignment) :
    ∀ (idx : Nat) (hidx : idx < w),
        ⟦(blastVar aig var).aig, (blastVar aig var).vec.get idx hidx, assign.toAIGAssignment⟧
          =
        ((BVExpr.var (w := w) var.ident).eval assign).getLsbD idx

Proof state:
case a
w : Nat
aig : AIG BVBit
var : BVVar w
assign : Assignment
idx✝ : Nat
hidx✝ : idx✝ < w
⊢ 0 ≤ idx✝

Tactic:
omega

Result:
no goals

Proof state:
w : Nat
aig : AIG BVBit
var : BVVar w
assign : Assignment
idx✝ : Nat
hidx✝ : idx✝ < w
⊢ ⟦assign.toAIGAssignment, { aig := (blastVar aig var).aig, ref := (blastVar aig var).vec.get idx✝ hidx✝ }⟧ =
    (eval assign (Std.Tactic.BVDecide.BVExpr.var var.ident)).getLsbD idx✝

Tactic:
apply blastVar.go_denote_eq

Result:
case a
w : Nat
aig : AIG BVBit
var : BVVar w
assign : Assignment
idx✝ : Nat
hidx✝ : idx✝ < w
⊢ 0 ≤ idx✝

Proof state:
w : Nat
aig : AIG BVBit
var : BVVar w
assign : Assignment
⊢ ∀ (idx : Nat) (hidx : idx < w),
    ⟦assign.toAIGAssignment, { aig := (blastVar aig var).aig, ref := (blastVar aig var).vec.get idx hidx }⟧ =
      (eval assign (Std.Tactic.BVDecide.BVExpr.var var.ident)).getLsbD idx

Tactic:
intros

Result:
w : Nat
aig : AIG BVBit
var : BVVar w
assign : Assignment
idx✝ : Nat
hidx✝ : idx✝ < w
⊢ ⟦assign.toAIGAssignment, { aig := (blastVar aig var).aig, ref := (blastVar aig var).vec.get idx✝ hidx✝ }⟧ =
    (eval assign (Std.Tactic.BVDecide.BVExpr.var var.ident)).getLsbD idx✝
-- Mathlib/CategoryTheory/Triangulated/Opposite/Functor.lean
@[reassoc]
lemma op_commShiftIso_hom_app (X : Cᵒᵖ) (n m : ℤ) (h : n + m = 0):
    (F.op.commShiftIso n).hom.app X =
      (F.map ((shiftFunctorOpIso C n m h).hom.app X).unop).op ≫
        ((F.commShiftIso m).inv.app X.unop).op ≫
        (shiftFunctorOpIso D n m h).inv.app (op (F.obj X.unop))

Proof state:
C : Type u_1
D : Type u_2
inst✝⁴ : Category.{u_4, u_1} C
inst✝³ : Category.{u_3, u_2} D
inst✝² : HasShift C ℤ
inst✝¹ : HasShift D ℤ
F : C ⥤ D
inst✝ : F.CommShift ℤ
X : Cᵒᵖ
n : ℤ
h : n + -n = 0
⊢ (F.op.commShiftIso n).hom.app X =
    (F.map ((shiftFunctorOpIso C n (-n) h).hom.app X).unop).op ≫
      ((F.commShiftIso (-n)).inv.app (unop X)).op ≫ (shiftFunctorOpIso D n (-n) h).inv.app (op (F.obj (unop X)))

Tactic:
rfl

Result:
no goals

Proof state:
C : Type u_1
D : Type u_2
inst✝⁴ : Category.{u_4, u_1} C
inst✝³ : Category.{u_3, u_2} D
inst✝² : HasShift C ℤ
inst✝¹ : HasShift D ℤ
F : C ⥤ D
inst✝ : F.CommShift ℤ
X : Cᵒᵖ
n m : ℤ
h : n + m = 0
⊢ m = -n

Tactic:
omega

Result:
no goals

Proof state:
C : Type u_1
D : Type u_2
inst✝⁴ : Category.{u_4, u_1} C
inst✝³ : Category.{u_3, u_2} D
inst✝² : HasShift C ℤ
inst✝¹ : HasShift D ℤ
F : C ⥤ D
inst✝ : F.CommShift ℤ
X : Cᵒᵖ
n m : ℤ
h : n + m = 0
⊢ (F.op.commShiftIso n).hom.app X =
    (F.map ((shiftFunctorOpIso C n m h).hom.app X).unop).op ≫
      ((F.commShiftIso m).inv.app (unop X)).op ≫ (shiftFunctorOpIso D n m h).inv.app (op (F.obj (unop X)))

Tactic:
obtain rfl : m = -n := by omega

Result:
C : Type u_1
D : Type u_2
inst✝⁴ : Category.{u_4, u_1} C
inst✝³ : Category.{u_3, u_2} D
inst✝² : HasShift C ℤ
inst✝¹ : HasShift D ℤ
F : C ⥤ D
inst✝ : F.CommShift ℤ
X : Cᵒᵖ
n : ℤ
h : n + -n = 0
⊢ (F.op.commShiftIso n).hom.app X =
    (F.map ((shiftFunctorOpIso C n (-n) h).hom.app X).unop).op ≫
      ((F.commShiftIso (-n)).inv.app (unop X)).op ≫ (shiftFunctorOpIso D n (-n) h).inv.app (op (F.obj (unop X)))
-- Mathlib/MeasureTheory/Integral/Average.lean
theorem exists_le_lintegral (hf : AEMeasurable f μ) : ∃ x, f x ≤ ∫⁻ a, f a ∂μ

Proof state:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
inst✝ : IsProbabilityMeasure μ
hf : AEMeasurable f μ
⊢ ∃ x, f x ≤ ∫⁻ (a : α), f a ∂μ

Tactic:
simpa only [laverage_eq_lintegral] using exists_le_laverage (IsProbabilityMeasure.ne_zero μ) hf

Result:
no goals
-- Mathlib/NumberTheory/LSeries/HurwitzZetaOdd.lean
theorem sinZeta_neg_two_mul_nat_sub_one (a : UnitAddCircle) (n : ℕ) :
    sinZeta a (-2 * n - 1) = 0

Proof state:
a : UnitAddCircle
n : ℕ
⊢ sinZeta a (-2 * ↑n - 1) = 0

Tactic:
rw [sinZeta, Gammaℝ_eq_zero_iff.mpr ⟨n, by rw [neg_mul, sub_add_cancel]⟩, div_zero]

Result:
no goals

Proof state:
a : UnitAddCircle
n : ℕ
⊢ -2 * ↑n - 1 + 1 = -(2 * ↑n)

Tactic:
rw [neg_mul, sub_add_cancel]

Result:
no goals
-- Mathlib/GroupTheory/SpecificGroups/ZGroup.lean
theorem of_squarefree (hG : Squarefree (Nat.card G)) : IsZGroup G

Proof state:
case intro
G : Type u_1
inst✝ : Group G
hG : Squarefree (Nat.card G)
this✝ : Finite G
p : ℕ
hp : Nat.Prime p
P : Sylow p G
this : Fact (Nat.Prime p)
k : ℕ
hk : Nat.card ↥↑P = p ^ k
⊢ IsCyclic ↥↑P

Tactic:
exact isCyclic_of_card_dvd_prime ((hk ▸ hG.pow_dvd_of_pow_dvd) P.card_subgroup_dvd_card)

Result:
no goals

Proof state:
G : Type u_1
inst✝ : Group G
hG : Squarefree (Nat.card G)
this : Finite G
p : ℕ
hp : Nat.Prime p
P : Sylow p G
⊢ IsCyclic ↥↑P

Tactic:
have := Fact.mk hp

Result:
G : Type u_1
inst✝ : Group G
hG : Squarefree (Nat.card G)
this✝ : Finite G
p : ℕ
hp : Nat.Prime p
P : Sylow p G
this : Fact (Nat.Prime p)
⊢ IsCyclic ↥↑P

Proof state:
G : Type u_1
inst✝ : Group G
hG : Squarefree (Nat.card G)
this : Finite G
⊢ IsZGroup G

Tactic:
refine ⟨fun p hp P ↦ ?_⟩

Result:
G : Type u_1
inst✝ : Group G
hG : Squarefree (Nat.card G)
this : Finite G
p : ℕ
hp : Nat.Prime p
P : Sylow p G
⊢ IsCyclic ↥↑P

Proof state:
G : Type u_1
inst✝ : Group G
hG : Squarefree (Nat.card G)
⊢ IsZGroup G

Tactic:
have : Finite G := Nat.finite_of_card_ne_zero hG.ne_zero

Result:
G : Type u_1
inst✝ : Group G
hG : Squarefree (Nat.card G)
this : Finite G
⊢ IsZGroup G

Proof state:
G : Type u_1
inst✝ : Group G
hG : Squarefree (Nat.card G)
this✝ : Finite G
p : ℕ
hp : Nat.Prime p
P : Sylow p G
this : Fact (Nat.Prime p)
⊢ IsCyclic ↥↑P

Tactic:
obtain ⟨k, hk⟩ := P.2.exists_card_eq

Result:
case intro
G : Type u_1
inst✝ : Group G
hG : Squarefree (Nat.card G)
this✝ : Finite G
p : ℕ
hp : Nat.Prime p
P : Sylow p G
this : Fact (Nat.Prime p)
k : ℕ
hk : Nat.card ↥↑P = p ^ k
⊢ IsCyclic ↥↑P
-- Mathlib/Algebra/Order/Interval/Multiset.lean
lemma map_add_left_Ioo (a b c : α) : (Ioo a b).map (c + ·) = Ioo (c + a) (c + b)

Proof state:
α : Type u_1
inst✝² : OrderedCancelAddCommMonoid α
inst✝¹ : ExistsAddOfLE α
inst✝ : LocallyFiniteOrder α
a b c : α
⊢ map (fun x => c + x) (Ioo a b) = Ioo (c + a) (c + b)

Tactic:
rw [Ioo, Ioo, ← Finset.image_add_left_Ioo, Finset.image_val,
((Finset.nodup _).map <| add_right_injective c).dedup]

Result:
no goals

Proof state:
α : Type u_1
inst✝² : OrderedCancelAddCommMonoid α
inst✝¹ : ExistsAddOfLE α
inst✝ : LocallyFiniteOrder α
a b c : α
⊢ map (fun x => c + x) (Ioo a b) = Ioo (c + a) (c + b)

Tactic:
classical rw [Ioo, Ioo, ← Finset.image_add_left_Ioo, Finset.image_val,
    ((Finset.nodup _).map <| add_right_injective c).dedup]

Result:
no goals
-- Mathlib/RingTheory/MvPolynomial/Symmetric/Defs.lean
theorem support_esymm' [DecidableEq σ] [Nontrivial R] (n : ℕ) : (esymm σ R n).support =
    (powersetCard n (univ : Finset σ)).biUnion fun t => {∑ i ∈ t, Finsupp.single i 1}

Proof state:
σ : Type u_5
R : Type u_6
inst✝³ : CommSemiring R
inst✝² : Fintype σ
inst✝¹ : DecidableEq σ
inst✝ : Nontrivial R
n : ℕ
⊢ ((powersetCard n univ).biUnion fun t => (Finsupp.single (∑ i ∈ t, Finsupp.single i 1) 1).support) =
    (powersetCard n univ).biUnion fun t => {∑ i ∈ t, Finsupp.single i 1}

Tactic:
congr

Result:
case e_t
σ : Type u_5
R : Type u_6
inst✝³ : CommSemiring R
inst✝² : Fintype σ
inst✝¹ : DecidableEq σ
inst✝ : Nontrivial R
n : ℕ
⊢ (fun t => (Finsupp.single (∑ i ∈ t, Finsupp.single i 1) 1).support) = fun t => {∑ i ∈ t, Finsupp.single i 1}

Proof state:
case e_t
σ : Type u_5
R : Type u_6
inst✝³ : CommSemiring R
inst✝² : Fintype σ
inst✝¹ : DecidableEq σ
inst✝ : Nontrivial R
n : ℕ
⊢ (fun t => (Finsupp.single (∑ i ∈ t, Finsupp.single i 1) 1).support) = fun t => {∑ i ∈ t, Finsupp.single i 1}

Tactic:
funext

Result:
case e_t.h
σ : Type u_5
R : Type u_6
inst✝³ : CommSemiring R
inst✝² : Fintype σ
inst✝¹ : DecidableEq σ
inst✝ : Nontrivial R
n : ℕ
x✝ : Finset σ
⊢ (Finsupp.single (∑ i ∈ x✝, Finsupp.single i 1) 1).support = {∑ i ∈ x✝, Finsupp.single i 1}

Proof state:
case e_t.h
σ : Type u_5
R : Type u_6
inst✝³ : CommSemiring R
inst✝² : Fintype σ
inst✝¹ : DecidableEq σ
inst✝ : Nontrivial R
n : ℕ
x✝ : Finset σ
⊢ (Finsupp.single (∑ i ∈ x✝, Finsupp.single i 1) 1).support = {∑ i ∈ x✝, Finsupp.single i 1}

Tactic:
exact Finsupp.support_single_ne_zero _ one_ne_zero

Result:
no goals

Proof state:
σ : Type u_5
R : Type u_6
inst✝³ : CommSemiring R
inst✝² : Fintype σ
inst✝¹ : DecidableEq σ
inst✝ : Nontrivial R
n : ℕ
⊢ (esymm σ R n).support = (powersetCard n univ).biUnion fun t => {∑ i ∈ t, Finsupp.single i 1}

Tactic:
rw [support_esymm'']

Result:
σ : Type u_5
R : Type u_6
inst✝³ : CommSemiring R
inst✝² : Fintype σ
inst✝¹ : DecidableEq σ
inst✝ : Nontrivial R
n : ℕ
⊢ ((powersetCard n univ).biUnion fun t => (Finsupp.single (∑ i ∈ t, Finsupp.single i 1) 1).support) =
    (powersetCard n univ).biUnion fun t => {∑ i ∈ t, Finsupp.single i 1}
-- Mathlib/Combinatorics/SimpleGraph/Maps.lean
lemma mapSpanningSubgraphs_injective {G G' : SimpleGraph V} (h : G ≤ G') :
    Injective (mapSpanningSubgraphs h) :=
  fun v w hvw ↦ by simpa [mapSpanningSubgraphs_apply] using hvw

Proof state:
V : Type u_1
G G' : SimpleGraph V
h : G ≤ G'
v w : V
hvw : (mapSpanningSubgraphs h) v = (mapSpanningSubgraphs h) w
⊢ v = w

Tactic:
simpa [mapSpanningSubgraphs_apply] using hvw

Result:
no goals
-- Mathlib/Algebra/Group/End.lean
theorem ofSubtype_injective : Function.Injective (ofSubtype : Perm (Subtype p) → Perm α)

Proof state:
α : Type u_4
p : α → Prop
inst✝ : DecidablePred p
x y : Perm (Subtype p)
a : Subtype p
h : (ofSubtype x) ↑a = (ofSubtype y) ↑a
⊢ x a = y a

Tactic:
rwa [ofSubtype_apply_coe, ofSubtype_apply_coe, SetCoe.ext_iff] at h

Result:
no goals

Proof state:
α : Type u_4
p : α → Prop
inst✝ : DecidablePred p
x y : Perm (Subtype p)
h : ∀ (x_1 : α), (ofSubtype x) x_1 = (ofSubtype y) x_1
⊢ ∀ (x_1 : Subtype p), x x_1 = y x_1

Tactic:
intro a

Result:
α : Type u_4
p : α → Prop
inst✝ : DecidablePred p
x y : Perm (Subtype p)
h : ∀ (x_1 : α), (ofSubtype x) x_1 = (ofSubtype y) x_1
a : Subtype p
⊢ x a = y a

Proof state:
α : Type u_4
p : α → Prop
inst✝ : DecidablePred p
x y : Perm (Subtype p)
h : ∀ (x_1 : α), (ofSubtype x) x_1 = (ofSubtype y) x_1
a : Subtype p
⊢ x a = y a

Tactic:
specialize h a

Result:
α : Type u_4
p : α → Prop
inst✝ : DecidablePred p
x y : Perm (Subtype p)
a : Subtype p
h : (ofSubtype x) ↑a = (ofSubtype y) ↑a
⊢ x a = y a

Proof state:
α : Type u_4
p : α → Prop
inst✝ : DecidablePred p
x y : Perm (Subtype p)
h : ofSubtype x = ofSubtype y
⊢ x = y

Tactic:
rw [Perm.ext_iff] at h ⊢

Result:
α : Type u_4
p : α → Prop
inst✝ : DecidablePred p
x y : Perm (Subtype p)
h : ∀ (x_1 : α), (ofSubtype x) x_1 = (ofSubtype y) x_1
⊢ ∀ (x_1 : Subtype p), x x_1 = y x_1

Proof state:
α : Type u_4
p : α → Prop
inst✝ : DecidablePred p
⊢ Function.Injective ⇑ofSubtype

Tactic:
intro x y h

Result:
α : Type u_4
p : α → Prop
inst✝ : DecidablePred p
x y : Perm (Subtype p)
h : ofSubtype x = ofSubtype y
⊢ x = y
-- Mathlib/SetTheory/Cardinal/Finite.lean
lemma card_le_card_of_injective {α : Type u} {β : Type v} [Finite β] (f : α → β)
    (hf : Injective f) : Nat.card α ≤ Nat.card β

Proof state:
α : Type u
β : Type v
inst✝ : Finite β
f : α → β
hf : Injective f
⊢ lift.{u, v} #β < ℵ₀

Tactic:
simp [lt_aleph0_of_finite]

Result:
no goals

Proof state:
α : Type u
β : Type v
inst✝ : Finite β
f : α → β
hf : Injective f
⊢ Nat.card α ≤ Nat.card β

Tactic:
simpa using toNat_le_toNat (lift_mk_le_lift_mk_of_injective hf) (by simp [lt_aleph0_of_finite])

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Circulant.lean
theorem cycleGraph_adj' {n : ℕ} {u v : Fin n} :
    (cycleGraph n).Adj u v ↔ (u - v).val = 1 ∨ (v - u).val = 1

Proof state:
n : ℕ
u v : Fin n
⊢ (cycleGraph n).Adj u v ↔ ↑(u - v) = 1 ∨ ↑(v - u) = 1

Tactic:
match n with
| 0 => exact u.elim0
| 1 => simp [cycleGraph_one_adj]
| n + 2 => simp [cycleGraph_adj, Fin.ext_iff]

Result:
no goals

Proof state:
n✝ n : ℕ
u v : Fin (n + 2)
⊢ (cycleGraph (n + 2)).Adj u v ↔ ↑(u - v) = 1 ∨ ↑(v - u) = 1

Tactic:
simp [cycleGraph_adj, Fin.ext_iff]

Result:
no goals

Proof state:
n : ℕ
u v : Fin 0
⊢ (cycleGraph 0).Adj u v ↔ ↑(u - v) = 1 ∨ ↑(v - u) = 1

Tactic:
exact u.elim0

Result:
no goals

Proof state:
n : ℕ
u v : Fin 1
⊢ (cycleGraph 1).Adj u v ↔ ↑(u - v) = 1 ∨ ↑(v - u) = 1

Tactic:
simp [cycleGraph_one_adj]

Result:
no goals
-- Mathlib/Data/List/Infix.lean
theorem inits_append : ∀ s t : List α, inits (s ++ t) = s.inits ++ t.inits.tail.map fun l => s ++ l
  | [], [] => by simp
  | [], a :: t => by simp
  | a :: s, t => by simp [inits_append s t, Function.comp_def]

Proof state:
α : Type u_1
a : α
t : List α
⊢ ([] ++ a :: t).inits = [].inits ++ map (fun l => [] ++ l) (a :: t).inits.tail

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
⊢ ([] ++ []).inits = [].inits ++ map (fun l => [] ++ l) [].inits.tail

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
a : α
s t : List α
⊢ (a :: s ++ t).inits = (a :: s).inits ++ map (fun l => a :: s ++ l) t.inits.tail

Tactic:
simp [inits_append s t, Function.comp_def]

Result:
no goals
-- Mathlib/Algebra/Pointwise/Stabilizer.lean
@[to_additive]
lemma mem_stabilizer_set' {s : Set α} (hs : s.Finite) :
    a ∈ stabilizer G s ↔ ∀ ⦃b⦄, b ∈ s → a • b ∈ s

Proof state:
case intro
G : Type u_1
α : Type u_3
inst✝¹ : Group G
inst✝ : MulAction G α
a : G
s : Finset α
⊢ a ∈ stabilizer G ↑s ↔ ∀ ⦃b : α⦄, b ∈ ↑s → a • b ∈ ↑s

Tactic:
classical simp [-mem_stabilizer_iff, mem_stabilizer_finset']

Result:
no goals

Proof state:
case intro
G : Type u_1
α : Type u_3
inst✝¹ : Group G
inst✝ : MulAction G α
a : G
s : Finset α
⊢ a ∈ stabilizer G ↑s ↔ ∀ ⦃b : α⦄, b ∈ ↑s → a • b ∈ ↑s

Tactic:
simp [-mem_stabilizer_iff, mem_stabilizer_finset']

Result:
no goals

Proof state:
G : Type u_1
α : Type u_3
inst✝¹ : Group G
inst✝ : MulAction G α
a : G
s : Set α
hs : s.Finite
⊢ a ∈ stabilizer G s ↔ ∀ ⦃b : α⦄, b ∈ s → a • b ∈ s

Tactic:
lift s to Finset α using hs

Result:
case intro
G : Type u_1
α : Type u_3
inst✝¹ : Group G
inst✝ : MulAction G α
a : G
s : Finset α
⊢ a ∈ stabilizer G ↑s ↔ ∀ ⦃b : α⦄, b ∈ ↑s → a • b ∈ ↑s
-- Mathlib/Data/Real/Irrational.lean
theorem irrational_sqrt_natCast_iff {n : ℕ} : Irrational (√n) ↔ ¬IsSquare n

Proof state:
n : ℕ
⊢ Irrational √↑n ↔ ¬IsSquare n

Tactic:
rw [← Rat.isSquare_natCast_iff, ← irrational_sqrt_ratCast_iff_of_nonneg n.cast_nonneg,
  Rat.cast_natCast]

Result:
no goals
-- Mathlib/Algebra/Polynomial/Div.lean
/-- Division by a monic polynomial doesn't change the leading coefficient. -/
lemma leadingCoeff_divByMonic_of_monic (hmonic : q.Monic)
    (hdegree : q.degree ≤ p.degree) : (p /ₘ q).leadingCoeff = p.leadingCoeff

Proof state:
R : Type u
inst✝ : CommRing R
p q : R[X]
hmonic : q.Monic
hdegree : q.degree ≤ p.degree
a✝ : Nontrivial R
h : q.leadingCoeff * (p /ₘ q).leadingCoeff ≠ 0
⊢ (p /ₘ q).leadingCoeff = (p %ₘ q + q * (p /ₘ q)).leadingCoeff

Tactic:
rw [leadingCoeff_add_of_degree_lt, leadingCoeff_monic_mul hmonic]

Result:
R : Type u
inst✝ : CommRing R
p q : R[X]
hmonic : q.Monic
hdegree : q.degree ≤ p.degree
a✝ : Nontrivial R
h : q.leadingCoeff * (p /ₘ q).leadingCoeff ≠ 0
⊢ (p %ₘ q).degree < (q * (p /ₘ q)).degree

Proof state:
R : Type u
inst✝ : CommRing R
p q : R[X]
hmonic : q.Monic
hdegree : q.degree ≤ p.degree
a✝ : Nontrivial R
⊢ (p /ₘ q).leadingCoeff = p.leadingCoeff

Tactic:
have h : q.leadingCoeff * (p /ₘ q).leadingCoeff ≠ 0 := by
  simpa [divByMonic_eq_zero_iff hmonic, hmonic.leadingCoeff,
    Nat.WithBot.one_le_iff_zero_lt] using hdegree

Result:
R : Type u
inst✝ : CommRing R
p q : R[X]
hmonic : q.Monic
hdegree : q.degree ≤ p.degree
a✝ : Nontrivial R
h : q.leadingCoeff * (p /ₘ q).leadingCoeff ≠ 0
⊢ (p /ₘ q).leadingCoeff = p.leadingCoeff

Proof state:
R : Type u
inst✝ : CommRing R
p q : R[X]
hmonic : q.Monic
hdegree : q.degree ≤ p.degree
a✝ : Nontrivial R
h : q.leadingCoeff * (p /ₘ q).leadingCoeff ≠ 0
⊢ (p %ₘ q).degree < p.degree

Tactic:
exact (degree_modByMonic_lt p hmonic).trans_le hdegree

Result:
no goals

Proof state:
R : Type u
inst✝ : CommRing R
p q : R[X]
hmonic : q.Monic
hdegree : q.degree ≤ p.degree
a✝ : Nontrivial R
h : q.leadingCoeff * (p /ₘ q).leadingCoeff ≠ 0
⊢ (p %ₘ q).degree < (q * (p /ₘ q)).degree

Tactic:
rw [degree_mul' h, degree_add_divByMonic hmonic hdegree]

Result:
R : Type u
inst✝ : CommRing R
p q : R[X]
hmonic : q.Monic
hdegree : q.degree ≤ p.degree
a✝ : Nontrivial R
h : q.leadingCoeff * (p /ₘ q).leadingCoeff ≠ 0
⊢ (p %ₘ q).degree < p.degree

Proof state:
R : Type u
inst✝ : CommRing R
p q : R[X]
hmonic : q.Monic
hdegree : q.degree ≤ p.degree
⊢ (p /ₘ q).leadingCoeff = p.leadingCoeff

Tactic:
nontriviality

Result:
R : Type u
inst✝ : CommRing R
p q : R[X]
hmonic : q.Monic
hdegree : q.degree ≤ p.degree
a✝ : Nontrivial R
⊢ (p /ₘ q).leadingCoeff = p.leadingCoeff

Proof state:
R : Type u
inst✝ : CommRing R
p q : R[X]
hmonic : q.Monic
hdegree : q.degree ≤ p.degree
a✝ : Nontrivial R
⊢ q.leadingCoeff * (p /ₘ q).leadingCoeff ≠ 0

Tactic:
simpa [divByMonic_eq_zero_iff hmonic, hmonic.leadingCoeff,
  Nat.WithBot.one_le_iff_zero_lt] using hdegree

Result:
no goals

Proof state:
R : Type u
inst✝ : CommRing R
p q : R[X]
hmonic : q.Monic
hdegree : q.degree ≤ p.degree
a✝ : Nontrivial R
h : q.leadingCoeff * (p /ₘ q).leadingCoeff ≠ 0
⊢ (p /ₘ q).leadingCoeff = p.leadingCoeff

Tactic:
nth_rw 2 [← modByMonic_add_div p hmonic]

Result:
R : Type u
inst✝ : CommRing R
p q : R[X]
hmonic : q.Monic
hdegree : q.degree ≤ p.degree
a✝ : Nontrivial R
h : q.leadingCoeff * (p /ₘ q).leadingCoeff ≠ 0
⊢ (p /ₘ q).leadingCoeff = (p %ₘ q + q * (p /ₘ q)).leadingCoeff