harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Data/Set/Card.lean
theorem ncard_union_le (s t : Set α) : (s ∪ t).ncard ≤ s.ncard + t.ncard

Proof state:
case inr
α : Type u_1
s t : Set α
h : (s ∪ t).Infinite
⊢ 0 ≤ s.ncard + t.ncard

Tactic:
apply zero_le

Result:
no goals

Proof state:
case inl
α : Type u_1
s t : Set α
h : (s ∪ t).Finite
⊢ (s ∪ t).encard ≤ s.encard + t.encard

Tactic:
apply encard_union_le

Result:
no goals

Proof state:
case inr
α : Type u_1
s t : Set α
h : (s ∪ t).Infinite
⊢ (s ∪ t).ncard ≤ s.ncard + t.ncard

Tactic:
rw [h.ncard]

Result:
case inr
α : Type u_1
s t : Set α
h : (s ∪ t).Infinite
⊢ 0 ≤ s.ncard + t.ncard

Proof state:
case inl
α : Type u_1
s t : Set α
h : (s ∪ t).Finite
⊢ ↑(s ∪ t).ncard ≤ ↑s.ncard + ↑t.ncard

Tactic:
rw [h.cast_ncard_eq, (h.subset subset_union_left).cast_ncard_eq,
  (h.subset subset_union_right).cast_ncard_eq]

Result:
case inl
α : Type u_1
s t : Set α
h : (s ∪ t).Finite
⊢ (s ∪ t).encard ≤ s.encard + t.encard

Proof state:
α : Type u_1
s t : Set α
⊢ (s ∪ t).ncard ≤ s.ncard + t.ncard

Tactic:
obtain (h | h) := (s ∪ t).finite_or_infinite

Result:
case inl
α : Type u_1
s t : Set α
h : (s ∪ t).Finite
⊢ (s ∪ t).ncard ≤ s.ncard + t.ncard

case inr
α : Type u_1
s t : Set α
h : (s ∪ t).Infinite
⊢ (s ∪ t).ncard ≤ s.ncard + t.ncard

Proof state:
case inl
α : Type u_1
s t : Set α
h : (s ∪ t).Finite
⊢ (s ∪ t).ncard ≤ s.ncard + t.ncard

Tactic:
to_encard_tac

Result:
case inl
α : Type u_1
s t : Set α
h : (s ∪ t).Finite
⊢ ↑(s ∪ t).ncard ≤ ↑s.ncard + ↑t.ncard
-- Mathlib/Topology/ContinuousOn.lean
theorem IsOpen.ite' (hs : IsOpen s) (hs' : IsOpen s')
    (ht : ∀ x ∈ frontier t, x ∈ s ↔ x ∈ s') : IsOpen (t.ite s s')

Proof state:
α : Type u_1
inst✝ : TopologicalSpace α
s s' t : Set α
hs : IsOpen s
hs' : IsOpen s'
ht : ∀ x ∈ frontier t, x ∈ s ↔ x ∈ s'
⊢ IsOpen (t.ite s s')

Tactic:
simp only [isOpen_iff_continuous_mem, Set.ite] at *

Result:
α : Type u_1
inst✝ : TopologicalSpace α
s s' t : Set α
ht : ∀ x ∈ frontier t, x ∈ s ↔ x ∈ s'
hs : Continuous fun x => x ∈ s
hs' : Continuous fun x => x ∈ s'
⊢ Continuous fun x => x ∈ s ∩ t ∪ s' \ t

Proof state:
α : Type u_1
inst✝ : TopologicalSpace α
s s' t : Set α
hs : IsOpen s
hs' : IsOpen s'
ht : ∀ x ∈ frontier t, x ∈ s ↔ x ∈ s'
⊢ IsOpen (t.ite s s')

Tactic:
classical
  simp only [isOpen_iff_continuous_mem, Set.ite] at *
  convert
    continuous_piecewise (fun x hx => propext (ht x hx)) hs.continuousOn hs'.continuousOn using 2
  rename_i x
  by_cases hx : x ∈ t <;> simp [hx]

Result:
no goals

Proof state:
case h.e'_5.h.a
α : Type u_1
inst✝ : TopologicalSpace α
s s' t : Set α
ht : ∀ x ∈ frontier t, x ∈ s ↔ x ∈ s'
hs : Continuous fun x => x ∈ s
hs' : Continuous fun x => x ∈ s'
x✝ : α
⊢ x✝ ∈ s ∩ t ∪ s' \ t ↔ t.piecewise (Membership.mem s) (Membership.mem s') x✝

Tactic:
rename_i x

Result:
case h.e'_5.h.a
α : Type u_1
inst✝ : TopologicalSpace α
s s' t : Set α
ht : ∀ x ∈ frontier t, x ∈ s ↔ x ∈ s'
hs : Continuous fun x => x ∈ s
hs' : Continuous fun x => x ∈ s'
x : α
⊢ x ∈ s ∩ t ∪ s' \ t ↔ t.piecewise (Membership.mem s) (Membership.mem s') x

Proof state:
case h.e'_5.h.a
α : Type u_1
inst✝ : TopologicalSpace α
s s' t : Set α
ht : ∀ x ∈ frontier t, x ∈ s ↔ x ∈ s'
hs : Continuous fun x => x ∈ s
hs' : Continuous fun x => x ∈ s'
x : α
⊢ x ∈ s ∩ t ∪ s' \ t ↔ t.piecewise (Membership.mem s) (Membership.mem s') x

Tactic:
by_cases hx : x ∈ t <;> simp [hx]

Result:
no goals

Proof state:
α : Type u_1
inst✝ : TopologicalSpace α
s s' t : Set α
ht : ∀ x ∈ frontier t, x ∈ s ↔ x ∈ s'
hs : Continuous fun x => x ∈ s
hs' : Continuous fun x => x ∈ s'
⊢ Continuous fun x => x ∈ s ∩ t ∪ s' \ t

Tactic:
convert
  continuous_piecewise (fun x hx => propext (ht x hx)) hs.continuousOn hs'.continuousOn using 2

Result:
case h.e'_5.h.a
α : Type u_1
inst✝ : TopologicalSpace α
s s' t : Set α
ht : ∀ x ∈ frontier t, x ∈ s ↔ x ∈ s'
hs : Continuous fun x => x ∈ s
hs' : Continuous fun x => x ∈ s'
x✝ : α
⊢ x✝ ∈ s ∩ t ∪ s' \ t ↔ t.piecewise (Membership.mem s) (Membership.mem s') x✝
-- Mathlib/.lake/packages/lean4/src/lean/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas.lean
theorem bitblast.go_eval_eq_eval (expr : BVLogicalExpr) (aig : AIG BVBit) (assign : BVExpr.Assignment) :
    ⟦ofBoolExprCached.go aig expr BVPred.bitblast, assign.toAIGAssignment⟧ = expr.eval assign

Proof state:
case gate
assign : BVExpr.Assignment
g : Gate
lhs rhs : BoolExpr BVPred
lih : ∀ (aig : AIG BVBit), ⟦assign.toAIGAssignment, (ofBoolExprCached.go aig lhs BVPred.bitblast).val⟧ = eval assign lhs
rih : ∀ (aig : AIG BVBit), ⟦assign.toAIGAssignment, (ofBoolExprCached.go aig rhs BVPred.bitblast).val⟧ = eval assign rhs
aig : AIG BVBit
⊢ ⟦assign.toAIGAssignment, (ofBoolExprCached.go aig (BoolExpr.gate g lhs rhs) BVPred.bitblast).val⟧ =
    eval assign (BoolExpr.gate g lhs rhs)

Tactic:
cases g <;> simp [ofBoolExprCached.go, Gate.eval, lih, rih]

Result:
no goals

Proof state:
case not
assign : BVExpr.Assignment
expr : BoolExpr BVPred
ih :
  ∀ (aig : AIG BVBit), ⟦assign.toAIGAssignment, (ofBoolExprCached.go aig expr BVPred.bitblast).val⟧ = eval assign expr
aig : AIG BVBit
⊢ ⟦assign.toAIGAssignment, (ofBoolExprCached.go aig expr.not BVPred.bitblast).val⟧ = eval assign expr.not

Tactic:
simp [ofBoolExprCached.go, ih]

Result:
no goals

Proof state:
case ite
assign : BVExpr.Assignment
discr lhs rhs : BoolExpr BVPred
dih :
  ∀ (aig : AIG BVBit), ⟦assign.toAIGAssignment, (ofBoolExprCached.go aig discr BVPred.bitblast).val⟧ = eval assign discr
lih : ∀ (aig : AIG BVBit), ⟦assign.toAIGAssignment, (ofBoolExprCached.go aig lhs BVPred.bitblast).val⟧ = eval assign lhs
rih : ∀ (aig : AIG BVBit), ⟦assign.toAIGAssignment, (ofBoolExprCached.go aig rhs BVPred.bitblast).val⟧ = eval assign rhs
aig : AIG BVBit
⊢ (if
        ⟦assign.toAIGAssignment,
            { aig := (ofBoolExprCached.go aig discr BVPred.bitblast).1.aig,
              ref := { gate := (ofBoolExprCached.go aig discr BVPred.bitblast).1.ref.gate, hgate := ?ite.hstart } }⟧ =
          true then
      ⟦assign.toAIGAssignment,
        (ofBoolExprCached.go (ofBoolExprCached.go aig discr BVPred.bitblast).1.aig lhs BVPred.bitblast).1⟧
    else
      ⟦assign.toAIGAssignment,
        {
          aig :=
            (ofBoolExprCached.go
                  (ofBoolExprCached.go (ofBoolExprCached.go aig discr BVPred.bitblast).1.aig lhs BVPred.bitblast).1.aig
                  rhs BVPred.bitblast).1.aig,
          ref :=
            (ofBoolExprCached.go
                  (ofBoolExprCached.go (ofBoolExprCached.go aig discr BVPred.bitblast).1.aig lhs BVPred.bitblast).1.aig
                  rhs BVPred.bitblast).1.ref }⟧) =
    bif eval assign discr then eval assign lhs else eval assign rhs

Tactic:
simp [dih, lih, rih]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Gamma/Beta.lean
theorem betaIntegral_convergent {u v : ℂ} (hu : 0 < re u) (hv : 0 < re v) :
    IntervalIntegrable (fun x =>
      (x : ℂ) ^ (u - 1) * (1 - (x : ℂ)) ^ (v - 1) : ℝ → ℂ) volume 0 1

Proof state:
case h.e'_3
u v : ℂ
hu : 0 < u.re
hv : 0 < v.re
⊢ (fun x => ↑(-x) ^ (u - 1) * (1 - ↑(-x)) ^ (v - 1)) = fun x => ↑(x + 1) ^ (v - 1) * (1 - ↑(x + 1)) ^ (u - 1)

Tactic:
ext1 x

Result:
case h.e'_3.h
u v : ℂ
hu : 0 < u.re
hv : 0 < v.re
x : ℝ
⊢ ↑(-x) ^ (u - 1) * (1 - ↑(-x)) ^ (v - 1) = ↑(x + 1) ^ (v - 1) * (1 - ↑(x + 1)) ^ (u - 1)

Proof state:
case h.e'_3.h.e_a.e_a
u v : ℂ
hu : 0 < u.re
hv : 0 < v.re
x : ℝ
⊢ ↑(-x) = 1 - ↑(x + 1)

Tactic:
push_cast

Result:
case h.e'_3.h.e_a.e_a
u v : ℂ
hu : 0 < u.re
hv : 0 < v.re
x : ℝ
⊢ -↑x = 1 - (↑x + 1)

Proof state:
u v : ℂ
hu : 0 < u.re
hv : 0 < v.re
⊢ IntervalIntegrable (fun x => ↑x ^ (u - 1) * (1 - ↑x) ^ (v - 1)) volume 0 1

Tactic:
refine (betaIntegral_convergent_left hu v).trans ?_

Result:
u v : ℂ
hu : 0 < u.re
hv : 0 < v.re
⊢ IntervalIntegrable (fun x => ↑x ^ (u - 1) * (1 - ↑x) ^ (v - 1)) volume (1 / 2) 1

Proof state:
u v : ℂ
hu : 0 < u.re
hv : 0 < v.re
⊢ IntervalIntegrable (fun x => ↑x ^ (u - 1) * (1 - ↑x) ^ (v - 1)) volume (1 / 2) 1

Tactic:
rw [IntervalIntegrable.iff_comp_neg]

Result:
u v : ℂ
hu : 0 < u.re
hv : 0 < v.re
⊢ IntervalIntegrable (fun x => ↑(-x) ^ (u - 1) * (1 - ↑(-x)) ^ (v - 1)) volume (-(1 / 2)) (-1)

Proof state:
case h.e'_6
u v : ℂ
hu : 0 < u.re
hv : 0 < v.re
⊢ -1 = 0 - 1

Tactic:
norm_num

Result:
no goals

Proof state:
case h.e'_3.h
u v : ℂ
hu : 0 < u.re
hv : 0 < v.re
x : ℝ
⊢ ↑(-x) ^ (u - 1) * (1 - ↑(-x)) ^ (v - 1) = ↑(x + 1) ^ (v - 1) * (1 - ↑(x + 1)) ^ (u - 1)

Tactic:
conv_lhs => rw [mul_comm]

Result:
case h.e'_3.h
u v : ℂ
hu : 0 < u.re
hv : 0 < v.re
x : ℝ
⊢ (1 - ↑(-x)) ^ (v - 1) * ↑(-x) ^ (u - 1) = ↑(x + 1) ^ (v - 1) * (1 - ↑(x + 1)) ^ (u - 1)

Proof state:
case h.e'_5
u v : ℂ
hu : 0 < u.re
hv : 0 < v.re
⊢ -(1 / 2) = 1 / 2 - 1

Tactic:
norm_num

Result:
no goals

Proof state:
case h.e'_3.h.e_a.e_a
u v : ℂ
hu : 0 < u.re
hv : 0 < v.re
x : ℝ
⊢ -↑x = 1 - (↑x + 1)

Tactic:
ring

Result:
no goals

Proof state:
u v : ℂ
hu : 0 < u.re
hv : 0 < v.re
⊢ IntervalIntegrable (fun x => ↑(-x) ^ (u - 1) * (1 - ↑(-x)) ^ (v - 1)) volume (-(1 / 2)) (-1)

Tactic:
convert ((betaIntegral_convergent_left hv u).comp_add_right 1).symm using 1

Result:
case h.e'_3
u v : ℂ
hu : 0 < u.re
hv : 0 < v.re
⊢ (fun x => ↑(-x) ^ (u - 1) * (1 - ↑(-x)) ^ (v - 1)) = fun x => ↑(x + 1) ^ (v - 1) * (1 - ↑(x + 1)) ^ (u - 1)

case h.e'_5
u v : ℂ
hu : 0 < u.re
hv : 0 < v.re
⊢ -(1 / 2) = 1 / 2 - 1

case h.e'_6
u v : ℂ
hu : 0 < u.re
hv : 0 < v.re
⊢ -1 = 0 - 1
-- Mathlib/FieldTheory/Galois/Basic.lean
theorem of_separable_splitting_field [sp : p.IsSplittingField F E] (hp : p.Separable) :
    IsGalois F E

Proof state:
case ih
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
p : F[X]
sp : Polynomial.IsSplittingField F E p
hp : p.Separable
hFE : FiniteDimensional F E
this : DecidableEq E := Classical.decEq E
s : Set E := p.rootSet E
adjoin_root : adjoin F s = ⊤
P : IntermediateField F E → Prop := fun K => Fintype.card (↥K →ₐ[F] E) = finrank F ↥K
K : IntermediateField F E
x : E
hx : x ∈ (p.aroots E).toFinset
hK : Fintype.card (↥K →ₐ[F] E) = finrank F ↥K
⊢ finrank F ↥(IntermediateField.restrictScalars F (↥K)⟮x⟯) = finrank F ↥(↥K)⟮x⟯

Tactic:
refine LinearEquiv.finrank_eq ?_

Result:
case ih
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
p : F[X]
sp : Polynomial.IsSplittingField F E p
hp : p.Separable
hFE : FiniteDimensional F E
this : DecidableEq E := Classical.decEq E
s : Set E := p.rootSet E
adjoin_root : adjoin F s = ⊤
P : IntermediateField F E → Prop := fun K => Fintype.card (↥K →ₐ[F] E) = finrank F ↥K
K : IntermediateField F E
x : E
hx : x ∈ (p.aroots E).toFinset
hK : Fintype.card (↥K →ₐ[F] E) = finrank F ↥K
⊢ ↥(IntermediateField.restrictScalars F (↥K)⟮x⟯) ≃ₗ[F] ↥(↥K)⟮x⟯
-- Mathlib/CategoryTheory/ComposableArrows.lean
lemma mk₄_surjective (X : ComposableArrows C 4) :
    ∃ (X₀ X₁ X₂ X₃ X₄ : C) (f₀ : X₀ ⟶ X₁) (f₁ : X₁ ⟶ X₂) (f₂ : X₂ ⟶ X₃) (f₃ : X₃ ⟶ X₄),
      X = mk₄ f₀ f₁ f₂ f₃ :=
  ⟨_, _, _, _, _, X.map' 0 1, X.map' 1 2, X.map' 2 3, X.map' 3 4,
    ext₄ rfl rfl rfl rfl rfl (by simp) (by simp) (by simp) (by simp)⟩

Proof state:
C : Type u_1
inst✝ : Category.{u_2, u_1} C
X : ComposableArrows C 4
⊢ X.map' 1 2 ⋯ ⋯ =
    eqToHom ⋯ ≫ (mk₄ (X.map' 0 1 ⋯ ⋯) (X.map' 1 2 ⋯ ⋯) (X.map' 2 3 ⋯ ⋯) (X.map' 3 4 ⋯ ⋯)).map' 1 2 ⋯ ⋯ ≫ eqToHom ⋯

Tactic:
simp

Result:
no goals

Proof state:
C : Type u_1
inst✝ : Category.{u_2, u_1} C
X : ComposableArrows C 4
⊢ X.map' 0 1 ⋯ ⋯ =
    eqToHom ⋯ ≫ (mk₄ (X.map' 0 1 ⋯ ⋯) (X.map' 1 2 ⋯ ⋯) (X.map' 2 3 ⋯ ⋯) (X.map' 3 4 ⋯ ⋯)).map' 0 1 ⋯ ⋯ ≫ eqToHom ⋯

Tactic:
simp

Result:
no goals

Proof state:
C : Type u_1
inst✝ : Category.{u_2, u_1} C
X : ComposableArrows C 4
⊢ X.map' 2 3 ⋯ ⋯ =
    eqToHom ⋯ ≫ (mk₄ (X.map' 0 1 ⋯ ⋯) (X.map' 1 2 ⋯ ⋯) (X.map' 2 3 ⋯ ⋯) (X.map' 3 4 ⋯ ⋯)).map' 2 3 ⋯ ⋯ ≫ eqToHom ⋯

Tactic:
simp

Result:
no goals

Proof state:
C : Type u_1
inst✝ : Category.{u_2, u_1} C
X : ComposableArrows C 4
⊢ X.map' 3 4 ⋯ ⋯ =
    eqToHom ⋯ ≫ (mk₄ (X.map' 0 1 ⋯ ⋯) (X.map' 1 2 ⋯ ⋯) (X.map' 2 3 ⋯ ⋯) (X.map' 3 4 ⋯ ⋯)).map' 3 4 ⋯ ⋯ ≫ eqToHom ⋯

Tactic:
simp

Result:
no goals
-- Mathlib/Algebra/Ring/Int/Parity.lean
lemma ne_of_odd_add (h : Odd (m + n)) : m ≠ n

Proof state:
m n : ℤ
h : Odd (m + n)
⊢ m ≠ n

Tactic:
rintro rfl

Result:
m : ℤ
h : Odd (m + m)
⊢ False

Proof state:
m : ℤ
h : Odd (m + m)
⊢ False

Tactic:
simp [← not_even_iff_odd] at h

Result:
no goals
-- Mathlib/Algebra/Homology/HomotopyCategory.lean
lemma quotient_inverts_homotopyEquivalences :
    (HomologicalComplex.homotopyEquivalences V c).IsInvertedBy (quotient V c)

Proof state:
case intro
ι : Type u_2
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
c : ComplexShape ι
K L : HomologicalComplex V c
e : HomotopyEquiv K L
⊢ IsIso ((quotient V c).map e.hom)

Tactic:
change IsIso (isoOfHomotopyEquiv e).hom

Result:
case intro
ι : Type u_2
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
c : ComplexShape ι
K L : HomologicalComplex V c
e : HomotopyEquiv K L
⊢ IsIso (isoOfHomotopyEquiv e).hom

Proof state:
ι : Type u_2
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
c : ComplexShape ι
⊢ (homotopyEquivalences V c).IsInvertedBy (quotient V c)

Tactic:
rintro K L _ ⟨e, rfl⟩

Result:
case intro
ι : Type u_2
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
c : ComplexShape ι
K L : HomologicalComplex V c
e : HomotopyEquiv K L
⊢ IsIso ((quotient V c).map e.hom)

Proof state:
case intro
ι : Type u_2
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
c : ComplexShape ι
K L : HomologicalComplex V c
e : HomotopyEquiv K L
⊢ IsIso (isoOfHomotopyEquiv e).hom

Tactic:
infer_instance

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/List/Associative.lean
theorem getValueCast?_append_of_containsKey_eq_false [BEq α] [LawfulBEq α]
    {l l' : List ((a : α) × β a)} {a : α} (hl' : containsKey a l' = false) :
    getValueCast? a (l ++ l') = getValueCast? a l

Proof state:
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : LawfulBEq α
l l' : List ((a : α) × β a)
a : α
hl' : containsKey a l' = false
⊢ getValueCast? a (l ++ l') = getValueCast? a l

Tactic:
rw [getValueCast?_eq_getEntry?, getValueCast?_eq_getEntry?, Option.dmap_congr getEntry?_append,
  Option.dmap_congr (by rw [getEntry?_eq_none.2 hl']), Option.dmap_congr (by rw [Option.or_none])]

Result:
no goals

Proof state:
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : LawfulBEq α
l l' : List ((a : α) × β a)
a : α
hl' : containsKey a l' = false
⊢ (getEntry? a l).or (getEntry? a l') = ?m.156535

Tactic:
rw [getEntry?_eq_none.2 hl']

Result:
no goals

Proof state:
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : LawfulBEq α
l l' : List ((a : α) × β a)
a : α
hl' : containsKey a l' = false
⊢ (getEntry? a l).or none = ?m.156597

Tactic:
rw [Option.or_none]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Attach.lean
theorem pmap_eq_pmapImpl : @pmap = @pmapImpl

Proof state:
case h.h.h.h.h.h.h
α : Type u_2
β : Type u_1
n : Nat
p : α → Prop
f : (a : α) → p a → β
L : Vector α n
h' : ∀ (a : α), a ∈ L → p a
⊢ pmap f L h' = Vector.pmapImpl f L h'

Tactic:
rcases L with ⟨L, rfl⟩

Result:
case h.h.h.h.h.h.h.mk
α : Type u_2
β : Type u_1
p : α → Prop
f : (a : α) → p a → β
L : Array α
h' : ∀ (a : α), a ∈ { toArray := L, size_toArray := ⋯ } → p a
⊢ pmap f { toArray := L, size_toArray := ⋯ } h' = Vector.pmapImpl f { toArray := L, size_toArray := ⋯ } h'

Proof state:
case h.h.h.h.h.h.h.mk.h
α : Type u_2
β : Type u_1
p : α → Prop
f : (a : α) → p a → β
L : Array α
h' : ∀ (a : α), a ∈ { toArray := L, size_toArray := ⋯ } → p a
⊢ ∀ (a : α), a ∈ L → ∀ (h₁ : p a) (h₂ : a ∈ L ∧ p a), f a h₁ = f a ⋯

Tactic:
intro a m h₁ h₂

Result:
case h.h.h.h.h.h.h.mk.h
α : Type u_2
β : Type u_1
p : α → Prop
f : (a : α) → p a → β
L : Array α
h' : ∀ (a : α), a ∈ { toArray := L, size_toArray := ⋯ } → p a
a : α
m : a ∈ L
h₁ : p a
h₂ : a ∈ L ∧ p a
⊢ f a h₁ = f a ⋯

Proof state:
⊢ @pmap = @Vector.pmapImpl

Tactic:
funext α β n p f L h'

Result:
case h.h.h.h.h.h.h
α : Type u_2
β : Type u_1
n : Nat
p : α → Prop
f : (a : α) → p a → β
L : Vector α n
h' : ∀ (a : α), a ∈ L → p a
⊢ pmap f L h' = Vector.pmapImpl f L h'

Proof state:
case h.h.h.h.h.h.h.mk
α : Type u_2
β : Type u_1
p : α → Prop
f : (a : α) → p a → β
L : Array α
h' : ∀ (a : α), a ∈ { toArray := L, size_toArray := ⋯ } → p a
⊢ pmap f { toArray := L, size_toArray := ⋯ } h' = Vector.pmapImpl f { toArray := L, size_toArray := ⋯ } h'

Tactic:
simp only [pmap, pmapImpl, attachWith_mk, map_mk, Array.map_attachWith, eq_mk]

Result:
case h.h.h.h.h.h.h.mk
α : Type u_2
β : Type u_1
p : α → Prop
f : (a : α) → p a → β
L : Array α
h' : ∀ (a : α), a ∈ { toArray := L, size_toArray := ⋯ } → p a
⊢ Array.pmap f L ⋯ = Array.pmap (fun a h => f a ⋯) L ⋯

Proof state:
case h.h.h.h.h.h.h.mk
α : Type u_2
β : Type u_1
p : α → Prop
f : (a : α) → p a → β
L : Array α
h' : ∀ (a : α), a ∈ { toArray := L, size_toArray := ⋯ } → p a
⊢ Array.pmap f L ⋯ = Array.pmap (fun a h => f a ⋯) L ⋯

Tactic:
apply Array.pmap_congr_left

Result:
case h.h.h.h.h.h.h.mk.h
α : Type u_2
β : Type u_1
p : α → Prop
f : (a : α) → p a → β
L : Array α
h' : ∀ (a : α), a ∈ { toArray := L, size_toArray := ⋯ } → p a
⊢ ∀ (a : α), a ∈ L → ∀ (h₁ : p a) (h₂ : a ∈ L ∧ p a), f a h₁ = f a ⋯

Proof state:
case h.h.h.h.h.h.h.mk.h
α : Type u_2
β : Type u_1
p : α → Prop
f : (a : α) → p a → β
L : Array α
h' : ∀ (a : α), a ∈ { toArray := L, size_toArray := ⋯ } → p a
a : α
m : a ∈ L
h₁ : p a
h₂ : a ∈ L ∧ p a
⊢ f a h₁ = f a ⋯

Tactic:
congr

Result:
no goals
-- Mathlib/Data/Rat/Defs.lean
@[simp]
lemma num_eq_zero {q : ℚ} : q.num = 0 ↔ q = 0

Proof state:
case mk'.mp
num✝ : ℤ
den✝ : ℕ
den_nz✝ : den✝ ≠ 0
reduced✝ : num✝.natAbs.Coprime den✝
⊢ { num := num✝, den := den✝, den_nz := den_nz✝, reduced := reduced✝ }.num = 0 →
    { num := num✝, den := den✝, den_nz := den_nz✝, reduced := reduced✝ } = 0

Tactic:
rintro rfl

Result:
case mk'.mp
den✝ : ℕ
den_nz✝ : den✝ ≠ 0
reduced✝ : (Int.natAbs 0).Coprime den✝
⊢ { num := 0, den := den✝, den_nz := den_nz✝, reduced := reduced✝ } = 0

Proof state:
case mk'.mp
den✝ : ℕ
den_nz✝ : den✝ ≠ 0
reduced✝ : (Int.natAbs 0).Coprime den✝
⊢ { num := 0, den := den✝, den_nz := den_nz✝, reduced := reduced✝ } = 0

Tactic:
exact mk'_zero _ _ _

Result:
no goals

Proof state:
q : ℚ
⊢ q.num = 0 ↔ q = 0

Tactic:
induction q

Result:
case mk'
num✝ : ℤ
den✝ : ℕ
den_nz✝ : den✝ ≠ 0
reduced✝ : num✝.natAbs.Coprime den✝
⊢ { num := num✝, den := den✝, den_nz := den_nz✝, reduced := reduced✝ }.num = 0 ↔
    { num := num✝, den := den✝, den_nz := den_nz✝, reduced := reduced✝ } = 0

Proof state:
case mk'.mpr
num✝ : ℤ
den✝ : ℕ
den_nz✝ : den✝ ≠ 0
reduced✝ : num✝.natAbs.Coprime den✝
⊢ { num := num✝, den := den✝, den_nz := den_nz✝, reduced := reduced✝ } = 0 →
    { num := num✝, den := den✝, den_nz := den_nz✝, reduced := reduced✝ }.num = 0

Tactic:
exact congr_arg num

Result:
no goals

Proof state:
case mk'
num✝ : ℤ
den✝ : ℕ
den_nz✝ : den✝ ≠ 0
reduced✝ : num✝.natAbs.Coprime den✝
⊢ { num := num✝, den := den✝, den_nz := den_nz✝, reduced := reduced✝ }.num = 0 ↔
    { num := num✝, den := den✝, den_nz := den_nz✝, reduced := reduced✝ } = 0

Tactic:
constructor

Result:
case mk'.mp
num✝ : ℤ
den✝ : ℕ
den_nz✝ : den✝ ≠ 0
reduced✝ : num✝.natAbs.Coprime den✝
⊢ { num := num✝, den := den✝, den_nz := den_nz✝, reduced := reduced✝ }.num = 0 →
    { num := num✝, den := den✝, den_nz := den_nz✝, reduced := reduced✝ } = 0

case mk'.mpr
num✝ : ℤ
den✝ : ℕ
den_nz✝ : den✝ ≠ 0
reduced✝ : num✝.natAbs.Coprime den✝
⊢ { num := num✝, den := den✝, den_nz := den_nz✝, reduced := reduced✝ } = 0 →
    { num := num✝, den := den✝, den_nz := den_nz✝, reduced := reduced✝ }.num = 0
-- Mathlib/Order/KrullDimension.lean
lemma height_add_one_le {a b : α} (hab : a < b) : height a + 1 ≤ height b

Proof state:
case top
α : Type u_1
inst✝ : Preorder α
a b : α
hab : a < b
hfin : height a = ⊤
⊢ ⊤ + 1 ≤ height b

Tactic:
have : ⊤ ≤ height b := by
  rw [← hfin]
  gcongr

Result:
case top
α : Type u_1
inst✝ : Preorder α
a b : α
hab : a < b
hfin : height a = ⊤
this : ⊤ ≤ height b
⊢ ⊤ + 1 ≤ height b

Proof state:
case coe.h.hfin
α : Type u_1
inst✝ : Preorder α
a b : α
hab : a < b
n : ℕ
hfin : height a = ↑n
⊢ height a < ⊤

Tactic:
simp [hfin]

Result:
no goals

Proof state:
α : Type u_1
inst✝ : Preorder α
a b : α
hab : a < b
⊢ height a + 1 ≤ height b

Tactic:
cases hfin : height a with
| top =>
  have : ⊤ ≤ height b := by
    rw [← hfin]
    gcongr
  simp [this]
| coe n =>
  apply Order.add_one_le_of_lt
  rw [← hfin]
  gcongr
  simp [hfin]

Result:
no goals

Proof state:
case top
α : Type u_1
inst✝ : Preorder α
a b : α
hab : a < b
hfin : height a = ⊤
this : ⊤ ≤ height b
⊢ ⊤ + 1 ≤ height b

Tactic:
simp [this]

Result:
no goals

Proof state:
case coe.h
α : Type u_1
inst✝ : Preorder α
a b : α
hab : a < b
n : ℕ
hfin : height a = ↑n
⊢ height a < height b

Tactic:
gcongr

Result:
case coe.h.hfin
α : Type u_1
inst✝ : Preorder α
a b : α
hab : a < b
n : ℕ
hfin : height a = ↑n
⊢ height a < ⊤

Proof state:
case coe.h
α : Type u_1
inst✝ : Preorder α
a b : α
hab : a < b
n : ℕ
hfin : height a = ↑n
⊢ ↑n < height b

Tactic:
rw [← hfin]

Result:
case coe.h
α : Type u_1
inst✝ : Preorder α
a b : α
hab : a < b
n : ℕ
hfin : height a = ↑n
⊢ height a < height b

Proof state:
case coe
α : Type u_1
inst✝ : Preorder α
a b : α
hab : a < b
n : ℕ
hfin : height a = ↑n
⊢ ↑n + 1 ≤ height b

Tactic:
apply Order.add_one_le_of_lt

Result:
case coe.h
α : Type u_1
inst✝ : Preorder α
a b : α
hab : a < b
n : ℕ
hfin : height a = ↑n
⊢ ↑n < height b

Proof state:
α : Type u_1
inst✝ : Preorder α
a b : α
hab : a < b
hfin : height a = ⊤
⊢ ⊤ ≤ height b

Tactic:
rw [← hfin]

Result:
α : Type u_1
inst✝ : Preorder α
a b : α
hab : a < b
hfin : height a = ⊤
⊢ height a ≤ height b

Proof state:
α : Type u_1
inst✝ : Preorder α
a b : α
hab : a < b
hfin : height a = ⊤
⊢ height a ≤ height b

Tactic:
gcongr

Result:
no goals
-- Mathlib/.lake/packages/batteries/Batteries/Data/UnionFind/Basic.lean
theorem rank'_lt_rankMax (self : UnionFind) (i : Nat) (h) : (self.arr[i]).rank < self.rankMax

Proof state:
self : UnionFind
i : Nat
h✝ : i < self.arr.size
a : UFNode
l : List UFNode
a✝ : UFNode
h : List.Mem a✝ l
⊢ a✝.rank ≤ max a.rank (List.foldr (fun x => max x.rank) 0 l)

Tactic:
exact Nat.le_trans (go h) (Nat.le_max_right ..)

Result:
no goals

Proof state:
self : UnionFind
i : Nat
h : i < self.arr.size
a : UFNode
l : List UFNode
⊢ a.rank ≤ List.foldr (fun x => max x.rank) 0 (a :: l)

Tactic:
dsimp

Result:
self : UnionFind
i : Nat
h : i < self.arr.size
a : UFNode
l : List UFNode
⊢ a.rank ≤ max a.rank (List.foldr (fun x => max x.rank) 0 l)

Proof state:
self : UnionFind
i : Nat
h : i < self.arr.size
a : UFNode
l : List UFNode
⊢ a.rank ≤ max a.rank (List.foldr (fun x => max x.rank) 0 l)

Tactic:
apply Nat.le_max_left

Result:
no goals

Proof state:
self : UnionFind
i : Nat
h✝ : i < self.arr.size
a : UFNode
l : List UFNode
a✝ : UFNode
h : List.Mem a✝ l
⊢ a✝.rank ≤ List.foldr (fun x => max x.rank) 0 (a :: l)

Tactic:
dsimp

Result:
self : UnionFind
i : Nat
h✝ : i < self.arr.size
a : UFNode
l : List UFNode
a✝ : UFNode
h : List.Mem a✝ l
⊢ a✝.rank ≤ max a.rank (List.foldr (fun x => max x.rank) 0 l)

Proof state:
self : UnionFind
i : Nat
h : i < self.arr.size
⊢ self.arr[i].rank < self.rankMax

Tactic:
simp only [Array.get_eq_getElem, rankMax, ← Array.foldr_toList]

Result:
self : UnionFind
i : Nat
h : i < self.arr.size
⊢ self.arr[i].rank < List.foldr (fun x => max x.rank) 0 self.arr.toList + 1

Proof state:
self : UnionFind
i : Nat
h : i < self.arr.size
⊢ self.arr[i].rank < List.foldr (fun x => max x.rank) 0 self.arr.toList + 1

Tactic:
exact Nat.lt_succ.2 <| go (self.arr.toList.getElem_mem _)

Result:
no goals