harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Data/Nat/Digits.lean
theorem base_pow_length_digits_le (b m : ℕ) (hb : 1 < b) :
    m ≠ 0 → b ^ (digits b m).length ≤ b * m

Proof state:
b m : ℕ
hb : 1 < b
⊢ m ≠ 0 → b ^ (b.digits m).length ≤ b * m

Tactic:
rcases b with (_ | _ | b) <;> try simp_all

Result:
case succ.succ
m b : ℕ
⊢ ¬m = 0 → (b + 1 + 1) ^ ((b + 1 + 1).digits m).length ≤ (b + 1 + 1) * m

Proof state:
case succ.succ
m b : ℕ
⊢ ¬m = 0 → (b + 1 + 1) ^ ((b + 1 + 1).digits m).length ≤ (b + 1 + 1) * m

Tactic:
exact base_pow_length_digits_le' b m

Result:
no goals

Proof state:
case succ.succ
m b : ℕ
hb : 1 < b + 1 + 1
⊢ m ≠ 0 → (b + 1 + 1) ^ ((b + 1 + 1).digits m).length ≤ (b + 1 + 1) * m

Tactic:
simp_all

Result:
case succ.succ
m b : ℕ
⊢ ¬m = 0 → (b + 1 + 1) ^ ((b + 1 + 1).digits m).length ≤ (b + 1 + 1) * m
-- Mathlib/CategoryTheory/Sites/Localization.lean
lemma W_adj_unit_app (adj : G ⊣ sheafToPresheaf J A) (P : Cᵒᵖ ⥤ A) : J.W (adj.unit.app P)

Proof state:
C : Type u_1
inst✝¹ : Category.{u_4, u_1} C
J : GrothendieckTopology C
A : Type u_2
inst✝ : Category.{u_3, u_2} A
G : (Cᵒᵖ ⥤ A) ⥤ Sheaf J A
adj : G ⊣ sheafToPresheaf J A
P : Cᵒᵖ ⥤ A
⊢ LeftBousfield.W (fun x => x ∈ Set.range (sheafToPresheaf J A).obj) (adj.unit.app P)

Tactic:
exact LeftBousfield.W_adj_unit_app adj P

Result:
no goals

Proof state:
C : Type u_1
inst✝¹ : Category.{u_4, u_1} C
J : GrothendieckTopology C
A : Type u_2
inst✝ : Category.{u_3, u_2} A
G : (Cᵒᵖ ⥤ A) ⥤ Sheaf J A
adj : G ⊣ sheafToPresheaf J A
P : Cᵒᵖ ⥤ A
⊢ J.W (adj.unit.app P)

Tactic:
rw [W_eq_W_range_sheafToPresheaf_obj]

Result:
C : Type u_1
inst✝¹ : Category.{u_4, u_1} C
J : GrothendieckTopology C
A : Type u_2
inst✝ : Category.{u_3, u_2} A
G : (Cᵒᵖ ⥤ A) ⥤ Sheaf J A
adj : G ⊣ sheafToPresheaf J A
P : Cᵒᵖ ⥤ A
⊢ LeftBousfield.W (fun x => x ∈ Set.range (sheafToPresheaf J A).obj) (adj.unit.app P)
-- Mathlib/Data/NNReal/Defs.lean
theorem nnabs_of_nonneg {x : ℝ} (h : 0 ≤ x) : nnabs x = toNNReal x

Proof state:
case a
x : ℝ
h : 0 ≤ x
⊢ ↑(nnabs x) = ↑x.toNNReal

Tactic:
rw [coe_toNNReal x h, coe_nnabs, abs_of_nonneg h]

Result:
no goals

Proof state:
x : ℝ
h : 0 ≤ x
⊢ nnabs x = x.toNNReal

Tactic:
ext

Result:
case a
x : ℝ
h : 0 ≤ x
⊢ ↑(nnabs x) = ↑x.toNNReal
-- Mathlib/Combinatorics/SimpleGraph/Clique.lean
theorem CliqueFree.mono (h : m ≤ n) : G.CliqueFree m → G.CliqueFree n

Proof state:
α : Type u_1
G : SimpleGraph α
m n : ℕ
h : m ≤ n
⊢ G.CliqueFree m → G.CliqueFree n

Tactic:
intro hG s hs

Result:
α : Type u_1
G : SimpleGraph α
m n : ℕ
h : m ≤ n
hG : G.CliqueFree m
s : Finset α
hs : G.IsNClique n s
⊢ False

Proof state:
case intro.intro
α : Type u_1
G : SimpleGraph α
m n : ℕ
h : m ≤ n
hG : G.CliqueFree m
s : Finset α
hs : G.IsNClique n s
t : Finset α
hts : t ⊆ s
ht : #t = m
⊢ False

Tactic:
exact hG _ ⟨hs.isClique.subset hts, ht⟩

Result:
no goals

Proof state:
α : Type u_1
G : SimpleGraph α
m n : ℕ
h : m ≤ n
hG : G.CliqueFree m
s : Finset α
hs : G.IsNClique n s
⊢ False

Tactic:
obtain ⟨t, hts, ht⟩ := exists_subset_card_eq (h.trans hs.card_eq.ge)

Result:
case intro.intro
α : Type u_1
G : SimpleGraph α
m n : ℕ
h : m ≤ n
hG : G.CliqueFree m
s : Finset α
hs : G.IsNClique n s
t : Finset α
hts : t ⊆ s
ht : #t = m
⊢ False
-- Mathlib/CategoryTheory/Limits/Shapes/Multiequalizer.lean
theorem hom_ext {W : C} (i j : multicoequalizer I ⟶ W)
    (h : ∀ b, Multicoequalizer.π I b ≫ i = Multicoequalizer.π I b ≫ j) : i = j :=
  colimit.hom_ext
    (by
      rintro (a | b)
      · simp_rw [← colimit.w I.multispan (WalkingMultispan.Hom.fst a), Category.assoc, h]
      · apply h)

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
J : MultispanShape
I : MultispanIndex J C
inst✝ : HasMulticoequalizer I
W : C
i j : multicoequalizer I ⟶ W
h : ∀ (b : J.R), π I b ≫ i = π I b ≫ j
⊢ ∀ (j_1 : WalkingMultispan J), colimit.ι I.multispan j_1 ≫ i = colimit.ι I.multispan j_1 ≫ j

Tactic:
rintro (a | b)

Result:
case left
C : Type u
inst✝¹ : Category.{v, u} C
J : MultispanShape
I : MultispanIndex J C
inst✝ : HasMulticoequalizer I
W : C
i j : multicoequalizer I ⟶ W
h : ∀ (b : J.R), π I b ≫ i = π I b ≫ j
a : J.L
⊢ colimit.ι I.multispan (WalkingMultispan.left a) ≫ i = colimit.ι I.multispan (WalkingMultispan.left a) ≫ j

case right
C : Type u
inst✝¹ : Category.{v, u} C
J : MultispanShape
I : MultispanIndex J C
inst✝ : HasMulticoequalizer I
W : C
i j : multicoequalizer I ⟶ W
h : ∀ (b : J.R), π I b ≫ i = π I b ≫ j
b : J.R
⊢ colimit.ι I.multispan (WalkingMultispan.right b) ≫ i = colimit.ι I.multispan (WalkingMultispan.right b) ≫ j

Proof state:
case right
C : Type u
inst✝¹ : Category.{v, u} C
J : MultispanShape
I : MultispanIndex J C
inst✝ : HasMulticoequalizer I
W : C
i j : multicoequalizer I ⟶ W
h : ∀ (b : J.R), π I b ≫ i = π I b ≫ j
b : J.R
⊢ colimit.ι I.multispan (WalkingMultispan.right b) ≫ i = colimit.ι I.multispan (WalkingMultispan.right b) ≫ j

Tactic:
apply h

Result:
no goals

Proof state:
case left
C : Type u
inst✝¹ : Category.{v, u} C
J : MultispanShape
I : MultispanIndex J C
inst✝ : HasMulticoequalizer I
W : C
i j : multicoequalizer I ⟶ W
h : ∀ (b : J.R), π I b ≫ i = π I b ≫ j
a : J.L
⊢ colimit.ι I.multispan (WalkingMultispan.left a) ≫ i = colimit.ι I.multispan (WalkingMultispan.left a) ≫ j

Tactic:
simp_rw [← colimit.w I.multispan (WalkingMultispan.Hom.fst a), Category.assoc, h]

Result:
no goals
-- Mathlib/Algebra/Group/Basic.lean
theorem mul_div_left_comm : a * (b / c) = b * (a / c)

Proof state:
α : Type u_1
inst✝ : DivisionCommMonoid α
a b c : α
⊢ a * (b / c) = b * (a / c)

Tactic:
simp

Result:
no goals
-- Mathlib/Algebra/MvPolynomial/CommRing.lean
theorem eval₂Hom_X {R : Type u} (c : ℤ →+* S) (f : MvPolynomial R ℤ →+* S) (x : MvPolynomial R ℤ) :
    eval₂ c (f ∘ X) x = f x

Proof state:
S : Type v
inst✝ : CommRing S
R : Type u
c : ℤ →+* S
f : MvPolynomial R ℤ →+* S
x : MvPolynomial R ℤ
n : ℤ
⊢ c n = ↑n

Tactic:
exact eq_intCast c n

Result:
no goals

Proof state:
S : Type v
inst✝ : CommRing S
R : Type u
c : ℤ →+* S
f : MvPolynomial R ℤ →+* S
x : MvPolynomial R ℤ
⊢ eval₂ c (⇑f ∘ X) x = f x

Tactic:
apply MvPolynomial.induction_on x
  (fun n => by
    rw [hom_C f, eval₂_C]
    exact eq_intCast c n)
  (fun p q hp hq => by
    rw [eval₂_add, hp, hq]
    exact (f.map_add _ _).symm)
  (fun p n hp => by
    rw [eval₂_mul, eval₂_X, hp]
    exact (f.map_mul _ _).symm)

Result:
no goals

Proof state:
S : Type v
inst✝ : CommRing S
R : Type u
c : ℤ →+* S
f : MvPolynomial R ℤ →+* S
x p : MvPolynomial R ℤ
n : R
hp : eval₂ c (⇑f ∘ X) p = f p
⊢ f p * (⇑f ∘ X) n = f (p * X n)

Tactic:
exact (f.map_mul _ _).symm

Result:
no goals

Proof state:
S : Type v
inst✝ : CommRing S
R : Type u
c : ℤ →+* S
f : MvPolynomial R ℤ →+* S
x p q : MvPolynomial R ℤ
hp : eval₂ c (⇑f ∘ X) p = f p
hq : eval₂ c (⇑f ∘ X) q = f q
⊢ f p + f q = f (p + q)

Tactic:
exact (f.map_add _ _).symm

Result:
no goals

Proof state:
S : Type v
inst✝ : CommRing S
R : Type u
c : ℤ →+* S
f : MvPolynomial R ℤ →+* S
x p : MvPolynomial R ℤ
n : R
hp : eval₂ c (⇑f ∘ X) p = f p
⊢ eval₂ c (⇑f ∘ X) (p * X n) = f (p * X n)

Tactic:
rw [eval₂_mul, eval₂_X, hp]

Result:
S : Type v
inst✝ : CommRing S
R : Type u
c : ℤ →+* S
f : MvPolynomial R ℤ →+* S
x p : MvPolynomial R ℤ
n : R
hp : eval₂ c (⇑f ∘ X) p = f p
⊢ f p * (⇑f ∘ X) n = f (p * X n)

Proof state:
S : Type v
inst✝ : CommRing S
R : Type u
c : ℤ →+* S
f : MvPolynomial R ℤ →+* S
x : MvPolynomial R ℤ
n : ℤ
⊢ eval₂ c (⇑f ∘ X) (C n) = f (C n)

Tactic:
rw [hom_C f, eval₂_C]

Result:
S : Type v
inst✝ : CommRing S
R : Type u
c : ℤ →+* S
f : MvPolynomial R ℤ →+* S
x : MvPolynomial R ℤ
n : ℤ
⊢ c n = ↑n

Proof state:
S : Type v
inst✝ : CommRing S
R : Type u
c : ℤ →+* S
f : MvPolynomial R ℤ →+* S
x p q : MvPolynomial R ℤ
hp : eval₂ c (⇑f ∘ X) p = f p
hq : eval₂ c (⇑f ∘ X) q = f q
⊢ eval₂ c (⇑f ∘ X) (p + q) = f (p + q)

Tactic:
rw [eval₂_add, hp, hq]

Result:
S : Type v
inst✝ : CommRing S
R : Type u
c : ℤ →+* S
f : MvPolynomial R ℤ →+* S
x p q : MvPolynomial R ℤ
hp : eval₂ c (⇑f ∘ X) p = f p
hq : eval₂ c (⇑f ∘ X) q = f q
⊢ f p + f q = f (p + q)
-- Mathlib/Algebra/Module/Presentation/Basic.lean
lemma isPresentation {solution : relations.Solution M}
    (h : IsPresentationCore.{max u v w₀} solution) :
    solution.IsPresentation where
  bijective

Proof state:
A : Type u
inst✝² : Ring A
relations : Relations A
M : Type v
inst✝¹ : AddCommGroup M
inst✝ : Module A M
solution : relations.Solution M
h : solution.IsPresentationCore
⊢ h.down.desc (ofQuotient relations) ∘ₗ solution.fromQuotient = LinearMap.id

Tactic:
aesop

Result:
no goals

Proof state:
A : Type u
inst✝² : Ring A
relations : Relations A
M : Type v
inst✝¹ : AddCommGroup M
inst✝ : Module A M
solution : relations.Solution M
h : solution.IsPresentationCore
⊢ Function.Bijective ⇑solution.fromQuotient

Tactic:
let e : relations.Quotient ≃ₗ[A] M :=
  LinearEquiv.ofLinear solution.fromQuotient
  ((down.{v} h).desc (ofQuotient relations))
  ((down.{max u w₀} h).postcomp_injective (by aesop)) (by aesop)

Result:
A : Type u
inst✝² : Ring A
relations : Relations A
M : Type v
inst✝¹ : AddCommGroup M
inst✝ : Module A M
solution : relations.Solution M
h : solution.IsPresentationCore
e : relations.Quotient ≃ₗ[A] M := LinearEquiv.ofLinear solution.fromQuotient (h.down.desc (ofQuotient relations)) ⋯ ⋯
⊢ Function.Bijective ⇑solution.fromQuotient

Proof state:
A : Type u
inst✝² : Ring A
relations : Relations A
M : Type v
inst✝¹ : AddCommGroup M
inst✝ : Module A M
solution : relations.Solution M
h : solution.IsPresentationCore
⊢ solution.postcomp (solution.fromQuotient ∘ₗ h.down.desc (ofQuotient relations)) = solution.postcomp LinearMap.id

Tactic:
aesop

Result:
no goals

Proof state:
A : Type u
inst✝² : Ring A
relations : Relations A
M : Type v
inst✝¹ : AddCommGroup M
inst✝ : Module A M
solution : relations.Solution M
h : solution.IsPresentationCore
e : relations.Quotient ≃ₗ[A] M := LinearEquiv.ofLinear solution.fromQuotient (h.down.desc (ofQuotient relations)) ⋯ ⋯
⊢ Function.Bijective ⇑solution.fromQuotient

Tactic:
exact e.bijective

Result:
no goals
-- Mathlib/Data/Sign.lean
theorem pos_iff {a : SignType} : 0 < a ↔ a = 1

Proof state:
a : SignType
⊢ 0 < a ↔ a = 1

Tactic:
cases a <;> decide

Result:
no goals
-- Mathlib/CategoryTheory/Limits/Shapes/Diagonal.lean
theorem diagonal_pullback_fst {X Y Z : C} (f : X ⟶ Z) (g : Y ⟶ Z) :
    diagonal (pullback.fst f g) =
      (pullbackSymmetry _ _).hom ≫
        ((Over.pullback f).map
              (Over.homMk (diagonal g) : Over.mk g ⟶ Over.mk (pullback.snd _ _ ≫ g))).left ≫
          (diagonalObjPullbackFstIso f g).inv

Proof state:
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : HasPullbacks C
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
⊢ diagonal (fst f g) =
    (pullbackSymmetry f (Over.mk g).hom).hom ≫
      ((Over.pullback f).map (Over.homMk (diagonal g) ⋯)).left ≫ (diagonalObjPullbackFstIso f g).inv

Tactic:
ext <;> dsimp <;> simp

Result:
no goals
-- Mathlib/LinearAlgebra/Matrix/Permutation.lean
theorem trace_permutation [AddCommMonoidWithOne R] :
    trace (σ.permMatrix R) = (Function.fixedPoints σ).ncard

Proof state:
n : Type u_1
R : Type u_2
inst✝² : DecidableEq n
σ : Perm n
inst✝¹ : Fintype n
inst✝ : AddCommMonoidWithOne R
⊢ ∑ i : n, (Perm.permMatrix R σ).diag i = ↑(Function.fixedPoints ⇑σ).ncard

Tactic:
simp [toPEquiv_apply, ← Set.ncard_coe_Finset, Function.fixedPoints, Function.IsFixedPt]

Result:
no goals

Proof state:
n : Type u_1
R : Type u_2
inst✝² : DecidableEq n
σ : Perm n
inst✝¹ : Fintype n
inst✝ : AddCommMonoidWithOne R
⊢ (Perm.permMatrix R σ).trace = ↑(Function.fixedPoints ⇑σ).ncard

Tactic:
delta trace

Result:
n : Type u_1
R : Type u_2
inst✝² : DecidableEq n
σ : Perm n
inst✝¹ : Fintype n
inst✝ : AddCommMonoidWithOne R
⊢ ∑ i : n, (Perm.permMatrix R σ).diag i = ↑(Function.fixedPoints ⇑σ).ncard
-- Mathlib/LinearAlgebra/Lagrange.lean
theorem sum_nodalWeight_mul_inv_sub_ne_zero (hvs : Set.InjOn v s) (hx : ∀ i ∈ s, x ≠ v i)
    (hs : s.Nonempty) : (∑ i ∈ s, nodalWeight s v i * (x - v i)⁻¹) ≠ 0 :=
  @right_ne_zero_of_mul_eq_one _ _ _ (eval x (nodal s v)) _ <| by
    simpa only [Pi.one_apply, interpolate_one hvs hs, eval_one, mul_one] using
      (eval_interpolate_not_at_node 1 hx).symm

Proof state:
F : Type u_1
inst✝¹ : Field F
ι : Type u_2
inst✝ : DecidableEq ι
s : Finset ι
v : ι → F
x : F
hvs : Set.InjOn v ↑s
hx : ∀ i ∈ s, x ≠ v i
hs : s.Nonempty
⊢ eval x (nodal s v) * ∑ i ∈ s, nodalWeight s v i * (x - v i)⁻¹ = 1

Tactic:
simpa only [Pi.one_apply, interpolate_one hvs hs, eval_one, mul_one] using
  (eval_interpolate_not_at_node 1 hx).symm

Result:
no goals
-- Mathlib/RingTheory/UniqueFactorizationDomain/FactorSet.lean
theorem factors_eq_some_iff_ne_zero {a : Associates α} :
    (∃ s : Multiset { p : Associates α // Irreducible p }, a.factors = s) ↔ a ≠ 0

Proof state:
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
a : Associates α
⊢ (∃ s, a.factors = ↑s) ↔ a ≠ 0

Tactic:
simp_rw [@eq_comm _ a.factors, ← WithTop.ne_top_iff_exists]

Result:
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
a : Associates α
⊢ a.factors ≠ ⊤ ↔ a ≠ 0

Proof state:
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
a : Associates α
⊢ a.factors ≠ ⊤ ↔ a ≠ 0

Tactic:
exact factors_eq_top_iff_zero.not

Result:
no goals
-- Mathlib/LinearAlgebra/Matrix/NonsingularInverse.lean
theorem det_conj {M : Matrix m m α} (h : IsUnit M) (N : Matrix m m α) :
    det (M * N * M⁻¹) = det N

Proof state:
m : Type u
α : Type v
inst✝² : CommRing α
inst✝¹ : Fintype m
inst✝ : DecidableEq m
M : Matrix m m α
h : IsUnit M
N : Matrix m m α
⊢ (M * N * M⁻¹).det = N.det

Tactic:
rw [← h.unit_spec, ← coe_units_inv, det_units_conj]

Result:
no goals
-- Mathlib/Order/Filter/Partial.lean
theorem ptendsto_of_ptendsto' {f : α →. β} {l₁ : Filter α} {l₂ : Filter β} :
    PTendsto' f l₁ l₂ → PTendsto f l₁ l₂

Proof state:
α : Type u
β : Type v
f : α →. β
l₁ : Filter α
l₂ : Filter β
⊢ PTendsto' f l₁ l₂ → PTendsto f l₁ l₂

Tactic:
rw [ptendsto_def, ptendsto'_def]

Result:
α : Type u
β : Type v
f : α →. β
l₁ : Filter α
l₂ : Filter β
⊢ (∀ s ∈ l₂, f.preimage s ∈ l₁) → ∀ s ∈ l₂, f.core s ∈ l₁

Proof state:
α : Type u
β : Type v
f : α →. β
l₁ : Filter α
l₂ : Filter β
⊢ (∀ s ∈ l₂, f.preimage s ∈ l₁) → ∀ s ∈ l₂, f.core s ∈ l₁

Tactic:
exact fun h s sl₂ => mem_of_superset (h s sl₂) (PFun.preimage_subset_core _ _)

Result:
no goals
-- Mathlib/Algebra/Quaternion.lean
theorem normSq_coe : normSq (x : ℍ[R]) = x ^ 2

Proof state:
R : Type u_3
inst✝ : CommRing R
x : R
⊢ normSq ↑x = x ^ 2

Tactic:
rw [normSq_def, star_coe, ← coe_mul, coe_re, sq]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Bool.lean
theorem or_left_comm : ∀ (x y z : Bool), (x || (y || z)) = (y || (x || z))

Proof state:
⊢ ∀ (x y z : Bool), (x || (y || z)) = (y || (x || z))

Tactic:
decide

Result:
no goals
-- Mathlib/.lake/packages/batteries/Batteries/Classes/SatisfiesM.lean
theorem imp [Functor m] [LawfulFunctor m] {x : m α}
    (h : SatisfiesM p x) (H : ∀ {a}, p a → q a) : SatisfiesM q x :=
  let ⟨x, h⟩ := h; ⟨(fun ⟨_, h⟩ => ⟨_, H h⟩) <$> x, by rw [← h, ← comp_map]; rfl⟩

Proof state:
m : Type u_1 → Type u_2
α : Type u_1
p q : α → Prop
inst✝¹ : Functor m
inst✝ : LawfulFunctor m
x✝ : m α
h✝ : SatisfiesM p x✝
H : ∀ {a : α}, p a → q a
x : m { a // p a }
h : Subtype.val <$> x = x✝
⊢ Subtype.val <$>
      (fun x =>
          match x with
          | ⟨val, h⟩ => ⟨val, ⋯⟩) <$>
        x =
    x✝

Tactic:
rw [← h, ← comp_map]

Result:
m : Type u_1 → Type u_2
α : Type u_1
p q : α → Prop
inst✝¹ : Functor m
inst✝ : LawfulFunctor m
x✝ : m α
h✝ : SatisfiesM p x✝
H : ∀ {a : α}, p a → q a
x : m { a // p a }
h : Subtype.val <$> x = x✝
⊢ (Subtype.val ∘ fun x =>
        match x with
        | ⟨val, h⟩ => ⟨val, ⋯⟩) <$>
      x =
    Subtype.val <$> x

Proof state:
m : Type u_1 → Type u_2
α : Type u_1
p q : α → Prop
inst✝¹ : Functor m
inst✝ : LawfulFunctor m
x✝ : m α
h✝ : SatisfiesM p x✝
H : ∀ {a : α}, p a → q a
x : m { a // p a }
h : Subtype.val <$> x = x✝
⊢ (Subtype.val ∘ fun x =>
        match x with
        | ⟨val, h⟩ => ⟨val, ⋯⟩) <$>
      x =
    Subtype.val <$> x

Tactic:
rfl

Result:
no goals
-- Mathlib/Data/Matroid/Constructions.lean
theorem eq_freeOn_iff : M = freeOn E ↔ M.E = E ∧ M.Indep E

Proof state:
case refine_1
α : Type u_1
E : Set α
⊢ (freeOn E).E = E ∧ (freeOn E).Indep E

Tactic:
simp [Subset.rfl]

Result:
no goals

Proof state:
case refine_1
α : Type u_1
M : Matroid α
E : Set α
⊢ M = freeOn E → M.E = E ∧ M.Indep E

Tactic:
rintro rfl

Result:
case refine_1
α : Type u_1
E : Set α
⊢ (freeOn E).E = E ∧ (freeOn E).Indep E

Proof state:
case refine_2
α : Type u_1
M : Matroid α
E : Set α
h : M.E = E ∧ M.Indep E
⊢ M = freeOn E

Tactic:
simp only [ext_iff_indep, freeOn_ground, freeOn_indep_iff, h.1, true_and]

Result:
case refine_2
α : Type u_1
M : Matroid α
E : Set α
h : M.E = E ∧ M.Indep E
⊢ ∀ ⦃I : Set α⦄, I ⊆ E → (M.Indep I ↔ I ⊆ E)

Proof state:
α : Type u_1
M : Matroid α
E : Set α
⊢ M = freeOn E ↔ M.E = E ∧ M.Indep E

Tactic:
refine ⟨?_, fun h ↦ ?_⟩

Result:
case refine_1
α : Type u_1
M : Matroid α
E : Set α
⊢ M = freeOn E → M.E = E ∧ M.Indep E

case refine_2
α : Type u_1
M : Matroid α
E : Set α
h : M.E = E ∧ M.Indep E
⊢ M = freeOn E

Proof state:
case refine_2
α : Type u_1
M : Matroid α
E : Set α
h : M.E = E ∧ M.Indep E
⊢ ∀ ⦃I : Set α⦄, I ⊆ E → (M.Indep I ↔ I ⊆ E)

Tactic:
exact fun I hIX ↦ iff_of_true (h.2.subset hIX) hIX

Result:
no goals
-- Mathlib/GroupTheory/Coset/Basic.lean
@[to_additive]
lemma rightRel_pi {ι : Type*} {β : ι → Type*} [∀ i, Group (β i)] (s' : ∀ i, Subgroup (β i)) :
    rightRel (Subgroup.pi Set.univ s') = @piSetoid _ _ fun i ↦ rightRel (s' i)

Proof state:
ι : Type u_2
β : ι → Type u_3
inst✝ : (i : ι) → Group (β i)
s' : (i : ι) → Subgroup (β i)
⊢ rightRel (Subgroup.pi univ s') = piSetoid

Tactic:
refine Setoid.ext fun x y ↦ ?_

Result:
ι : Type u_2
β : ι → Type u_3
inst✝ : (i : ι) → Group (β i)
s' : (i : ι) → Subgroup (β i)
x y : (i : ι) → β i
⊢ (rightRel (Subgroup.pi univ s')) x y ↔ piSetoid x y

Proof state:
ι : Type u_2
β : ι → Type u_3
inst✝ : (i : ι) → Group (β i)
s' : (i : ι) → Subgroup (β i)
x y : (i : ι) → β i
⊢ (rightRel (Subgroup.pi univ s')) x y ↔ piSetoid x y

Tactic:
simp [Setoid.piSetoid_apply, rightRel_apply, Subgroup.mem_pi]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Integrals.lean
theorem integral_id : ∫ x in a..b, x = (b ^ 2 - a ^ 2) / 2

Proof state:
a b : ℝ
this : ∫ (x : ℝ) in a..b, x = (b ^ 2 - a ^ 2) / 2
⊢ ∫ (x : ℝ) in a..b, x = (b ^ 2 - a ^ 2) / 2

Tactic:
exact this

Result:
no goals

Proof state:
a b : ℝ
⊢ ∫ (x : ℝ) in a..b, x = (b ^ 2 - a ^ 2) / 2

Tactic:
have := @integral_pow a b 1

Result:
a b : ℝ
this : ∫ (x : ℝ) in a..b, x ^ 1 = (b ^ (1 + 1) - a ^ (1 + 1)) / (↑1 + 1)
⊢ ∫ (x : ℝ) in a..b, x = (b ^ 2 - a ^ 2) / 2

Proof state:
a b : ℝ
this : ∫ (x : ℝ) in a..b, x ^ 1 = (b ^ (1 + 1) - a ^ (1 + 1)) / (↑1 + 1)
⊢ ∫ (x : ℝ) in a..b, x = (b ^ 2 - a ^ 2) / 2

Tactic:
norm_num at this

Result:
a b : ℝ
this : ∫ (x : ℝ) in a..b, x = (b ^ 2 - a ^ 2) / 2
⊢ ∫ (x : ℝ) in a..b, x = (b ^ 2 - a ^ 2) / 2
-- Mathlib/AlgebraicGeometry/EllipticCurve/DivisionPolynomial/Basic.lean
lemma baseChange_Ψ₃ : (W.baseChange B).Ψ₃ = (W.baseChange A).Ψ₃.map f

Proof state:
R : Type r
S : Type s
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing S
W : WeierstrassCurve R
inst✝⁸ : Algebra R S
A : Type u
inst✝⁷ : CommRing A
inst✝⁶ : Algebra R A
inst✝⁵ : Algebra S A
inst✝⁴ : IsScalarTower R S A
B : Type v
inst✝³ : CommRing B
inst✝² : Algebra R B
inst✝¹ : Algebra S B
inst✝ : IsScalarTower R S B
f : A →ₐ[S] B
⊢ (W.baseChange B).Ψ₃ = Polynomial.map (↑f) (W.baseChange A).Ψ₃

Tactic:
rw [← map_Ψ₃, map_baseChange]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/RawLemmas.lean
theorem getD_insertMany_list_of_mem [LawfulBEq α] (h : m.1.WF)
    {l : List ((a : α) × β a)} {k k' : α} (k_beq : k == k') {v : β k} {fallback : β k'}
    (distinct : l.Pairwise (fun a b => (a.1 == b.1) = false))
    (mem : ⟨k, v⟩ ∈ l) :
    (m.insertMany l).1.getD k' fallback = cast (by congr; apply LawfulBEq.eq_of_beq k_beq) v

Proof state:
α : Type u
β : α → Type v
m : Raw₀ α β
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : LawfulBEq α
h : m.val.WF
l : List ((a : α) × β a)
k k' : α
k_beq : (k == k') = true
v : β k
fallback : β k'
distinct : List.Pairwise (fun a b => (a.fst == b.fst) = false) l
mem : ⟨k, v⟩ ∈ l
⊢ (m.insertMany l).val.getD k' fallback = cast ⋯ v

Tactic:
simp_to_model [insertMany] using List.getValueCastD_insertList_of_mem

Result:
no goals

Proof state:
α : Type u
β : α → Type v
m : Raw₀ α β
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : LawfulBEq α
h : m.val.WF
l : List ((a : α) × β a)
k k' : α
k_beq : (k == k') = true
v : β k
fallback : β k'
distinct : List.Pairwise (fun a b => (a.fst == b.fst) = false) l
mem : ⟨k, v⟩ ∈ l
⊢ β k = β k'

Tactic:
congr

Result:
case e_a
α : Type u
β : α → Type v
m : Raw₀ α β
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : LawfulBEq α
h : m.val.WF
l : List ((a : α) × β a)
k k' : α
k_beq : (k == k') = true
v : β k
fallback : β k'
distinct : List.Pairwise (fun a b => (a.fst == b.fst) = false) l
mem : ⟨k, v⟩ ∈ l
⊢ k = k'

Proof state:
case e_a
α : Type u
β : α → Type v
m : Raw₀ α β
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : LawfulBEq α
h : m.val.WF
l : List ((a : α) × β a)
k k' : α
k_beq : (k == k') = true
v : β k
fallback : β k'
distinct : List.Pairwise (fun a b => (a.fst == b.fst) = false) l
mem : ⟨k, v⟩ ∈ l
⊢ k = k'

Tactic:
apply LawfulBEq.eq_of_beq k_beq

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Nat/SOM.lean
theorem Mon.append_denote (ctx : Context) (m₁ m₂ : Mon) : (m₁ ++ m₂).denote ctx = m₁.denote ctx * m₂.denote ctx

Proof state:
ctx : Context
m₁✝ m₂ : Mon
v : Var
m₁ : List Var
⊢ denote ctx (v :: m₁ ++ m₂) = denote ctx (v :: m₁) * denote ctx m₂

Tactic:
simp! [append_denote ctx m₁ m₂, Nat.mul_assoc]

Result:
no goals

Proof state:
ctx : Context
m₁ m₂ : Mon
⊢ denote ctx (m₁ ++ m₂) = denote ctx m₁ * denote ctx m₂

Tactic:
match m₁ with
| [] => simp! [Nat.one_mul]
| v :: m₁ => simp! [append_denote ctx m₁ m₂, Nat.mul_assoc]

Result:
no goals

Proof state:
ctx : Context
m₁ m₂ : Mon
⊢ denote ctx ([] ++ m₂) = denote ctx [] * denote ctx m₂

Tactic:
simp! [Nat.one_mul]

Result:
no goals
-- Mathlib/.lake/packages/batteries/Batteries/Data/RBMap/WF.lean
theorem reverse_setBlack {t : RBNode α} : (setBlack t).reverse = setBlack t.reverse

Proof state:
α : Type u_1
t : RBNode α
⊢ t.setBlack.reverse = t.reverse.setBlack

Tactic:
unfold setBlack

Result:
α : Type u_1
t : RBNode α
⊢ (match t with
      | nil => nil
      | node c l v r => node black l v r).reverse =
    match t.reverse with
    | nil => nil
    | node c l v r => node black l v r

Proof state:
α : Type u_1
t : RBNode α
⊢ (match t with
      | nil => nil
      | node c l v r => node black l v r).reverse =
    match t.reverse with
    | nil => nil
    | node c l v r => node black l v r

Tactic:
split <;> simp

Result:
no goals
-- Mathlib/Algebra/Lie/Submodule.lean
theorem incl_idealRange : I.incl.idealRange = I

Proof state:
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
I : LieIdeal R L
⊢ I.incl.idealRange = I

Tactic:
rw [LieHom.idealRange_eq_lieSpan_range, ← LieSubalgebra.coe_toSubmodule, ←
  LieSubmodule.toSubmodule_inj, incl_range, toLieSubalgebra_toSubmodule,
  LieSubmodule.coe_lieSpan_submodule_eq_iff]

Result:
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
I : LieIdeal R L
⊢ ∃ N, ↑N = ↑I

Proof state:
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
I : LieIdeal R L
⊢ ∃ N, ↑N = ↑I

Tactic:
use I

Result:
no goals
-- Mathlib/RingTheory/TwoSidedIdeal/Lattice.lean
lemma mem_iInf {ι : Type*} {I : ι → TwoSidedIdeal R} {x : R} :
    x ∈ iInf I ↔ ∀ i, x ∈ I i :=
  show (∀ _, _) ↔ _ by simp [mem_iff]

Proof state:
R : Type u_1
inst✝ : NonUnitalNonAssocRing R
ι : Type u_2
I : ι → TwoSidedIdeal R
x : R
⊢ (∀ x_1 ∈ ringCon '' Set.range I, x_1 x 0) ↔ ∀ (i : ι), x ∈ I i

Tactic:
simp [mem_iff]

Result:
no goals
-- Mathlib/Algebra/NoZeroSMulDivisors/Basic.lean
theorem self_eq_neg
    (R) (M) [Semiring R] [CharZero R] [AddCommGroup M] [Module R M] [NoZeroSMulDivisors R M]
    {v : M} : v = -v ↔ v = 0

Proof state:
R : Type u_3
M : Type u_4
inst✝⁴ : Semiring R
inst✝³ : CharZero R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : NoZeroSMulDivisors R M
v : M
⊢ v = -v ↔ v = 0

Tactic:
rw [← two_nsmul_eq_zero R M, two_smul, add_eq_zero_iff_eq_neg]

Result:
no goals