harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Data/Nat/Log.lean
theorem log_div_mul_self (b n : ℕ) : log b (n / b * b) = log b n

Proof state:
b n : ℕ
⊢ log b (n / b * b) = log b n

Tactic:
rcases le_or_lt b 1 with hb | hb

Result:
case inl
b n : ℕ
hb : b ≤ 1
⊢ log b (n / b * b) = log b n

case inr
b n : ℕ
hb : 1 < b
⊢ log b (n / b * b) = log b n

Proof state:
b n : ℕ
hb : 1 < b
h : b ≤ n
⊢ 0 < b

Tactic:
omega

Result:
no goals

Proof state:
case inr.inr
b n : ℕ
hb : 1 < b
h : b ≤ n
⊢ log b (n / b * b) = log b n

Tactic:
rw [log_mul_base hb (Nat.div_pos h (by omega)).ne', log_div_base,
  Nat.sub_add_cancel (succ_le_iff.2 <| log_pos hb h)]

Result:
no goals

Proof state:
case inr.inl
b n : ℕ
hb : 1 < b
h : n < b
⊢ log b (n / b * b) = log b n

Tactic:
rw [div_eq_of_lt h, Nat.zero_mul, log_zero_right, log_of_lt h]

Result:
no goals

Proof state:
case inr
b n : ℕ
hb : 1 < b
⊢ log b (n / b * b) = log b n

Tactic:
rcases lt_or_le n b with h | h

Result:
case inr.inl
b n : ℕ
hb : 1 < b
h : n < b
⊢ log b (n / b * b) = log b n

case inr.inr
b n : ℕ
hb : 1 < b
h : b ≤ n
⊢ log b (n / b * b) = log b n

Proof state:
case inl
b n : ℕ
hb : b ≤ 1
⊢ log b (n / b * b) = log b n

Tactic:
rw [log_of_left_le_one hb, log_of_left_le_one hb]

Result:
no goals
-- Mathlib/NumberTheory/Zsqrtd/QuadraticReciprocity.lean
theorem prime_of_nat_prime_of_mod_four_eq_three (p : ℕ) [Fact p.Prime] (hp3 : p % 4 = 3) :
    Prime (p : ℤ[i]) :=
  irreducible_iff_prime.1 <|
    by_contradiction fun hpi =>
      let ⟨a, b, hab⟩ := sq_add_sq_of_nat_prime_of_not_irreducible p hpi
      have : ∀ a b : ZMod 4, a ^ 2 + b ^ 2 ≠ (p : ZMod 4)

Proof state:
p : ℕ
inst✝ : Fact (Nat.Prime p)
hp3 : p % 4 = 3
hpi : ¬Irreducible ↑p
a b : ℕ
hab : a ^ 2 + b ^ 2 = p
⊢ ∀ (a b : ZMod 4), a ^ 2 + b ^ 2 ≠ ↑p

Tactic:
rw [← ZMod.natCast_mod p 4, hp3]

Result:
p : ℕ
inst✝ : Fact (Nat.Prime p)
hp3 : p % 4 = 3
hpi : ¬Irreducible ↑p
a b : ℕ
hab : a ^ 2 + b ^ 2 = p
⊢ ∀ (a b : ZMod 4), a ^ 2 + b ^ 2 ≠ ↑3

Proof state:
p : ℕ
inst✝ : Fact (Nat.Prime p)
hp3 : p % 4 = 3
hpi : ¬Irreducible ↑p
a b : ℕ
hab : a ^ 2 + b ^ 2 = p
this : ∀ (a b : ZMod 4), a ^ 2 + b ^ 2 ≠ ↑p
⊢ ↑a ^ 2 + ↑b ^ 2 = ↑(a ^ 2 + b ^ 2)

Tactic:
simp

Result:
no goals

Proof state:
p : ℕ
inst✝ : Fact (Nat.Prime p)
hp3 : p % 4 = 3
hpi : ¬Irreducible ↑p
a b : ℕ
hab : a ^ 2 + b ^ 2 = p
⊢ ∀ (a b : ZMod 4), a ^ 2 + b ^ 2 ≠ ↑3

Tactic:
decide

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem setIfInBounds_mkArray_self : (mkArray n a).setIfInBounds i a = mkArray n a

Proof state:
case h
n : Nat
α✝ : Type u_1
a : α✝
i : Nat
⊢ ((mkArray n a).setIfInBounds i a).toList = (mkArray n a).toList

Tactic:
simp

Result:
no goals

Proof state:
n : Nat
α✝ : Type u_1
a : α✝
i : Nat
⊢ (mkArray n a).setIfInBounds i a = mkArray n a

Tactic:
apply Array.ext'

Result:
case h
n : Nat
α✝ : Type u_1
a : α✝
i : Nat
⊢ ((mkArray n a).setIfInBounds i a).toList = (mkArray n a).toList
-- Mathlib/AlgebraicTopology/AlternatingFaceMapComplex.lean
theorem obj_d_eq (X : SimplicialObject C) (n : ℕ) :
    (AlternatingFaceMapComplex.obj X).d (n + 1) n
      = ∑ i : Fin (n + 2), (-1 : ℤ) ^ (i : ℕ) • X.δ i

Proof state:
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
n : ℕ
⊢ (obj X).d (n + 1) n = ∑ i : Fin (n + 2), (-1) ^ ↑i • X.δ i

Tactic:
apply ChainComplex.of_d

Result:
no goals
-- Mathlib/MeasureTheory/Constructions/Cylinders.lean
theorem inter_cylinder (s₁ s₂ : Finset ι) (S₁ : Set (∀ i : s₁, α i)) (S₂ : Set (∀ i : s₂, α i))
    [DecidableEq ι] :
    cylinder s₁ S₁ ∩ cylinder s₂ S₂ =
      cylinder (s₁ ∪ s₂)
        (Finset.restrict₂ Finset.subset_union_left ⁻¹' S₁ ∩
          Finset.restrict₂ Finset.subset_union_right ⁻¹' S₂)

Proof state:
ι : Type u_1
α : ι → Type u_2
s₁ s₂ : Finset ι
S₁ : Set ((i : { x // x ∈ s₁ }) → α ↑i)
S₂ : Set ((i : { x // x ∈ s₂ }) → α ↑i)
inst✝ : DecidableEq ι
⊢ cylinder s₁ S₁ ∩ cylinder s₂ S₂ = cylinder (s₁ ∪ s₂) (Finset.restrict₂ ⋯ ⁻¹' S₁ ∩ Finset.restrict₂ ⋯ ⁻¹' S₂)

Tactic:
ext1 f

Result:
case h
ι : Type u_1
α : ι → Type u_2
s₁ s₂ : Finset ι
S₁ : Set ((i : { x // x ∈ s₁ }) → α ↑i)
S₂ : Set ((i : { x // x ∈ s₂ }) → α ↑i)
inst✝ : DecidableEq ι
f : (i : ι) → α i
⊢ f ∈ cylinder s₁ S₁ ∩ cylinder s₂ S₂ ↔ f ∈ cylinder (s₁ ∪ s₂) (Finset.restrict₂ ⋯ ⁻¹' S₁ ∩ Finset.restrict₂ ⋯ ⁻¹' S₂)

Proof state:
case h
ι : Type u_1
α : ι → Type u_2
s₁ s₂ : Finset ι
S₁ : Set ((i : { x // x ∈ s₁ }) → α ↑i)
S₂ : Set ((i : { x // x ∈ s₂ }) → α ↑i)
inst✝ : DecidableEq ι
f : (i : ι) → α i
⊢ s₁.restrict f ∈ S₁ ∧ s₂.restrict f ∈ S₂ ↔
    (s₁ ∪ s₂).restrict f ∈ Finset.restrict₂ ⋯ ⁻¹' S₁ ∧ (s₁ ∪ s₂).restrict f ∈ Finset.restrict₂ ⋯ ⁻¹' S₂

Tactic:
rfl

Result:
no goals

Proof state:
case h
ι : Type u_1
α : ι → Type u_2
s₁ s₂ : Finset ι
S₁ : Set ((i : { x // x ∈ s₁ }) → α ↑i)
S₂ : Set ((i : { x // x ∈ s₂ }) → α ↑i)
inst✝ : DecidableEq ι
f : (i : ι) → α i
⊢ f ∈ cylinder s₁ S₁ ∩ cylinder s₂ S₂ ↔ f ∈ cylinder (s₁ ∪ s₂) (Finset.restrict₂ ⋯ ⁻¹' S₁ ∩ Finset.restrict₂ ⋯ ⁻¹' S₂)

Tactic:
simp only [mem_inter_iff, mem_cylinder, mem_setOf_eq]

Result:
case h
ι : Type u_1
α : ι → Type u_2
s₁ s₂ : Finset ι
S₁ : Set ((i : { x // x ∈ s₁ }) → α ↑i)
S₂ : Set ((i : { x // x ∈ s₂ }) → α ↑i)
inst✝ : DecidableEq ι
f : (i : ι) → α i
⊢ s₁.restrict f ∈ S₁ ∧ s₂.restrict f ∈ S₂ ↔
    (s₁ ∪ s₂).restrict f ∈ Finset.restrict₂ ⋯ ⁻¹' S₁ ∧ (s₁ ∪ s₂).restrict f ∈ Finset.restrict₂ ⋯ ⁻¹' S₂
-- Mathlib/GroupTheory/Perm/Centralizer.lean
/-- The number of cycles of given length -/
lemma card_of_cycleType_singleton {n : ℕ} (hn' : 2 ≤ n) (hα : n ≤ card α) :
    ({g | g.cycleType = {n}} : Finset (Perm α)).card = (n - 1)! * (choose (card α) n)

Proof state:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
n : ℕ
hn' : 2 ≤ n
hα : n ≤ card α
hn₀ : n ≠ 0
⊢ (Finset.filter (fun g => g.cycleType = {n}) Finset.univ).card = (n - 1)! * (card α).choose n

Tactic:
have aux : n ! = (n - 1)! * n := by rw [mul_comm, mul_factorial_pred (by omega)]

Result:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
n : ℕ
hn' : 2 ≤ n
hα : n ≤ card α
hn₀ : n ≠ 0
aux : n ! = (n - 1)! * n
⊢ (Finset.filter (fun g => g.cycleType = {n}) Finset.univ).card = (n - 1)! * (card α).choose n

Proof state:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
n : ℕ
hn' : 2 ≤ n
hα : n ≤ card α
⊢ (Finset.filter (fun g => g.cycleType = {n}) Finset.univ).card = (n - 1)! * (card α).choose n

Tactic:
have hn₀ : n ≠ 0 := by omega

Result:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
n : ℕ
hn' : 2 ≤ n
hα : n ≤ card α
hn₀ : n ≠ 0
⊢ (Finset.filter (fun g => g.cycleType = {n}) Finset.univ).card = (n - 1)! * (card α).choose n

Proof state:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
n : ℕ
hn' : 2 ≤ n
hα : n ≤ card α
hn₀ : n ≠ 0
⊢ 0 < n

Tactic:
omega

Result:
no goals

Proof state:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
n : ℕ
hn' : 2 ≤ n
hα : n ≤ card α
hn₀ : n ≠ 0
aux : n ! = (n - 1)! * n
⊢ (Finset.filter (fun g => g.cycleType = {n}) Finset.univ).card * (n * (card α - n)!) = (card α)!

Tactic:
simpa [ite_and, if_pos hα, if_pos hn', mul_comm _ n, mul_assoc]
  using card_of_cycleType_mul_eq α {n}

Result:
no goals

Proof state:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
n : ℕ
hn' : 2 ≤ n
hα : n ≤ card α
hn₀ : n ≠ 0
⊢ n ! = (n - 1)! * n

Tactic:
rw [mul_comm, mul_factorial_pred (by omega)]

Result:
no goals

Proof state:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
n : ℕ
hn' : 2 ≤ n
hα : n ≤ card α
hn₀ : n ≠ 0
aux : n ! = (n - 1)! * n
⊢ (Finset.filter (fun g => g.cycleType = {n}) Finset.univ).card = (n - 1)! * (card α).choose n

Tactic:
rw [mul_comm, ← Nat.mul_left_inj hn₀, mul_assoc, ← aux, ← Nat.mul_left_inj (factorial_ne_zero _),
  Nat.choose_mul_factorial_mul_factorial hα, mul_assoc]

Result:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
n : ℕ
hn' : 2 ≤ n
hα : n ≤ card α
hn₀ : n ≠ 0
aux : n ! = (n - 1)! * n
⊢ (Finset.filter (fun g => g.cycleType = {n}) Finset.univ).card * (n * (card α - n)!) = (card α)!

Proof state:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
n : ℕ
hn' : 2 ≤ n
hα : n ≤ card α
⊢ n ≠ 0

Tactic:
omega

Result:
no goals
-- Mathlib/GroupTheory/Coxeter/Basic.lean
theorem simple_mul_simple_cancel_right {w : W} (i : B) : w * s i * s i = w

Proof state:
B : Type u_1
W : Type u_3
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
w : W
i : B
⊢ w * cs.simple i * cs.simple i = w

Tactic:
simp [mul_assoc]

Result:
no goals
-- Mathlib/Logic/Relation.lean
theorem flip_comp : flip (r ∘r p) = flip p ∘r flip r

Proof state:
case h.h.a
α : Type u_1
β : Type u_2
γ : Type u_3
r : α → β → Prop
p : β → γ → Prop
c : γ
a : α
⊢ flip (r ∘r p) c a ↔ (flip p ∘r flip r) c a

Tactic:
constructor

Result:
case h.h.a.mp
α : Type u_1
β : Type u_2
γ : Type u_3
r : α → β → Prop
p : β → γ → Prop
c : γ
a : α
⊢ flip (r ∘r p) c a → (flip p ∘r flip r) c a

case h.h.a.mpr
α : Type u_1
β : Type u_2
γ : Type u_3
r : α → β → Prop
p : β → γ → Prop
c : γ
a : α
⊢ (flip p ∘r flip r) c a → flip (r ∘r p) c a

Proof state:
case h.h.a.mp
α : Type u_1
β : Type u_2
γ : Type u_3
r : α → β → Prop
p : β → γ → Prop
c : γ
a : α
⊢ flip (r ∘r p) c a → (flip p ∘r flip r) c a

Tactic:
exact fun ⟨b, hab, hbc⟩ ↦ ⟨b, hbc, hab⟩

Result:
no goals

Proof state:
case h.h.a.mpr
α : Type u_1
β : Type u_2
γ : Type u_3
r : α → β → Prop
p : β → γ → Prop
c : γ
a : α
⊢ (flip p ∘r flip r) c a → flip (r ∘r p) c a

Tactic:
exact fun ⟨b, hbc, hab⟩ ↦ ⟨b, hab, hbc⟩

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
r : α → β → Prop
p : β → γ → Prop
⊢ flip (r ∘r p) = flip p ∘r flip r

Tactic:
funext c a

Result:
case h.h
α : Type u_1
β : Type u_2
γ : Type u_3
r : α → β → Prop
p : β → γ → Prop
c : γ
a : α
⊢ flip (r ∘r p) c a = (flip p ∘r flip r) c a

Proof state:
case h.h
α : Type u_1
β : Type u_2
γ : Type u_3
r : α → β → Prop
p : β → γ → Prop
c : γ
a : α
⊢ flip (r ∘r p) c a = (flip p ∘r flip r) c a

Tactic:
apply propext

Result:
case h.h.a
α : Type u_1
β : Type u_2
γ : Type u_3
r : α → β → Prop
p : β → γ → Prop
c : γ
a : α
⊢ flip (r ∘r p) c a ↔ (flip p ∘r flip r) c a
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Nat/Div/Basic.lean
theorem mul_div_le (m n : Nat) : n * (m / n) ≤ m

Proof state:
m n : Nat
⊢ n * (m / n) ≤ m

Tactic:
match n, Nat.eq_zero_or_pos n with
| _, Or.inl rfl => rw [Nat.zero_mul]; exact m.zero_le
| n, Or.inr h => rw [Nat.mul_comm, ← Nat.le_div_iff_mul_le h]; exact Nat.le_refl _

Result:
no goals

Proof state:
m n✝ n : Nat
h : n > 0
⊢ n * (m / n) ≤ m

Tactic:
rw [Nat.mul_comm, ← Nat.le_div_iff_mul_le h]

Result:
m n✝ n : Nat
h : n > 0
⊢ m / n ≤ m / n

Proof state:
m n : Nat
⊢ 0 * (m / 0) ≤ m

Tactic:
rw [Nat.zero_mul]

Result:
m n : Nat
⊢ 0 ≤ m

Proof state:
m n✝ n : Nat
h : n > 0
⊢ m / n ≤ m / n

Tactic:
exact Nat.le_refl _

Result:
no goals

Proof state:
m n : Nat
⊢ 0 ≤ m

Tactic:
exact m.zero_le

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Nat/Lemmas.lean
theorem min_assoc : ∀ (a b c : Nat), min (min a b) c = min a (min b c)
  | 0, _, _ => by rw [Nat.zero_min, Nat.zero_min, Nat.zero_min]
  | _, 0, _ => by rw [Nat.zero_min, Nat.min_zero, Nat.zero_min]
  | _, _, 0 => by rw [Nat.min_zero, Nat.min_zero, Nat.min_zero]
  | _+1, _+1, _+1 => by simp only [Nat.succ_min_succ]; exact congrArg succ <| Nat.min_assoc ..

Proof state:
n✝² n✝¹ n✝ : Nat
⊢ min (min (n✝² + 1) (n✝¹ + 1)) (n✝ + 1) = min (n✝² + 1) (min (n✝¹ + 1) (n✝ + 1))

Tactic:
simp only [Nat.succ_min_succ]

Result:
n✝² n✝¹ n✝ : Nat
⊢ (min (min n✝² n✝¹) n✝).succ = (min n✝² (min n✝¹ n✝)).succ

Proof state:
n✝² n✝¹ n✝ : Nat
⊢ (min (min n✝² n✝¹) n✝).succ = (min n✝² (min n✝¹ n✝)).succ

Tactic:
exact congrArg succ <| Nat.min_assoc ..

Result:
no goals

Proof state:
x✝¹ x✝ : Nat
⊢ min (min 0 x✝¹) x✝ = min 0 (min x✝¹ x✝)

Tactic:
rw [Nat.zero_min, Nat.zero_min, Nat.zero_min]

Result:
no goals

Proof state:
x✝¹ x✝ : Nat
⊢ min (min x✝¹ 0) x✝ = min x✝¹ (min 0 x✝)

Tactic:
rw [Nat.zero_min, Nat.min_zero, Nat.zero_min]

Result:
no goals

Proof state:
x✝¹ x✝ : Nat
⊢ min (min x✝¹ x✝) 0 = min x✝¹ (min x✝ 0)

Tactic:
rw [Nat.min_zero, Nat.min_zero, Nat.min_zero]

Result:
no goals
-- Mathlib/Data/Fin/Tuple/Basic.lean
theorem insertNth_apply_above {i j : Fin (n + 1)} (h : i < j) (x : α i)
    (p : ∀ k, α (i.succAbove k)) :
    i.insertNth x p j = @Eq.recOn _ _ (fun x _ ↦ α x) _
    (succAbove_pred_of_lt _ _ h) (p <| j.pred _)

Proof state:
n : ℕ
α : Fin (n + 1) → Sort u_1
i j : Fin (n + 1)
h : i < j
x : α i
p : (k : Fin n) → α (i.succAbove k)
⊢ i.insertNth x p j = Eq.recOn ⋯ (p (j.pred ⋯))

Tactic:
rw [insertNth, succAboveCases, dif_neg (Fin.ne_of_gt h), dif_neg (Fin.lt_asymm h)]

Result:
no goals
-- Mathlib/Data/Matroid/Closure.lean
lemma IsFlat.iInter {ι : Type*} [Nonempty ι] {Fs : ι → Set α}
    (hFs : ∀ i, M.IsFlat (Fs i)) : M.IsFlat (⋂ i, Fs i)

Proof state:
case h.e'_4
α : Type u_2
M : Matroid α
ι : Type u_3
inst✝ : Nonempty ι
Fs : ι → Set α
hFs : ∀ (i : ι), M.IsFlat (Fs i)
I X : Set α
hI : M.IsBasis I (⋂ i, Fs i)
hIX : M.IsBasis I X
i : ι
J : Set α
hIJ : M.IsBasis J (Fs i)
hJ : I ⊆ J
⊢ Fs i ∪ X = Fs i ∪ (J ∪ X)

Tactic:
rw [← union_assoc, union_eq_self_of_subset_right hIJ.subset]

Result:
no goals

Proof state:
α : Type u_2
M : Matroid α
ι : Type u_3
inst✝ : Nonempty ι
Fs : ι → Set α
hFs : ∀ (i : ι), M.IsFlat (Fs i)
I X : Set α
hI : M.IsBasis I (⋂ i, Fs i)
hIX : M.IsBasis I X
i : ι
⊢ X ⊆ Fs i

Tactic:
obtain ⟨J, hIJ, hJ⟩ := hI.indep.subset_isBasis_of_subset (hI.subset.trans (iInter_subset _ i))

Result:
case intro.intro
α : Type u_2
M : Matroid α
ι : Type u_3
inst✝ : Nonempty ι
Fs : ι → Set α
hFs : ∀ (i : ι), M.IsFlat (Fs i)
I X : Set α
hI : M.IsBasis I (⋂ i, Fs i)
hIX : M.IsBasis I X
i : ι
J : Set α
hIJ : M.IsBasis J (Fs i)
hJ : I ⊆ J
⊢ X ⊆ Fs i

Proof state:
α : Type u_2
M : Matroid α
ι : Type u_3
inst✝ : Nonempty ι
Fs : ι → Set α
hFs : ∀ (i : ι), M.IsFlat (Fs i)
⊢ M.IsFlat (⋂ i, Fs i)

Tactic:
refine ⟨fun I X hI hIX ↦ subset_iInter fun i ↦ ?_,
  (iInter_subset _ (Classical.arbitrary _)).trans (hFs _).subset_ground⟩

Result:
α : Type u_2
M : Matroid α
ι : Type u_3
inst✝ : Nonempty ι
Fs : ι → Set α
hFs : ∀ (i : ι), M.IsFlat (Fs i)
I X : Set α
hI : M.IsBasis I (⋂ i, Fs i)
hIX : M.IsBasis I X
i : ι
⊢ X ⊆ Fs i

Proof state:
case intro.intro
α : Type u_2
M : Matroid α
ι : Type u_3
inst✝ : Nonempty ι
Fs : ι → Set α
hFs : ∀ (i : ι), M.IsFlat (Fs i)
I X : Set α
hI : M.IsBasis I (⋂ i, Fs i)
hIX : M.IsBasis I X
i : ι
J : Set α
hIJ : M.IsBasis J (Fs i)
hJ : I ⊆ J
⊢ X ⊆ Fs i

Tactic:
refine subset_union_right.trans ((hFs i).1 (X := Fs i ∪ X) hIJ ?_)

Result:
case intro.intro
α : Type u_2
M : Matroid α
ι : Type u_3
inst✝ : Nonempty ι
Fs : ι → Set α
hFs : ∀ (i : ι), M.IsFlat (Fs i)
I X : Set α
hI : M.IsBasis I (⋂ i, Fs i)
hIX : M.IsBasis I X
i : ι
J : Set α
hIJ : M.IsBasis J (Fs i)
hJ : I ⊆ J
⊢ M.IsBasis J (Fs i ∪ X)

Proof state:
case intro.intro
α : Type u_2
M : Matroid α
ι : Type u_3
inst✝ : Nonempty ι
Fs : ι → Set α
hFs : ∀ (i : ι), M.IsFlat (Fs i)
I X : Set α
hI : M.IsBasis I (⋂ i, Fs i)
hIX : M.IsBasis I X
i : ι
J : Set α
hIJ : M.IsBasis J (Fs i)
hJ : I ⊆ J
⊢ M.IsBasis J (Fs i ∪ X)

Tactic:
convert hIJ.isBasis_union (hIX.isBasis_union_of_subset hIJ.indep hJ) using 1

Result:
case h.e'_4
α : Type u_2
M : Matroid α
ι : Type u_3
inst✝ : Nonempty ι
Fs : ι → Set α
hFs : ∀ (i : ι), M.IsFlat (Fs i)
I X : Set α
hI : M.IsBasis I (⋂ i, Fs i)
hIX : M.IsBasis I X
i : ι
J : Set α
hIJ : M.IsBasis J (Fs i)
hJ : I ⊆ J
⊢ Fs i ∪ X = Fs i ∪ (J ∪ X)
-- Mathlib/NumberTheory/Modular.lean
theorem im_lt_im_S_smul (h : normSq z < 1) : z.im < (S • z).im

Proof state:
z : ℍ
h : normSq ↑z < 1
⊢ z.im < (S • z).im

Tactic:
have : z.im < z.im / normSq (z : ℂ) := by
  have imz : 0 < z.im := im_pos z
  apply (lt_div_iff₀ z.normSq_pos).mpr
  nlinarith

Result:
z : ℍ
h : normSq ↑z < 1
this : z.im < z.im / normSq ↑z
⊢ z.im < (S • z).im

Proof state:
z : ℍ
h : normSq ↑z < 1
imz : 0 < z.im
⊢ z.im < z.im / normSq ↑z

Tactic:
apply (lt_div_iff₀ z.normSq_pos).mpr

Result:
z : ℍ
h : normSq ↑z < 1
imz : 0 < z.im
⊢ z.im * normSq ↑z < z.im

Proof state:
z : ℍ
h : normSq ↑z < 1
⊢ z.im < z.im / normSq ↑z

Tactic:
have imz : 0 < z.im := im_pos z

Result:
z : ℍ
h : normSq ↑z < 1
imz : 0 < z.im
⊢ z.im < z.im / normSq ↑z

Proof state:
case h.e'_4
z : ℍ
h : normSq ↑z < 1
this : z.im < z.im / normSq ↑z
⊢ z.im / normSq (denom (↑S) z) = z.im / normSq ↑z

Tactic:
simp [denom, coe_S]

Result:
no goals

Proof state:
z : ℍ
h : normSq ↑z < 1
this : z.im < z.im / normSq ↑z
⊢ z.im < (S • z).im

Tactic:
convert this

Result:
case h.e'_4
z : ℍ
h : normSq ↑z < 1
this : z.im < z.im / normSq ↑z
⊢ (S • z).im = z.im / normSq ↑z

Proof state:
case h.e'_4
z : ℍ
h : normSq ↑z < 1
this : z.im < z.im / normSq ↑z
⊢ (S • z).im = z.im / normSq ↑z

Tactic:
simp only [ModularGroup.im_smul_eq_div_normSq]

Result:
case h.e'_4
z : ℍ
h : normSq ↑z < 1
this : z.im < z.im / normSq ↑z
⊢ z.im / normSq (denom (↑S) z) = z.im / normSq ↑z

Proof state:
z : ℍ
h : normSq ↑z < 1
imz : 0 < z.im
⊢ z.im * normSq ↑z < z.im

Tactic:
nlinarith

Result:
no goals
-- Mathlib/.lake/packages/batteries/Batteries/Data/AssocList.lean
theorem find?_eq_findEntry? [BEq α] (a : α) (l : AssocList α β) :
    find? a l = (l.findEntry? a).map (·.2)

Proof state:
α : Type u_1
β : Type u_2
inst✝ : BEq α
a : α
l : AssocList α β
⊢ find? a l = Option.map (fun x => x.snd) (findEntry? a l)

Tactic:
induction l <;> simp [find?, List.find?_cons]

Result:
case cons
α : Type u_1
β : Type u_2
inst✝ : BEq α
a key✝ : α
value✝ : β
tail✝ : AssocList α β
tail_ih✝ : find? a tail✝ = Option.map (fun x => x.snd) (findEntry? a tail✝)
⊢ (match key✝ == a with
    | true => some value✝
    | false => find? a tail✝) =
    Option.map (fun x => x.snd)
      (match key✝ == a with
      | true => some (key✝, value✝)
      | false => List.find? (fun x => x.fst == a) tail✝.toList)

Proof state:
case cons
α : Type u_1
β : Type u_2
inst✝ : BEq α
a key✝ : α
value✝ : β
tail✝ : AssocList α β
tail_ih✝ : find? a tail✝ = Option.map (fun x => x.snd) (findEntry? a tail✝)
⊢ (match key✝ == a with
    | true => some value✝
    | false => find? a tail✝) =
    Option.map (fun x => x.snd)
      (match key✝ == a with
      | true => some (key✝, value✝)
      | false => List.find? (fun x => x.fst == a) tail✝.toList)

Tactic:
split <;> simp [*]

Result:
no goals
-- Mathlib/Algebra/Order/GroupWithZero/Unbundled.lean
theorem posMulMono_iff_mulPosMono : PosMulMono α ↔ MulPosMono α

Proof state:
α : Type u_3
inst✝³ : Mul α
inst✝² : Std.Commutative fun x1 x2 => x1 * x2
inst✝¹ : Zero α
inst✝ : Preorder α
⊢ PosMulMono α ↔ MulPosMono α

Tactic:
simp only [posMulMono_iff, mulPosMono_iff, Std.Commutative.comm]

Result:
no goals
-- Mathlib/Order/SuccPred/Limit.lean
theorem not_isSuccPrelimit_iff' : ¬ IsSuccPrelimit a ↔ a ∈ range (succ : α → α)

Proof state:
α : Type u_1
a : α
inst✝² : PartialOrder α
inst✝¹ : SuccOrder α
inst✝ : NoMaxOrder α
⊢ ¬IsSuccPrelimit a ↔ a ∈ range succ

Tactic:
simp_rw [isSuccPrelimit_iff_succ_ne, not_forall, not_ne_iff, mem_range]

Result:
no goals
-- Mathlib/Tactic/Module.lean
theorem eval_algebraMap [CommSemiring S] [Semiring R] [Algebra S R] [AddMonoid M] [SMul S M]
    [MulAction R M] [IsScalarTower S R M] (l : NF S M) :
    (l.algebraMap R).eval = l.eval

Proof state:
case e_a.e_f
S : Type u_1
R : Type u_2
M : Type u_3
inst✝⁶ : CommSemiring S
inst✝⁵ : Semiring R
inst✝⁴ : Algebra S R
inst✝³ : AddMonoid M
inst✝² : SMul S M
inst✝¹ : MulAction R M
inst✝ : IsScalarTower S R M
l : NF S M
⊢ ((fun x => x.1 • x.2) ∘ fun x => ((_root_.algebraMap S R) x.1, x.2)) = fun x => x.1 • x.2

Tactic:
ext

Result:
case e_a.e_f.h
S : Type u_1
R : Type u_2
M : Type u_3
inst✝⁶ : CommSemiring S
inst✝⁵ : Semiring R
inst✝⁴ : Algebra S R
inst✝³ : AddMonoid M
inst✝² : SMul S M
inst✝¹ : MulAction R M
inst✝ : IsScalarTower S R M
l : NF S M
x✝ : S × M
⊢ ((fun x => x.1 • x.2) ∘ fun x => ((_root_.algebraMap S R) x.1, x.2)) x✝ = x✝.1 • x✝.2

Proof state:
S : Type u_1
R : Type u_2
M : Type u_3
inst✝⁶ : CommSemiring S
inst✝⁵ : Semiring R
inst✝⁴ : Algebra S R
inst✝³ : AddMonoid M
inst✝² : SMul S M
inst✝¹ : MulAction R M
inst✝ : IsScalarTower S R M
l : NF S M
⊢ (map ((fun x => x.1 • x.2) ∘ fun x => ((_root_.algebraMap S R) x.1, x.2)) l).sum = (map (fun x => x.1 • x.2) l).sum

Tactic:
congr

Result:
case e_a.e_f
S : Type u_1
R : Type u_2
M : Type u_3
inst✝⁶ : CommSemiring S
inst✝⁵ : Semiring R
inst✝⁴ : Algebra S R
inst✝³ : AddMonoid M
inst✝² : SMul S M
inst✝¹ : MulAction R M
inst✝ : IsScalarTower S R M
l : NF S M
⊢ ((fun x => x.1 • x.2) ∘ fun x => ((_root_.algebraMap S R) x.1, x.2)) = fun x => x.1 • x.2

Proof state:
case e_a.e_f.h
S : Type u_1
R : Type u_2
M : Type u_3
inst✝⁶ : CommSemiring S
inst✝⁵ : Semiring R
inst✝⁴ : Algebra S R
inst✝³ : AddMonoid M
inst✝² : SMul S M
inst✝¹ : MulAction R M
inst✝ : IsScalarTower S R M
l : NF S M
x✝ : S × M
⊢ ((fun x => x.1 • x.2) ∘ fun x => ((_root_.algebraMap S R) x.1, x.2)) x✝ = x✝.1 • x✝.2

Tactic:
simp [IsScalarTower.algebraMap_smul]

Result:
no goals

Proof state:
S : Type u_1
R : Type u_2
M : Type u_3
inst✝⁶ : CommSemiring S
inst✝⁵ : Semiring R
inst✝⁴ : Algebra S R
inst✝³ : AddMonoid M
inst✝² : SMul S M
inst✝¹ : MulAction R M
inst✝ : IsScalarTower S R M
l : NF S M
⊢ (algebraMap R l).eval = l.eval

Tactic:
simp only [NF.eval, algebraMap, map_map]

Result:
S : Type u_1
R : Type u_2
M : Type u_3
inst✝⁶ : CommSemiring S
inst✝⁵ : Semiring R
inst✝⁴ : Algebra S R
inst✝³ : AddMonoid M
inst✝² : SMul S M
inst✝¹ : MulAction R M
inst✝ : IsScalarTower S R M
l : NF S M
⊢ (map ((fun x => x.1 • x.2) ∘ fun x => ((_root_.algebraMap S R) x.1, x.2)) l).sum = (map (fun x => x.1 • x.2) l).sum
-- Mathlib/SetTheory/Ordinal/Topology.lean
theorem mem_closure_iff_bsup :
    a ∈ closure s ↔
      ∃ (o : Ordinal) (_ho : o ≠ 0) (f : ∀ a < o, Ordinal),
        (∀ i hi, f i hi ∈ s) ∧ bsup.{u, u} o f = a

Proof state:
s : Set Ordinal.{u}
a : Ordinal.{u}
⊢ a ∈ closure s ↔ ∃ o, ∃ (_ : o ≠ 0), ∃ f, (∀ (i : Ordinal.{u}) (hi : i < o), f i hi ∈ s) ∧ o.bsup f = a

Tactic:
apply ((mem_closure_tfae a s).out 0 4).trans

Result:
s : Set Ordinal.{u}
a : Ordinal.{u}
⊢ (∃ o, o ≠ 0 ∧ ∃ f, (∀ (x : Ordinal.{u}) (hx : x < o), f x hx ∈ s) ∧ o.bsup f = a) ↔
    ∃ o, ∃ (_ : o ≠ 0), ∃ f, (∀ (i : Ordinal.{u}) (hi : i < o), f i hi ∈ s) ∧ o.bsup f = a

Proof state:
s : Set Ordinal.{u}
a : Ordinal.{u}
⊢ (∃ o, o ≠ 0 ∧ ∃ f, (∀ (x : Ordinal.{u}) (hx : x < o), f x hx ∈ s) ∧ o.bsup f = a) ↔
    ∃ o, ∃ (_ : o ≠ 0), ∃ f, (∀ (i : Ordinal.{u}) (hi : i < o), f i hi ∈ s) ∧ o.bsup f = a

Tactic:
simp_rw [exists_prop]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Erase.lean
theorem eraseP_replicate_of_neg {n : Nat} {a : α} (h : ¬p a) :
    (replicate n a).eraseP p = replicate n a

Proof state:
α : Type u_1
p : α → Bool
n : Nat
a : α
h : ¬p a = true
⊢ eraseP p (replicate n a) = replicate n a

Tactic:
rw [eraseP_of_forall_not (by simp_all)]

Result:
no goals

Proof state:
α : Type u_1
p : α → Bool
n : Nat
a : α
h : ¬p a = true
⊢ ∀ (a_1 : α), a_1 ∈ replicate n a → ¬p a_1 = true

Tactic:
simp_all

Result:
no goals
-- Mathlib/Geometry/Manifold/Algebra/LieGroup.lean
theorem ContMDiffWithinAt.div₀
    (hf : ContMDiffWithinAt I' I n f s a) (hg : ContMDiffWithinAt I' I n g s a) (h₀ : g a ≠ 0) :
    ContMDiffWithinAt I' I n (f / g) s a

Proof state:
𝕜 : Type u_1
inst✝¹³ : NontriviallyNormedField 𝕜
n : WithTop ℕ∞
H : Type u_2
inst✝¹² : TopologicalSpace H
E : Type u_3
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace 𝕜 E
I : ModelWithCorners 𝕜 E H
G : Type u_4
inst✝⁹ : TopologicalSpace G
inst✝⁸ : ChartedSpace H G
inst✝⁷ : GroupWithZero G
inst✝⁶ : ContMDiffInv₀ I n G
inst✝⁵ : ContMDiffMul I n G
E' : Type u_5
inst✝⁴ : NormedAddCommGroup E'
inst✝³ : NormedSpace 𝕜 E'
H' : Type u_6
inst✝² : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M : Type u_7
inst✝¹ : TopologicalSpace M
inst✝ : ChartedSpace H' M
f g : M → G
s : Set M
a : M
hf : ContMDiffWithinAt I' I n f s a
hg : ContMDiffWithinAt I' I n g s a
h₀ : g a ≠ 0
⊢ ContMDiffWithinAt I' I n (f / g) s a

Tactic:
simpa [div_eq_mul_inv] using hf.mul (hg.inv₀ h₀)

Result:
no goals
-- Mathlib/Data/Real/Basic.lean
theorem cauchy_one : (1 : ℝ).cauchy = 1 :=
  show one.cauchy = 1 by rw [one_def]

Proof state:
⊢ Real.one.cauchy = 1

Tactic:
rw [one_def]

Result:
no goals