harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Combinatorics/SimpleGraph/Connectivity/WalkDecomp.lean
theorem support_takeUntil_subset {u v w : V} (p : G.Walk v w) (h : u ∈ p.support) :
    (p.takeUntil u h).support ⊆ p.support := fun x hx => by
  rw [← take_spec p h, mem_support_append_iff]
  exact Or.inl hx

Proof state:
V : Type u
G : SimpleGraph V
inst✝ : DecidableEq V
u v w : V
p : G.Walk v w
h : u ∈ p.support
x : V
hx : x ∈ (p.takeUntil u h).support
⊢ x ∈ p.support

Tactic:
rw [← take_spec p h, mem_support_append_iff]

Result:
V : Type u
G : SimpleGraph V
inst✝ : DecidableEq V
u v w : V
p : G.Walk v w
h : u ∈ p.support
x : V
hx : x ∈ (p.takeUntil u h).support
⊢ x ∈ (p.takeUntil u h).support ∨ x ∈ (p.dropUntil u h).support

Proof state:
V : Type u
G : SimpleGraph V
inst✝ : DecidableEq V
u v w : V
p : G.Walk v w
h : u ∈ p.support
x : V
hx : x ∈ (p.takeUntil u h).support
⊢ x ∈ (p.takeUntil u h).support ∨ x ∈ (p.dropUntil u h).support

Tactic:
exact Or.inl hx

Result:
no goals
-- Mathlib/MeasureTheory/Measure/Tilted.lean
lemma tilted_zero (μ : Measure α) [IsProbabilityMeasure μ] : μ.tilted 0 = μ

Proof state:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
inst✝ : IsProbabilityMeasure μ
⊢ μ.tilted 0 = μ

Tactic:
simp

Result:
no goals
-- Mathlib/LinearAlgebra/CliffordAlgebra/Fold.lean
theorem foldr'Aux_foldr'Aux (f : M →ₗ[R] CliffordAlgebra Q × N →ₗ[R] N)
    (hf : ∀ m x fx, f m (ι Q m * x, f m (x, fx)) = Q m • fx) (v : M) (x_fx) :
    foldr'Aux Q f v (foldr'Aux Q f v x_fx) = Q v • x_fx

Proof state:
case mk
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup N
inst✝¹ : Module R M
inst✝ : Module R N
Q : QuadraticForm R M
f : M →ₗ[R] CliffordAlgebra Q × N →ₗ[R] N
hf : ∀ (m : M) (x : CliffordAlgebra Q) (fx : N), (f m) ((ι Q) m * x, (f m) (x, fx)) = Q m • fx
v : M
x : CliffordAlgebra Q
fx : N
⊢ ((foldr'Aux Q f) v) (((foldr'Aux Q f) v) (x, fx)) = Q v • (x, fx)

Tactic:
simp only [foldr'Aux_apply_apply]

Result:
case mk
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup N
inst✝¹ : Module R M
inst✝ : Module R N
Q : QuadraticForm R M
f : M →ₗ[R] CliffordAlgebra Q × N →ₗ[R] N
hf : ∀ (m : M) (x : CliffordAlgebra Q) (fx : N), (f m) ((ι Q) m * x, (f m) (x, fx)) = Q m • fx
v : M
x : CliffordAlgebra Q
fx : N
⊢ ((ι Q) v * ((ι Q) v * x), (f v) ((ι Q) v * x, (f v) (x, fx))) = Q v • (x, fx)

Proof state:
case mk
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup N
inst✝¹ : Module R M
inst✝ : Module R N
Q : QuadraticForm R M
f : M →ₗ[R] CliffordAlgebra Q × N →ₗ[R] N
hf : ∀ (m : M) (x : CliffordAlgebra Q) (fx : N), (f m) ((ι Q) m * x, (f m) (x, fx)) = Q m • fx
v : M
x : CliffordAlgebra Q
fx : N
⊢ ((ι Q) v * ((ι Q) v * x), (f v) ((ι Q) v * x, (f v) (x, fx))) = Q v • (x, fx)

Tactic:
rw [← mul_assoc, ι_sq_scalar, ← Algebra.smul_def, hf, Prod.smul_mk]

Result:
no goals

Proof state:
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup N
inst✝¹ : Module R M
inst✝ : Module R N
Q : QuadraticForm R M
f : M →ₗ[R] CliffordAlgebra Q × N →ₗ[R] N
hf : ∀ (m : M) (x : CliffordAlgebra Q) (fx : N), (f m) ((ι Q) m * x, (f m) (x, fx)) = Q m • fx
v : M
x_fx : CliffordAlgebra Q × N
⊢ ((foldr'Aux Q f) v) (((foldr'Aux Q f) v) x_fx) = Q v • x_fx

Tactic:
obtain ⟨x, fx⟩ := x_fx

Result:
case mk
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup N
inst✝¹ : Module R M
inst✝ : Module R N
Q : QuadraticForm R M
f : M →ₗ[R] CliffordAlgebra Q × N →ₗ[R] N
hf : ∀ (m : M) (x : CliffordAlgebra Q) (fx : N), (f m) ((ι Q) m * x, (f m) (x, fx)) = Q m • fx
v : M
x : CliffordAlgebra Q
fx : N
⊢ ((foldr'Aux Q f) v) (((foldr'Aux Q f) v) (x, fx)) = Q v • (x, fx)
-- Mathlib/Algebra/Group/Units/Defs.lean
theorem inv_mul_eq_iff_eq_mul {b c : α} : ↑a⁻¹ * b = c ↔ b = a * c :=
  ⟨fun h => by rw [← h, mul_inv_cancel_left], fun h => by rw [h, inv_mul_cancel_left]⟩

Proof state:
α : Type u
inst✝ : Monoid α
a : αˣ
b c : α
h : b = ↑a * c
⊢ ↑a⁻¹ * b = c

Tactic:
rw [h, inv_mul_cancel_left]

Result:
no goals

Proof state:
α : Type u
inst✝ : Monoid α
a : αˣ
b c : α
h : ↑a⁻¹ * b = c
⊢ b = ↑a * c

Tactic:
rw [← h, mul_inv_cancel_left]

Result:
no goals
-- Mathlib/Order/Atoms.lean
theorem IsSimpleOrder.bot_ne_top [LE α] [BoundedOrder α] [IsSimpleOrder α] : (⊥ : α) ≠ (⊤ : α)

Proof state:
case intro.intro.inr.inr
α : Type u_2
inst✝² : LE α
inst✝¹ : BoundedOrder α
inst✝ : IsSimpleOrder α
h : ⊤ ≠ ⊤
⊢ ⊥ ≠ ⊤

Tactic:
simpa

Result:
no goals

Proof state:
α : Type u_2
inst✝² : LE α
inst✝¹ : BoundedOrder α
inst✝ : IsSimpleOrder α
⊢ ⊥ ≠ ⊤

Tactic:
obtain ⟨a, b, h⟩ := exists_pair_ne α

Result:
case intro.intro
α : Type u_2
inst✝² : LE α
inst✝¹ : BoundedOrder α
inst✝ : IsSimpleOrder α
a b : α
h : a ≠ b
⊢ ⊥ ≠ ⊤

Proof state:
case intro.intro
α : Type u_2
inst✝² : LE α
inst✝¹ : BoundedOrder α
inst✝ : IsSimpleOrder α
a b : α
h : a ≠ b
⊢ ⊥ ≠ ⊤

Tactic:
rcases eq_bot_or_eq_top a with (rfl | rfl) <;> rcases eq_bot_or_eq_top b with (rfl | rfl) <;>
  first |simpa|simpa using h.symm

Result:
no goals

Proof state:
case intro.intro.inr.inr
α : Type u_2
inst✝² : LE α
inst✝¹ : BoundedOrder α
inst✝ : IsSimpleOrder α
h : ⊤ ≠ ⊤
⊢ ⊥ ≠ ⊤

Tactic:
simpa using h.symm

Result:
no goals
-- Mathlib/Algebra/TrivSqZeroExt.lean
theorem inv_one : (1 : tsze R M)⁻¹ = (1 : tsze R M)

Proof state:
R : Type u
M : Type v
inst✝³ : DivisionSemiring R
inst✝² : AddCommGroup M
inst✝¹ : Module Rᵐᵒᵖ M
inst✝ : Module R M
⊢ 1⁻¹ = 1

Tactic:
rw [← inl_one, TrivSqZeroExt.inv_inl, inv_one]

Result:
no goals
-- Mathlib/Algebra/Homology/ExactSequence.lean
/-- If `S : ComposableArrows C (n + 2)` is such that the first two arrows form
an exact sequence and that the tail `S.δ₀` is exact, then `S` is also exact.
See `ShortComplex.SnakeInput.snake_lemma` in `Algebra.Homology.ShortComplex.SnakeLemma`
for a use of this lemma. -/
lemma exact_of_δ₀ {S : ComposableArrows C (n + 2)}
    (h : (mk₂ (S.map' 0 1) (S.map' 1 2)).Exact) (h₀ : S.δ₀.Exact) : S.Exact

Proof state:
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : HasZeroMorphisms C
n : ℕ
S : ComposableArrows C (n + 2)
h : (mk₂ (S.map' 0 1 ⋯ ⋯) (S.map' 1 2 ⋯ ⋯)).Exact
h₀ : S.δ₀.Exact
⊢ (mk₂ (S.map' 0 1 ⋯ ⋯) (S.map' 1 2 ⋯ ⋯)).Exact ∧ S.δ₀.Exact

Tactic:
constructor <;> assumption

Result:
no goals

Proof state:
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : HasZeroMorphisms C
n : ℕ
S : ComposableArrows C (n + 2)
h : (mk₂ (S.map' 0 1 ⋯ ⋯) (S.map' 1 2 ⋯ ⋯)).Exact
h₀ : S.δ₀.Exact
⊢ S.Exact

Tactic:
rw [exact_iff_δ₀]

Result:
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : HasZeroMorphisms C
n : ℕ
S : ComposableArrows C (n + 2)
h : (mk₂ (S.map' 0 1 ⋯ ⋯) (S.map' 1 2 ⋯ ⋯)).Exact
h₀ : S.δ₀.Exact
⊢ (mk₂ (S.map' 0 1 ⋯ ⋯) (S.map' 1 2 ⋯ ⋯)).Exact ∧ S.δ₀.Exact
-- Mathlib/Algebra/ContinuedFractions/Translations.lean
theorem zeroth_conv'_eq_h : g.convs' 0 = g.h

Proof state:
K : Type u_1
g : GenContFract K
inst✝ : DivisionRing K
⊢ g.convs' 0 = g.h

Tactic:
simp [convs']

Result:
no goals
-- Mathlib/Data/Nat/Factors.lean
theorem Prime.primeFactorsList_pow {p : ℕ} (hp : p.Prime) (n : ℕ) :
    (p ^ n).primeFactorsList = List.replicate n p

Proof state:
p : ℕ
hp : Prime p
n : ℕ
⊢ replicate n p ~ (p ^ n).primeFactorsList

Tactic:
apply Nat.primeFactorsList_unique (List.prod_replicate n p)

Result:
p : ℕ
hp : Prime p
n : ℕ
⊢ ∀ p_1 ∈ replicate n p, Prime p_1

Proof state:
p : ℕ
hp : Prime p
n : ℕ
⊢ ∀ p_1 ∈ replicate n p, Prime p_1

Tactic:
intro q hq

Result:
p : ℕ
hp : Prime p
n q : ℕ
hq : q ∈ replicate n p
⊢ Prime q

Proof state:
p : ℕ
hp : Prime p
n q : ℕ
hq : q ∈ replicate n p
⊢ Prime q

Tactic:
rwa [eq_of_mem_replicate hq]

Result:
no goals

Proof state:
p : ℕ
hp : Prime p
n : ℕ
⊢ (p ^ n).primeFactorsList = replicate n p

Tactic:
symm

Result:
p : ℕ
hp : Prime p
n : ℕ
⊢ replicate n p = (p ^ n).primeFactorsList

Proof state:
p : ℕ
hp : Prime p
n : ℕ
⊢ replicate n p = (p ^ n).primeFactorsList

Tactic:
rw [← List.replicate_perm]

Result:
p : ℕ
hp : Prime p
n : ℕ
⊢ replicate n p ~ (p ^ n).primeFactorsList
-- Mathlib/CategoryTheory/Localization/Predicate.lean
theorem of_iso {L₁ L₂ : C ⥤ D} (e : L₁ ≅ L₂) [L₁.IsLocalization W] : L₂.IsLocalization W

Proof state:
C : Type u_1
D : Type u_2
inst✝² : Category.{u_4, u_1} C
inst✝¹ : Category.{u_5, u_2} D
W : MorphismProperty C
L₁ L₂ : C ⥤ D
e : L₁ ≅ L₂
inst✝ : L₁.IsLocalization W
⊢ L₂.IsLocalization W

Tactic:
have h := Localization.inverts L₁ W

Result:
C : Type u_1
D : Type u_2
inst✝² : Category.{u_4, u_1} C
inst✝¹ : Category.{u_5, u_2} D
W : MorphismProperty C
L₁ L₂ : C ⥤ D
e : L₁ ≅ L₂
inst✝ : L₁.IsLocalization W
h : W.IsInvertedBy L₁
⊢ L₂.IsLocalization W

Proof state:
C : Type u_1
D : Type u_2
inst✝² : Category.{u_4, u_1} C
inst✝¹ : Category.{u_5, u_2} D
W : MorphismProperty C
L₁ L₂ : C ⥤ D
e : L₁ ≅ L₂
inst✝ : L₁.IsLocalization W
h : W.IsInvertedBy L₁
⊢ L₂.IsLocalization W

Tactic:
rw [MorphismProperty.IsInvertedBy.iff_of_iso W e] at h

Result:
C : Type u_1
D : Type u_2
inst✝² : Category.{u_4, u_1} C
inst✝¹ : Category.{u_5, u_2} D
W : MorphismProperty C
L₁ L₂ : C ⥤ D
e : L₁ ≅ L₂
inst✝ : L₁.IsLocalization W
h : W.IsInvertedBy L₂
⊢ L₂.IsLocalization W

Proof state:
C : Type u_1
D : Type u_2
inst✝² : Category.{u_4, u_1} C
inst✝¹ : Category.{u_5, u_2} D
W : MorphismProperty C
L₁ L₂ : C ⥤ D
e : L₁ ≅ L₂
inst✝ : L₁.IsLocalization W
h : W.IsInvertedBy L₂
F₁ : W.Localization ⥤ D := Construction.lift L₁ ⋯
⊢ L₂.IsLocalization W

Tactic:
let F₂ := Localization.Construction.lift L₂ h

Result:
C : Type u_1
D : Type u_2
inst✝² : Category.{u_4, u_1} C
inst✝¹ : Category.{u_5, u_2} D
W : MorphismProperty C
L₁ L₂ : C ⥤ D
e : L₁ ≅ L₂
inst✝ : L₁.IsLocalization W
h : W.IsInvertedBy L₂
F₁ : W.Localization ⥤ D := Construction.lift L₁ ⋯
F₂ : W.Localization ⥤ D := Construction.lift L₂ h
⊢ L₂.IsLocalization W

Proof state:
C : Type u_1
D : Type u_2
inst✝² : Category.{u_4, u_1} C
inst✝¹ : Category.{u_5, u_2} D
W : MorphismProperty C
L₁ L₂ : C ⥤ D
e : L₁ ≅ L₂
inst✝ : L₁.IsLocalization W
h : W.IsInvertedBy L₂
F₁ : W.Localization ⥤ D := Construction.lift L₁ ⋯
F₂ : W.Localization ⥤ D := Construction.lift L₂ h
⊢ L₂.IsLocalization W

Tactic:
exact
  { inverts := h
    isEquivalence := Functor.isEquivalence_of_iso (liftNatIso W.Q W L₁ L₂ F₁ F₂ e) }

Result:
no goals

Proof state:
C : Type u_1
D : Type u_2
inst✝² : Category.{u_4, u_1} C
inst✝¹ : Category.{u_5, u_2} D
W : MorphismProperty C
L₁ L₂ : C ⥤ D
e : L₁ ≅ L₂
inst✝ : L₁.IsLocalization W
h : W.IsInvertedBy L₂
⊢ L₂.IsLocalization W

Tactic:
let F₁ := Localization.Construction.lift L₁ (Localization.inverts L₁ W)

Result:
C : Type u_1
D : Type u_2
inst✝² : Category.{u_4, u_1} C
inst✝¹ : Category.{u_5, u_2} D
W : MorphismProperty C
L₁ L₂ : C ⥤ D
e : L₁ ≅ L₂
inst✝ : L₁.IsLocalization W
h : W.IsInvertedBy L₂
F₁ : W.Localization ⥤ D := Construction.lift L₁ ⋯
⊢ L₂.IsLocalization W
-- Mathlib/Algebra/Order/GroupWithZero/Canonical.lean
@[simp] lemma unzero_le_unzero {a b : WithZero α} (ha hb) :
    unzero (x := a) ha ≤ unzero (x := b) hb ↔ a ≤ b

Proof state:
case intro
α : Type u_1
inst✝ : Preorder α
b : WithZero α
hb : b ≠ 0
a : α
ha : ↑a ≠ 0
⊢ unzero ha ≤ unzero hb ↔ ↑a ≤ b

Tactic:
lift b to α using id hb

Result:
case intro.intro
α : Type u_1
inst✝ : Preorder α
a : α
ha : ↑a ≠ 0
b : α
hb : ↑b ≠ 0
⊢ unzero ha ≤ unzero hb ↔ ↑a ≤ ↑b

Proof state:
α : Type u_1
inst✝ : Preorder α
a b : WithZero α
ha : a ≠ 0
hb : b ≠ 0
⊢ unzero ha ≤ unzero hb ↔ a ≤ b

Tactic:
lift a to α using id ha

Result:
case intro
α : Type u_1
inst✝ : Preorder α
b : WithZero α
hb : b ≠ 0
a : α
ha : ↑a ≠ 0
⊢ unzero ha ≤ unzero hb ↔ ↑a ≤ b

Proof state:
case intro.intro
α : Type u_1
inst✝ : Preorder α
a : α
ha : ↑a ≠ 0
b : α
hb : ↑b ≠ 0
⊢ unzero ha ≤ unzero hb ↔ ↑a ≤ ↑b

Tactic:
simp

Result:
no goals
-- Mathlib/Analysis/LocallyConvex/WithSeminorms.lean
theorem cont_withSeminorms_normedSpace (F) [SeminormedAddCommGroup F] [NormedSpace 𝕝₂ F]
    [TopologicalSpace E] {p : ι → Seminorm 𝕝 E} (hp : WithSeminorms p)
    (f : E →ₛₗ[τ₁₂] F) (hf : ∃ (s : Finset ι) (C : ℝ≥0), (normSeminorm 𝕝₂ F).comp f ≤ C • s.sup p) :
    Continuous f

Proof state:
𝕝 : Type u_3
𝕝₂ : Type u_4
E : Type u_5
ι : Type u_8
inst✝⁸ : AddCommGroup E
inst✝⁷ : NormedField 𝕝
inst✝⁶ : Module 𝕝 E
inst✝⁵ : NormedField 𝕝₂
τ₁₂ : 𝕝 →+* 𝕝₂
inst✝⁴ : RingHomIsometric τ₁₂
inst✝³ : Nonempty ι
F : Type u_10
inst✝² : SeminormedAddCommGroup F
inst✝¹ : NormedSpace 𝕝₂ F
inst✝ : TopologicalSpace E
p : ι → Seminorm 𝕝 E
hp : WithSeminorms p
f : E →ₛₗ[τ₁₂] F
hf : ∃ s C, (normSeminorm 𝕝₂ F).comp f ≤ C • s.sup p
⊢ Continuous ⇑f

Tactic:
rw [← Seminorm.isBounded_const (Fin 1)] at hf

Result:
𝕝 : Type u_3
𝕝₂ : Type u_4
E : Type u_5
ι : Type u_8
inst✝⁸ : AddCommGroup E
inst✝⁷ : NormedField 𝕝
inst✝⁶ : Module 𝕝 E
inst✝⁵ : NormedField 𝕝₂
τ₁₂ : 𝕝 →+* 𝕝₂
inst✝⁴ : RingHomIsometric τ₁₂
inst✝³ : Nonempty ι
F : Type u_10
inst✝² : SeminormedAddCommGroup F
inst✝¹ : NormedSpace 𝕝₂ F
inst✝ : TopologicalSpace E
p : ι → Seminorm 𝕝 E
hp : WithSeminorms p
f : E →ₛₗ[τ₁₂] F
hf : IsBounded p (fun x => normSeminorm 𝕝₂ F) f
⊢ Continuous ⇑f

Proof state:
𝕝 : Type u_3
𝕝₂ : Type u_4
E : Type u_5
ι : Type u_8
inst✝⁸ : AddCommGroup E
inst✝⁷ : NormedField 𝕝
inst✝⁶ : Module 𝕝 E
inst✝⁵ : NormedField 𝕝₂
τ₁₂ : 𝕝 →+* 𝕝₂
inst✝⁴ : RingHomIsometric τ₁₂
inst✝³ : Nonempty ι
F : Type u_10
inst✝² : SeminormedAddCommGroup F
inst✝¹ : NormedSpace 𝕝₂ F
inst✝ : TopologicalSpace E
p : ι → Seminorm 𝕝 E
hp : WithSeminorms p
f : E →ₛₗ[τ₁₂] F
hf : IsBounded p (fun x => normSeminorm 𝕝₂ F) f
⊢ Continuous ⇑f

Tactic:
exact continuous_from_bounded hp (norm_withSeminorms 𝕝₂ F) f hf

Result:
no goals
-- Mathlib/Combinatorics/SetFamily/Compression/UV.lean
lemma _root_.Set.Sized.uvCompression (huv : #u = #v) (h𝒜 : (𝒜 : Set (Finset α)).Sized r) :
    (𝓒 u v 𝒜 : Set (Finset α)).Sized r

Proof state:
α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
u v : Finset α
r : ℕ
huv : #u = #v
h𝒜 : Set.Sized r ↑𝒜
⊢ Set.Sized r ↑(𝓒 u v 𝒜)

Tactic:
simp_rw [Set.Sized, mem_coe, mem_compression]

Result:
α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
u v : Finset α
r : ℕ
huv : #u = #v
h𝒜 : Set.Sized r ↑𝒜
⊢ ∀ ⦃x : Finset α⦄, (x ∈ 𝒜 ∧ compress u v x ∈ 𝒜 ∨ x ∉ 𝒜 ∧ ∃ b ∈ 𝒜, compress u v b = x) → #x = r

Proof state:
case inl
α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
u v : Finset α
r : ℕ
huv : #u = #v
h𝒜 : Set.Sized r ↑𝒜
s : Finset α
hs : s ∈ 𝒜 ∧ compress u v s ∈ 𝒜
⊢ #s = r

Tactic:
exact h𝒜 hs.1

Result:
no goals

Proof state:
case inr.intro.intro.intro
α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
u v : Finset α
r : ℕ
huv : #u = #v
h𝒜 : Set.Sized r ↑𝒜
t : Finset α
ht : t ∈ 𝒜
huvt : compress u v t ∉ 𝒜
⊢ #(compress u v t) = r

Tactic:
rw [card_compress huv, h𝒜 ht]

Result:
no goals

Proof state:
α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
u v : Finset α
r : ℕ
huv : #u = #v
h𝒜 : Set.Sized r ↑𝒜
⊢ ∀ ⦃x : Finset α⦄, (x ∈ 𝒜 ∧ compress u v x ∈ 𝒜 ∨ x ∉ 𝒜 ∧ ∃ b ∈ 𝒜, compress u v b = x) → #x = r

Tactic:
rintro s (hs | ⟨huvt, t, ht, rfl⟩)

Result:
case inl
α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
u v : Finset α
r : ℕ
huv : #u = #v
h𝒜 : Set.Sized r ↑𝒜
s : Finset α
hs : s ∈ 𝒜 ∧ compress u v s ∈ 𝒜
⊢ #s = r

case inr.intro.intro.intro
α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
u v : Finset α
r : ℕ
huv : #u = #v
h𝒜 : Set.Sized r ↑𝒜
t : Finset α
ht : t ∈ 𝒜
huvt : compress u v t ∉ 𝒜
⊢ #(compress u v t) = r
-- Mathlib/Algebra/Prime/Lemmas.lean
theorem MulEquiv.prime_iff {E : Type*} [EquivLike E M N] [MulEquivClass E M N] (e : E) :
    Prime (e p) ↔ Prime p

Proof state:
M : Type u_1
N : Type u_2
inst✝³ : CommMonoidWithZero M
inst✝² : CommMonoidWithZero N
p : M
E : Type u_5
inst✝¹ : EquivLike E M N
inst✝ : MulEquivClass E M N
e✝ : E
e : M ≃* N := ↑e✝
h : Prime p
a : N
⊢ e (e.symm a) = a

Tactic:
simp

Result:
no goals

Proof state:
M : Type u_1
N : Type u_2
inst✝³ : CommMonoidWithZero M
inst✝² : CommMonoidWithZero N
p : M
E : Type u_5
inst✝¹ : EquivLike E M N
inst✝ : MulEquivClass E M N
e✝ : E
e : M ≃* N := ↑e✝
a : M
⊢ e.symm (e a) = a

Tactic:
simp

Result:
no goals

Proof state:
M : Type u_1
N : Type u_2
inst✝³ : CommMonoidWithZero M
inst✝² : CommMonoidWithZero N
p : M
E : Type u_5
inst✝¹ : EquivLike E M N
inst✝ : MulEquivClass E M N
e : E
⊢ Prime (e p) ↔ Prime p

Tactic:
let e := MulEquivClass.toMulEquiv e

Result:
M : Type u_1
N : Type u_2
inst✝³ : CommMonoidWithZero M
inst✝² : CommMonoidWithZero N
p : M
E : Type u_5
inst✝¹ : EquivLike E M N
inst✝ : MulEquivClass E M N
e✝ : E
e : M ≃* N := ↑e✝
⊢ Prime (e✝ p) ↔ Prime p

Proof state:
M : Type u_1
N : Type u_2
inst✝³ : CommMonoidWithZero M
inst✝² : CommMonoidWithZero N
p : M
E : Type u_5
inst✝¹ : EquivLike E M N
inst✝ : MulEquivClass E M N
e✝ : E
e : M ≃* N := ↑e✝
⊢ Prime (e✝ p) ↔ Prime p

Tactic:
exact ⟨comap_prime e e.symm fun a => by simp,
  fun h => (comap_prime e.symm e fun a => by simp) <| (e.symm_apply_apply p).substr h⟩

Result:
no goals
-- Mathlib/Algebra/Order/Monoid/Unbundled/Basic.lean
theorem mul_le_iff_le_one_left [MulOneClass α] [i : @Std.Commutative α (· * ·)]
    [MulLeftMono α] {a b : α} (ha : MulLECancellable a) :
    b * a ≤ a ↔ b ≤ 1

Proof state:
α : Type u_1
inst✝² : LE α
inst✝¹ : MulOneClass α
i : Std.Commutative fun x1 x2 => x1 * x2
inst✝ : MulLeftMono α
a b : α
ha : MulLECancellable a
⊢ b * a ≤ a ↔ b ≤ 1

Tactic:
rw [i.comm, ha.mul_le_iff_le_one_right]

Result:
no goals
-- Mathlib/Data/Seq/WSeq.lean
theorem drop.aux_none : ∀ n, @drop.aux α n none = Computation.pure none
  | 0 => rfl
  | n + 1 =>
    show Computation.bind (Computation.pure none) (drop.aux n) = Computation.pure none by
      rw [ret_bind, drop.aux_none n]

Proof state:
α : Type u
n : ℕ
⊢ (Computation.pure none).bind (aux n) = Computation.pure none

Tactic:
rw [ret_bind, drop.aux_none n]

Result:
no goals
-- Mathlib/Analysis/InnerProductSpace/TwoDim.lean
theorem inner_rightAngleRotation_left (x y : E) : ⟪J x, y⟫ = ω x y

Proof state:
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
x y : E
⊢ inner (o.rightAngleRotation x) y = (o.areaForm x) y

Tactic:
rw [rightAngleRotation]

Result:
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
x y : E
⊢ inner ((LinearIsometryEquiv.ofLinearIsometry o.rightAngleRotationAux₂ (-o.rightAngleRotationAux₁) ⋯ ⋯) x) y =
    (o.areaForm x) y

Proof state:
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
x y : E
⊢ inner ((LinearIsometryEquiv.ofLinearIsometry o.rightAngleRotationAux₂ (-o.rightAngleRotationAux₁) ⋯ ⋯) x) y =
    (o.areaForm x) y

Tactic:
exact o.inner_rightAngleRotationAux₁_left x y

Result:
no goals
-- Mathlib/Algebra/Squarefree/Basic.lean
theorem squarefree_iff_irreducible_sq_not_dvd_of_exists_irreducible {r : R}
    (hr : ∃ x : R, Irreducible x) : Squarefree r ↔ ∀ x : R, Irreducible x → ¬x * x ∣ r

Proof state:
R : Type u_1
inst✝¹ : CommMonoidWithZero R
inst✝ : WfDvdMonoid R
r : R
hr : ∃ x, Irreducible x
⊢ Squarefree r ↔ ∀ (x : R), Irreducible x → ¬x * x ∣ r

Tactic:
rw [irreducible_sq_not_dvd_iff_eq_zero_and_no_irreducibles_or_squarefree, ← not_exists]

Result:
R : Type u_1
inst✝¹ : CommMonoidWithZero R
inst✝ : WfDvdMonoid R
r : R
hr : ∃ x, Irreducible x
⊢ Squarefree r ↔ (r = 0 ∧ ¬∃ x, Irreducible x) ∨ Squarefree r

Proof state:
R : Type u_1
inst✝¹ : CommMonoidWithZero R
inst✝ : WfDvdMonoid R
r : R
hr : ∃ x, Irreducible x
⊢ Squarefree r ↔ (r = 0 ∧ ¬∃ x, Irreducible x) ∨ Squarefree r

Tactic:
simp only [hr, not_true, false_or, and_false]

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Matching.lean
lemma even_card_of_isPerfectMatching [Fintype V] [DecidableEq V] [DecidableRel G.Adj]
    (c : ConnectedComponent G) (hM : M.IsPerfectMatching) :
    Even (Fintype.card c.supp)

Proof state:
V : Type u_1
G : SimpleGraph V
M : G.Subgraph
inst✝² : Fintype V
inst✝¹ : DecidableEq V
inst✝ : DecidableRel G.Adj
c : G.ConnectedComponent
hM : M.IsPerfectMatching
this : DecidablePred fun x => x ∈ (M.induce c.supp).verts := fun a => G.instDecidableMemSupp c a
⊢ Even (Fintype.card ↑c.supp)

Tactic:
simpa using (hM.induce_connectedComponent_isMatching c).even_card

Result:
no goals

Proof state:
V : Type u_1
G : SimpleGraph V
M : G.Subgraph
inst✝² : Fintype V
inst✝¹ : DecidableEq V
inst✝ : DecidableRel G.Adj
c : G.ConnectedComponent
hM : M.IsPerfectMatching
⊢ Even (Fintype.card ↑c.supp)

Tactic:
letI : DecidablePred fun x ↦ x ∈ (M.induce c.supp).verts := fun a ↦ G.instDecidableMemSupp c a

Result:
V : Type u_1
G : SimpleGraph V
M : G.Subgraph
inst✝² : Fintype V
inst✝¹ : DecidableEq V
inst✝ : DecidableRel G.Adj
c : G.ConnectedComponent
hM : M.IsPerfectMatching
this : DecidablePred fun x => x ∈ (M.induce c.supp).verts := fun a => G.instDecidableMemSupp c a
⊢ Even (Fintype.card ↑c.supp)
-- Mathlib/Algebra/Polynomial/Basic.lean
theorem coeff_mem_coeffs (p : R[X]) (n : ℕ) (h : p.coeff n ≠ 0) : p.coeff n ∈ p.coeffs

Proof state:
R : Type u
inst✝ : Semiring R
p : R[X]
n : ℕ
h : p.coeff n ≠ 0
⊢ ∃ a, ¬p.coeff a = 0 ∧ p.coeff a = p.coeff n

Tactic:
exact ⟨n, h, rfl⟩

Result:
no goals

Proof state:
R : Type u
inst✝ : Semiring R
p : R[X]
n : ℕ
h : p.coeff n ≠ 0
⊢ p.coeff n ∈ p.coeffs

Tactic:
classical
simp only [coeffs, exists_prop, mem_support_iff, Finset.mem_image, Ne]
exact ⟨n, h, rfl⟩

Result:
no goals

Proof state:
R : Type u
inst✝ : Semiring R
p : R[X]
n : ℕ
h : p.coeff n ≠ 0
⊢ p.coeff n ∈ p.coeffs

Tactic:
simp only [coeffs, exists_prop, mem_support_iff, Finset.mem_image, Ne]

Result:
R : Type u
inst✝ : Semiring R
p : R[X]
n : ℕ
h : p.coeff n ≠ 0
⊢ ∃ a, ¬p.coeff a = 0 ∧ p.coeff a = p.coeff n
-- Mathlib/RingTheory/DedekindDomain/Ideal.lean
theorem mul_left_le_iff [IsDedekindDomain A] {J : FractionalIdeal A⁰ K} (hJ : J ≠ 0) {I I'} :
    J * I ≤ J * I' ↔ I ≤ I'

Proof state:
A : Type u_2
K : Type u_3
inst✝⁴ : CommRing A
inst✝³ : Field K
inst✝² : Algebra A K
inst✝¹ : IsFractionRing A K
inst✝ : IsDedekindDomain A
J : FractionalIdeal A⁰ K
hJ : J ≠ 0
I I' : FractionalIdeal A⁰ K
⊢ J * I ≤ J * I' ↔ I ≤ I'

Tactic:
convert mul_right_le_iff hJ using 1

Result:
case h.e'_1.a
A : Type u_2
K : Type u_3
inst✝⁴ : CommRing A
inst✝³ : Field K
inst✝² : Algebra A K
inst✝¹ : IsFractionRing A K
inst✝ : IsDedekindDomain A
J : FractionalIdeal A⁰ K
hJ : J ≠ 0
I I' : FractionalIdeal A⁰ K
⊢ J * I ≤ J * I' ↔ I * J ≤ I' * J

Proof state:
case h.e'_1.a
A : Type u_2
K : Type u_3
inst✝⁴ : CommRing A
inst✝³ : Field K
inst✝² : Algebra A K
inst✝¹ : IsFractionRing A K
inst✝ : IsDedekindDomain A
J : FractionalIdeal A⁰ K
hJ : J ≠ 0
I I' : FractionalIdeal A⁰ K
⊢ J * I ≤ J * I' ↔ I * J ≤ I' * J

Tactic:
simp only [mul_comm]

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

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

Tactic:
rw [Nat.div_zero]

Result:
m : Nat
⊢ ofNat 0 = -↑0

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

Tactic:
rfl

Result:
no goals
-- Mathlib/LinearAlgebra/Prod.lean
theorem map_inl : p.map (inl R M M₂) = prod p ⊥

Proof state:
case h.mk
R : Type u
M : Type v
M₂ : Type w
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R M
inst✝ : Module R M₂
p : Submodule R M
x : M
y : M₂
⊢ (x, y) ∈ map (inl R M M₂) p ↔ (x, y) ∈ p.prod ⊥

Tactic:
simp only [and_left_comm, eq_comm, mem_map, Prod.mk.inj_iff, inl_apply, mem_bot, exists_eq_left',
  mem_prod]

Result:
no goals

Proof state:
R : Type u
M : Type v
M₂ : Type w
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R M
inst✝ : Module R M₂
p : Submodule R M
⊢ map (inl R M M₂) p = p.prod ⊥

Tactic:
ext ⟨x, y⟩

Result:
case h.mk
R : Type u
M : Type v
M₂ : Type w
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R M
inst✝ : Module R M₂
p : Submodule R M
x : M
y : M₂
⊢ (x, y) ∈ map (inl R M M₂) p ↔ (x, y) ∈ p.prod ⊥