harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Int/DivModLemmas.lean
theorem natAbs_dvd {a b : Int} : (a.natAbs : Int) ∣ b ↔ a ∣ b :=
  match natAbs_eq a with
  | .inl e => by rw [← e]
  | .inr e => by rw [← Int.neg_dvd, ← e]

Proof state:
a b : Int
e : a = -↑a.natAbs
⊢ ↑a.natAbs ∣ b ↔ a ∣ b

Tactic:
rw [← Int.neg_dvd, ← e]

Result:
no goals

Proof state:
a b : Int
e : a = ↑a.natAbs
⊢ ↑a.natAbs ∣ b ↔ a ∣ b

Tactic:
rw [← e]

Result:
no goals
-- Mathlib/Algebra/Polynomial/Basic.lean
theorem support_ofFinsupp (p) : support (⟨p⟩ : R[X]) = p.support

Proof state:
R : Type u
inst✝ : Semiring R
p : R[ℕ]
⊢ { toFinsupp := p }.support = p.support

Tactic:
rw [support]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Attach.lean
theorem count_attachWith [DecidableEq α] {p : α → Prop} (l : Array α) (H : ∀ a ∈ l, p a) (a : {x // p x}) :
    (l.attachWith p H).count a = l.count ↑a

Proof state:
α : Type u_1
inst✝ : DecidableEq α
p : α → Prop
l : Array α
H : ∀ (a : α), a ∈ l → p a
a : { x // p x }
⊢ count a (l.attachWith p H) = count a.val l

Tactic:
cases l

Result:
case mk
α : Type u_1
inst✝ : DecidableEq α
p : α → Prop
a : { x // p x }
toList✝ : List α
H : ∀ (a : α), a ∈ { toList := toList✝ } → p a
⊢ count a ({ toList := toList✝ }.attachWith p H) = count a.val { toList := toList✝ }

Proof state:
case mk
α : Type u_1
inst✝ : DecidableEq α
p : α → Prop
a : { x // p x }
toList✝ : List α
H : ∀ (a : α), a ∈ { toList := toList✝ } → p a
⊢ count a ({ toList := toList✝ }.attachWith p H) = count a.val { toList := toList✝ }

Tactic:
simp

Result:
no goals
-- Mathlib/ModelTheory/Satisfiability.lean
theorem models_iff_not_satisfiable (φ : L.Sentence) : T ⊨ᵇ φ ↔ ¬IsSatisfiable (T ∪ {φ.not})

Proof state:
L : Language
T : L.Theory
φ : L.Sentence
M : T.ModelType
h : ↑M ⊨ Formula.not φ
⊢ Nonempty (T ∪ {Formula.not φ}).ModelType

Tactic:
refine
  ⟨{  Carrier := M
      is_model := ⟨fun ψ hψ => hψ.elim (realize_sentence_of_mem _) fun h' => ?_⟩ }⟩

Result:
L : Language
T : L.Theory
φ : L.Sentence
M : T.ModelType
h : ↑M ⊨ Formula.not φ
ψ : L.Sentence
hψ : ψ ∈ T ∪ {Formula.not φ}
h' : ψ ∈ {Formula.not φ}
⊢ ↑M ⊨ ψ

Proof state:
L : Language
T : L.Theory
φ : L.Sentence
⊢ T ⊨ᵇ φ ↔ ¬(T ∪ {Formula.not φ}).IsSatisfiable

Tactic:
rw [models_sentence_iff, IsSatisfiable]

Result:
L : Language
T : L.Theory
φ : L.Sentence
⊢ (∀ (M : T.ModelType), ↑M ⊨ φ) ↔ ¬Nonempty (T ∪ {Formula.not φ}).ModelType

Proof state:
L : Language
T : L.Theory
φ : L.Sentence
M : T.ModelType
h : ↑M ⊨ Formula.not φ
ψ : L.Sentence
hψ : ψ ∈ T ∪ {Formula.not φ}
h' : ψ ∈ {Formula.not φ}
⊢ ↑M ⊨ Formula.not φ

Tactic:
exact h

Result:
no goals

Proof state:
L : Language
T : L.Theory
φ : L.Sentence
M : T.ModelType
h : ↑M ⊨ Formula.not φ
ψ : L.Sentence
hψ : ψ ∈ T ∪ {Formula.not φ}
h' : ψ ∈ {Formula.not φ}
⊢ ↑M ⊨ ψ

Tactic:
rw [Set.mem_singleton_iff.1 h']

Result:
L : Language
T : L.Theory
φ : L.Sentence
M : T.ModelType
h : ↑M ⊨ Formula.not φ
ψ : L.Sentence
hψ : ψ ∈ T ∪ {Formula.not φ}
h' : ψ ∈ {Formula.not φ}
⊢ ↑M ⊨ Formula.not φ

Proof state:
L : Language
T : L.Theory
φ : L.Sentence
⊢ (∀ (M : T.ModelType), ↑M ⊨ φ) ↔ ¬Nonempty (T ∪ {Formula.not φ}).ModelType

Tactic:
refine
  ⟨fun h1 h2 =>
    (Sentence.realize_not _).1
      (realize_sentence_of_mem (T ∪ {Formula.not φ})
        (Set.subset_union_right (Set.mem_singleton _)))
      (h1 (h2.some.subtheoryModel Set.subset_union_left)),
    fun h M => ?_⟩

Result:
L : Language
T : L.Theory
φ : L.Sentence
h : ¬Nonempty (T ∪ {Formula.not φ}).ModelType
M : T.ModelType
⊢ ↑M ⊨ φ

Proof state:
L : Language
T : L.Theory
φ : L.Sentence
h : ¬Nonempty (T ∪ {Formula.not φ}).ModelType
M : T.ModelType
⊢ ↑M ⊨ φ

Tactic:
contrapose! h

Result:
L : Language
T : L.Theory
φ : L.Sentence
M : T.ModelType
h : ¬↑M ⊨ φ
⊢ Nonempty (T ∪ {Formula.not φ}).ModelType

Proof state:
L : Language
T : L.Theory
φ : L.Sentence
M : T.ModelType
h : ¬↑M ⊨ φ
⊢ Nonempty (T ∪ {Formula.not φ}).ModelType

Tactic:
rw [← Sentence.realize_not] at h

Result:
L : Language
T : L.Theory
φ : L.Sentence
M : T.ModelType
h : ↑M ⊨ Formula.not φ
⊢ Nonempty (T ∪ {Formula.not φ}).ModelType
-- Mathlib/GroupTheory/GroupAction/Quotient.lean
theorem Quotient.coe_smul_out [QuotientAction β H] (b : β) (q : α ⧸ H) : ↑(b • q.out) = b • q

Proof state:
α : Type u
β : Type v
inst✝³ : Group α
inst✝² : Monoid β
inst✝¹ : MulAction β α
H : Subgroup α
inst✝ : QuotientAction β H
b : β
q : α ⧸ H
⊢ ↑(b • Quotient.out q) = b • q

Tactic:
simp

Result:
no goals
-- Mathlib/LinearAlgebra/Matrix/SesquilinearForm.lean
theorem LinearMap.toMatrix₂_mul (B : M₁ →ₗ[R] M₂ →ₗ[R] R) (M : Matrix m m' R) :
    LinearMap.toMatrix₂ b₁ b₂ B * M =
      LinearMap.toMatrix₂ b₁ b₂' (B.compl₂ (toLin b₂' b₂ M))

Proof state:
R : Type u_1
M₁ : Type u_6
M₂ : Type u_7
M₂' : Type u_9
n : Type u_11
m : Type u_12
m' : Type u_14
inst✝¹² : CommSemiring R
inst✝¹¹ : AddCommMonoid M₁
inst✝¹⁰ : Module R M₁
inst✝⁹ : AddCommMonoid M₂
inst✝⁸ : Module R M₂
inst✝⁷ : DecidableEq n
inst✝⁶ : Fintype n
inst✝⁵ : DecidableEq m
inst✝⁴ : Fintype m
b₁ : Basis n R M₁
b₂ : Basis m R M₂
inst✝³ : AddCommMonoid M₂'
inst✝² : Module R M₂'
b₂' : Basis m' R M₂'
inst✝¹ : Fintype m'
inst✝ : DecidableEq m'
B : M₁ →ₗ[R] M₂ →ₗ[R] R
M : Matrix m m' R
⊢ (toMatrix₂ b₁ b₂) B * M = (toMatrix₂ b₁ b₂') (B.compl₂ ((toLin b₂' b₂) M))

Tactic:
rw [LinearMap.toMatrix₂_compl₂ b₁ b₂, toMatrix_toLin]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Complex/LogBounds.lean
lemma norm_log_one_add_le {z : ℂ} (hz : ‖z‖ < 1) :
    ‖log (1 + z)‖ ≤ ‖z‖ ^ 2 * (1 - ‖z‖)⁻¹ / 2 + ‖z‖

Proof state:
z : ℂ
hz : ‖z‖ < 1
⊢ ‖log (1 + z) - z + z‖ ≤ ‖z‖ ^ 2 * (1 - ‖z‖)⁻¹ / 2 + ‖z‖

Tactic:
apply le_trans (norm_add_le _ _)

Result:
z : ℂ
hz : ‖z‖ < 1
⊢ ‖log (1 + z) - z‖ + ‖z‖ ≤ ‖z‖ ^ 2 * (1 - ‖z‖)⁻¹ / 2 + ‖z‖

Proof state:
z : ℂ
hz : ‖z‖ < 1
⊢ ‖log (1 + z)‖ ≤ ‖z‖ ^ 2 * (1 - ‖z‖)⁻¹ / 2 + ‖z‖

Tactic:
rw [← sub_add_cancel (log (1 + z)) z]

Result:
z : ℂ
hz : ‖z‖ < 1
⊢ ‖log (1 + z) - z + z‖ ≤ ‖z‖ ^ 2 * (1 - ‖z‖)⁻¹ / 2 + ‖z‖

Proof state:
z : ℂ
hz : ‖z‖ < 1
⊢ ‖log (1 + z) - z‖ + ‖z‖ ≤ ‖z‖ ^ 2 * (1 - ‖z‖)⁻¹ / 2 + ‖z‖

Tactic:
exact add_le_add_right (Complex.norm_log_one_add_sub_self_le hz) ‖z‖

Result:
no goals
-- Mathlib/LinearAlgebra/AffineSpace/AffineSubspace/Basic.lean
theorem vectorSpan_range_eq_span_range_vsub_left (p : ι → P) (i0 : ι) :
    vectorSpan k (Set.range p) = Submodule.span k (Set.range fun i : ι => p i0 -ᵥ p i)

Proof state:
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
ι : Type u_4
p : ι → P
i0 : ι
⊢ vectorSpan k (range p) = Submodule.span k (range fun i => p i0 -ᵥ p i)

Tactic:
rw [vectorSpan_eq_span_vsub_set_left k (Set.mem_range_self i0), ← Set.range_comp]

Result:
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
ι : Type u_4
p : ι → P
i0 : ι
⊢ Submodule.span k (range ((fun x => p i0 -ᵥ x) ∘ p)) = Submodule.span k (range fun i => p i0 -ᵥ p i)

Proof state:
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
ι : Type u_4
p : ι → P
i0 : ι
⊢ Submodule.span k (range ((fun x => p i0 -ᵥ x) ∘ p)) = Submodule.span k (range fun i => p i0 -ᵥ p i)

Tactic:
congr

Result:
no goals
-- Mathlib/ModelTheory/FinitelyGenerated.lean
theorem fg_bot : (⊥ : L.Substructure M).FG :=
  ⟨∅, by rw [Finset.coe_empty, closure_empty]⟩

Proof state:
L : Language
M : Type u_1
inst✝ : L.Structure M
⊢ (closure L).toFun ↑∅ = ⊥

Tactic:
rw [Finset.coe_empty, closure_empty]

Result:
no goals
-- Mathlib/Data/Rat/Cast/Defs.lean
@[norm_cast]
lemma cast_add_of_ne_zero (hq : (q.den : α) ≠ 0) (hr : (r.den : α) ≠ 0) :
    ↑(q + r) = (q + r : α)

Proof state:
α : Type u_3
inst✝ : DivisionSemiring α
q r : ℚ≥0
hq : ↑q.den ≠ 0
hr : ↑r.den ≠ 0
⊢ (↑q.num * ↑r.den + ↑q.den * ↑r.num) / (↑q.den * ↑r.den) = (↑q.num * ↑r.den + ↑q.den * ↑r.num) / (↑q.den * ↑r.den)

Tactic:
rfl

Result:
no goals

Proof state:
case hb
α : Type u_3
inst✝ : DivisionSemiring α
q r : ℚ≥0
hq : ↑q.den ≠ 0
hr : ↑r.den ≠ 0
⊢ ↑(q.den * r.den) ≠ 0

Tactic:
push_cast

Result:
case hb
α : Type u_3
inst✝ : DivisionSemiring α
q r : ℚ≥0
hq : ↑q.den ≠ 0
hr : ↑r.den ≠ 0
⊢ ↑q.den * ↑r.den ≠ 0

Proof state:
α : Type u_3
inst✝ : DivisionSemiring α
q r : ℚ≥0
hq : ↑q.den ≠ 0
hr : ↑r.den ≠ 0
⊢ ↑(q + r) = ↑q + ↑r

Tactic:
rw [add_def, cast_divNat_of_ne_zero, cast_def, cast_def, mul_comm _ q.den,
  (Nat.commute_cast _ _).div_add_div (Nat.commute_cast _ _) hq hr]

Result:
α : Type u_3
inst✝ : DivisionSemiring α
q r : ℚ≥0
hq : ↑q.den ≠ 0
hr : ↑r.den ≠ 0
⊢ ↑(q.num * r.den + q.den * r.num) / ↑(q.den * r.den) = (↑q.num * ↑r.den + ↑q.den * ↑r.num) / (↑q.den * ↑r.den)

case hb
α : Type u_3
inst✝ : DivisionSemiring α
q r : ℚ≥0
hq : ↑q.den ≠ 0
hr : ↑r.den ≠ 0
⊢ ↑(q.den * r.den) ≠ 0

Proof state:
case hb
α : Type u_3
inst✝ : DivisionSemiring α
q r : ℚ≥0
hq : ↑q.den ≠ 0
hr : ↑r.den ≠ 0
⊢ ↑q.den * ↑r.den ≠ 0

Tactic:
exact mul_ne_zero hq hr

Result:
no goals

Proof state:
α : Type u_3
inst✝ : DivisionSemiring α
q r : ℚ≥0
hq : ↑q.den ≠ 0
hr : ↑r.den ≠ 0
⊢ ↑(q.num * r.den + q.den * r.num) / ↑(q.den * r.den) = (↑q.num * ↑r.den + ↑q.den * ↑r.num) / (↑q.den * ↑r.den)

Tactic:
push_cast

Result:
α : Type u_3
inst✝ : DivisionSemiring α
q r : ℚ≥0
hq : ↑q.den ≠ 0
hr : ↑r.den ≠ 0
⊢ (↑q.num * ↑r.den + ↑q.den * ↑r.num) / (↑q.den * ↑r.den) = (↑q.num * ↑r.den + ↑q.den * ↑r.num) / (↑q.den * ↑r.den)
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/RawLemmas.lean
theorem get?_modify [EquivBEq α] [LawfulHashable α] {k k' : α} {f : β → β} (h : m.WF) :
    Const.get? (Const.modify m k f) k' =
      if k == k' then
        Const.get? m k |>.map f
      else
        Const.get? m k'

Proof state:
α : Type u
inst✝³ : BEq α
inst✝² : Hashable α
β : Type v
m : Raw α fun x => β
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
k k' : α
f : β → β
h : m.WF
⊢ get? (modify m k f) k' = if (k == k') = true then Option.map f (get? m k) else get? m k'

Tactic:
simp_to_raw using Raw₀.Const.get?_modify

Result:
no goals
-- Mathlib/Data/Nat/Bits.lean
theorem bits_append_bit (n : ℕ) (b : Bool) (hn : n = 0 → b = true) :
    (bit b n).bits = b :: n.bits

Proof state:
case h
n : ℕ
b : Bool
hn : n = 0 → b = true
⊢ [false] = [] ∨ (n = 0 → b = true)

Tactic:
simpa

Result:
no goals

Proof state:
n : ℕ
b : Bool
hn : n = 0 → b = true
⊢ (bit b n).bits = b :: n.bits

Tactic:
rw [Nat.bits, Nat.bits, binaryRec_eq]

Result:
case h
n : ℕ
b : Bool
hn : n = 0 → b = true
⊢ [false] = [] ∨ (n = 0 → b = true)
-- Mathlib/NumberTheory/NumberField/Units/Basic.lean
theorem coe_pow (x : (𝓞 K)ˣ) (n : ℕ) : ((x ^ n : (𝓞 K)ˣ) : K) = (x : K) ^ n

Proof state:
K : Type u_1
inst✝ : Field K
x : (𝓞 K)ˣ
n : ℕ
⊢ (algebraMap (𝓞 K) K) ↑(x ^ n) = (algebraMap (𝓞 K) K) ↑x ^ n

Tactic:
rw [← map_pow, ← val_pow_eq_pow_val]

Result:
no goals
-- Mathlib/AlgebraicGeometry/Restrict.lean
@[reassoc (attr := simp)]
lemma map_resLE (i : V' ≤ V) :
    X.homOfLE i ≫ f.resLE U V e = f.resLE U V' (i.trans e)

Proof state:
X Y : Scheme
f : X ⟶ Y
U : Y.Opens
V V' : X.Opens
e : V ≤ f ⁻¹ᵁ U
i : V' ≤ V
⊢ X.homOfLE i ≫ resLE f U V e = resLE f U V' ⋯

Tactic:
simp_rw [← resLE_id, resLE_comp_resLE, Category.id_comp]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Tactic/BVDecide/LRAT/Internal/Formula/Lemmas.lean
theorem deleteOne_preserves_rupUnits {n : Nat} (f : DefaultFormula n) (id : Nat) :
    (deleteOne f id).rupUnits = f.rupUnits

Proof state:
n : Nat
f : DefaultFormula n
id : Nat
⊢ (f.deleteOne id).rupUnits = f.rupUnits

Tactic:
simp only [deleteOne]

Result:
n : Nat
f : DefaultFormula n
id : Nat
⊢ (match f.clauses[id]! with
      | none => { clauses := f.clauses, rupUnits := f.rupUnits, ratUnits := f.ratUnits, assignments := f.assignments }
      | some { clause := [l], nodupkey := nodupkey, nodup := nodup } =>
        { clauses := f.clauses.set! id none, rupUnits := f.rupUnits, ratUnits := f.ratUnits,
          assignments := f.assignments.modify l.fst.val (removeAssignment l.snd) }
      | some val =>
        { clauses := f.clauses.set! id none, rupUnits := f.rupUnits, ratUnits := f.ratUnits,
          assignments := f.assignments }).rupUnits =
    f.rupUnits

Proof state:
n : Nat
f : DefaultFormula n
id : Nat
⊢ (match f.clauses[id]! with
      | none => { clauses := f.clauses, rupUnits := f.rupUnits, ratUnits := f.ratUnits, assignments := f.assignments }
      | some { clause := [l], nodupkey := nodupkey, nodup := nodup } =>
        { clauses := f.clauses.set! id none, rupUnits := f.rupUnits, ratUnits := f.ratUnits,
          assignments := f.assignments.modify l.fst.val (removeAssignment l.snd) }
      | some val =>
        { clauses := f.clauses.set! id none, rupUnits := f.rupUnits, ratUnits := f.ratUnits,
          assignments := f.assignments }).rupUnits =
    f.rupUnits

Tactic:
split <;> simp only

Result:
no goals
-- Mathlib/LinearAlgebra/CliffordAlgebra/Prod.lean
lemma toProd_comp_ofProd : (toProd Q₁ Q₂).comp (ofProd Q₁ Q₂) = AlgHom.id _ _

Proof state:
R : Type u_1
M₁ : Type u_2
M₂ : Type u_3
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M₁
inst✝² : AddCommGroup M₂
inst✝¹ : Module R M₁
inst✝ : Module R M₂
Q₁ : QuadraticForm R M₁
Q₂ : QuadraticForm R M₂
⊢ (toProd Q₁ Q₂).comp (ofProd Q₁ Q₂) = AlgHom.id R (CliffordAlgebra (QuadraticMap.prod Q₁ Q₂))

Tactic:
ext m <;> dsimp

Result:
case a.hl.h
R : Type u_1
M₁ : Type u_2
M₂ : Type u_3
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M₁
inst✝² : AddCommGroup M₂
inst✝¹ : Module R M₁
inst✝ : Module R M₂
Q₁ : QuadraticForm R M₁
Q₂ : QuadraticForm R M₂
m : M₁
⊢ (toProd Q₁ Q₂) ((ofProd Q₁ Q₂) ((ι (QuadraticMap.prod Q₁ Q₂)) (m, 0))) = (ι (QuadraticMap.prod Q₁ Q₂)) (m, 0)

case a.hr.h
R : Type u_1
M₁ : Type u_2
M₂ : Type u_3
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M₁
inst✝² : AddCommGroup M₂
inst✝¹ : Module R M₁
inst✝ : Module R M₂
Q₁ : QuadraticForm R M₁
Q₂ : QuadraticForm R M₂
m : M₂
⊢ (toProd Q₁ Q₂) ((ofProd Q₁ Q₂) ((ι (QuadraticMap.prod Q₁ Q₂)) (0, m))) = (ι (QuadraticMap.prod Q₁ Q₂)) (0, m)

Proof state:
case a.hl.h
R : Type u_1
M₁ : Type u_2
M₂ : Type u_3
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M₁
inst✝² : AddCommGroup M₂
inst✝¹ : Module R M₁
inst✝ : Module R M₂
Q₁ : QuadraticForm R M₁
Q₂ : QuadraticForm R M₂
m : M₁
⊢ (toProd Q₁ Q₂) ((ofProd Q₁ Q₂) ((ι (QuadraticMap.prod Q₁ Q₂)) (m, 0))) = (ι (QuadraticMap.prod Q₁ Q₂)) (m, 0)

Tactic:
rw [ofProd_ι_mk, map_add, toProd_one_tmul_ι, toProd_ι_tmul_one, Prod.mk_zero_zero,
  LinearMap.map_zero, add_zero]

Result:
no goals

Proof state:
case a.hr.h
R : Type u_1
M₁ : Type u_2
M₂ : Type u_3
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M₁
inst✝² : AddCommGroup M₂
inst✝¹ : Module R M₁
inst✝ : Module R M₂
Q₁ : QuadraticForm R M₁
Q₂ : QuadraticForm R M₂
m : M₂
⊢ (toProd Q₁ Q₂) ((ofProd Q₁ Q₂) ((ι (QuadraticMap.prod Q₁ Q₂)) (0, m))) = (ι (QuadraticMap.prod Q₁ Q₂)) (0, m)

Tactic:
rw [ofProd_ι_mk, map_add, toProd_one_tmul_ι, toProd_ι_tmul_one, Prod.mk_zero_zero,
  LinearMap.map_zero, zero_add]

Result:
no goals
-- Mathlib/Order/Hom/Lattice.lean
theorem cancel_left {g : InfTopHom β γ} {f₁ f₂ : InfTopHom α β} (hg : Injective g) :
    g.comp f₁ = g.comp f₂ ↔ f₁ = f₂ :=
  ⟨fun h => InfTopHom.ext fun a => hg <| by rw [← comp_apply, h, comp_apply], congr_arg _⟩

Proof state:
α : Type u_3
β : Type u_4
γ : Type u_5
inst✝⁵ : Min α
inst✝⁴ : Top α
inst✝³ : Min β
inst✝² : Top β
inst✝¹ : Min γ
inst✝ : Top γ
g : InfTopHom β γ
f₁ f₂ : InfTopHom α β
hg : Injective ⇑g
h : g.comp f₁ = g.comp f₂
a : α
⊢ g (f₁ a) = g (f₂ a)

Tactic:
rw [← comp_apply, h, comp_apply]

Result:
no goals
-- Mathlib/Order/Fin/Basic.lean
theorem rev_last_eq_bot (n : ℕ) : rev (last n) = ⊥

Proof state:
n : ℕ
⊢ (last n).rev = ⊥

Tactic:
rw [rev_last, bot_eq_zero]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Perm.lean
theorem Perm.symm {l₁ l₂ : List α} (h : l₁ ~ l₂) : l₂ ~ l₁

Proof state:
case nil
α : Type u_1
l₁ l₂ : List α
⊢ [] ~ []

Tactic:
exact nil

Result:
no goals

Proof state:
case swap
α : Type u_1
l₁ l₂ : List α
x✝ y✝ : α
l✝ : List α
⊢ x✝ :: y✝ :: l✝ ~ y✝ :: x✝ :: l✝

Tactic:
exact swap ..

Result:
no goals

Proof state:
α : Type u_1
l₁ l₂ : List α
h : l₁ ~ l₂
⊢ l₂ ~ l₁

Tactic:
induction h with
| nil => exact nil
| cons _ _ ih => exact cons _ ih
| swap => exact swap ..
| trans _ _ ih₁ ih₂ => exact trans ih₂ ih₁

Result:
no goals

Proof state:
case trans
α : Type u_1
l₁ l₂ l₁✝ l₂✝ l₃✝ : List α
a✝¹ : l₁✝ ~ l₂✝
a✝ : l₂✝ ~ l₃✝
ih₁ : l₂✝ ~ l₁✝
ih₂ : l₃✝ ~ l₂✝
⊢ l₃✝ ~ l₁✝

Tactic:
exact trans ih₂ ih₁

Result:
no goals

Proof state:
case cons
α : Type u_1
l₁ l₂ : List α
x✝ : α
l₁✝ l₂✝ : List α
a✝ : l₁✝ ~ l₂✝
ih : l₂✝ ~ l₁✝
⊢ x✝ :: l₂✝ ~ x✝ :: l₁✝

Tactic:
exact cons _ ih

Result:
no goals
-- Mathlib/Data/Finsupp/Weight.lean
theorem NonTorsionWeight.ne_zero [Nontrivial R] [NonTorsionWeight R w] (s : σ) :
    w s ≠ 0 := fun h ↦ by
  rw [← one_smul R (w s)] at h
  apply zero_ne_one.symm (α := R)
  exact NonTorsionWeight.eq_zero_of_smul_eq_zero h

Proof state:
σ : Type u_1
M : Type u_2
R : Type u_3
inst✝⁴ : Semiring R
w : σ → M
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : Nontrivial R
inst✝ : NonTorsionWeight R w
s : σ
h : 1 • w s = 0
⊢ 1 = 0

Tactic:
exact NonTorsionWeight.eq_zero_of_smul_eq_zero h

Result:
no goals

Proof state:
σ : Type u_1
M : Type u_2
R : Type u_3
inst✝⁴ : Semiring R
w : σ → M
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : Nontrivial R
inst✝ : NonTorsionWeight R w
s : σ
h : w s = 0
⊢ False

Tactic:
rw [← one_smul R (w s)] at h

Result:
σ : Type u_1
M : Type u_2
R : Type u_3
inst✝⁴ : Semiring R
w : σ → M
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : Nontrivial R
inst✝ : NonTorsionWeight R w
s : σ
h : 1 • w s = 0
⊢ False

Proof state:
σ : Type u_1
M : Type u_2
R : Type u_3
inst✝⁴ : Semiring R
w : σ → M
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : Nontrivial R
inst✝ : NonTorsionWeight R w
s : σ
h : 1 • w s = 0
⊢ False

Tactic:
apply zero_ne_one.symm (α := R)

Result:
σ : Type u_1
M : Type u_2
R : Type u_3
inst✝⁴ : Semiring R
w : σ → M
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : Nontrivial R
inst✝ : NonTorsionWeight R w
s : σ
h : 1 • w s = 0
⊢ 1 = 0
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem getElem_shrink_loop (a : Array α) (n : Nat) (i : Nat) (h : i < (shrink.loop n a).size) :
    (shrink.loop n a)[i] = a[i]'(by simp at h; omega)

Proof state:
case succ
α : Type u_1
n : Nat
ih : ∀ (a : Array α) (i : Nat) (h : i < (shrink.loop n a).size), (shrink.loop n a)[i] = a[i]
a : Array α
i : Nat
h : i < (shrink.loop (n + 1) a).size
⊢ (shrink.loop (n + 1) a)[i] = a[i]

Tactic:
simp [shrink.loop, ih]

Result:
no goals

Proof state:
case zero
α : Type u_1
a : Array α
i : Nat
h : i < (shrink.loop 0 a).size
⊢ (shrink.loop 0 a)[i] = a[i]

Tactic:
simp [shrink.loop]

Result:
no goals

Proof state:
α : Type ?u.487385
a : Array α
n i : Nat
h : i < (shrink.loop n a).size
⊢ i < a.size

Tactic:
simp at h

Result:
α : Type ?u.487385
a : Array α
n i : Nat
h : i < a.size - n
⊢ i < a.size

Proof state:
α : Type ?u.487385
a : Array α
n i : Nat
h : i < a.size - n
⊢ i < a.size

Tactic:
omega

Result:
no goals

Proof state:
α : Type u_1
a : Array α
n i : Nat
h : i < (shrink.loop n a).size
⊢ (shrink.loop n a)[i] = a[i]

Tactic:
induction n generalizing a i with
| zero => simp [shrink.loop]
| succ n ih =>
  simp [shrink.loop, ih]

Result:
no goals
-- Mathlib/Analysis/Calculus/FDeriv/RestrictScalars.lean
theorem differentiableAt_iff_restrictScalars (hf : DifferentiableAt 𝕜 f x) :
    DifferentiableAt 𝕜' f x ↔ ∃ g' : E →L[𝕜'] F, g'.restrictScalars 𝕜 = fderiv 𝕜 f x

Proof state:
𝕜 : Type u_1
inst✝¹⁰ : NontriviallyNormedField 𝕜
𝕜' : Type u_2
inst✝⁹ : NontriviallyNormedField 𝕜'
inst✝⁸ : NormedAlgebra 𝕜 𝕜'
E : Type u_3
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace 𝕜 E
inst✝⁵ : NormedSpace 𝕜' E
inst✝⁴ : IsScalarTower 𝕜 𝕜' E
F : Type u_4
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedSpace 𝕜' F
inst✝ : IsScalarTower 𝕜 𝕜' F
f : E → F
x : E
hf : DifferentiableAt 𝕜 f x
⊢ DifferentiableAt 𝕜' f x ↔ ∃ g', restrictScalars 𝕜 g' = fderiv 𝕜 f x

Tactic:
rw [← differentiableWithinAt_univ, ← fderivWithin_univ]

Result:
𝕜 : Type u_1
inst✝¹⁰ : NontriviallyNormedField 𝕜
𝕜' : Type u_2
inst✝⁹ : NontriviallyNormedField 𝕜'
inst✝⁸ : NormedAlgebra 𝕜 𝕜'
E : Type u_3
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace 𝕜 E
inst✝⁵ : NormedSpace 𝕜' E
inst✝⁴ : IsScalarTower 𝕜 𝕜' E
F : Type u_4
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedSpace 𝕜' F
inst✝ : IsScalarTower 𝕜 𝕜' F
f : E → F
x : E
hf : DifferentiableAt 𝕜 f x
⊢ DifferentiableWithinAt 𝕜' f univ x ↔ ∃ g', restrictScalars 𝕜 g' = fderivWithin 𝕜 f univ x

Proof state:
𝕜 : Type u_1
inst✝¹⁰ : NontriviallyNormedField 𝕜
𝕜' : Type u_2
inst✝⁹ : NontriviallyNormedField 𝕜'
inst✝⁸ : NormedAlgebra 𝕜 𝕜'
E : Type u_3
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace 𝕜 E
inst✝⁵ : NormedSpace 𝕜' E
inst✝⁴ : IsScalarTower 𝕜 𝕜' E
F : Type u_4
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedSpace 𝕜' F
inst✝ : IsScalarTower 𝕜 𝕜' F
f : E → F
x : E
hf : DifferentiableAt 𝕜 f x
⊢ DifferentiableWithinAt 𝕜' f univ x ↔ ∃ g', restrictScalars 𝕜 g' = fderivWithin 𝕜 f univ x

Tactic:
exact
  differentiableWithinAt_iff_restrictScalars 𝕜 hf.differentiableWithinAt uniqueDiffWithinAt_univ

Result:
no goals
-- Mathlib/Topology/Category/TopCat/Opens.lean
theorem map_iSup (f : X ⟶ Y) {ι : Type*} (U : ι → Opens Y) :
    (map f).obj (iSup U) = iSup ((map f).obj ∘ U)

Proof state:
case h
X Y : TopCat
f : X ⟶ Y
ι : Type u_1
U : ι → Opens ↑Y
⊢ ↑{ carrier := ⇑(ConcreteCategory.hom f) ⁻¹' ⋃ i, ↑(U i), is_open' := ⋯ } =
    ↑{ carrier := ⋃ i, ↑(((map f).obj ∘ U) i), is_open' := ⋯ }

Tactic:
dsimp

Result:
case h
X Y : TopCat
f : X ⟶ Y
ι : Type u_1
U : ι → Opens ↑Y
⊢ ⇑(ConcreteCategory.hom f) ⁻¹' ⋃ i, ↑(U i) = ⋃ i, ⇑(ConcreteCategory.hom f) ⁻¹' ↑(U i)

Proof state:
case h
X Y : TopCat
f : X ⟶ Y
ι : Type u_1
U : ι → Opens ↑Y
⊢ ⇑(ConcreteCategory.hom f) ⁻¹' ⋃ i, ↑(U i) = ⋃ i, ⇑(ConcreteCategory.hom f) ⁻¹' ↑(U i)

Tactic:
rw [Set.preimage_iUnion]

Result:
no goals

Proof state:
case h
X Y : TopCat
f : X ⟶ Y
ι : Type u_1
U : ι → Opens ↑Y
⊢ ↑((map f).obj (iSup U)) = ↑(iSup ((map f).obj ∘ U))

Tactic:
rw [iSup_def, iSup_def, map_obj]

Result:
case h
X Y : TopCat
f : X ⟶ Y
ι : Type u_1
U : ι → Opens ↑Y
⊢ ↑{ carrier := ⇑(ConcreteCategory.hom f) ⁻¹' ⋃ i, ↑(U i), is_open' := ⋯ } =
    ↑{ carrier := ⋃ i, ↑(((map f).obj ∘ U) i), is_open' := ⋯ }

Proof state:
X Y : TopCat
f : X ⟶ Y
ι : Type u_1
U : ι → Opens ↑Y
⊢ (map f).obj (iSup U) = iSup ((map f).obj ∘ U)

Tactic:
ext1

Result:
case h
X Y : TopCat
f : X ⟶ Y
ι : Type u_1
U : ι → Opens ↑Y
⊢ ↑((map f).obj (iSup U)) = ↑(iSup ((map f).obj ∘ U))
-- Mathlib/MeasureTheory/PiSystem.lean
theorem has_compl_iff {a} : d.Has aᶜ ↔ d.Has a :=
  ⟨fun h => by simpa using d.has_compl h, fun h => d.has_compl h⟩

Proof state:
α : Type u_3
d : DynkinSystem α
a : Set α
h : d.Has aᶜ
⊢ d.Has a

Tactic:
simpa using d.has_compl h

Result:
no goals
-- Mathlib/Order/Fin/Tuple.lean
/-- Note this lemma can only be written about non-dependent tuples as `insertNth (last n) = snoc` is
not a definitional equality. -/
@[simp] lemma insertNthOrderIso_last (n : ℕ) (α : Type*) [LE α] :
    insertNthOrderIso (fun _ ↦ α) (last n) = snocOrderIso (fun _ ↦ α)

Proof state:
n : ℕ
α : Type u_2
inst✝ : LE α
⊢ insertNthOrderIso (fun x => α) (last n) = snocOrderIso fun x => α

Tactic:
ext

Result:
case h.h.h
n : ℕ
α : Type u_2
inst✝ : LE α
x✝¹ : α × (Fin n → α)
x✝ : Fin (n + 1)
⊢ (insertNthOrderIso (fun x => α) (last n)) x✝¹ x✝ = (snocOrderIso fun x => α) x✝¹ x✝

Proof state:
case h.h.h
n : ℕ
α : Type u_2
inst✝ : LE α
x✝¹ : α × (Fin n → α)
x✝ : Fin (n + 1)
⊢ (insertNthOrderIso (fun x => α) (last n)) x✝¹ x✝ = (snocOrderIso fun x => α) x✝¹ x✝

Tactic:
simp

Result:
no goals