harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/RingTheory/LinearDisjoint.lean
theorem of_isField' {A : Type v} [CommRing A] {B : Type w} [CommRing B]
    [Algebra R A] [Algebra R B] (H : IsField (A ⊗[R] B))
    (fa : A →ₐ[R] S) (fb : B →ₐ[R] S) (hfa : Function.Injective fa) (hfb : Function.Injective fb) :
    fa.range.LinearDisjoint fb.range

Proof state:
R : Type u
S : Type v
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
A : Type v
inst✝³ : CommRing A
B : Type w
inst✝² : CommRing B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
H : IsField (A ⊗[R] B)
fa : A →ₐ[R] S
fb : B →ₐ[R] S
hfa : Function.Injective ⇑fa
hfb : Function.Injective ⇑fb
⊢ fa.range.LinearDisjoint fb.range

Tactic:
apply of_isField

Result:
case H
R : Type u
S : Type v
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
A : Type v
inst✝³ : CommRing A
B : Type w
inst✝² : CommRing B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
H : IsField (A ⊗[R] B)
fa : A →ₐ[R] S
fb : B →ₐ[R] S
hfa : Function.Injective ⇑fa
hfb : Function.Injective ⇑fb
⊢ IsField (↥fa.range ⊗[R] ↥fb.range)

Proof state:
case H
R : Type u
S : Type v
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
A : Type v
inst✝³ : CommRing A
B : Type w
inst✝² : CommRing B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
H : IsField (A ⊗[R] B)
fa : A →ₐ[R] S
fb : B →ₐ[R] S
hfa : Function.Injective ⇑fa
hfb : Function.Injective ⇑fb
⊢ IsField (↥fa.range ⊗[R] ↥fb.range)

Tactic:
exact Algebra.TensorProduct.congr (AlgEquiv.ofInjective fa hfa)
  (AlgEquiv.ofInjective fb hfb) |>.symm.toMulEquiv.isField _ H

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem foldlM_reverse' [Monad m] (l : Array α) (f : β → α → m β) (b)
    (w : stop = l.size) :
    l.reverse.foldlM f b 0 stop = l.foldrM (fun x y => f y x) b

Proof state:
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝ : Monad m
l : Array α
f : β → α → m β
b : β
⊢ foldlM f b l.reverse 0 l.size = foldrM (fun x y => f y x) b l

Tactic:
rcases l with ⟨l⟩

Result:
case mk
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝ : Monad m
f : β → α → m β
b : β
l : List α
⊢ foldlM f b { toList := l }.reverse 0 { toList := l }.size = foldrM (fun x y => f y x) b { toList := l }

Proof state:
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
stop : Nat
inst✝ : Monad m
l : Array α
f : β → α → m β
b : β
w : stop = l.size
⊢ foldlM f b l.reverse 0 stop = foldrM (fun x y => f y x) b l

Tactic:
subst w

Result:
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝ : Monad m
l : Array α
f : β → α → m β
b : β
⊢ foldlM f b l.reverse 0 l.size = foldrM (fun x y => f y x) b l

Proof state:
case mk
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝ : Monad m
f : β → α → m β
b : β
l : List α
⊢ foldlM f b { toList := l }.reverse 0 { toList := l }.size = foldrM (fun x y => f y x) b { toList := l }

Tactic:
simp [List.foldlM_reverse]

Result:
no goals
-- Mathlib/Computability/TMConfig.lean
theorem exists_code.comp {m n} {f : List.Vector ℕ n →. ℕ} {g : Fin n → List.Vector ℕ m →. ℕ}
    (hf : ∃ c : Code, ∀ v : List.Vector ℕ n, c.eval v.1 = pure <$> f v)
    (hg : ∀ i, ∃ c : Code, ∀ v : List.Vector ℕ m, c.eval v.1 = pure <$> g i v) :
    ∃ c : Code, ∀ v : List.Vector ℕ m,
      c.eval v.1 = pure <$> ((List.Vector.mOfFn fun i => g i v) >>= f)

Proof state:
case succ.intro
m n : ℕ
IH :
  ∀ {g : Fin n → List.Vector ℕ m →. ℕ},
    (∀ (i : Fin n), ∃ c, ∀ (v : List.Vector ℕ m), c.eval ↑v = pure <$> g i v) →
      ∃ c, ∀ (v : List.Vector ℕ m), c.eval ↑v = Subtype.val <$> Vector.mOfFn fun i => g i v
g : Fin (n + 1) → List.Vector ℕ m →. ℕ
hg : ∀ (i : Fin (n + 1)), ∃ c, ∀ (v : List.Vector ℕ m), c.eval ↑v = pure <$> g i v
cg : Code
hg₁ : ∀ (v : List.Vector ℕ m), cg.eval ↑v = pure <$> g 0 v
⊢ ∃ c, ∀ (v : List.Vector ℕ m), c.eval ↑v = Subtype.val <$> Vector.mOfFn fun i => g i v

Tactic:
obtain ⟨cl, hl⟩ := IH fun i => hg i.succ

Result:
case succ.intro.intro
m n : ℕ
IH :
  ∀ {g : Fin n → List.Vector ℕ m →. ℕ},
    (∀ (i : Fin n), ∃ c, ∀ (v : List.Vector ℕ m), c.eval ↑v = pure <$> g i v) →
      ∃ c, ∀ (v : List.Vector ℕ m), c.eval ↑v = Subtype.val <$> Vector.mOfFn fun i => g i v
g : Fin (n + 1) → List.Vector ℕ m →. ℕ
hg : ∀ (i : Fin (n + 1)), ∃ c, ∀ (v : List.Vector ℕ m), c.eval ↑v = pure <$> g i v
cg : Code
hg₁ : ∀ (v : List.Vector ℕ m), cg.eval ↑v = pure <$> g 0 v
cl : Code
hl : ∀ (v : List.Vector ℕ m), cl.eval ↑v = Subtype.val <$> Vector.mOfFn fun i => g i.succ v
⊢ ∃ c, ∀ (v : List.Vector ℕ m), c.eval ↑v = Subtype.val <$> Vector.mOfFn fun i => g i v

Proof state:
m n : ℕ
IH :
  ∀ {g : Fin n → List.Vector ℕ m →. ℕ},
    (∀ (i : Fin n), ∃ c, ∀ (v : List.Vector ℕ m), c.eval ↑v = pure <$> g i v) →
      ∃ c, ∀ (v : List.Vector ℕ m), c.eval ↑v = Subtype.val <$> Vector.mOfFn fun i => g i v
g : Fin (n + 1) → List.Vector ℕ m →. ℕ
hg : ∀ (i : Fin (n + 1)), ∃ c, ∀ (v : List.Vector ℕ m), c.eval ↑v = pure <$> g i v
cg : Code
hg₁ : ∀ (v : List.Vector ℕ m), cg.eval ↑v = pure <$> g 0 v
cl : Code
hl : ∀ (v : List.Vector ℕ m), cl.eval ↑v = Subtype.val <$> Vector.mOfFn fun i => g i.succ v
v : List.Vector ℕ m
⊢ (do
      let a ← g 0 v
      let a_1 ← Vector.mOfFn fun i => g i.succ v
      Part.some (a :: ↑a_1)) =
    do
    let a ← g 0 v
    let a_1 ← Vector.mOfFn fun i => g i.succ v
    Subtype.val <$> Part.some (a ::ᵥ a_1)

Tactic:
rfl

Result:
no goals
-- Mathlib/LinearAlgebra/SesquilinearForm.lean
theorem isRefl (H : B.IsSymm) : B.IsRefl := fun x y H1 ↦ by
  rw [← H.eq]
  simp [H1]

Proof state:
R : Type u_1
M : Type u_5
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
I : R →+* R
B : M →ₛₗ[I] M →ₗ[R] R
H : B.IsSymm
x y : M
H1 : (B x) y = 0
⊢ I ((B x) y) = 0

Tactic:
simp [H1]

Result:
no goals

Proof state:
R : Type u_1
M : Type u_5
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
I : R →+* R
B : M →ₛₗ[I] M →ₗ[R] R
H : B.IsSymm
x y : M
H1 : (B x) y = 0
⊢ (B y) x = 0

Tactic:
rw [← H.eq]

Result:
R : Type u_1
M : Type u_5
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
I : R →+* R
B : M →ₛₗ[I] M →ₗ[R] R
H : B.IsSymm
x y : M
H1 : (B x) y = 0
⊢ I ((B x) y) = 0
-- Mathlib/Analysis/Convex/Visible.lean
lemma isVisible_iff_lineMap (hxy : x ≠ y) :
    IsVisible 𝕜 s x y ↔ ∀ δ ∈ Set.Ioo (0 : 𝕜) 1, lineMap x y δ ∉ s

Proof state:
𝕜 : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : LinearOrderedField 𝕜
inst✝² : AddCommGroup V
inst✝¹ : Module 𝕜 V
inst✝ : AddTorsor V P
s : Set P
x y : P
hxy : x ≠ y
⊢ IsVisible 𝕜 s x y ↔ ∀ δ ∈ Set.Ioo 0 1, (lineMap x y) δ ∉ s

Tactic:
simp [IsVisible, sbtw_iff_mem_image_Ioo_and_ne, hxy]

Result:
𝕜 : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : LinearOrderedField 𝕜
inst✝² : AddCommGroup V
inst✝¹ : Module 𝕜 V
inst✝ : AddTorsor V P
s : Set P
x y : P
hxy : x ≠ y
⊢ (∀ ⦃z : P⦄, z ∈ s → ∀ (x_1 : 𝕜), 0 < x_1 → x_1 < 1 → ¬(lineMap x y) x_1 = z) ↔
    ∀ (δ : 𝕜), 0 < δ → δ < 1 → (lineMap x y) δ ∉ s

Proof state:
𝕜 : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : LinearOrderedField 𝕜
inst✝² : AddCommGroup V
inst✝¹ : Module 𝕜 V
inst✝ : AddTorsor V P
s : Set P
x y : P
hxy : x ≠ y
⊢ (∀ ⦃z : P⦄, z ∈ s → ∀ (x_1 : 𝕜), 0 < x_1 → x_1 < 1 → ¬(lineMap x y) x_1 = z) ↔
    ∀ (δ : 𝕜), 0 < δ → δ < 1 → (lineMap x y) δ ∉ s

Tactic:
aesop

Result:
no goals
-- Mathlib/Order/Atoms.lean
theorem isCoatom_iff [OrderTop α] [IsCoatomic α] [OrderTop β] {l : α → β} {u : β → α}
    (gi : GaloisInsertion l u) (h_coatom : ∀ a : α, IsCoatom a → u (l a) = a) (b : β) :
    IsCoatom (u b) ↔ IsCoatom b

Proof state:
α : Type u_2
β : Type u_3
inst✝⁴ : PartialOrder α
inst✝³ : PartialOrder β
inst✝² : OrderTop α
inst✝¹ : IsCoatomic α
inst✝ : OrderTop β
l : α → β
u : β → α
gi : GaloisInsertion l u
h_coatom : ∀ (a : α), IsCoatom a → u (l a) = a
b : β
⊢ IsCoatom (u b) ↔ IsCoatom b

Tactic:
refine ⟨fun hb => gi.isCoatom_of_image hb, fun hb => ?_⟩

Result:
α : Type u_2
β : Type u_3
inst✝⁴ : PartialOrder α
inst✝³ : PartialOrder β
inst✝² : OrderTop α
inst✝¹ : IsCoatomic α
inst✝ : OrderTop β
l : α → β
u : β → α
gi : GaloisInsertion l u
h_coatom : ∀ (a : α), IsCoatom a → u (l a) = a
b : β
hb : IsCoatom b
⊢ IsCoatom (u b)

Proof state:
α : Type u_2
β : Type u_3
inst✝⁴ : PartialOrder α
inst✝³ : PartialOrder β
inst✝² : OrderTop α
inst✝¹ : IsCoatomic α
inst✝ : OrderTop β
l : α → β
u : β → α
gi : GaloisInsertion l u
h_coatom : ∀ (a : α), IsCoatom a → u (l a) = a
b : β
hb : IsCoatom b
⊢ IsCoatom (u b)

Tactic:
obtain ⟨a, ha, hab⟩ :=
  (eq_top_or_exists_le_coatom (u b)).resolve_left fun h =>
    hb.1 <| (gi.gc.u_top ▸ gi.l_u_eq ⊤ : l ⊤ = ⊤) ▸ gi.l_u_eq b ▸ congr_arg l h

Result:
case intro.intro
α : Type u_2
β : Type u_3
inst✝⁴ : PartialOrder α
inst✝³ : PartialOrder β
inst✝² : OrderTop α
inst✝¹ : IsCoatomic α
inst✝ : OrderTop β
l : α → β
u : β → α
gi : GaloisInsertion l u
h_coatom : ∀ (a : α), IsCoatom a → u (l a) = a
b : β
hb : IsCoatom b
a : α
ha : IsCoatom a
hab : u b ≤ a
⊢ IsCoatom (u b)

Proof state:
case intro.intro
α : Type u_2
β : Type u_3
inst✝⁴ : PartialOrder α
inst✝³ : PartialOrder β
inst✝² : OrderTop α
inst✝¹ : IsCoatomic α
inst✝ : OrderTop β
l : α → β
u : β → α
gi : GaloisInsertion l u
h_coatom : ∀ (a : α), IsCoatom a → u (l a) = a
b : β
hb : IsCoatom b
a : α
ha : IsCoatom a
hab : u b ≤ a
⊢ IsCoatom (u b)

Tactic:
have : l a = b :=
  (hb.le_iff.mp (gi.l_u_eq b ▸ gi.gc.monotone_l hab : b ≤ l a)).resolve_left fun hla =>
    ha.1 (gi.gc.u_top ▸ h_coatom a ha ▸ congr_arg u hla)

Result:
case intro.intro
α : Type u_2
β : Type u_3
inst✝⁴ : PartialOrder α
inst✝³ : PartialOrder β
inst✝² : OrderTop α
inst✝¹ : IsCoatomic α
inst✝ : OrderTop β
l : α → β
u : β → α
gi : GaloisInsertion l u
h_coatom : ∀ (a : α), IsCoatom a → u (l a) = a
b : β
hb : IsCoatom b
a : α
ha : IsCoatom a
hab : u b ≤ a
this : l a = b
⊢ IsCoatom (u b)

Proof state:
case intro.intro
α : Type u_2
β : Type u_3
inst✝⁴ : PartialOrder α
inst✝³ : PartialOrder β
inst✝² : OrderTop α
inst✝¹ : IsCoatomic α
inst✝ : OrderTop β
l : α → β
u : β → α
gi : GaloisInsertion l u
h_coatom : ∀ (a : α), IsCoatom a → u (l a) = a
b : β
hb : IsCoatom b
a : α
ha : IsCoatom a
hab : u b ≤ a
this : l a = b
⊢ IsCoatom (u b)

Tactic:
exact this ▸ (h_coatom a ha).symm ▸ ha

Result:
no goals
-- Mathlib/MeasureTheory/Function/LpSeminorm/TriangleInequality.lean
theorem LpAddConst_of_one_le {p : ℝ≥0∞} (hp : 1 ≤ p) : LpAddConst p = 1

Proof state:
p : ℝ≥0∞
hp : 1 ≤ p
⊢ LpAddConst p = 1

Tactic:
rw [LpAddConst, if_neg]

Result:
case hnc
p : ℝ≥0∞
hp : 1 ≤ p
⊢ p ∉ Set.Ioo 0 1

Proof state:
case hnc
p : ℝ≥0∞
hp : 1 ≤ p
⊢ p ∉ Set.Ioo 0 1

Tactic:
intro h

Result:
case hnc
p : ℝ≥0∞
hp : 1 ≤ p
h : p ∈ Set.Ioo 0 1
⊢ False

Proof state:
case hnc
p : ℝ≥0∞
hp : 1 ≤ p
h : p ∈ Set.Ioo 0 1
⊢ False

Tactic:
exact lt_irrefl _ (h.2.trans_le hp)

Result:
no goals
-- Mathlib/Algebra/Polynomial/Monic.lean
theorem nextCoeff_mul (hp : Monic p) (hq : Monic q) :
    nextCoeff (p * q) = nextCoeff p + nextCoeff q

Proof state:
R : Type u
inst✝ : Semiring R
p q : R[X]
hp : p.Monic
hq : q.Monic
a✝ : Nontrivial R
⊢ (p * q).nextCoeff = p.nextCoeff + q.nextCoeff

Tactic:
simp only [← coeff_one_reverse]

Result:
R : Type u
inst✝ : Semiring R
p q : R[X]
hp : p.Monic
hq : q.Monic
a✝ : Nontrivial R
⊢ (p * q).reverse.coeff 1 = p.reverse.coeff 1 + q.reverse.coeff 1

Proof state:
R : Type u
inst✝ : Semiring R
p q : R[X]
hp : p.Monic
hq : q.Monic
a✝ : Nontrivial R
⊢ (p * q).reverse.coeff 1 = p.reverse.coeff 1 + q.reverse.coeff 1

Tactic:
rw [reverse_mul] <;> simp [hp.leadingCoeff, hq.leadingCoeff, mul_coeff_one, add_comm]

Result:
no goals

Proof state:
R : Type u
inst✝ : Semiring R
p q : R[X]
hp : p.Monic
hq : q.Monic
⊢ (p * q).nextCoeff = p.nextCoeff + q.nextCoeff

Tactic:
nontriviality

Result:
R : Type u
inst✝ : Semiring R
p q : R[X]
hp : p.Monic
hq : q.Monic
a✝ : Nontrivial R
⊢ (p * q).nextCoeff = p.nextCoeff + q.nextCoeff
-- Mathlib/Topology/EMetricSpace/Defs.lean
theorem edist_pos {x y : γ} : 0 < edist x y ↔ x ≠ y

Proof state:
γ : Type w
inst✝ : EMetricSpace γ
x y : γ
⊢ 0 < edist x y ↔ x ≠ y

Tactic:
simp [← not_le]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Log/Base.lean
theorem natCeil_logb_natCast (b : ℕ) (n : ℕ) : ⌈logb b n⌉₊ = Nat.clog b n

Proof state:
case succ.succ.inr
n b : ℕ
hn : n ≠ 0
⊢ ⌈logb ↑(b + 1 + 1) ↑n⌉₊ = Nat.clog (b + 1 + 1) n

Tactic:
rw [← Nat.cast_inj (R := ℤ), Int.natCast_ceil_eq_ceil, ceil_logb_natCast (by simp),
  Int.clog_natCast]

Result:
case succ.succ.inr
n b : ℕ
hn : n ≠ 0
⊢ 0 ≤ logb ↑(b + 1 + 1) ↑n

Proof state:
case succ.succ
n b : ℕ
⊢ ⌈logb ↑(b + 1 + 1) ↑n⌉₊ = Nat.clog (b + 1 + 1) n

Tactic:
obtain rfl | hn := eq_or_ne n 0

Result:
case succ.succ.inl
b : ℕ
⊢ ⌈logb ↑(b + 1 + 1) ↑0⌉₊ = Nat.clog (b + 1 + 1) 0

case succ.succ.inr
n b : ℕ
hn : n ≠ 0
⊢ ⌈logb ↑(b + 1 + 1) ↑n⌉₊ = Nat.clog (b + 1 + 1) n

Proof state:
n b : ℕ
hn : n ≠ 0
⊢ 0 ≤ ↑n

Tactic:
simp

Result:
no goals

Proof state:
case zero
n : ℕ
⊢ ⌈logb ↑0 ↑n⌉₊ = Nat.clog 0 n

Tactic:
simp [Real.logb]

Result:
no goals

Proof state:
n b : ℕ
hn : n ≠ 0
⊢ 1 < ↑(b + 1 + 1)

Tactic:
simp [Nat.cast_add_one_pos]

Result:
no goals

Proof state:
case succ.succ.inl
b : ℕ
⊢ ⌈logb ↑(b + 1 + 1) ↑0⌉₊ = Nat.clog (b + 1 + 1) 0

Tactic:
simp

Result:
no goals

Proof state:
b n : ℕ
⊢ ⌈logb ↑b ↑n⌉₊ = Nat.clog b n

Tactic:
obtain _ | _ | b := b

Result:
case zero
n : ℕ
⊢ ⌈logb ↑0 ↑n⌉₊ = Nat.clog 0 n

case succ.zero
n : ℕ
⊢ ⌈logb ↑(0 + 1) ↑n⌉₊ = Nat.clog (0 + 1) n

case succ.succ
n b : ℕ
⊢ ⌈logb ↑(b + 1 + 1) ↑n⌉₊ = Nat.clog (b + 1 + 1) n

Proof state:
n b : ℕ
hn : n ≠ 0
⊢ 1 ≤ n

Tactic:
omega

Result:
no goals

Proof state:
case succ.zero
n : ℕ
⊢ ⌈logb ↑(0 + 1) ↑n⌉₊ = Nat.clog (0 + 1) n

Tactic:
simp [Real.logb]

Result:
no goals

Proof state:
case succ.succ.inr
n b : ℕ
hn : n ≠ 0
⊢ 0 ≤ logb ↑(b + 1 + 1) ↑n

Tactic:
exact logb_nonneg (by simp [Nat.cast_add_one_pos]) (Nat.one_le_cast.2 (by omega))

Result:
no goals
-- Mathlib/Combinatorics/Enumerative/Composition.lean
theorem mem_range_embedding_iff' {j : Fin n} {i : Fin c.length} :
    j ∈ Set.range (c.embedding i) ↔ i = c.index j

Proof state:
case mpr
n : ℕ
c : Composition n
j : Fin n
i : Fin c.length
⊢ i = c.index j → j ∈ Set.range ⇑(c.embedding i)

Tactic:
intro h

Result:
case mpr
n : ℕ
c : Composition n
j : Fin n
i : Fin c.length
h : i = c.index j
⊢ j ∈ Set.range ⇑(c.embedding i)

Proof state:
case mp
n : ℕ
c : Composition n
j : Fin n
i : Fin c.length
⊢ j ∈ Set.range ⇑(c.embedding i) → i = c.index j

Tactic:
rw [← not_imp_not]

Result:
case mp
n : ℕ
c : Composition n
j : Fin n
i : Fin c.length
⊢ ¬i = c.index j → j ∉ Set.range ⇑(c.embedding i)

Proof state:
case mpr
n : ℕ
c : Composition n
j : Fin n
i : Fin c.length
h : i = c.index j
⊢ j ∈ Set.range ⇑(c.embedding i)

Tactic:
rw [h]

Result:
case mpr
n : ℕ
c : Composition n
j : Fin n
i : Fin c.length
h : i = c.index j
⊢ j ∈ Set.range ⇑(c.embedding (c.index j))

Proof state:
case mp
n : ℕ
c : Composition n
j : Fin n
i : Fin c.length
h : ¬i = c.index j
⊢ j ∉ Set.range ⇑(c.embedding i)

Tactic:
exact Set.disjoint_right.1 (c.disjoint_range h) (c.mem_range_embedding j)

Result:
no goals

Proof state:
case mp
n : ℕ
c : Composition n
j : Fin n
i : Fin c.length
⊢ ¬i = c.index j → j ∉ Set.range ⇑(c.embedding i)

Tactic:
intro h

Result:
case mp
n : ℕ
c : Composition n
j : Fin n
i : Fin c.length
h : ¬i = c.index j
⊢ j ∉ Set.range ⇑(c.embedding i)

Proof state:
case mpr
n : ℕ
c : Composition n
j : Fin n
i : Fin c.length
h : i = c.index j
⊢ j ∈ Set.range ⇑(c.embedding (c.index j))

Tactic:
exact c.mem_range_embedding j

Result:
no goals

Proof state:
n : ℕ
c : Composition n
j : Fin n
i : Fin c.length
⊢ j ∈ Set.range ⇑(c.embedding i) ↔ i = c.index j

Tactic:
constructor

Result:
case mp
n : ℕ
c : Composition n
j : Fin n
i : Fin c.length
⊢ j ∈ Set.range ⇑(c.embedding i) → i = c.index j

case mpr
n : ℕ
c : Composition n
j : Fin n
i : Fin c.length
⊢ i = c.index j → j ∈ Set.range ⇑(c.embedding i)
-- Mathlib/Data/Multiset/Fintype.lean
lemma coe_consEquiv_of_ne {v : α} (x : v ::ₘ m) (hx : ↑x ≠ v) :
    consEquiv x = some ⟨x.1, x.2.cast (by simp [hx])⟩

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
m : Multiset α
v : α
x : (v ::ₘ m).ToType
hx : x.fst ≠ v
⊢ count x.fst (v ::ₘ m) = count x.fst m

Tactic:
simp [hx]

Result:
no goals

Proof state:
α : Type u_1
inst✝ : DecidableEq α
m : Multiset α
v : α
x : (v ::ₘ m).ToType
hx : x.fst ≠ v
⊢ ⟨x.fst, ⟨↑x.snd, ⋯⟩⟩ = ⟨x.fst, Fin.cast ⋯ x.snd⟩

Tactic:
rfl

Result:
no goals

Proof state:
α : Type u_1
inst✝ : DecidableEq α
m : Multiset α
v : α
x : (v ::ₘ m).ToType
hx : x.fst ≠ v
⊢ consEquiv x = some ⟨x.fst, Fin.cast ⋯ x.snd⟩

Tactic:
simp [consEquiv, hx]

Result:
α : Type u_1
inst✝ : DecidableEq α
m : Multiset α
v : α
x : (v ::ₘ m).ToType
hx : x.fst ≠ v
⊢ ⟨x.fst, ⟨↑x.snd, ⋯⟩⟩ = ⟨x.fst, Fin.cast ⋯ x.snd⟩
-- Mathlib/Data/Fin/Tuple/Basic.lean
theorem le_cons [∀ i, Preorder (α i)] {x : α 0} {q : ∀ i, α i} {p : ∀ i : Fin n, α i.succ} :
    q ≤ cons x p ↔ q 0 ≤ x ∧ tail q ≤ p :=
  forall_fin_succ.trans <| and_congr Iff.rfl <| forall_congr' fun j ↦ by simp [tail]

Proof state:
n : ℕ
α : Fin (n + 1) → Type u_1
inst✝ : (i : Fin (n + 1)) → Preorder (α i)
x : α 0
q : (i : Fin (n + 1)) → α i
p : (i : Fin n) → α i.succ
j : Fin n
⊢ q j.succ ≤ cons x p j.succ ↔ tail q j ≤ p j

Tactic:
simp [tail]

Result:
no goals
-- Mathlib/Data/Set/Pointwise/SMul.lean
theorem zero_mem_smul_set_iff (ha : a ≠ 0) : (0 : β) ∈ a • t ↔ (0 : β) ∈ t

Proof state:
case intro.intro
α : Type u_2
β : Type u_3
inst✝³ : Zero β
inst✝² : SMulZeroClass α β
t : Set β
a : α
inst✝¹ : Zero α
inst✝ : NoZeroSMulDivisors α β
ha : a ≠ 0
b : β
hb : b ∈ t
h : (fun x => a • x) b = 0
⊢ 0 ∈ t

Tactic:
rwa [(eq_zero_or_eq_zero_of_smul_eq_zero h).resolve_left ha] at hb

Result:
no goals

Proof state:
α : Type u_2
β : Type u_3
inst✝³ : Zero β
inst✝² : SMulZeroClass α β
t : Set β
a : α
inst✝¹ : Zero α
inst✝ : NoZeroSMulDivisors α β
ha : a ≠ 0
⊢ 0 ∈ a • t → 0 ∈ t

Tactic:
rintro ⟨b, hb, h⟩

Result:
case intro.intro
α : Type u_2
β : Type u_3
inst✝³ : Zero β
inst✝² : SMulZeroClass α β
t : Set β
a : α
inst✝¹ : Zero α
inst✝ : NoZeroSMulDivisors α β
ha : a ≠ 0
b : β
hb : b ∈ t
h : (fun x => a • x) b = 0
⊢ 0 ∈ t

Proof state:
α : Type u_2
β : Type u_3
inst✝³ : Zero β
inst✝² : SMulZeroClass α β
t : Set β
a : α
inst✝¹ : Zero α
inst✝ : NoZeroSMulDivisors α β
ha : a ≠ 0
⊢ 0 ∈ a • t ↔ 0 ∈ t

Tactic:
refine ⟨?_, zero_mem_smul_set⟩

Result:
α : Type u_2
β : Type u_3
inst✝³ : Zero β
inst✝² : SMulZeroClass α β
t : Set β
a : α
inst✝¹ : Zero α
inst✝ : NoZeroSMulDivisors α β
ha : a ≠ 0
⊢ 0 ∈ a • t → 0 ∈ t
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem getElem_replicate {n w : Nat} (x : BitVec w) (h : i < w * n) :
    (x.replicate n)[i] = if h' : w = 0 then false else x[i % w]'(@Nat.mod_lt i w (by omega))

Proof state:
i n w : Nat
x : BitVec w
h : i < w * n
⊢ (replicate n x)[i] = if h' : w = 0 then false else x[i % w]

Tactic:
simp only [← getLsbD_eq_getElem, getLsbD_replicate]

Result:
i n w : Nat
x : BitVec w
h : i < w * n
⊢ (decide (i < w * n) && x.getLsbD (i % w)) = if h : w = 0 then false else x.getLsbD (i % w)

Proof state:
i n w : Nat
x : BitVec w
h : i < w * n
h' : ¬w = 0
⊢ w > 0

Tactic:
omega

Result:
no goals

Proof state:
i n w : Nat
x : BitVec w
h : i < w * n
⊢ (decide (i < w * n) && x.getLsbD (i % w)) = if h : w = 0 then false else x.getLsbD (i % w)

Tactic:
by_cases h' : w = 0 <;> simp [h'] <;> omega

Result:
no goals
-- Mathlib/Algebra/Lie/Derivation/Killing.lean
/-- Every derivation of a finite-dimensional Killing Lie algebra is an inner derivation. -/
lemma exists_eq_ad (D : 𝔻) : ∃ x, ad R L x = D

Proof state:
R : Type u_1
L : Type u_2
inst✝⁴ : Field R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
inst✝¹ : Module.Finite R L
inst✝ : LieAlgebra.IsKilling R L
D : LieDerivation R L L
⊢ D ∈ ⊤

Tactic:
exact Submodule.mem_top

Result:
no goals

Proof state:
R : Type u_1
L : Type u_2
inst✝⁴ : Field R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
inst✝¹ : Module.Finite R L
inst✝ : LieAlgebra.IsKilling R L
D : LieDerivation R L L
⊢ D ∈ (ad R L).range

Tactic:
rw [range_ad_eq_top R L]

Result:
R : Type u_1
L : Type u_2
inst✝⁴ : Field R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
inst✝¹ : Module.Finite R L
inst✝ : LieAlgebra.IsKilling R L
D : LieDerivation R L L
⊢ D ∈ ⊤

Proof state:
R : Type u_1
L : Type u_2
inst✝⁴ : Field R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
inst✝¹ : Module.Finite R L
inst✝ : LieAlgebra.IsKilling R L
D : LieDerivation R L L
⊢ ∃ x, (ad R L) x = D

Tactic:
change D ∈ 𝕀

Result:
R : Type u_1
L : Type u_2
inst✝⁴ : Field R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
inst✝¹ : Module.Finite R L
inst✝ : LieAlgebra.IsKilling R L
D : LieDerivation R L L
⊢ D ∈ (ad R L).range
-- Mathlib/Algebra/Homology/HomotopyCategory/MappingCone.lean
lemma lift_desc_f {K L : CochainComplex C ℤ} (α : Cocycle K F 1) (β : Cochain K G 0)
    (eq : δ 0 1 β + α.1.comp (Cochain.ofHom φ) (add_zero 1) = 0)
    (α' : Cochain F L (-1)) (β' : G ⟶ L)
    (eq' : δ (-1) 0 α' = Cochain.ofHom (φ ≫ β')) (n n' : ℤ) (hnn' : n + 1 = n') :
    (lift φ α β eq).f n ≫ (desc φ α' β' eq').f n =
    α.1.v n n' hnn' ≫ α'.v n' n (by omega) + β.v n n (add_zero n) ≫ β'.f n

Proof state:
C : Type u_1
D : Type u_2
inst✝⁴ : Category.{?u.262081, u_1} C
inst✝³ : Category.{?u.262085, u_2} D
inst✝² : Preadditive C
inst✝¹ : Preadditive D
F G : CochainComplex C ℤ
φ : F ⟶ G
inst✝ : HasHomotopyCofiber φ
K L : CochainComplex C ℤ
α : Cocycle K F 1
β : Cochain K G 0
eq : δ 0 1 β + (↑α).comp (Cochain.ofHom φ) ⋯ = 0
α' : Cochain F L (-1)
β' : G ⟶ L
eq' : δ (-1) 0 α' = Cochain.ofHom (φ ≫ β')
n n' : ℤ
hnn' : n + 1 = n'
⊢ n' + -1 = n

Tactic:
omega

Result:
no goals

Proof state:
C : Type u_1
inst✝² : Category.{u_3, u_1} C
inst✝¹ : Preadditive C
F G : CochainComplex C ℤ
φ : F ⟶ G
inst✝ : HasHomotopyCofiber φ
K L : CochainComplex C ℤ
α : Cocycle K F 1
β : Cochain K G 0
eq : δ 0 1 β + (↑α).comp (Cochain.ofHom φ) ⋯ = 0
α' : Cochain F L (-1)
β' : G ⟶ L
eq' : δ (-1) 0 α' = Cochain.ofHom (φ ≫ β')
n n' : ℤ
hnn' : n + 1 = n'
⊢ (lift φ α β eq).f n ≫ (desc φ α' β' eq').f n = (↑α).v n n' hnn' ≫ α'.v n' n ⋯ + β.v n n ⋯ ≫ β'.f n

Tactic:
simp only [lift, desc, Cocycle.homOf_f, liftCocycle_coe, descCocycle_coe, Cocycle.ofHom_coe,
  liftCochain_v_descCochain_v φ α.1 β α' (Cochain.ofHom β') (zero_add 1) (neg_add_cancel 1) 0
  (add_zero 0) n n n (add_zero n) (add_zero n) n' hnn', Cochain.ofHom_v]

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Basic.lean
theorem fromEdgeSet_union (s t : Set (Sym2 V)) :
    fromEdgeSet (s ∪ t) = fromEdgeSet s ⊔ fromEdgeSet t

Proof state:
V : Type u
s t : Set (Sym2 V)
⊢ fromEdgeSet (s ∪ t) = fromEdgeSet s ⊔ fromEdgeSet t

Tactic:
ext v w

Result:
case Adj.h.h.a
V : Type u
s t : Set (Sym2 V)
v w : V
⊢ (fromEdgeSet (s ∪ t)).Adj v w ↔ (fromEdgeSet s ⊔ fromEdgeSet t).Adj v w

Proof state:
case Adj.h.h.a
V : Type u
s t : Set (Sym2 V)
v w : V
⊢ (fromEdgeSet (s ∪ t)).Adj v w ↔ (fromEdgeSet s ⊔ fromEdgeSet t).Adj v w

Tactic:
simp [Set.mem_union, or_and_right]

Result:
no goals
-- Mathlib/ModelTheory/Order.lean
theorem noTopOrder_of_dlo [M ⊨ L.dlo] : NoTopOrder M :=
  realize_noTopOrder_iff.1 (L.dlo.realize_sentence_of_mem (by
    simp only [dlo, Set.union_insert, Set.union_singleton, Set.mem_insert_iff, true_or]))

Proof state:
L : Language
M : Type w'
inst✝⁴ : L.IsOrdered
inst✝³ : L.Structure M
inst✝² : LE M
inst✝¹ : L.OrderedStructure M
inst✝ : M ⊨ L.dlo
⊢ L.noTopOrderSentence ∈ L.dlo

Tactic:
simp only [dlo, Set.union_insert, Set.union_singleton, Set.mem_insert_iff, true_or]

Result:
no goals
-- Mathlib/Algebra/Group/Subgroup/Defs.lean
theorem mul_mem_cancel_left {x y : G} (h : x ∈ H) : x * y ∈ H ↔ y ∈ H :=
  ⟨fun hab => by simpa using mul_mem (inv_mem h) hab, mul_mem h⟩

Proof state:
G : Type u_1
inst✝² : Group G
S : Type u_4
H : S
inst✝¹ : SetLike S G
inst✝ : SubgroupClass S G
x y : G
h : x ∈ H
hab : x * y ∈ H
⊢ y ∈ H

Tactic:
simpa using mul_mem (inv_mem h) hab

Result:
no goals