harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Data/Nat/Init.lean
lemma eq_of_dvd_of_lt_two_mul (ha : a ≠ 0) (hdvd : b ∣ a) (hlt : a < 2 * b) : a = b

Proof state:
a b : ℕ
ha : a ≠ 0
hdvd : b ∣ a
hlt : a < 2 * b
⊢ a = b

Tactic:
obtain ⟨_ | _ | c, rfl⟩ := hdvd

Result:
case intro.zero
b : ℕ
ha : b * 0 ≠ 0
hlt : b * 0 < 2 * b
⊢ b * 0 = b

case intro.succ.zero
b : ℕ
ha : b * (0 + 1) ≠ 0
hlt : b * (0 + 1) < 2 * b
⊢ b * (0 + 1) = b

case intro.succ.succ
b c : ℕ
ha : b * (c + 1 + 1) ≠ 0
hlt : b * (c + 1 + 1) < 2 * b
⊢ b * (c + 1 + 1) = b

Proof state:
case intro.succ.zero
b : ℕ
ha : b * (0 + 1) ≠ 0
hlt : b * (0 + 1) < 2 * b
⊢ b * (0 + 1) = b

Tactic:
exact Nat.mul_one _

Result:
no goals

Proof state:
b c : ℕ
ha : b * (c + 1 + 1) ≠ 0
hlt : (c + 1 + 1) * b < 2 * b
⊢ 2 ≤ c + 1 + 1

Tactic:
omega

Result:
no goals

Proof state:
case intro.succ.succ
b c : ℕ
ha : b * (c + 1 + 1) ≠ 0
hlt : b * (c + 1 + 1) < 2 * b
⊢ b * (c + 1 + 1) = b

Tactic:
rw [Nat.mul_comm] at hlt

Result:
case intro.succ.succ
b c : ℕ
ha : b * (c + 1 + 1) ≠ 0
hlt : (c + 1 + 1) * b < 2 * b
⊢ b * (c + 1 + 1) = b

Proof state:
case intro.zero
b : ℕ
ha : b * 0 ≠ 0
hlt : b * 0 < 2 * b
⊢ b * 0 = b

Tactic:
simp at ha

Result:
no goals

Proof state:
case intro.succ.succ
b c : ℕ
ha : b * (c + 1 + 1) ≠ 0
hlt : (c + 1 + 1) * b < 2 * b
⊢ b * (c + 1 + 1) = b

Tactic:
cases Nat.not_le_of_lt hlt (Nat.mul_le_mul_right _ (by omega))

Result:
no goals
-- Mathlib/Algebra/GCDMonoid/Multiset.lean
theorem normalize_gcd (s : Multiset α) : normalize s.gcd = s.gcd :=
  Multiset.induction_on s (by simp) fun a s _ ↦ by simp

Proof state:
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
s : Multiset α
⊢ normalize (gcd 0) = gcd 0

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
s✝ : Multiset α
a : α
s : Multiset α
x✝ : normalize s.gcd = s.gcd
⊢ normalize (a ::ₘ s).gcd = (a ::ₘ s).gcd

Tactic:
simp

Result:
no goals
-- Mathlib/Algebra/Group/Int/Units.lean
lemma isUnit_eq_one_or (hu : IsUnit u) : u = 1 ∨ u = -1

Proof state:
u : ℤ
hu : IsUnit u
⊢ u = 1 ∨ u = -1

Tactic:
simpa only [natAbs_of_isUnit hu] using natAbs_eq u

Result:
no goals
-- Mathlib/MeasureTheory/Decomposition/Jordan.lean
theorem of_diff_eq_zero_of_symmDiff_eq_zero_positive (hu : MeasurableSet u) (hv : MeasurableSet v)
    (hsu : 0 ≤[u] s) (hsv : 0 ≤[v] s) (hs : s (u ∆ v) = 0) : s (u \ v) = 0 ∧ s (v \ u) = 0

Proof state:
α : Type u_1
inst✝ : MeasurableSpace α
s : SignedMeasure α
u v : Set α
hu : MeasurableSet u
hv : MeasurableSet v
hsu : ∀ ⦃j : Set α⦄, MeasurableSet j → j ⊆ u → ↑0 j ≤ ↑s j
hsv : ∀ ⦃j : Set α⦄, MeasurableSet j → j ⊆ v → ↑0 j ≤ ↑s j
hs : ↑s (u \ v) + ↑s (v \ u) = 0
a : 0 ≤ ↑s (u \ v)
b : 0 ≤ ↑s (v \ u)
⊢ ↑s (u \ v) = 0 ∧ ↑s (v \ u) = 0

Tactic:
constructor

Result:
case left
α : Type u_1
inst✝ : MeasurableSpace α
s : SignedMeasure α
u v : Set α
hu : MeasurableSet u
hv : MeasurableSet v
hsu : ∀ ⦃j : Set α⦄, MeasurableSet j → j ⊆ u → ↑0 j ≤ ↑s j
hsv : ∀ ⦃j : Set α⦄, MeasurableSet j → j ⊆ v → ↑0 j ≤ ↑s j
hs : ↑s (u \ v) + ↑s (v \ u) = 0
a : 0 ≤ ↑s (u \ v)
b : 0 ≤ ↑s (v \ u)
⊢ ↑s (u \ v) = 0

case right
α : Type u_1
inst✝ : MeasurableSpace α
s : SignedMeasure α
u v : Set α
hu : MeasurableSet u
hv : MeasurableSet v
hsu : ∀ ⦃j : Set α⦄, MeasurableSet j → j ⊆ u → ↑0 j ≤ ↑s j
hsv : ∀ ⦃j : Set α⦄, MeasurableSet j → j ⊆ v → ↑0 j ≤ ↑s j
hs : ↑s (u \ v) + ↑s (v \ u) = 0
a : 0 ≤ ↑s (u \ v)
b : 0 ≤ ↑s (v \ u)
⊢ ↑s (v \ u) = 0

Proof state:
α : Type u_1
inst✝ : MeasurableSpace α
s : SignedMeasure α
u v : Set α
hu : MeasurableSet u
hv : MeasurableSet v
hsu : 0 ≤[u] s
hsv : 0 ≤[v] s
hs : ↑s (u ∆ v) = 0
⊢ ↑s (u \ v) = 0 ∧ ↑s (v \ u) = 0

Tactic:
rw [restrict_le_restrict_iff] at hsu hsv

Result:
α : Type u_1
inst✝ : MeasurableSpace α
s : SignedMeasure α
u v : Set α
hu : MeasurableSet u
hv : MeasurableSet v
hsu : ∀ ⦃j : Set α⦄, MeasurableSet j → j ⊆ u → ↑0 j ≤ ↑s j
hsv : ∀ ⦃j : Set α⦄, MeasurableSet j → j ⊆ v → ↑0 j ≤ ↑s j
hs : ↑s (u ∆ v) = 0
⊢ ↑s (u \ v) = 0 ∧ ↑s (v \ u) = 0

case hi
α : Type u_1
inst✝ : MeasurableSpace α
s : SignedMeasure α
u v : Set α
hu : MeasurableSet u
hv : MeasurableSet v
hsu : ∀ ⦃j : Set α⦄, MeasurableSet j → j ⊆ u → ↑0 j ≤ ↑s j
hsv : 0 ≤[v] s
hs : ↑s (u ∆ v) = 0
⊢ MeasurableSet v

case hi
α : Type u_1
inst✝ : MeasurableSpace α
s : SignedMeasure α
u v : Set α
hu : MeasurableSet u
hv : MeasurableSet v
hsu : 0 ≤[u] s
hsv : 0 ≤[v] s
hs : ↑s (u ∆ v) = 0
⊢ MeasurableSet u

Proof state:
case hi
α : Type u_1
inst✝ : MeasurableSpace α
s : SignedMeasure α
u v : Set α
hu : MeasurableSet u
hv : MeasurableSet v
hsu : 0 ≤[u] s
hsv : 0 ≤[v] s
hs : ↑s (u ∆ v) = 0
⊢ MeasurableSet u

Tactic:
first | linarith | assumption

Result:
no goals
-- Mathlib/Topology/Algebra/InfiniteSum/Module.lean
/-- Infinite sums commute with scalar multiplication. Version for scalars living in a
  `DivisionRing`; no summability hypothesis. This could be made to work for a
  `[GroupWithZero γ]` if there was such a thing as `DistribMulActionWithZero`. -/
lemma tsum_const_smul'' {γ : Type*} [DivisionRing γ] [Module γ α] [ContinuousConstSMul γ α]
    [T2Space α] (g : γ) : ∑' (i : β), g • f i = g • ∑' (i : β), f i

Proof state:
α : Type u_1
β : Type u_2
inst✝⁵ : TopologicalSpace α
inst✝⁴ : AddCommMonoid α
f : β → α
γ : Type u_5
inst✝³ : DivisionRing γ
inst✝² : Module γ α
inst✝¹ : ContinuousConstSMul γ α
inst✝ : T2Space α
g : γ
⊢ ∑' (i : β), g • f i = g • ∑' (i : β), f i

Tactic:
rcases eq_or_ne g 0 with rfl | hg

Result:
case inl
α : Type u_1
β : Type u_2
inst✝⁵ : TopologicalSpace α
inst✝⁴ : AddCommMonoid α
f : β → α
γ : Type u_5
inst✝³ : DivisionRing γ
inst✝² : Module γ α
inst✝¹ : ContinuousConstSMul γ α
inst✝ : T2Space α
⊢ ∑' (i : β), 0 • f i = 0 • ∑' (i : β), f i

case inr
α : Type u_1
β : Type u_2
inst✝⁵ : TopologicalSpace α
inst✝⁴ : AddCommMonoid α
f : β → α
γ : Type u_5
inst✝³ : DivisionRing γ
inst✝² : Module γ α
inst✝¹ : ContinuousConstSMul γ α
inst✝ : T2Space α
g : γ
hg : g ≠ 0
⊢ ∑' (i : β), g • f i = g • ∑' (i : β), f i

Proof state:
case inr
α : Type u_1
β : Type u_2
inst✝⁵ : TopologicalSpace α
inst✝⁴ : AddCommMonoid α
f : β → α
γ : Type u_5
inst✝³ : DivisionRing γ
inst✝² : Module γ α
inst✝¹ : ContinuousConstSMul γ α
inst✝ : T2Space α
g : γ
hg : g ≠ 0
⊢ ∑' (i : β), g • f i = g • ∑' (i : β), f i

Tactic:
exact tsum_const_smul' (Units.mk0 g hg)

Result:
no goals

Proof state:
case inl
α : Type u_1
β : Type u_2
inst✝⁵ : TopologicalSpace α
inst✝⁴ : AddCommMonoid α
f : β → α
γ : Type u_5
inst✝³ : DivisionRing γ
inst✝² : Module γ α
inst✝¹ : ContinuousConstSMul γ α
inst✝ : T2Space α
⊢ ∑' (i : β), 0 • f i = 0 • ∑' (i : β), f i

Tactic:
simp

Result:
no goals
-- Mathlib/Data/Ordmap/Ordset.lean
theorem Valid'.merge_aux₁ {o₁ o₂ ls ll lx lr rs rl rx rr t}
    (hl : Valid' o₁ (@Ordnode.node α ls ll lx lr) o₂) (hr : Valid' o₁ (.node rs rl rx rr) o₂)
    (h : delta * ls < rs) (v : Valid' o₁ t rx) (e : size t = ls + size rl) :
    Valid' o₁ (.balanceL t rx rr) o₂ ∧ size (.balanceL t rx rr) = ls + rs

Proof state:
α : Type u_1
inst✝ : Preorder α
o₁ : WithBot α
o₂ : WithTop α
ls : ℕ
ll : Ordnode α
lx : α
lr : Ordnode α
rs : ℕ
rl : Ordnode α
rx : α
rr t : Ordnode α
hl : Valid' o₁ (Ordnode.node ls ll lx lr) o₂
hr : Valid' o₁ (Ordnode.node rs rl rx rr) o₂
h : 3 * (ll.size + lr.size + 1) < rl.size + rr.size + 1
v : Valid' o₁ t ↑rx
e : t.size = ll.size + lr.size + 1 + rl.size
hr₁ : rl.size ≤ delta * rr.size
hr₂ : rr.size ≤ delta * rl.size
H₂ : 1 ≤ t.size → 1 ≤ rr.size → rr.size ≤ delta * t.size
⊢ ll.size + lr.size + rl.size + 1 = 0 → rr.size ≤ 1

Tactic:
rintro ⟨⟩

Result:
no goals
-- Mathlib/Data/Real/EReal.lean
lemma inv_lt_top (x : EReal) : x⁻¹ < ⊤

Proof state:
x : EReal
⊢ x⁻¹ < ⊤

Tactic:
cases x with
| h_bot => exact inv_bot ▸ zero_lt_top
| h_top => exact EReal.inv_top ▸ zero_lt_top
| h_real x => exact (coe_inv x).symm ▸ coe_lt_top (x⁻¹)

Result:
no goals

Proof state:
case h_real
x : ℝ
⊢ (↑x)⁻¹ < ⊤

Tactic:
exact (coe_inv x).symm ▸ coe_lt_top (x⁻¹)

Result:
no goals

Proof state:
case h_bot

⊢ ⊥⁻¹ < ⊤

Tactic:
exact inv_bot ▸ zero_lt_top

Result:
no goals

Proof state:
case h_top

⊢ ⊤⁻¹ < ⊤

Tactic:
exact EReal.inv_top ▸ zero_lt_top

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Regularity/Uniform.lean
private lemma aux {i j : ℕ} (hj : 0 < j) : j * (j - 1) * (i / j + 1) ^ 2 < (i + j) ^ 2

Proof state:
i j : ℕ
hj : 0 < j
this : j * (j - 1) < j ^ 2
⊢ j * (j - 1) * (i / j + 1) ^ 2 < (i + j) ^ 2

Tactic:
apply (Nat.mul_lt_mul_of_pos_right this <| pow_pos Nat.succ_pos' _).trans_le

Result:
i j : ℕ
hj : 0 < j
this : j * (j - 1) < j ^ 2
⊢ j ^ 2 * (i / j).succ ^ 2 ≤ (i + j) ^ 2

Proof state:
i j : ℕ
hj : 0 < j
⊢ j * (j - 1) < j ^ 2

Tactic:
rw [sq]

Result:
i j : ℕ
hj : 0 < j
⊢ j * (j - 1) < j * j

Proof state:
i j : ℕ
hj : 0 < j
⊢ j * (j - 1) * (i / j + 1) ^ 2 < (i + j) ^ 2

Tactic:
have : j * (j - 1) < j ^ 2 := by
  rw [sq]; exact Nat.mul_lt_mul_of_pos_left (Nat.sub_lt hj zero_lt_one) hj

Result:
i j : ℕ
hj : 0 < j
this : j * (j - 1) < j ^ 2
⊢ j * (j - 1) * (i / j + 1) ^ 2 < (i + j) ^ 2

Proof state:
i j : ℕ
hj : 0 < j
this : j * (j - 1) < j ^ 2
⊢ (j * (i / j).succ) ^ 2 ≤ (i + j) ^ 2

Tactic:
exact Nat.pow_le_pow_of_le_left (add_le_add_right (Nat.mul_div_le i j) _) _

Result:
no goals

Proof state:
i j : ℕ
hj : 0 < j
this : j * (j - 1) < j ^ 2
⊢ j ^ 2 * (i / j).succ ^ 2 ≤ (i + j) ^ 2

Tactic:
rw [← mul_pow]

Result:
i j : ℕ
hj : 0 < j
this : j * (j - 1) < j ^ 2
⊢ (j * (i / j).succ) ^ 2 ≤ (i + j) ^ 2

Proof state:
i j : ℕ
hj : 0 < j
⊢ j * (j - 1) < j * j

Tactic:
exact Nat.mul_lt_mul_of_pos_left (Nat.sub_lt hj zero_lt_one) hj

Result:
no goals
-- Mathlib/MeasureTheory/Measure/LevyProkhorovMetric.lean
lemma right_measure_le_of_levyProkhorovEDist_lt {μ ν : Measure Ω} {c : ℝ≥0∞}
    (h : levyProkhorovEDist μ ν < c) {B : Set Ω} (B_mble : MeasurableSet B) :
    ν B ≤ μ (thickening c.toReal B) + c

Proof state:
case intro.intro
Ω : Type u_1
inst✝¹ : MeasurableSpace Ω
inst✝ : PseudoEMetricSpace Ω
μ ν : Measure Ω
c : ℝ≥0∞
h : levyProkhorovEDist μ ν < c
B : Set Ω
B_mble : MeasurableSet B
c' : ℝ≥0∞
hc' :
  c' ∈ {ε | ∀ (B : Set Ω), MeasurableSet B → μ B ≤ ν (thickening ε.toReal B) + ε ∧ ν B ≤ μ (thickening ε.toReal B) + ε}
lt_c : c' < c
⊢ ν B ≤ μ (thickening c.toReal B) + c

Tactic:
exact meas_le_of_le_of_forall_le_meas_thickening_add ν μ lt_c.le (hc' B B_mble).2

Result:
no goals

Proof state:
Ω : Type u_1
inst✝¹ : MeasurableSpace Ω
inst✝ : PseudoEMetricSpace Ω
μ ν : Measure Ω
c : ℝ≥0∞
h : levyProkhorovEDist μ ν < c
B : Set Ω
B_mble : MeasurableSet B
⊢ ν B ≤ μ (thickening c.toReal B) + c

Tactic:
obtain ⟨c', ⟨hc', lt_c⟩⟩ := sInf_lt_iff.mp h

Result:
case intro.intro
Ω : Type u_1
inst✝¹ : MeasurableSpace Ω
inst✝ : PseudoEMetricSpace Ω
μ ν : Measure Ω
c : ℝ≥0∞
h : levyProkhorovEDist μ ν < c
B : Set Ω
B_mble : MeasurableSet B
c' : ℝ≥0∞
hc' :
  c' ∈ {ε | ∀ (B : Set Ω), MeasurableSet B → μ B ≤ ν (thickening ε.toReal B) + ε ∧ ν B ≤ μ (thickening ε.toReal B) + ε}
lt_c : c' < c
⊢ ν B ≤ μ (thickening c.toReal B) + c
-- Mathlib/ModelTheory/Substructures.lean
@[simp]
lemma mem_closure_iff_of_isRelational [L.IsRelational] (s : Set M) (m : M) :
    m ∈ closure L s ↔ m ∈ s

Proof state:
L : Language
M : Type w
inst✝¹ : L.Structure M
inst✝ : L.IsRelational
s : Set M
m : M
⊢ m ∈ (closure L).toFun s ↔ m ∈ s

Tactic:
rw [← SetLike.mem_coe, closure_eq_of_isRelational]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Attach.lean
theorem getElem_pmap {p : α → Prop} (f : ∀ a, p a → β) {l : Vector α n} (h : ∀ a ∈ l, p a) {i : Nat}
    (hn : i < n) :
    (pmap f l h)[i] = f (l[i]) (h _ (by simp))

Proof state:
case mk
α : Type u_1
β : Type u_2
n : Nat
p : α → Prop
f : (a : α) → p a → β
i : Nat
hn : i < n
toArray✝ : Array α
size_toArray✝ : toArray✝.size = n
h : ∀ (a : α), a ∈ { toArray := toArray✝, size_toArray := size_toArray✝ } → p a
⊢ (pmap f { toArray := toArray✝, size_toArray := size_toArray✝ } h)[i] =
    f { toArray := toArray✝, size_toArray := size_toArray✝ }[i] ⋯

Tactic:
simp

Result:
no goals

Proof state:
α : Type ?u.29435
β : Type ?u.29493
n : Nat
p : α → Prop
f : (a : α) → p a → β
l : Vector α n
h : ∀ (a : α), a ∈ l → p a
i : Nat
hn : i < n
⊢ l[i] ∈ l

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
n : Nat
p : α → Prop
f : (a : α) → p a → β
l : Vector α n
h : ∀ (a : α), a ∈ l → p a
i : Nat
hn : i < n
⊢ (pmap f l h)[i] = f l[i] ⋯

Tactic:
cases l

Result:
case mk
α : Type u_1
β : Type u_2
n : Nat
p : α → Prop
f : (a : α) → p a → β
i : Nat
hn : i < n
toArray✝ : Array α
size_toArray✝ : toArray✝.size = n
h : ∀ (a : α), a ∈ { toArray := toArray✝, size_toArray := size_toArray✝ } → p a
⊢ (pmap f { toArray := toArray✝, size_toArray := size_toArray✝ } h)[i] =
    f { toArray := toArray✝, size_toArray := size_toArray✝ }[i] ⋯
-- Mathlib/AlgebraicGeometry/ValuativeCriterion.lean
/-- The **valuative criterion** for universally closed morphisms. -/
@[stacks 01KF]
lemma UniversallyClosed.of_valuativeCriterion [QuasiCompact f]
    (hf : ValuativeCriterion.Existence f) : UniversallyClosed f

Proof state:
X Y : Scheme
f : X ⟶ Y
inst✝ : QuasiCompact f
hf : ValuativeCriterion.Existence f
⊢ UniversallyClosed f

Tactic:
rw [eq_valuativeCriterion]

Result:
X Y : Scheme
f : X ⟶ Y
inst✝ : QuasiCompact f
hf : ValuativeCriterion.Existence f
⊢ (ValuativeCriterion.Existence ⊓ @QuasiCompact) f

Proof state:
X Y : Scheme
f : X ⟶ Y
inst✝ : QuasiCompact f
hf : ValuativeCriterion.Existence f
⊢ (ValuativeCriterion.Existence ⊓ @QuasiCompact) f

Tactic:
exact ⟨hf, ‹_›⟩

Result:
no goals
-- Mathlib/SetTheory/Ordinal/Exponential.lean
theorem sup_opow_nat {o : Ordinal} (ho : 0 < o) : (sup fun n : ℕ => o ^ n) = o ^ ω

Proof state:
ho : 0 < 1
n : ℕ
⊢ 1 ^ ↑n ≤ 1

Tactic:
rw [one_opow]

Result:
no goals

Proof state:
case inr
ho : 0 < 1
⊢ (sup fun n => 1 ^ ↑n) = 1

Tactic:
refine le_antisymm (sup_le fun n => by rw [one_opow]) ?_

Result:
case inr
ho : 0 < 1
⊢ 1 ≤ sup fun n => 1 ^ ↑n

Proof state:
case inl
o : Ordinal.{u_1}
ho : 0 < o
ho₁ : 1 < o
⊢ (sup fun n => o ^ ↑n) = o ^ ω

Tactic:
exact (isNormal_opow ho₁).apply_omega0

Result:
no goals

Proof state:
o : Ordinal.{u_1}
ho : 0 < o
⊢ (sup fun n => o ^ n) = o ^ ω

Tactic:
simp_rw [← opow_natCast]

Result:
o : Ordinal.{u_1}
ho : 0 < o
⊢ (sup fun n => o ^ ↑n) = o ^ ω

Proof state:
o : Ordinal.{u_1}
ho : 0 < o
⊢ (sup fun n => o ^ ↑n) = o ^ ω

Tactic:
rcases (one_le_iff_pos.2 ho).lt_or_eq with ho₁ | rfl

Result:
case inl
o : Ordinal.{u_1}
ho : 0 < o
ho₁ : 1 < o
⊢ (sup fun n => o ^ ↑n) = o ^ ω

case inr
ho : 0 < 1
⊢ (sup fun n => 1 ^ ↑n) = 1 ^ ω

Proof state:
case h.e'_3
ho : 0 < 1
⊢ 1 = 1 ^ ↑0

Tactic:
rw [Nat.cast_zero, opow_zero]

Result:
no goals

Proof state:
case inr
ho : 0 < 1
⊢ 1 ≤ sup fun n => 1 ^ ↑n

Tactic:
convert le_sup (fun n : ℕ => 1 ^ (n : Ordinal)) 0

Result:
case h.e'_3
ho : 0 < 1
⊢ 1 = 1 ^ ↑0

Proof state:
case inr
ho : 0 < 1
⊢ (sup fun n => 1 ^ ↑n) = 1 ^ ω

Tactic:
rw [one_opow]

Result:
case inr
ho : 0 < 1
⊢ (sup fun n => 1 ^ ↑n) = 1
-- Mathlib/Data/Prod/TProd.lean
theorem elim_of_ne (hj : j ∈ i :: l) (hji : j ≠ i) (v : TProd α (i :: l)) :
    v.elim hj = TProd.elim v.2 ((List.mem_cons.mp hj).resolve_left hji)

Proof state:
ι : Type u
α : ι → Type v
i j : ι
l : List ι
inst✝ : DecidableEq ι
hj : j ∈ i :: l
hji : j ≠ i
v : TProd α (i :: l)
⊢ v.elim hj = TProd.elim v.2 ⋯

Tactic:
simp [TProd.elim, hji]

Result:
no goals
-- Mathlib/Geometry/RingedSpace/LocallyRingedSpace.lean
@[simp]
lemma iso_hom_base_inv_base_apply {X Y : LocallyRingedSpace.{u}} (e : X ≅ Y) (x : X) :
    (e.inv.base (e.hom.base x)) = x

Proof state:
X Y : LocallyRingedSpace
e : X ≅ Y
x : ↑X.toTopCat
⊢ (ConcreteCategory.hom e.inv.base) ((ConcreteCategory.hom e.hom.base) x) = x

Tactic:
show (e.hom.base ≫ e.inv.base) x = 𝟙 X.toPresheafedSpace x

Result:
X Y : LocallyRingedSpace
e : X ≅ Y
x : ↑X.toTopCat
⊢ (ConcreteCategory.hom (e.hom.base ≫ e.inv.base)) x = (ConcreteCategory.hom (𝟙 X.toPresheafedSpace).base) x

Proof state:
X Y : LocallyRingedSpace
e : X ≅ Y
x : ↑X.toTopCat
⊢ (ConcreteCategory.hom (e.hom.base ≫ e.inv.base)) x = (ConcreteCategory.hom (𝟙 X.toPresheafedSpace).base) x

Tactic:
simp

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem _root_.List.contains_toArray [BEq α] {l : List α} {a : α} :
    l.toArray.contains a = l.contains a

Proof state:
α : Type u_1
inst✝ : BEq α
l : List α
a : α
⊢ l.toArray.contains a = l.contains a

Tactic:
simp [Array.contains, List.any_beq]

Result:
no goals
-- Mathlib/RingTheory/PowerSeries/Inverse.lean
theorem isUnit_divided_by_X_pow_order {f : k⟦X⟧} (hf : f ≠ 0) :
    IsUnit (divided_by_X_pow_order hf) :=
  ⟨Unit_of_divided_by_X_pow_order f,
    by simp only [Unit_of_divided_by_X_pow_order, dif_neg hf, Units.val_mk]⟩

Proof state:
k : Type u_2
inst✝ : Field k
f : k⟦X⟧
hf : f ≠ 0
⊢ ↑f.Unit_of_divided_by_X_pow_order = divided_by_X_pow_order hf

Tactic:
simp only [Unit_of_divided_by_X_pow_order, dif_neg hf, Units.val_mk]

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/AdjMatrix.lean
theorem toGraph_adjMatrix_eq [MulZeroOneClass α] [Nontrivial α] :
    (G.isAdjMatrix_adjMatrix α).toGraph = G

Proof state:
V : Type u_1
α : Type u_2
G : SimpleGraph V
inst✝² : DecidableRel G.Adj
inst✝¹ : MulZeroOneClass α
inst✝ : Nontrivial α
⊢ ⋯.toGraph = G

Tactic:
ext

Result:
case Adj.h.h.a
V : Type u_1
α : Type u_2
G : SimpleGraph V
inst✝² : DecidableRel G.Adj
inst✝¹ : MulZeroOneClass α
inst✝ : Nontrivial α
x✝¹ x✝ : V
⊢ ⋯.toGraph.Adj x✝¹ x✝ ↔ G.Adj x✝¹ x✝

Proof state:
case Adj.h.h.a
V : Type u_1
α : Type u_2
G : SimpleGraph V
inst✝² : DecidableRel G.Adj
inst✝¹ : MulZeroOneClass α
inst✝ : Nontrivial α
x✝¹ x✝ : V
⊢ ⋯.toGraph.Adj x✝¹ x✝ ↔ G.Adj x✝¹ x✝

Tactic:
simp only [IsAdjMatrix.toGraph_adj, adjMatrix_apply, ite_eq_left_iff, zero_ne_one]

Result:
case Adj.h.h.a
V : Type u_1
α : Type u_2
G : SimpleGraph V
inst✝² : DecidableRel G.Adj
inst✝¹ : MulZeroOneClass α
inst✝ : Nontrivial α
x✝¹ x✝ : V
⊢ ¬G.Adj x✝¹ x✝ → False ↔ G.Adj x✝¹ x✝

Proof state:
case Adj.h.h.a
V : Type u_1
α : Type u_2
G : SimpleGraph V
inst✝² : DecidableRel G.Adj
inst✝¹ : MulZeroOneClass α
inst✝ : Nontrivial α
x✝¹ x✝ : V
⊢ ¬G.Adj x✝¹ x✝ → False ↔ G.Adj x✝¹ x✝

Tactic:
apply Classical.not_not

Result:
no goals
-- Mathlib/Geometry/Manifold/MFDeriv/NormedSpace.lean
theorem MDifferentiableAt.clm_apply {g : M → F₁ →L[𝕜] F₂} {f : M → F₁} {x : M}
    (hg : MDifferentiableAt I 𝓘(𝕜, F₁ →L[𝕜] F₂) g x) (hf : MDifferentiableAt I 𝓘(𝕜, F₁) f x) :
    MDifferentiableAt I 𝓘(𝕜, F₂) (fun x => g x (f x)) x :=
  DifferentiableWithinAt.comp_mdifferentiableWithinAt (t := univ)
    (g := fun x : (F₁ →L[𝕜] F₂) × F₁ => x.1 x.2)
    (by apply (Differentiable.differentiableAt _).differentiableWithinAt
        exact differentiable_fst.clm_apply differentiable_snd) (hg.prod_mk_space hf)
    (by simp_rw [mapsTo_univ])

Proof state:
𝕜 : Type u_1
inst✝⁹ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace 𝕜 E
H : Type u_3
inst✝⁶ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝⁵ : TopologicalSpace M
inst✝⁴ : ChartedSpace H M
F₁ : Type u_14
inst✝³ : NormedAddCommGroup F₁
inst✝² : NormedSpace 𝕜 F₁
F₂ : Type u_15
inst✝¹ : NormedAddCommGroup F₂
inst✝ : NormedSpace 𝕜 F₂
g : M → F₁ →L[𝕜] F₂
f : M → F₁
x : M
hg : MDifferentiableAt I 𝓘(𝕜, F₁ →L[𝕜] F₂) g x
hf : MDifferentiableAt I 𝓘(𝕜, F₁) f x
⊢ DifferentiableWithinAt 𝕜 (fun x => x.1 x.2) univ (g x, f x)

Tactic:
apply (Differentiable.differentiableAt _).differentiableWithinAt

Result:
𝕜 : Type u_1
inst✝⁹ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace 𝕜 E
H : Type u_3
inst✝⁶ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝⁵ : TopologicalSpace M
inst✝⁴ : ChartedSpace H M
F₁ : Type u_14
inst✝³ : NormedAddCommGroup F₁
inst✝² : NormedSpace 𝕜 F₁
F₂ : Type u_15
inst✝¹ : NormedAddCommGroup F₂
inst✝ : NormedSpace 𝕜 F₂
g : M → F₁ →L[𝕜] F₂
f : M → F₁
x : M
hg : MDifferentiableAt I 𝓘(𝕜, F₁ →L[𝕜] F₂) g x
hf : MDifferentiableAt I 𝓘(𝕜, F₁) f x
⊢ Differentiable 𝕜 fun x => x.1 x.2

Proof state:
𝕜 : Type u_1
inst✝⁹ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace 𝕜 E
H : Type u_3
inst✝⁶ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝⁵ : TopologicalSpace M
inst✝⁴ : ChartedSpace H M
F₁ : Type u_14
inst✝³ : NormedAddCommGroup F₁
inst✝² : NormedSpace 𝕜 F₁
F₂ : Type u_15
inst✝¹ : NormedAddCommGroup F₂
inst✝ : NormedSpace 𝕜 F₂
g : M → F₁ →L[𝕜] F₂
f : M → F₁
x : M
hg : MDifferentiableAt I 𝓘(𝕜, F₁ →L[𝕜] F₂) g x
hf : MDifferentiableAt I 𝓘(𝕜, F₁) f x
⊢ MapsTo (fun x => (g x, f x)) univ univ

Tactic:
simp_rw [mapsTo_univ]

Result:
no goals

Proof state:
𝕜 : Type u_1
inst✝⁹ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace 𝕜 E
H : Type u_3
inst✝⁶ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝⁵ : TopologicalSpace M
inst✝⁴ : ChartedSpace H M
F₁ : Type u_14
inst✝³ : NormedAddCommGroup F₁
inst✝² : NormedSpace 𝕜 F₁
F₂ : Type u_15
inst✝¹ : NormedAddCommGroup F₂
inst✝ : NormedSpace 𝕜 F₂
g : M → F₁ →L[𝕜] F₂
f : M → F₁
x : M
hg : MDifferentiableAt I 𝓘(𝕜, F₁ →L[𝕜] F₂) g x
hf : MDifferentiableAt I 𝓘(𝕜, F₁) f x
⊢ Differentiable 𝕜 fun x => x.1 x.2

Tactic:
exact differentiable_fst.clm_apply differentiable_snd

Result:
no goals
-- Mathlib/RingTheory/SimpleModule/Basic.lean
theorem covBy_iff_quot_is_simple {A B : Submodule R M} (hAB : A ≤ B) :
    A ⋖ B ↔ IsSimpleModule R (B ⧸ Submodule.comap B.subtype A)

Proof state:
R : Type u_2
inst✝² : Ring R
M : Type u_4
inst✝¹ : AddCommGroup M
inst✝ : Module R M
A B : Submodule R M
hAB : A ≤ B
f : Submodule R ↥B ≃o ↑(Set.Iic B) := B.mapIic
hf : f = B.mapIic
⊢ IsCoatom ⟨A, hAB⟩ ↔ IsCoatom (B.mapIic (Submodule.comap B.subtype A))

Tactic:
simp [-OrderIso.isCoatom_iff, Submodule.map_comap_subtype, inf_eq_right.2 hAB]

Result:
no goals

Proof state:
R : Type u_2
inst✝² : Ring R
M : Type u_4
inst✝¹ : AddCommGroup M
inst✝ : Module R M
A B : Submodule R M
hAB : A ≤ B
⊢ A ⋖ B ↔ IsSimpleModule R (↥B ⧸ Submodule.comap B.subtype A)

Tactic:
set f : Submodule R B ≃o Set.Iic B := B.mapIic with hf

Result:
R : Type u_2
inst✝² : Ring R
M : Type u_4
inst✝¹ : AddCommGroup M
inst✝ : Module R M
A B : Submodule R M
hAB : A ≤ B
f : Submodule R ↥B ≃o ↑(Set.Iic B) := B.mapIic
hf : f = B.mapIic
⊢ A ⋖ B ↔ IsSimpleModule R (↥B ⧸ Submodule.comap B.subtype A)

Proof state:
R : Type u_2
inst✝² : Ring R
M : Type u_4
inst✝¹ : AddCommGroup M
inst✝ : Module R M
A B : Submodule R M
hAB : A ≤ B
f : Submodule R ↥B ≃o ↑(Set.Iic B) := B.mapIic
hf : f = B.mapIic
⊢ A ⋖ B ↔ IsSimpleModule R (↥B ⧸ Submodule.comap B.subtype A)

Tactic:
rw [covBy_iff_coatom_Iic hAB, isSimpleModule_iff_isCoatom, ← OrderIso.isCoatom_iff f, hf]

Result:
R : Type u_2
inst✝² : Ring R
M : Type u_4
inst✝¹ : AddCommGroup M
inst✝ : Module R M
A B : Submodule R M
hAB : A ≤ B
f : Submodule R ↥B ≃o ↑(Set.Iic B) := B.mapIic
hf : f = B.mapIic
⊢ IsCoatom ⟨A, hAB⟩ ↔ IsCoatom (B.mapIic (Submodule.comap B.subtype A))
-- Mathlib/Order/Filter/Basic.lean
theorem Eventually.choice {r : α → β → Prop} {l : Filter α} [l.NeBot] (h : ∀ᶠ x in l, ∃ y, r x y) :
    ∃ f : α → β, ∀ᶠ x in l, r x (f x)

Proof state:
α : Type u
β : Type v
r : α → β → Prop
l : Filter α
inst✝ : l.NeBot
h : ∀ᶠ (x : α) in l, ∃ y, r x y
this : Nonempty β
f : α → β
hf : ∀ (x : α), (∃ y, r x y) → r x (f x)
⊢ ∃ f, ∀ᶠ (x : α) in l, r x (f x)

Tactic:
exact ⟨f, h.mono hf⟩

Result:
no goals

Proof state:
α : Type u
β : Type v
r : α → β → Prop
l : Filter α
inst✝ : l.NeBot
h : ∀ᶠ (x : α) in l, ∃ y, r x y
⊢ ∃ f, ∀ᶠ (x : α) in l, r x (f x)

Tactic:
haveI : Nonempty β := let ⟨_, hx⟩ := h.exists; hx.nonempty

Result:
α : Type u
β : Type v
r : α → β → Prop
l : Filter α
inst✝ : l.NeBot
h : ∀ᶠ (x : α) in l, ∃ y, r x y
this : Nonempty β
⊢ ∃ f, ∀ᶠ (x : α) in l, r x (f x)

Proof state:
α : Type u
β : Type v
r : α → β → Prop
l : Filter α
inst✝ : l.NeBot
h : ∀ᶠ (x : α) in l, ∃ y, r x y
this : Nonempty β
⊢ ∃ f, ∀ᶠ (x : α) in l, r x (f x)

Tactic:
choose! f hf using fun x (hx : ∃ y, r x y) => hx

Result:
α : Type u
β : Type v
r : α → β → Prop
l : Filter α
inst✝ : l.NeBot
h : ∀ᶠ (x : α) in l, ∃ y, r x y
this : Nonempty β
f : α → β
hf : ∀ (x : α), (∃ y, r x y) → r x (f x)
⊢ ∃ f, ∀ᶠ (x : α) in l, r x (f x)